×

Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits. (English) Zbl 1468.68120

Summary: 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.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B70 Logic in computer science
68N18 Functional programming and lambda calculus
68P05 Data structures
68V20 Formalization of mathematics in connection with theorem provers
PDFBibTeX XMLCite
Full Text: DOI HAL

References:

[1] Aho, A.V., Hopcroft, J.E., Ullman, J.D.: The Design and Analysis of Computer Algorithms. Addison-Wesley, Boston (1974) · Zbl 0326.68005
[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) · Zbl 1398.68101 · doi:10.1145/2636922
[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) · Zbl 1367.68046
[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) · Zbl 1445.68057
[5] Appel, A.W.: Compiling with Continuations. Cambridge University Press, Cambridge (1992)
[6] Aspinall, D., Beringer, L., Hofmann, M., Loidl, H., Momigliano, A.: A program logic for resources. Theor. Comput. Sci. 389(3), 411-445 (2007) · Zbl 1133.68010 · doi:10.1016/j.tcs.2007.09.003
[7] Aspinall, D., Hofmann, M., Konečný, M.: A type system with usage aspects. J. Funct. Program. 18(2), 141-178 (2008) · Zbl 1142.68019 · doi:10.1017/S0956796807006399
[8] Atkey, R.: Amortised resource analysis with separation logic. Log. Methods Comput. Sci. 7(2:17) (2011) · Zbl 1260.68083
[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) · Zbl 1367.68046
[10] Baker, H.G.: List processing in real time on a serial computer. Commun. ACM 21(4), 280-294 (1978) · Zbl 0371.68009 · doi:10.1145/359460.359470
[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) · Zbl 1069.68095
[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) · Zbl 1323.68202
[15] Charguéraud. A. Characteristic formulae for the verification of imperative programs. Unpublished (2013) · Zbl 1323.68366
[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) · Zbl 1465.68172
[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) · Zbl 1302.68087
[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) · Zbl 1187.68679
[24] Crary, K., Weirich, S.: Resource bound certification. In: Principles of Programming Languages (POPL), pp. 184-198 (2000) · Zbl 1323.68368
[25] Danielsson, N.A.: Lightweight semiformal time complexity analysis for purely functional data structures. In: Principles of Programming Languages (POPL) (2008) · Zbl 1295.68060
[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) · doi:10.1145/130616.130620
[28] Galil, Z., Italiano, G.F.: Data structures and algorithms for disjoint set union problems. ACM Comput. Surv. 23(3), 319-344 (1991) · doi:10.1145/116873.116878
[29] Galler, B.A., Fischer, M.J.: An improved equivalence algorithm. Commun. ACM 7(5), 301-303 (1964) · Zbl 0129.10302 · doi:10.1145/364099.364331
[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) · Zbl 1485.68030
[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) · doi:10.1145/356458.356463
[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) · Zbl 1260.68074
[33] Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. ACM Trans. Programm. Lang. Syst. 34(3), 14:1-14:62 (2012) · Zbl 1284.68132 · doi:10.1145/2362389.2362393
[34] Hoffmann, J., Marmar, M., Shao, Z.: Quantitative reasoning for proving lock-freedom. In: Logic in Computer Science (LICS), pp. 124-133 (2013) · Zbl 1366.68171
[35] Hoffmann, J., Das, A., Weng, S.: Towards automatic resource bound analysis for OCaml. In: Principles of Programming Languages (POPL), pp. 359-373 (2017) · Zbl 1380.68123
[36] Hofmann, M.: A type system for bounded space and functional in-place update. Nordic J. Comput. 7(4), 258-289 (2000) · Zbl 0971.68023
[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) · Zbl 1321.68180
[38] Hopcroft, J.E., Ullman, J.D.: Set merging algorithms. SIAM J. Comput. 2(4), 294-303 (1973) · Zbl 0253.68003 · doi:10.1137/0202024
[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) · Zbl 07662226
[41] Hutton, G.: A tutorial on the universality and expressiveness of fold. J. Funct. Program. 9(4), 355-372 (1999) · Zbl 0948.68036 · doi:10.1017/S0956796899003500
[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) · Zbl 1346.68135
[43] Jung, R., Krebbers, R., Birkedal, L., Dreyer, D.: Higher-order ghost state. In: International Conference on Functional Programming (ICFP), pp. 256-269 (2016) · Zbl 1361.68066
[44] Kaplan, H., Shafrir, N., Tarjan, R.E.: Union-find with deletions. In: Symposium on Discrete Algorithms (SODA), pp. 19-28 (2002) · Zbl 1093.68577
[45] Kozen, D.C.: The design and analysis of algorithms. Texts and Monographs in Computer Science, Springer (1992) · Zbl 0757.68083
[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) · Zbl 1485.68069
[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) · doi:10.1145/42190.42347
[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) · Zbl 1380.68099
[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) · Zbl 1475.68457
[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) · Zbl 1187.68158
[56] Nanevski, A., Morrisett, G., Birkedal, L.: Hoare type theory, polymorphism and separation. J. Funct. Program. 18(5-6), 865-911 (2008) · Zbl 1155.68354 · doi:10.1017/S0956796808006953
[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) · Zbl 1323.68142
[58] Nipkow, T.: Amortized complexity verified. In: Interactive Theorem Proving (ITP). Lecture Notes in Computer Science, vol. 9236, pp. 310-324. Springer (2015) · Zbl 1465.68059
[59] Okasaki, C.: Purely Functional Data Structures. Cambridge University Press, Cambridge (1999) · Zbl 0941.68032
[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) · Zbl 1026.68020
[65] Seidel, R., Sharir, M.: Top-down analysis of path compression. SIAM J. Comput. 34(3), 515-525 (2005) · Zbl 1075.68105 · doi:10.1137/S0097539703439088
[66] Tarjan, R.E.: Efficiency of a good but not linear set union algorithm. J. ACM 22(2), 215-225 (1975) · Zbl 0307.68029 · doi:10.1145/321879.321884
[67] Tarjan, R.E.: Amortized computational complexity. SIAM J. Algebraic Discrete Method 6(2), 306-318 (1985) · Zbl 0599.68046 · doi:10.1137/0606031
[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) · Zbl 0632.68043 · doi:10.1145/62.2160
[70] Wegbreit, B.: Mechanical program analysis. Commun. ACM 18(9), 528-539 (1975) · Zbl 0306.68008 · doi:10.1145/361002.361016
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.