Document Open Access Logo

Mailbox Abstractions for Static Analysis of Actor Programs

Authors Quentin Stiévenart, Jens Nicolay, Wolfgang De Meuter, Coen De Roover

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2017.25.pdf
  • Filesize: 0.72 MB
  • 30 pages

Document Identifiers

Author Details

Quentin Stiévenart
Jens Nicolay
Wolfgang De Meuter
Coen De Roover

Cite As Get BibTex

Quentin Stiévenart, Jens Nicolay, Wolfgang De Meuter, and Coen De Roover. Mailbox Abstractions for Static Analysis of Actor Programs. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 25:1-25:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.ECOOP.2017.25

Abstract

Properties such as the absence of errors or bounds on mailbox sizes are hard to deduce statically for actor-based programs.
This is because actor-based programs exhibit several sources of unboundedness, in addition to the non-determinism that is inherent to the concurrent execution of actors.
We developed a static technique based on abstract interpretation to soundly reason in a finite amount of time about the possible executions of an actor-based program.
We use our technique to statically verify the absence of errors in actor-based programs, and to compute upper bounds on the actors' mailboxes.
Sound abstraction of these mailboxes is crucial to the precision of any such technique.
We provide several mailbox abstractions and categorize them according to the extent to which they preserve message ordering and multiplicity of messages in a mailbox.
We formally prove the soundness of each mailbox abstraction, and empirically evaluate their precision and performance trade-offs on a corpus of benchmark programs.
The results show that our technique can statically verify the absence of errors for more benchmark programs than the state-of-the-art analysis.

Subject Classification

Keywords
  • static analysis
  • abstraction
  • abstract interpretation
  • actors
  • mailbox

Metrics

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

Supplementary Materials

References

  1. Gul Agha. Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge, MA, USA, 1986. Google Scholar
  2. Gul Agha, Ian A. Mason, Scott F. Smith, and Carolyn L. Talcott. A foundation for actor computation. J. Funct. Program., 7(1):1-72, 1997. Google Scholar
  3. Joe Armstrong. Programming erlang : software for a concurrent world. Pragmatic programmers. Pragmatic Bookshelf, 2007. Google Scholar
  4. Thomas Arts, Mads Dam, Lars-Åke Fredlund, and Dilian Gurov. System description: Verification of distributed erlang programs. In Automated Deduction - CADE-15, 15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998, Proceedings, pages 38-41, 1998. Google Scholar
  5. Thomas Arts and Thomas Noll. Verifying generic erlang client-server implementations. In Implementation of Functional Languages, 12th International Workshop, IFL 2000, Aachen, Germany, September 4-7, 2000, Selected Papers, pages 37-52, 2000. Google Scholar
  6. Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Ofer Strichman, and Yunshan Zhu. Bounded model checking. Advances in Computers, 58:117-148, 2003. Google Scholar
  7. Maria Christakis and Konstantinos Sagonas. Static detection of race conditions in erlang. In Practical Aspects of Declarative Languages, 12th International Symposium, PADL 2010, Madrid, Spain, January 18-19, 2010. Proceedings, pages 119-133, 2010. Google Scholar
  8. Maria Christakis and Konstantinos Sagonas. Static detection of deadlocks in erlang. Technical report, 2011. Google Scholar
  9. Patrick Cousot. The verification grand challenge and abstract interpretation. In Verified Software: Theories, Tools, Experiments, First IFIP TC 2/WG 2.3 Conference, VSTTE 2005, Zurich, Switzerland, October 10-13, 2005, Revised Selected Papers and Discussions, pages 189-201, 2005. Google Scholar
  10. Patrick Cousot and Radhia Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pages 238-252. ACM, 1977. Google Scholar
  11. Fabien Dagnat and Marc Pantel. Static analysis of communications for erlang. In Proceedings of 8th International Erlang/OTP User Conference, 2002. Google Scholar
  12. Mads Dam and Lars-Åke Fredlund. On the verification of open distributed systems. In Proceedings of the 1998 ACM symposium on Applied Computing, SAC'98, Atlanta, GA, USA, February 27 - March 1, 1998, pages 532-540, 1998. Google Scholar
  13. Joeri De Koster, Stefan Marr, Tom Van Cutsem, and Theo D'Hondt. Domains: Sharing state in the communicating event-loop actor model. Computer Languages, Systems & Structures, 45:132-160, 2016. Google Scholar
  14. Joeri De Koster, Tom Van Cutsem, and Wolfgang De Meuter. 43 years of actors: a taxonomy of actor models and their key properties. In Proceedings of the 6th International Workshop on Programming Based on Actors, Agents, and Decentralized Control, AGERE 2016, Amsterdam, The Netherlands, October 30, 2016, pages 31-40, 2016. Google Scholar
  15. Emanuele D'Osualdo. Verification of Message Passing Concurrent Systems. PhD thesis, University of Oxford, 2015. Google Scholar
  16. Emanuele D'Osualdo, Jonathan Kochems, and Luke Ong. Soter: an automatic safety verifier for erlang. In Proceedings of the 2nd edition on Programming systems, languages and applications based on actors, agents, and decentralized control abstractions, AGERE! 2012, October 21-22, 2012, Tucson, Arizona, USA, pages 137-140, 2012. Google Scholar
  17. Emanuele D'Osualdo, Jonathan Kochems, and Luke Ong. Automatic verification of erlang-style concurrency. In Static Analysis - 20th International Symposium, SAS 2013, Seattle, WA, USA, June 20-22, 2013. Proceedings, pages 454-476, 2013. Google Scholar
  18. Cormac Flanagan and Patrice Godefroid. Dynamic partial-order reduction for model checking software. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005, pages 110-121, 2005. Google Scholar
  19. Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The essence of compiling with continuations. In Proceedings of the ACM SIGPLAN'93 Conference on Programming Language Design and Implementation (PLDI), Albuquerque, New Mexico, USA, June 23-25, 1993, pages 237-247, 1993. Google Scholar
  20. Simon Fowler, Sam Lindley, and Philip Wadler. Mixing metaphors: Actors as channels and channels as actors. arXiv preprint arXiv:1611.06276, 2016. Google Scholar
  21. Pierre-Loïc Garoche. Static Analysis of an Actor-based Process Calculus by Abstract Interpretation. PhD thesis, National Polytechnic Institute of Toulouse, France, 2008. Google Scholar
  22. Pierre-Loïc Garoche, Marc Pantel, and Xavier Thirioux. Static safety for an actor dedicated process calculus by abstract interpretation. In Formal Methods for Open Object-Based Distributed Systems, 8th IFIP WG 6.1 International Conference, FMOODS 2006, Bologna, Italy, June 14-16, 2006, Proceedings, pages 78-92, 2006. Google Scholar
  23. Thomas Gilray, Michael D. Adams, and Matthew Might. Allocation characterizes polyvariance: a unified methodology for polyvariant control-flow analysis. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016, pages 407-420, 2016. Google Scholar
  24. Munish K. Gupta. Akka essentials. Packt Publishing Ltd, 2012. Google Scholar
  25. Philipp Haller. On the integration of the actor model in mainstream technologies: the scala perspective. In Proceedings of the 2nd edition on Programming systems, languages and applications based on actors, agents, and decentralized control abstractions, AGERE! 2012, October 21-22, 2012, Tucson, Arizona, USA, pages 1-6, 2012. Google Scholar
  26. Frank Huch. Verification of erlang programs using abstract interpretation and model checking. In Proceedings of the fourth ACM SIGPLAN International Conference on Functional Programming (ICFP '99), Paris, France, September 27-29, 1999., pages 261-272, 1999. Google Scholar
  27. Shams Mahmood Imam and Vivek Sarkar. Savina - an actor benchmark suite: Enabling empirical evaluation of actor libraries. In Proceedings of the 4th International Workshop on Programming based on Actors Agents & Decentralized Control, AGERE! 2014, Portland, OR, USA, October 20, 2014, pages 67-80, 2014. Google Scholar
  28. Steven Lauterburg, Mirco Dotta, Darko Marinov, and Gul Agha. A framework for state-space exploration of java-based actor programs. In ASE 2009, 24th IEEE/ACM International Conference on Automated Software Engineering, Auckland, New Zealand, November 16-20, 2009, pages 468-479, 2009. Google Scholar
  29. Anders Lindgren. A prototype of a soft type system for erlang. Master’s thesis, Uppsala University, 1996. Google Scholar
  30. Simon Marlow and Philip Wadler. A practical subtyping system for erlang. In Proceedings of the 1997 ACM SIGPLAN International Conference on Functional Programming (ICFP '97), Amsterdam, The Netherlands, June 9-11, 1997., pages 136-149, 1997. Google Scholar
  31. Jan Midtgaard. Control-flow analysis of functional programs. ACM Comput. Surv., 44(3):10, 2012. Google Scholar
  32. Matthew Might and Panagiotis Manolios. A posteriorisoundness for non-deterministic abstract interpretations. In Verification, Model Checking, and Abstract Interpretation, 10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20, 2009. Proceedings, pages 260-274, 2009. Google Scholar
  33. Matthew Might and Olin Shivers. Improving flow analyses via gammacfa: abstract garbage collection and counting. In Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming, ICFP 2006, Portland, Oregon, USA, September 16-21, 2006, pages 13-25, 2006. Google Scholar
  34. Matthew Might and David Van Horn. A family of abstract interpretations for static analysis of concurrent higher-order programs. In Static Analysis - 18th International Symposium, SAS 2011, Venice, Italy, September 14-16, 2011. Proceedings, pages 180-197, 2011. Google Scholar
  35. Doron A. Peled. Ten years of partial order reduction. In Computer Aided Verification, 10th International Conference, CAV '98, Vancouver, BC, Canada, June 28 - July 2, 1998, Proceedings, pages 17-28, 1998. Google Scholar
  36. Koushik Sen and Gul Agha. Automated systematic testing of open distributed programs. In Fundamental Approaches to Software Engineering, 9th International Conference, FASE 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 27-28, 2006, Proceedings, pages 339-356, 2006. Google Scholar
  37. Quentin Stiévenart, Maarten Vandercammen, Wolfgang De Meuter, and Coen De Roover. Scala-AM: A modular static analysis framework. In 16th IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2016, Raleigh, NC, USA, October 2-3, 2016, pages 85-90, 2016. Google Scholar
  38. David Van Horn and Matthew Might. Abstracting abstract machines: a systematic approach to higher-order program analysis. Commun. ACM, 54(9):101-109, 2011. Google Scholar
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 About DROPS Imprint Privacy Contact