Skip to main content
SpringerLink
Log in

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

  • Published:
Journal of Automated Reasoning Aims and scope Submit manuscript

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10

Similar content being viewed by others

Notes

  1. This explanation is deliberately slightly informal. It is written as though an OCaml value v could be viewed as a Coq value, and avoids mentioning the type of v. In reality, CFML includes machinery for translating an OCaml type \(\tau \) to a Coq type \(\llbracket \tau \rrbracket \) and reflecting an OCaml value v as a Coq value \(\llbracket v \rrbracket \) of type \(\llbracket \tau \rrbracket \). For more details about this translation, the reader is referred to Charguéraud’s work [15].

  2. Hilbert’s \(\epsilon \) operator applies to a predicate P of type \(A\rightarrow \textsf {Prop}\), where A is an inhabited type. It produces a value v of type A such that \(\exists x.P\, x\) implies \(P\,v\).

  3. One known source of unsoundness in CFML is the gap between OCaml machine integers and Coq ideal integers, which we have discussed already (Sect. 2.2).

  4. This argument assumes that the programming language has neither iteration statements (while, for, etc.) nor unstructured control statements (break, continue, goto, etc.). One way of dealing with these statements is to encode them in terms of recursive functions, so that, after this encoding, “counting every function call” is indeed sufficient.

  5. Requiring \((Q\;v \,\star \,\top )\;m'\) is equivalent to requiring that \(Q\;v\) be satisfied by some fragment of \(m'\). This condition is more permissive than \(Q\;v\;m'\). This yields extra flexibility: the postcondition need not describe all of the final heap; it may describe just a part of it. This interpretation allows validating the “garbage collection” rule, that is, rule  in Fig. 5.

References

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

    MATH  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  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)

  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)

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  7. Aspinall, D., Hofmann, M., Konečný, M.: A type system with usage aspects. J. Funct. Program. 18(2), 141–178 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Article  MATH  Google Scholar 

  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)

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

  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)

  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)

  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)

  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)

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

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

    MATH  Google Scholar 

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

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

  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)

  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)

    Article  Google Scholar 

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

    Article  Google Scholar 

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

    Article  MATH  Google Scholar 

  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)

    Article  Google Scholar 

  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)

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

    Article  MATH  Google Scholar 

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

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

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

    MathSciNet  MATH  Google Scholar 

  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)

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

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Article  MATH  Google Scholar 

  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)

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

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

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

  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)

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

  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)

    Article  Google Scholar 

  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)

    Google Scholar 

  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)

  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)

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

    Article  MathSciNet  MATH  Google Scholar 

  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)

  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)

    MATH  Google Scholar 

  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)

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

  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)

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

  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)

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Inria, Paris, France

    Arthur Charguéraud & François Pottier

  2. LRI, CNRS & Université Paris-Sud, Orsay, France

    Arthur Charguéraud

Authors
  1. Arthur Charguéraud
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. François Pottier
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Arthur Charguéraud.

Additional information

This research was partly supported by the French National Research Agency (ANR) under the Grant ANR-15-CE25-0008.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Charguéraud, A., Pottier, F. Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits. J Autom Reasoning 62, 331–365 (2019). https://doi.org/10.1007/s10817-017-9431-7

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

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

Keywords

Search

Navigation