research-article

Optimizing abstract abstract machines

Authors:

Nicholas Labich,

David Van HornAuthors Info & Claims

ICFP '13: Proceedings of the 18th ACM SIGPLAN international conference on Functional programming

Pages 443 - 454

https://doi.org/10.1145/2500365.2500604

Published: 25 September 2013 Publication History

Abstract

The technique of abstracting abstract machines (AAM) provides a systematic approach for deriving computable approximations of evaluators that are easily proved sound. This article contributes a complementary step-by-step process for subsequently going from a naive analyzer derived under the AAM approach, to an efficient and correct implementation. The end result of the process is a two to three order-of-magnitude improvement over the systematically derived analyzer, making it competitive with hand-optimized implementations that compute fundamentally less precise results.

References

[1]

Dominique Boucher and Marc Feeley. Abstract compilation: A new implementation paradigm for static analysis. In Tibor Gyimóthy, editor, Compiler Construction: 6th International Conference, CC'96 Linköping, Sweden, April 24-26, 1996 Proceedings, pages 192--207, 1996.

Digital Library

[2]

Martin Bravenboer and Yannis Smaragdakis. Strictly declarative specification of sophisticated points-to analyses. In OOPSLA '09: Proceedings of the 24th annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, 2009.

Digital Library

[3]

M. C. Browne, E. M. Clarke, and O. Grümberg. Characterizing finite kripke structures in propositional temporal logic. Theor. Comput. Sci., 59(1--2):115--131, 1988.

Digital Library

[4]

Patrick Cousot and Radhia Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL '77: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 238--252. ACM, 1977.

Digital Library

[5]

Patrick Cousot and Radhia Cousot. Systematic design of program analysis frameworks. In Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL '79, pages 269--282. ACM, 1979.

Digital Library

[6]

Olivier Danvy. An Analytical Approach to Program as Data Objects. DSc thesis, Department of Computer Science, Aarhus University, 2006.

[7]

Olivier Danvy and Lasse R. Nielsen. Refocusing in reduction semantics. Research Report BRICS RS-04-26, Department of Computer Science, Aarhus University, 2004.

[8]

E. D'Osualdo, J. Kochems, and C.-H. L. Ong. Automatic verification of Erlang-style concurrency. Technical report, University of Oxford DCS Technical Report, 2012. http://mjolnir.cs.ox.ac.uk/soter/papers/erlang-verif.pdf.

[9]

E. D'Osualdo, J. Kochems, and C.-H. L. Ong. Soter: An automatic safety verifier for Erlang. Technical report, University of Oxford DCS Technical Report, 2012. http://mjolnir.cs.ox.ac.uk/soter/papers/soter-demo.pdf.

[10]

Christopher Earl, Ilya Sergey, Matthew Might, and David Van Horn. Introspective pushdown analysis of higher-order programs. In Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming, ICFP '12, pages 177--188. ACM, 2012.

Digital Library

[11]

Marc Feeley and Guy Lapalme. Using closures for code generation. Comput. Lang., 12(1):47--66, 1987.

Digital Library

[12]

Matthias Felleisen, Robert B. Findler, and Matthew Flatt. Semantics Engineering with PLT Redex. MIT Press, 2009.

Digital Library

[13]

Pieter H. Hartel, Marc Feeley, Martin Alt, Lennart Augustsson, Peter Baumann, Marcel Beemster, Emmanuel Chailloux, Christine H. Flood, Wolfgang Grieskamp, John H. G. Van Groningen, Kevin Hammond, Bogumil Hausman, Melody Y. Ivory, Richard E. Jones, Jasper Kamperman, Peter Lee, Xavier Leroy, Rafael D. Lins, Sandra Loosemore, Niklas Röjemo, Manuel Serrano, Jean P. Talpin, Jon Thackray, Stephen Thomas, Pum Walters, Pierre Weis, and Peter Wentworth. Benchmarking implementations of functional languages with "pseudoknot", a float-intensive benchmark. Journal of Functional Programming, 6(04):621--655, 1996.

[14]

Suresh Jagannathan, Peter Thiemann, Stephen Weeks, and Andrew Wright. Single and loving it: must-alias analysis for higher-order languages. In POPL '98: Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 329--341. ACM, 1998.

Digital Library

[15]

Suresh Jagannathan and Stephen Weeks. A unified treatment of flow analysis in higher-order languages. In POPL '95: Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 393--407. ACM Press, 1995.

Digital Library

[16]

P. J. Landin. The next 700 programming languages. Commun. ACM, 9(3):157--166, 1966.

Digital Library

[17]

Peter J. Landin. The mechanical evaluation of expressions. The Computer Journal, 6(4):308--320, 1964.

[18]

Philippe Meunier, Robert B. Findler, and Matthias Felleisen. Modular set-based analysis from contracts. In POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 218--231. ACM, 2006.

Digital Library

[19]

Jan Midtgaard. Control-flow analysis of functional programs. ACM Computing Surveys, 2011.

Digital Library

[20]

Matthew Might and David Van Horn. A family of abstract interpretations for static analysis of concurrent Higher-Order programs. In Eran Yahav, editor, Static Analysis, volume 6887 of Lecture Notes in Computer Science, pages 180--197. Springer Berlin Heidelberg, 2011.

Digital Library

[21]

Matthew Might and Panagiotis Manolios. A posteriori soundness for non-deterministic abstract interpretations. In Proceedings of the 10th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI '09, pages 260--274. Springer-Verlag, 2009.

Digital Library

[22]

Matthew Might and Olin Shivers. Improving flow analyses via(Γ)CFA: Abstract garbage collection and counting. In Proceedings of the 11th ACM International Conference on Functional Programming (ICFP 2006), pages 13--25, 2006.

Digital Library

[23]

Matthew Might and David Van Horn. Scalable and precise abstractions of programs for trustworthy software. Technical report, 2012.

[24]

Greg Morrisett. Harvard university course cs252r: Advanced functional language compilation. http://www.eecs.harvard.edu/ greg/cs252rfa12/.

[25]

Flemming Nielson and Hanne R. Nielson. Infinitary control flow analysis: a collecting semantics for closure analysis. In POPL '97: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 332--345. ACM Press, 1997.

Digital Library

[26]

G. D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, 1981.

[27]

John C. Reynolds. Definitional interpreters for Higher-Order programming languages. Higher-Order and Symbolic Computation, 11(4):363--397, 1998.

Digital Library

[28]

Paul A. Steckler and Mitchell Wand. Lightweight closure conversion. ACM Trans. Program. Lang. Syst., 19(1):48--86, 1997.

Digital Library

[29]

Sam Tobin-Hochstadt and David Van Horn. Higher-order symbolic execution via contracts. In Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA '12, pages 537--554. ACM, 2012.

Digital Library

[30]

David Van Horn and Matthew Might. Abstracting abstract machines: a systematic approach to higher-order program analysis. Communications of the ACM, 54:101--109, 2011.

Digital Library

[31]

David Van Horn and Matthew Might. An analytic framework for JavaScript. CoRR, abs/1109.4467, 2011.

[32]

David Van Horn and Matthew Might. Systematic abstraction of abstract machines. Journal of Functional Programming, 22(Special Issue 4-5):705--746, 2012.

Digital Library

[33]

Dimitrios Vardoulakis and Olin Shivers. CFA2: a Context-Free approach to Control-Flow analysis. Logical Methods in Computer Science, 7(2), 2011.

[34]

Andrew K. Wright and Suresh Jagannathan. Polymorphic splitting: an effective polyvariant flow analysis. ACM Trans. Program. Lang. Syst., 20(1):166--207, 1998.

Digital Library

[35]

Feng Zhao. An O(N) algorithm for Three-Dimensional N-Body simulations. Master's thesis, MIT, 1987.

Cited By

Quiring BVan Horn D(2024)Deriving with Derivatives: Optimizing Incremental Fixpoints for Higher-Order Flow AnalysisProceedings of the ACM on Programming Languages10.1145/36746508:ICFP(728-755)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674650
Van Molle MVandenbogaerde BDe Roover CSaraiva JDegueule TScott E(2023)Cross-Level Debugging for Static AnalysersProceedings of the 16th ACM SIGPLAN International Conference on Software Language Engineering10.1145/3623476.3623512(138-148)Online publication date: 23-Oct-2023
https://dl.acm.org/doi/10.1145/3623476.3623512
Koppel JKearl JSolar-Lezama A(2022)Automatically deriving control-flow graph generators from operational semanticsProceedings of the ACM on Programming Languages10.1145/35476486:ICFP(742-771)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547648
Show More Cited By

Index Terms

Optimizing abstract abstract machines
1. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program analysis
    2. Program semantics

Recommendations

Optimizing abstract abstract machines
ICFP '13

The technique of abstracting abstract machines (AAM) provides a systematic approach for deriving computable approximations of evaluators that are easily proved sound. This article contributes a complementary step-by-step process for subsequently going ...
Abstracting abstract machines
ICFP '10: Proceedings of the 15th ACM SIGPLAN international conference on Functional programming

We describe a derivational approach to abstract interpretation that yields novel and transparently sound static analyses when applied to well-established abstract machines. To demonstrate the technique and support our claim, we transform the CEK machine ...
Abstracting abstract machines
ICFP '10

We describe a derivational approach to abstract interpretation that yields novel and transparently sound static analyses when applied to well-established abstract machines. To demonstrate the technique and support our claim, we transform the CEK machine ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICFP '13: Proceedings of the 18th ACM SIGPLAN international conference on Functional programming

September 2013

484 pages

ISBN:9781450323260

DOI:10.1145/2500365

General Chair:
Greg Morrisett
Harvard University, USA
,
Program Chair:
Tarmo Uustalu
Institute of Cybernetics at TUT, Estonia

ACM SIGPLAN Notices Volume 48, Issue 9
ICFP '13
September 2013
457 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2544174
Editor:
Mark W. Bailey
Hamilton College, Clinton, NY
Issue’s Table of Contents

Copyright © 2013 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages
Northeastern University

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 25 September 2013

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ICFP'13

Sponsor:

SIGPLAN

ICFP'13: ACM SIGPLAN International Conference on Functional Programming

September 25 - 27, 2013

Massachusetts, Boston, USA

Acceptance Rates

ICFP '13 Paper Acceptance Rate 40 of 133 submissions, 30%;

Overall Acceptance Rate 333 of 1,064 submissions, 31%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

19
Total Citations
View Citations
269
Total Downloads

Downloads (Last 12 months)16
Downloads (Last 6 weeks)4

Reflects downloads up to 18 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Quiring BVan Horn D(2024)Deriving with Derivatives: Optimizing Incremental Fixpoints for Higher-Order Flow AnalysisProceedings of the ACM on Programming Languages10.1145/36746508:ICFP(728-755)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674650
Van Molle MVandenbogaerde BDe Roover CSaraiva JDegueule TScott E(2023)Cross-Level Debugging for Static AnalysersProceedings of the 16th ACM SIGPLAN International Conference on Software Language Engineering10.1145/3623476.3623512(138-148)Online publication date: 23-Oct-2023
https://dl.acm.org/doi/10.1145/3623476.3623512
Koppel JKearl JSolar-Lezama A(2022)Automatically deriving control-flow graph generators from operational semanticsProceedings of the ACM on Programming Languages10.1145/35476486:ICFP(742-771)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547648
Montagu BJensen TFreund SYahav E(2021)Trace-based control-flow analysisProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454057(482-496)Online publication date: 19-Jun-2021
https://dl.acm.org/doi/10.1145/3453483.3454057
Stiévenart QVan Es NVan der Plas JDe Roover C(2021)A parallel worklist algorithm and its exploration heuristics for static modular analysesJournal of Systems and Software10.1016/j.jss.2021.111042181:COnline publication date: 1-Nov-2021
https://dl.acm.org/doi/10.1016/j.jss.2021.111042
Wei GBračevac OTan SRompf T(2020)Compiling symbolic execution with staging and algebraic effectsProceedings of the ACM on Programming Languages10.1145/34282324:OOPSLA(1-33)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428232
Van Es NStievenart QVan der Plas JDe Roover C(2020)A Parallel Worklist Algorithm for Modular Analyses2020 IEEE 20th International Working Conference on Source Code Analysis and Manipulation (SCAM)10.1109/SCAM51674.2020.00006(1-12)Online publication date: Sep-2020
https://doi.org/10.1109/SCAM51674.2020.00006
Wei GChen YRompf T(2019)Staged abstract interpreters: fast and modular whole-program analysis via meta-programmingProceedings of the ACM on Programming Languages10.1145/33605523:OOPSLA(1-32)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360552
Facchinetti LPalmer ZSmith S(2019)Higher-order Demand-driven Program AnalysisACM Transactions on Programming Languages and Systems10.1145/331034041:3(1-53)Online publication date: 2-Jul-2019
https://dl.acm.org/doi/10.1145/3310340
Nicolay JStiévenart QDe Meuter WDe Roover C(2019)Effect-Driven Flow AnalysisVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-11245-5_12(247-274)Online publication date: 11-Jan-2019
https://doi.org/10.1007/978-3-030-11245-5_12
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents