Verifying a Realistic Mutable Hash Table
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2021
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866913214061608960 |
|---|---|
| author | Chassot, Samuel Kunčak, Viktor |
| author_facet | Chassot, Samuel Kunčak, Viktor |
| contents | In this work, we verify the mutable LongMap from the Scala standard library, a hash table using open addressing within a single array, using the Stainless program verifier. As a reference implementation, we write an immutable map based on a list of tuples. We then show that LongMap's operations correspond to operations of this association list. To express the resizing of the hash table array, we introduce a new reference swapping construct in Stainless. This allows us to apply the decorator pattern without introducing aliasing. Our verification effort led us to find and fix a bug in the original implementation that manifests for large hash tables. Our performance analysis shows the verified version to be within a 1.5 factor of the original data structure. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2107_08824 |
| institution | arXiv |
| publishDate | 2021 |
| record_format | arxiv |
| spellingShingle | Verifying a Realistic Mutable Hash Table Chassot, Samuel Kunčak, Viktor Software Engineering Programming Languages In this work, we verify the mutable LongMap from the Scala standard library, a hash table using open addressing within a single array, using the Stainless program verifier. As a reference implementation, we write an immutable map based on a list of tuples. We then show that LongMap's operations correspond to operations of this association list. To express the resizing of the hash table array, we introduce a new reference swapping construct in Stainless. This allows us to apply the decorator pattern without introducing aliasing. Our verification effort led us to find and fix a bug in the original implementation that manifests for large hash tables. Our performance analysis shows the verified version to be within a 1.5 factor of the original data structure. |
| title | Verifying a Realistic Mutable Hash Table |
| topic | Software Engineering Programming Languages |
| url | https://arxiv.org/abs/2107.08824 |