nach oben

Journal of Automated Reasoning

Erschienen in:

01.03.2023

Efficient Extensional Binary Tries

verfasst von: Andrew W. Appel, Xavier Leroy

Erschienen in: Journal of Automated Reasoning | Ausgabe 1/2023

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Lookup tables (finite maps) are a ubiquitous data structure. In pure functional languages they are best represented using trees instead of hash tables. In pure functional languages within constructive logic, without a primitive integer type, they are well represented using binary tries instead of search trees. In this work, we introduce canonical binary tries, an improved binary-trie data structure that enjoys a natural extensionality property, quite useful in proofs, and supports sparseness more efficiently. We provide full proofs of correctness in Coq. We provide microbenchmark measurements of canonical binary tries versus several other data structures for finite maps, in a variety of application contexts; as well as measurement of canonical versus original tries in two big, real systems. The application context of data structures contained in theorem statements imposes unusual requirements for which canonical tries are particularly well suited.

Vorheriger Artikel Optimal Deterministic Controller Synthesis from Steady-State Distributions

Nächster Artikel Correction: Towards Formalising Schutz’ Axioms for Minkowski Spacetime in Isabelle/HOL

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

All proofs mentioned in this paper are machine-checked unless explicitly noted otherwise.

Persistent arrays give a functional semantics layered on an imperative (destructive-update) implementation, but these are not suitable because they would require extending the logic’s kernel of axioms.

In fact, no programming language has a primitive integer type with constant-time comparisons; they typically have a range-limited integer type \(-2^k\le i < 2^k\) or a modular integer type \((i \bmod 2^k)\). Most versions of Coq 2005-present have not had a built-in integer type with fast comparisons; and relying on them would increase the size of the trusted base, that is, Coq kernel code, Coq axioms, Coq extraction to OCaml, and OCaml operations upon which we rely.

In OCaml, an arity-k constructor applied to arguments takes \(k+1\) words, including one for the constructor-tag. In Coq, an arity-k constructor is represented as one arity-2 OCaml construction plus one length-k array, which take (respectively) 3 words and \(k+1\) words as represented in OCaml within the Coq kernel. The arity-2 OCaml construction also points to a description of the constructor, but that description is shared among all its uses so we don’t count it.

Andreas Abel, personal communications, Aug-Sept 2022. Examples of problematic unifications can be found at https://github.com/agda/agda/issues/483.

In table 1, performance of PTrees in VST could be predicted in row “Coq execution, vm_compute, Sparse test,” column Sigma versus columns Original and Canonical; whereas PTree performance in CompCert could be predicted in row “Extraction to OCaml, Sparse test”, same columns.

This Coq verification is at https://github.com/PrincetonUniversity/VST/releases/tag/v2.9.1 in subdirectory progs/VSUpile.

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-022-09655-x/MediaObjects/10817_2022_9655_Figjs_HTML.gif

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-022-09655-x/MediaObjects/10817_2022_9655_Figjt_HTML.gif

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-022-09655-x/MediaObjects/10817_2022_9655_Figju_HTML.gif

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-022-09655-x/MediaObjects/10817_2022_9655_Figjv_HTML.gif

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-022-09655-x/MediaObjects/10817_2022_9655_Figjw_HTML.gif

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-022-09655-x/MediaObjects/10817_2022_9655_Figjx_HTML.gif

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-022-09655-x/MediaObjects/10817_2022_9655_Figjy_HTML.gif

Measurements were performed on a Lenovo t440p laptop with Intel Core i7-4810MQ @ 2.8GHz with 32GB memory, using Coq 8.14/8.15.1 in 32-bit mode with virtual-memory limit of 1GB. The Clight abstract-syntax-tree files were produced by

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-022-09655-x/MediaObjects/10817_2022_9655_Figjz_HTML.gif

in its default

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-022-09655-x/MediaObjects/10817_2022_9655_Figka_HTML.gif

mode.

Abel, A., Coquand, T., Pagano, M.: A modular type-checking algorithm for type theory with singleton types and proof irrelevance. Log. Methods Comput. Sci. (2011). https://doi.org/10.2168/LMCS-7(2:4)2011MathSciNetCrossRefMATH

Appel, A.W.: Verified Software Toolchain. In: 20th European Symposium on Programming (ESOP’11), LNCS, vol. 6602, 1–17. Springer (2011). https://doi.org/10.1007/978-3-642-19718-5_1

Appel, A.W.: Verified Functional Algorithms, Software Foundations, vol. 3. softwarefoundations.org (2017). https://softwarefoundations.cis.upenn.edu/vfa-current

Appel, A.W., Dockins, R., Hobor, A., Beringer, L., Dodds, J., Stewart, G., Blazy, S., Leroy, X.: Program logics for certified compilers. Cambridge University Press, Cambridge (2014)CrossRefMATH

Beringer, L.: Verified software units. In: 30th European Symposium on Programming (ESOP’21), LNCS, vol. 12648, 118–147. Springer (2021). https://doi.org/10.1007/978-3-030-72019-3_5

Beringer, L., Appel, A.W.: Abstraction and subsumption in modular verification of C programs. Formal Methods Syst. Des. 58(1), 322–345 (2021). https://doi.org/10.1007/s10703-020-00353-1CrossRefMATH

Boyer, R.S., Moore, J.S.: Single-threaded objects in ACL2. In: Practical Aspects of Declarative Languages, 4th International Symposium (PADL’02), LNCS, vol. 2257, pp. 9–27. Springer (2002). https://doi.org/10.1007/3-540-45587-6_3

Cao, Q., Beringer, L., Gruetter, S., Dodds, J., Appel, A.W.: VST-Floyd: a separation logic tool to verify correctness of C programs. J. Autom. Reason. 61(1–4), 367–422 (2018). https://doi.org/10.1007/s10817-018-9457-5MathSciNetCrossRefMATH

Filliâtre, J.-C., Letouzey, P.: Functors for proofs and programs. In: 13th European Symposium on Programming, ESOP 2004, LNCS, vol. 2986, pp. 370–384. Springer (2004). https://doi.org/10.1007/978-3-540-24725-8_26

10.

Gordon, M.J., Milner, R., Wadsworth, C.P.: Edinburgh LCF: A Mechanised Logic of Computation. Lecture Notes in Computer Science, vol. 78. Springer, New York (1979)

11.

Jourdan, J.H., Laporte, V., Blazy, S., Leroy, X., Pichardie, D.: A formally-verified C static analyzer. In: POPL 2015: 42nd symposium Principles of Programming Languages, pp. 247–259. ACM (2015). https://doi.org/10.1145/2676726.2676966

12.

Krebbers, R., et al.: The Coq-std++ extended standard library, module stdpp.pmap (2012–2021). https://plv.mpi-sws.org/coqdoc/stdpp/stdpp.pmap.html

13.

Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009). https://doi.org/10.1145/1538788.1538814CrossRef

14.

Leroy, X., Appel, A.W.: Canonical binary trees, the Coq development, version 2 (2022). https://github.com/xavierleroy/canonical-binary-tries/tree/v2. Software Heritage ID swh:1:dir:02996583ae02411d8e1e7c3f20bc12b0eebbf96a

15.

Leroy, X., Appel, A.W., Doligez, D.: The CompCert verified C compiler, module Maps (2021–2022). https://compcert.org/doc-3.10/html/compcert.lib.Maps.html. Software Heritage ID swh:1:cnt:0d83aa98a1d7cc150a3164ad487d9cde9c00a64f

16.

Leroy, X., Doligez, D.: The CompCert verified C compiler, module Maps (2005–2021). https://compcert.org/doc-3.9/html/compcert.lib.Maps.html. Software Heritage ID swh:1:cnt:6bc6e14bf54f778029e13b192aaab53dd5e819a4

17.

Letouzey, P.: MMaps: Modular finite maps over ordered types (2015–2020). https://github.com/letouzey/coq-mmaps

18.

Nipkow, T., Blanchette, J., Eberl, M., Gómez-Londoño, A., Lammich, P., Sternagel, C., Wimmer, S., Zhan, B.: Functional Algorithms, Verified! (2021). https://functional-algorithms-verified.org

19.

Pujet, L., Tabareau, N.: Observational equality: now for good. Proc. ACM Program. Lang. (2022). https://doi.org/10.1145/3498693CrossRef

Titel: Efficient Extensional Binary Tries
verfasst von: Andrew W. Appel
Xavier Leroy
Publikationsdatum: 01.03.2023
Verlag: Springer Netherlands
Erschienen in: Journal of Automated Reasoning / Ausgabe 1/2023
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-022-09655-x

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 1/2023

Correction: Towards Formalising Schutz’ Axioms for Minkowski Spacetime in Isabelle/HOL

Superposition for Higher-Order Logic

Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic

A Solver for Arrays with Concatenation

Computer-Aided Constructions of Commafree Codes

Measuring the Readability of Geometric Proofs: The Area Method Case