More Web Proxy on the site http://driver.im/

article

Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits

Authors:

Arthur Charguéraud,

François PottierAuthors Info & Claims

Journal of Automated Reasoning, Volume 62, Issue 3

Pages 331 - 365

https://doi.org/10.1007/s10817-017-9431-7

Published: 01 March 2019 Publication History

Abstract

Union-Find is a famous example of a simple data structure whose amortized asymptotic time complexity analysis is nontrivial. We present a Coq formalization of this analysis, following Alstrup et al.'s recent proof. Moreover, we implement Union-Find as an OCaml library and formally endow it with a modular specification that offers a full functional correctness guarantee as well as an amortized complexity bound. In order to reason in Coq about imperative OCaml code, we use the CFML tool, which implements Separation Logic for a subset of OCaml, and which we extend with time credits. Although it was known in principle that amortized analysis can be explained in terms of time credits and that time credits can be viewed as resources in Separation Logic, we believe our work is the first practical demonstration of this approach. Finally, in order to explain the meta-theoretical foundations of our approach, we define a Separation Logic with time credits for an untyped call-by-value $$\lambda $$?-calculus, and formally verify its soundness.

References

[1]

Aho, A.V., Hopcroft, J.E., Ullman, J.D.: The Design and Analysis of Computer Algorithms. Addison-Wesley, Boston (1974)

Digital Library

[2]

Alstrup, S., Thorup, M., GØrtz, I.L., Rauhe, T., Zwick, U.: Union-find with constant time deletions. ACM Trans. Algorithms 11(1), 6:1---6:28 (2014)

Digital Library

[3]

Amadio, R., Régis-Gianas, Y.: Certifying and reasoning on cost annotations of functional programs. In: Foundational and Practical Aspects of Resource Analysis. Lecture Notes in Computer Science, vol. 7177, pp. 72---89. Springer (2011)

Digital Library

[4]

Amadio, R.M., Ayache, N., Bobot, F., Boender, J., Campbell, B., Garnier, I., Madet, A., McKinna, J., Mulligan, D.P., Piccolo, M., Pollack, R., Régis-Gianas, Y., Coen, C.S., Stark, I., Tranquilli, P. Certified complexity (CerCo). In: Foundational and Practical Aspects of Resource Analysis. Lecture Notes in Computer Science, vol. 8552, pp. 1---18. Springer (2014)

[5]

Appel, A.W.: Compiling with Continuations. Cambridge University Press, Cambridge (1992)

Digital Library

[6]

Aspinall, D., Beringer, L., Hofmann, M., Loidl, H., Momigliano, A.: A program logic for resources. Theor. Comput. Sci. 389(3), 411---445 (2007)

Digital Library

[7]

Aspinall, D., Hofmann, M., Koneă?n?, M.: A type system with usage aspects. J. Funct. Program. 18(2), 141---178 (2008)

Digital Library

[8]

Atkey, R.: Amortised resource analysis with separation logic. Log. Methods Comput. Sci. 7(2:17) (2011)

[9]

Ayache, N., Amadio, R.M., Régis-Gianas, Y.: Certifying and reasoning on cost annotations in C programs. In: Formal Methods for Industrial Critical Systems. Lecture Notes in Computer Science, vol. 7437, pp. 32---46. Springer (2012)

[10]

Baker, H.G.: List processing in real time on a serial computer. Commun. ACM 21(4), 280---294 (1978)

Digital Library

[11]

Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development---Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series, Springer (2004)

Digital Library

[12]

Blelloch, G.E., Greiner, J.: Parallelism in sequential functional languages. In: Functional Programming Languages and Computer Architecture (FPCA), pp. 226---237 (1995)

Digital Library

[13]

Carbonneaux, Q., Hoffmann, J., Ramananandro, T., Shao, Z.: End-to-end verification of stack-space bounds for C programs. In: Programming Language Design and Implementation (PLDI), pp. 270---281 (2014)

Digital Library

[14]

Charguéraud, A.: Characteristic formulae for mechanized program verification. PhD thesis, Université Paris 7 (2010)

[15]

Charguéraud. A. Characteristic formulae for the verification of imperative programs. Unpublished (2013)

[16]

Charguéraud, A., Pottier, F.: Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation. In: Interactive Theorem Proving (ITP). Lecture Notes in Computer Science, vol. 9236, pp. 137---153. Springer (2015)

[17]

Charguéraud, A., Pottier, F.: Online accompanying material (2017)

[18]

Chlipala, A.: The Bedrock structured programming system: combining generative metaprogramming and Hoare logic in an extensible program verifier. In: International Conference on Functional Programming (ICFP), pp. 391---402 (2013)

Digital Library

[19]

Chlipala, A., Malecha, G., Morrisett, G., Shinnar, A., Wisnesky, R.: Effective interactive proofs for higher-order imperative programs. In: International Conference on Functional Programming (ICFP), pp. 79---90 (2009)

Digital Library

[20]

Chlipala, A., Malecha, G., Morrisett, G., Shinnar, A., Sozeau, M., Wisnesky, R.: Ynot (2011)

[21]

Clochard, M., Filliâtre, J.C., Paskevich, A.: How to avoid proving the absence of integer overflows. In: Verified Software: Theories, Tools and Experiments. Lecture Notes in Computer Science, vol. 9593, pp. 94---109. Springer (2015)

Digital Library

[22]

Conchon, S., Filliâtre, J.: A persistent union-find data structure. In: ACM Workshop on ML, pp. 37---46 (2007)

Digital Library

[23]

Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. MIT Press, Cambridge (2009)

Digital Library

[24]

Crary, K., Weirich, S.: Resource bound certification. In: Principles of Programming Languages (POPL), pp. 184---198 (2000)

Digital Library

[25]

Danielsson, N.A.: Lightweight semiformal time complexity analysis for purely functional data structures. In: Principles of Programming Languages (POPL) (2008)

Digital Library

[26]

Danner, N., Paykin, J., Royer, J.S.: A static cost analysis for a higher-order language. In: Programming Languages Meets Program Verification (PLPV), pp. 25---34 (2013)

Digital Library

[27]

Dornic, V., Jouvelot, P., Gifford, D.K.: Polymorphic time systems for estimating program complexity. ACM Lett. Program. Lang. Syst. 1(1), 33---45 (1992)

Digital Library

[28]

Galil, Z., Italiano, G.F.: Data structures and algorithms for disjoint set union problems. ACM Comput. Surv. 23(3), 319---344 (1991)

Digital Library

[29]

Galler, B.A., Fischer, M.J.: An improved equivalence algorithm. Commun. ACM 7(5), 301---303 (1964)

Digital Library

[30]

Guéneau, A., Myreen, M.O., Kumar, R., Norrish, M.: Verified characteristic formulae for CakeML. In: European Symposium on Programming (ESOP). Lecture Notes in Computer Science, vol. 10201, pp. 584---610. Springer (2017)

[31]

Harfst, G.C., Reingold, E.M.: A potential-based amortized analysis of the union-find data structure. SIGACT News 31(3), 86---95 (2000)

Digital Library

[32]

Hoffmann, J., Hofmann, M.: Amortized resource analysis with polynomial potential. In: European Symposium on Programming (ESOP). Lecture Notes in Computer Science, vol. 6012, pp. 287---306. Springer (2010)

Digital Library

[33]

Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. ACM Trans. Programm. Lang. Syst. 34(3), 14:1---14:62 (2012)

Digital Library

[34]

Hoffmann, J., Marmar, M., Shao, Z.: Quantitative reasoning for proving lock-freedom. In: Logic in Computer Science (LICS), pp. 124---133 (2013)

Digital Library

[35]

Hoffmann, J., Das, A., Weng, S.: Towards automatic resource bound analysis for OCaml. In: Principles of Programming Languages (POPL), pp. 359---373 (2017)

Digital Library

[36]

Hofmann, M.: A type system for bounded space and functional in-place update. Nordic J. Comput. 7(4), 258---289 (2000)

Digital Library

[37]

Hofmann, M., Jost, S.: Static prediction of heap space usage for first-order functional programs. In: Principles of Programming Languages (POPL), pp. 185---197 (2003)

Digital Library

[38]

Hopcroft, J.E., Ullman, J.D.: Set merging algorithms. SIAM J. Comput. 2(4), 294---303 (1973)

Digital Library

[39]

Howell, R.R.: On asymptotic notation with multiple variables. Tech. Rep. 2007-4, Kansas State University (2008)

[40]

Howell, R.R.: Algorithms: a top-down approach. Draft (2012)

[41]

Hutton, G.: A tutorial on the universality and expressiveness of fold. J. Funct. Program. 9(4), 355---372 (1999)

Digital Library

[42]

Jung, R., Swasey, D., Sieczkowski, F., Svendsen, K., Turon, A., Birkedal, L., Dreyer, D.: Iris: monoids and invariants as an orthogonal basis for concurrent reasoning. In: Principles of Programming Languages (POPL), pp. 637---650 (2015)

Digital Library

[43]

Jung, R., Krebbers, R., Birkedal, L., Dreyer, D.: Higher-order ghost state. In: International Conference on Functional Programming (ICFP), pp. 256---269 (2016)

Digital Library

[44]

Kaplan, H., Shafrir, N., Tarjan, R.E.: Union-find with deletions. In: Symposium on Discrete Algorithms (SODA), pp. 19---28 (2002)

Digital Library

[45]

Kozen, D.C.: The design and analysis of algorithms. Texts and Monographs in Computer Science, Springer (1992)

Digital Library

[46]

Krebbers, R., Jung, R., Bizjak, A., Jourdan, J.H., Dreyer, D., Birkedal, L.: The essence of higher-order concurrent separation logic. In: European Symposium on Programming (ESOP). Lecture Notes in Computer Science, vol. 10201, pp. 696---723. Springer (2017)

Digital Library

[47]

Krishnaswami, N.R.: Verifying higher-order imperative programs with higher-order separation logic. PhD thesis, School of Computer Science, Carnegie Mellon University (2012)

Digital Library

[48]

Lammich, P., Meis, R.: A separation logic framework for Imperative HOL. Archive of Formal Proofs (2012)

[49]

Le Métayer, D.: ACE: an automatic complexity evaluator. ACM Trans. Program. Lang. Syst. 10(2), 248---266 (1988)

Digital Library

[50]

Leino, K.R.M., Moskal, M.: VACID-0: Verification of ample correctness of invariants of data-structures, edition 0, manuscript KRML 209 (2010)

[51]

MacKenzie, K., Wolverson, N.: Camelot and Grail: resource-aware functional programming for the JVM. Trends Funct. Program. 4, 29---46 (2003)

[52]

Madhavan, R., Kulal, S., Kuncak, V.: Contract-based resource verification for higher-order functions with memoization. In: Principles of Programming Languages (POPL), pp. 330---343 (2017)

Digital Library

[53]

McCarthy, J.A., Fetscher, B., New, M.S., Feltey, D., Findler, R.B.: A Coq library for internal verification of running-times. In: Functional and Logic Programming, Lecture Notes in Computer Science, vol. 9613, pp. 144---162. Springer (2016)

[54]

Müller, P., Schwerhoff, M., Summers, A.J.: Automatic verification of iterated separating conjunctions using symbolic execution. In: Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 9779, pp. 405---425. Springer (2016)

[55]

Nanevski, A., Ahmed, A., Morrisett, G., Birkedal, L.: Abstract predicates and mutable ADTs in Hoare type theory. In: European Symposium on Programming (ESOP). Lecture Notes in Computer Science, vol. 4421, pp. 189---204. Springer (2007)

Digital Library

[56]

Nanevski, A., Morrisett, G., Birkedal, L.: Hoare type theory, polymorphism and separation. J. Funct. Program. 18(5---6), 865---911 (2008)

Digital Library

[57]

Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P., Birkedal, L.: Ynot: dependent types for imperative programs. In: International Conference on Functional Programming (ICFP), pp. 229---240 (2008)

Digital Library

[58]

Nipkow, T.: Amortized complexity verified. In: Interactive Theorem Proving (ITP). Lecture Notes in Computer Science, vol. 9236, pp. 310---324. Springer (2015)

[59]

Okasaki, C.: Purely Functional Data Structures. Cambridge University Press, Cambridge (1999)

Digital Library

[60]

Patwary, M.M.A., Blair, J., Manne, F.: Experiments on union-find algorithms for the disjoint-set data structure. In: International Symposium on Experimental Algorithms (SEA). Lecture Notes in Computer Science, vol. 6049, pp. 411---423. Springer (2010)

Digital Library

[61]

Pilkiewicz, A., Pottier, F.: The essence of monotonic state. In: Types in Language Design and Implementation (TLDI) (2011)

Digital Library

[62]

Reistad, B., Gifford, D.K.: Static dependent costs for estimating execution time. In: ACM Symposium on Lisp and Functional Programming (LFP), pp. 65---78 (1994)

Digital Library

[63]

Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Logic in Computer Science (LICS), pp. 55---74 (2002)

Digital Library

[64]

Sands, D., Gustavsson, J., Moran, A.: Lambda calculi and linear speedups. In: The Essence of Computation, Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones. Lecture Notes in Computer Science, vol. 2566, pp. 60---84. Springer (2002)

Digital Library

[65]

Seidel, R., Sharir, M.: Top-down analysis of path compression. SIAM J. Comput. 34(3), 515---525 (2005)

Digital Library

[66]

Tarjan, R.E.: Efficiency of a good but not linear set union algorithm. J. ACM 22(2), 215---225 (1975)

Digital Library

[67]

Tarjan, R.E.: Amortized computational complexity. SIAM J. Algebraic Discrete Method 6(2), 306---318 (1985)

[68]

Tarjan, R.E. Class notes: Disjoint set union (1999)

[69]

Tarjan, R.E., van Leeuwen, J.: Worst-case analysis of set union algorithms. J. ACM 31(2), 245---281 (1984)

Digital Library

[70]

Wegbreit, B.: Mechanical program analysis. Commun. ACM 18(9), 528---539 (1975)

Digital Library

Cited By

Haselwarter PLi Kde Medeiros MGregersen SAguirre ATassarotti JBirkedal L(2024)Tachis: Higher-Order Separation Logic with Credits for Expected CostsProceedings of the ACM on Programming Languages10.1145/36897538:OOPSLA2(1189-1218)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689753
Allain CClément BMoine AScherer G(2024)Snapshottable StoresProceedings of the ACM on Programming Languages10.1145/36746378:ICFP(338-369)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674637
Aguirre AHaselwarter Pde Medeiros MLi KGregersen STassarotti JBirkedal L(2024)Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36746358:ICFP(284-316)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674635
Show More Cited By

Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits
1. Theory of computation

Recommendations

Higher-Order Separation Logic in Isabelle/HOLCF

We formalize higher-order separation logic for a first-order imperative language with procedures and local variables in Isabelle/HOLCF. The assertion language is modeled in such a way that one may use any theory defined in Isabelle/HOLCF to construct ...
Interactive proofs in higher-order concurrent separation logic
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

When using a proof assistant to reason in an embedded logic -- like separation logic -- one cannot benefit from the proof contexts and basic tactics of the proof assistant. This results in proofs that are at a too low level of abstraction because they ...
Interactive proofs in higher-order concurrent separation logic
POPL '17

When using a proof assistant to reason in an embedded logic -- like separation logic -- one cannot benefit from the proof contexts and basic tactics of the proof assistant. This results in proofs that are at a too low level of abstraction because they ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Journal of Automated Reasoning

Journal of Automated Reasoning Volume 62, Issue 3

March 2019

127 pages

ISSN:0168-7433

Issue’s Table of Contents

Copyright © Copyright © 2019 Springer Nature B.V.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 March 2019

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

23
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 23 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Haselwarter PLi Kde Medeiros MGregersen SAguirre ATassarotti JBirkedal L(2024)Tachis: Higher-Order Separation Logic with Credits for Expected CostsProceedings of the ACM on Programming Languages10.1145/36897538:OOPSLA2(1189-1218)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689753
Allain CClément BMoine AScherer G(2024)Snapshottable StoresProceedings of the ACM on Programming Languages10.1145/36746378:ICFP(338-369)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674637
Aguirre AHaselwarter Pde Medeiros MLi KGregersen STassarotti JBirkedal L(2024)Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36746358:ICFP(284-316)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674635
Gregersen SAguirre AHaselwarter PTassarotti JBirkedal L(2024)Almost-Sure Termination by Guarded RefinementProceedings of the ACM on Programming Languages10.1145/36746328:ICFP(203-233)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674632
Pham LSaad FHoffmann J(2024)Robust Resource Bounds with Static Analysis and Bayesian InferenceProceedings of the ACM on Programming Languages10.1145/36563808:PLDI(76-101)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656380
Wang ZCao QTao Y(2024)Verifying Programs with Logic and Extended Proof Rules: Deep Embedding vs. Shallow EmbeddingJournal of Automated Reasoning10.1007/s10817-024-09706-568:3Online publication date: 10-Aug-2024
https://dl.acm.org/doi/10.1007/s10817-024-09706-5
Zhang TSharma UKapritsos M(2023)Performal: Formal Verification of Latency Properties for Distributed SystemsProceedings of the ACM on Programming Languages10.1145/35912357:PLDI(368-393)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591235
Charguéraud AChlipala AErbsen AGruetter S(2023)Omnisemantics: Smooth Handling of NondeterminismACM Transactions on Programming Languages and Systems10.1145/357983445:1(1-43)Online publication date: 8-Mar-2023
https://dl.acm.org/doi/10.1145/3579834
Batz KKaminski BKatoen JMatheja CVerscht L(2023)A Calculus for Amortized Expected RuntimesProceedings of the ACM on Programming Languages10.1145/35712607:POPL(1957-1986)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571260
Banerjee ANagasamudram RNaumann DNikouei M(2023)A Relational Program Logic with Data Abstraction and Dynamic FramingACM Transactions on Programming Languages and Systems10.1145/355149744:4(1-136)Online publication date: 10-Jan-2023
https://dl.acm.org/doi/10.1145/3551497
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents