Document Open Access Logo

mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity

Authors Clément Aubert , Thomas Rubiano, Neea Rusch , Thomas Seiller

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2022.26.pdf
  • Filesize: 0.93 MB
  • 23 pages

Document Identifiers

Author Details

Clément Aubert
  • School of Computer and Cyber Sciences, Augusta University, GA, USA
Thomas Rubiano
  • LIPN - UMR 7030 Université Sorbonne Paris Nord, France
Neea Rusch
  • School of Computer and Cyber Sciences, Augusta University, GA, USA
Thomas Seiller
  • LIPN - UMR 7030 Université Sorbonne Paris Nord, France
  • CNRS, Paris, France

Funding

This research is supported by the https://face-foundation.org/higher-education/thomas-jefferson-fund/ of the Embassy of France in the United States and the FACE Foundation (https://face-foundation.org/), and has benefited from the research meeting 21453 "Static Analyses of Program Flows: Types and Certificate for Complexity" (https://www.dagstuhl.de/21453) in Schloss Dagstuhl. Th. Rubiano and Th. Seiller are supported by the Île-de-France region through the DIM RFSI project "CoHOp".

Acknowledgements

The authors wish to express their gratitude to Assya Sellak for her contribution to this work, to the reviewers of previous versions for their comments, and to the https://fscd-conference.org/ community: in particular, the reviews we received were extremely interesting, and generated new directions and questions, for which we are thankful.

Cite AsGet BibTex

Clément Aubert, Thomas Rubiano, Neea Rusch, and Thomas Seiller. mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 26:1-26:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.FSCD.2022.26

Abstract

Implicit Computational Complexity (ICC) drives better understanding of complexity classes, but it also guides the development of resources-aware languages and static source code analyzers. Among the methods developed, the mwp-flow analysis [Jones and Lars Kristiansen, 2009] certifies polynomial bounds on the size of the values manipulated by an imperative program. This result is obtained by bounding the transitions between states instead of focusing on states in isolation, as most static analyzers do, and is not concerned with termination or tight bounds on values. Those differences, along with its built-in compositionality, make the mwp-flow analysis a good target for determining how ICC-inspired techniques diverge compared with more traditional static analysis methods. This paper’s contributions are three-fold: we fine-tune the internal machinery of the original analysis to make it tractable in practice; we extend the analysis to function calls and leverage its machinery to compute the result of the analysis efficiently; and we implement the resulting analysis as a lightweight tool to automatically perform data-size analysis of C programs. This documented effort prepares and enables the development of certified complexity analysis, by transforming a costly analysis into a tractable program, that furthermore decorrelates the problem of deciding if a bound exist with the problem of computing it.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Automated static analysis
  • Theory of computation → Complexity theory and logic
  • Theory of computation → Logic and verification
Keywords
  • Static Program Analysis
  • Implicit Computational Complexity
  • Automatic Complexity Analysis
  • Program Verification

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. Elvira Albert, Puri Arenas, Samir Genaim, German Puebla, and Damiano Zanardini. COSTA: design and implementation of a cost and termination analyzer for java bytecode. In Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem P. de Roever, editors, Formal Methods for Components and Objects, 6th International Symposium, FMCO 2007, Amsterdam, The Netherlands, October 24-26, 2007, Revised Lectures, volume 5382 of LNCS, pages 113-132. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-92188-2_5.
  2. Roberto M. Amadio, Nicholas Ayache, François Bobot, Jaap Boender, Brian Campbell, Ilias Garnier, Antoine Madet, James McKinna, Dominic P. Mulligan, Mauro Piccolo, Randy Pollack, Yann Régis-Gianas, Claudio Sacerdoti Coen, Ian Stark, and Paolo Tranquilli. Certified complexity (cerco). In Ugo Dal Lago and Ricardo Peña, editors, Foundational and Practical Aspects of Resource Analysis - Third International Workshop, FOPARA 2013, Bertinoro, Italy, August 29-31, 2013, Revised Selected Papers, volume 8552 of LNCS, pages 1-18. Springer, 2013. URL: https://doi.org/10.1007/978-3-319-12466-7_1.
  3. Clément Aubert, Thomas Rubiano, Neea Rusch, and Thomas Seiller. Lqicm on c toy parser. URL: https://github.com/statycc/LQICM_On_C_Toy_Parser.
  4. Clément Aubert, Thomas Rubiano, Neea Rusch, and Thomas Seiller. mwp-analysis improvement and implementation: Realizing implicit computational complexity. Preliminary technical report, March 2022. URL: https://hal.archives-ouvertes.fr/hal-03596285.
  5. Martin Avanzini and Ugo Dal Lago. Automating sized-type inference for complexity analysis. Proc. ACM Program. Lang., 1(ICFP):43:1-43:29, 2017. URL: https://doi.org/10.1145/3110287.
  6. Patrick Baillot and Kazushige Terui. Light types for polynomial time computation in lambda-calculus. In LICS, pages 266-275. IEEE Computer Society, 2004. URL: https://doi.org/10.1109/LICS.2004.1319621.
  7. Gilles Barthe, Delphine Demange, and David Pichardie. Formal verification of an SSA-based middle-end for compcert. ACM Trans. Program. Lang. Syst., 36(1):4:1-4:35, 2014. URL: https://doi.org/10.1145/2579080.
  8. Stephen J. Bellantoni and Stephen Arthur Cook. A new recursion-theoretic characterization of the polytime functions (extended abstract). In S. Rao Kosaraju, Mike Fellows, Avi Wigderson, and John A. Ellis, editors, STOC, pages 283-93. ACM, 1992. URL: https://doi.org/10.1145/129712.129740.
  9. Amir M. Ben-Amram. On decidable growth-rate properties of imperative programs. In Patrick Baillot, editor, Proceedings International Workshop on Developments in Implicit Computational complExity, DICE 2010, Paphos, Cyprus, 27-28th March 2010, volume 23 of EPTCS, pages 1-14, 2010. URL: https://doi.org/10.4204/EPTCS.23.1.
  10. Amir M. Ben-Amram and Geoff W. Hamilton. Tight polynomial worst-case bounds for loop programs. Log. Meth. Comput. Sci., 16(2), 2020. URL: https://doi.org/10.23638/LMCS-16(2:4)2020.
  11. Amir M. Ben-Amram, Neil D. Jones, and Lars Kristiansen. Linear, polynomial or exponential? complexity inference in polynomial time. In Arnold Beckmann and Costas Dimitracopoulos andBenedikt Löwe, editors, Logic and Theory of Algorithms, 4th Conference on Computability inEurope, CiE 2008, Athens, Greece, June 15-20, 2008, Proceedings, volume 5028 of LNCS, pages 67-76. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-69407-6_7.
  12. Quentin Carbonneaux, Jan Hoffmann, and Zhong Shao. Compositional certified resource bounds. In David Grove and Stephen M. Blackburn, editors, Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015, pages 467-478. ACM, 2015. URL: https://doi.org/10.1145/2737924.2737955.
  13. Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Robert M. Graham, Michael A. Harrison, and Ravi Sethi, editors, Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, pages 238-252. ACM, 1977. URL: https://doi.org/10.1145/512950.512973.
  14. Patrick Cousot and Radhia Cousot. Static determination of dynamic properties of recursive procedures. In Erich J. Neuhold, editor, Formal Description of Programming Concepts: Proceedings of the IFIP Working Conference on Formal Description of Programming Concepts, St. Andrews, NB, Canada, August 1-5, 1977, pages 237-278. North-Holland, 1977. Google Scholar
  15. Ugo Dal Lago. A short introduction to implicit computational complexity. In Nick Bezhanishvili and Valentin Goranko, editors, ESSLLI, volume 7388 of LNCS, pages 89-109. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-31485-8_3.
  16. Antonio Flores-Montoya. Upper and lower amortized cost bounds of programs expressed as cost relations. In John S. Fitzgerald, Constance L. Heitmeyer, Stefania Gnesi, and Anna Philippou, editors, FM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings, volume 9995 of LNCS, pages 254-273, 2016. URL: https://doi.org/10.1007/978-3-319-48989-6_16.
  17. Jürgen Giesl, Cornelius Aschermann, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Jera Fuhs, Carstenand Hensel, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, and René Swiderski, Stephanie andThiemann. Analyzing program termination and complexity automatically with aprove. J. Autom. Reasoning, 58(1):3-31, 2017. URL: https://doi.org/10.1007/s10817-016-9388-y.
  18. Jürgen Giesl, Albert Rubio, Christian Sternagel, Johannes Waldmann, and Akihisa Yamada. The termination and complexity competition. In Dirk Beyer, Marieke Huisman, Fabrice Kordon, and Bernhard Steffen, editors, Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III, volume 11429 of LNCS, pages 156-166. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17502-3_10.
  19. Sumit Gulwani, Krishna K. Mehra, and Trishul Chilimbi. Speed: Precise and efficient static estimation of program computational complexity. In Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '09, pages 127-139, New York, NY, USA, 2009. Association for Computing Machinery. URL: https://doi.org/10.1145/1480881.1480898.
  20. Armaël Guéneau. Mechanized Verification of the Correctness and Asymptotic Complexity of Programs. (Vérification mécanisée de la correction et complexité asymptotique de programmes). PhD thesis, Inria, Paris, France, 2019. URL: https://tel.archives-ouvertes.fr/tel-02437532.
  21. Emmanuel Hainry, Emmanuel Jeandel, Romain Péchoux, and Olivier Zeyen. Complexityparser: An automatic tool for certifying poly-time complexity of Java programs. In Antonio Cerone and Peter Csaba Ölveczky, editors, Theoretical Aspects of Computing - ICTAC 2021 - 18th International Colloquium, Virtual Event, Nur-Sultan, Kazakhstan, September 8-10, 2021, Proceedings, volume 12819 of LNCS, pages 357-365. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-85315-0_20.
  22. Jan Hoffmann, Klaus Aehlig, and Martin Hofmann. Resource aware ML. In P. Madhusudan and Sanjit A. Seshia, editors, Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, volume 7358 of LNCS, pages 781-786. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31424-7_64.
  23. Neil D. Jones and Lars Kristiansen. A flow calculus of mwp-bounds for complexity analysis. ACM Trans. Comput. Log., 10(4):28:1-28:41, 2009. URL: https://doi.org/10.1145/1555746.1555752.
  24. Neil D. Jones and Flemming Nielson. Abstract interpretation: A semantics-based tool for program analysis. In Samson Abramsky, Dov M. Gabbay, and Thomas Stephen Edward Maibaum, editors, Semantic Modelling, volume 4 of Handbook of Logic in Computer Science, pages 527-636. Oxford University Press, 1995. Google Scholar
  25. Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, and David Pichardie. A formally-verified C static analyzer. In Sriram K. Rajamani and David Walker, editors, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium onPrinciples of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 247-259. ACM, 2015. URL: https://doi.org/10.1145/2676726.2676966.
  26. Yves Lafont. Soft linear logic and polynomial time. Theor. Comput. Sci., 318(1):163-180, 2004. URL: https://doi.org/10.1016/j.tcs.2003.10.018.
  27. Daniel Leivant. Stratified functional programs and computational complexity. In Mary S. Van Deusen and Bernard Lang, editors, Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 325-333. ACM Press, 1993. URL: https://doi.org/10.1145/158511.158659.
  28. Xavier Leroy. Formal verification of a realistic compiler. Commun. ACM, 52(7):107-115, 2009. URL: https://doi.org/10.1145/1538788.1538814.
  29. Benjamin Lichtman and Jan Hoffmann. Arrays and references in resource aware ML. In Dale Miller, editor, 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017, September 3-9, 2017, Oxford, UK, volume 84 of LIPIcs, pages 26:1-26:20. Schloss Dagstuhl, 2017. URL: https://doi.org/10.4230/LIPIcs.FSCD.2017.26.
  30. Jean-Yves Moyen. Implicit Complexity in Theory and Practice. Habilitation thesis, University of Copenhagen, 2017. URL: https://lipn.univ-paris13.fr/~moyen/papiers/Habilitation_JY_Moyen.pdf.
  31. Jean-Yves Moyen, Thomas Rubiano, and Thomas Seiller. Loop quasi-invariant chunk detection. In Deepak D'Souza and K. Narayan Kumar, editors, ATVA, volume 10482 of LNCS. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-68167-2_7.
  32. Jean-Yves Moyen, Thomas Rubiano, and Thomas Seiller. Loop quasi-invariant chunk motion by peeling with statement composition. In Guillaume Bonfante and Georg Moser, editors, Proceedings 8th Workshop on Developments in Implicit Computational Complexity and 5th Workshop on Foundational and Practical Aspects of Resource Analysis, DICE-FOPARA@ETAPS 2017, Uppsala, Sweden, April 22-23, 2017, volume 248 of EPTCS, pages 47-59, 2017. URL: https://doi.org/10.4204/EPTCS.248.9.
  33. pymwp’s documentation, 2021. URL: https://statycc.github.io/pymwp/.
  34. Coq Team. Coq documentation, 2022. URL: https://coq.github.io/doc/.
  35. Joris van der Hoeven and Robin Larrieu. Fast Gröbner basis computation and polynomial reduction for generic bivariate ideals. Applicable Algebra in Engineering, Communication and Computing, 30(6):509-539, December 2019. URL: https://doi.org/10.1007/s00200-019-00389-9.
  36. Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic. Formal verification of SSA-based optimizations for LLVM. In Hans-Juergen Boehm and Cormac Flanagan, editors, ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '13, Seattle, WA, USA, June 16-19, 2013, pages 175-186. ACM, 2013. URL: https://doi.org/10.1145/2491956.2462164.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact