Blame-Correct Support for Receiver Properties in Recursively-Structured Actor Contracts
Article No.: 254, Pages 515 - 543
Abstract
Actor languages model concurrency as processes that communicate through asynchronous message sends.Unfortunately, as the complexity of these systems increases, it becomes more difficult to compose and integrate their components. This is because of assumptions made by components about their communication partners which may not be upheld when they remain implicit. In this paper, we bring design-by-contract programming to actor programs through a contract system that enables expressing constraints on receiver-related properties.Expressing properties about the expected receiver of a message, and about this receiver's communication behavior, requires two novel types of contracts.Through their recursive structure, these contracts can govern entire communication chains. We implement the contract system for an actor extension of Scheme, describe it formally, and show how to assign blame in case of a contract violation.Finally, we prove our contract system and its blame assignment correct by formulating and proving a blame correctness theorem.
References
[1]
Gul Agha. 1986. Actors: a model of concurrent computation in distributed systems. MIT press.
[2]
Laura Bocchi, Kohei Honda, Emilio Tuosto, and Nobuko Yoshida. 2010. A Theory of Design-by-Contract for Distributed Multiparty Interactions. In CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, August 31-September 3, 2010. Proceedings, Paul Gastin and François Laroussinie (Eds.) (Lecture Notes in Computer Science, Vol. 6269). Springer, 162–176. https://doi.org/10.1007/978-3-642-15375-4_12
[3]
Tom Van Cutsem, Elisa Gonzalez Boix, Christophe Scholliers, Andoni Lombide Carreton, Dries Harnie, Kevin Pinte, and Wolfgang De Meuter. 2014. AmbientTalk: programming responsive mobile peer-to-peer applications with actors. Comput. Lang. Syst. Struct., 40, 3-4 (2014), 112–136. https://doi.org/10.1016/J.CL.2014.05.002
[4]
Christos Dimoulas, Robert Bruce Findler, Cormac Flanagan, and Matthias Felleisen. 2011. Correct blame for contracts: no more scapegoating. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, January 26-28, 2011, Thomas Ball and Mooly Sagiv (Eds.). ACM, 215–226. https://doi.org/10.1145/1926385.1926410
[5]
Christos Dimoulas, Max S. New, Robert Bruce Findler, and Matthias Felleisen. 2016. Oh Lord, please don’t let contracts be misunderstood (functional pearl). In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP ‘16), Jacques Garrigue, Gabriele Keller, and Eijiro Sumii (Eds.). ACM, 117–131. https://doi.org/10.1145/2951913.2951930
[6]
Christos Dimoulas, Sam Tobin-Hochstadt, and Matthias Felleisen. 2012. Complete Monitors for Behavioral Contracts. In Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, March 24 - April 1, 2012. Proceedings, Helmut Seidl (Ed.) (Lecture Notes in Computer Science, Vol. 7211). Springer, 214–233. https://doi.org/10.1007/978-3-642-28869-2_11
[7]
Tim Disney, Cormac Flanagan, and Jay McCarthy. 2011. Temporal higher-order contracts. In Proceeding of the 16th ACM SIGPLAN International Conference on Functional Programming, ICFP 2011, September 19-21, 2011, Manuel M. T. Chakravarty, Zhenjiang Hu, and Olivier Danvy (Eds.). ACM, 176–188. https://doi.org/10.1145/2034773.2034800
[8]
Robert Bruce Findler and Matthias Felleisen. 2002. Contracts for higher-order functions. In Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP ’02), 2002, Mitchell Wand and Simon L. Peyton Jones (Eds.). ACM, 48–59. https://doi.org/10.1145/581478.581484
[9]
Simon Fowler, Sam Lindley, and Philip Wadler. 2017. Mixing Metaphors: Actors as Channels and Channels as Actors. In 31st European Conference on Object-Oriented Programming, ECOOP 2017, June 19-23, 2017, Peter Müller (Ed.) (LIPIcs, Vol. 74). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 11:1–11:28. https://doi.org/10.4230/LIPICS.ECOOP.2017.11
[10]
Teodoro Freund, Yann Hamdaoui, and Arnaud Spiwack. 2021. Union and intersection contracts are hard, actually. In DLS 2021: Proceedings of the 17th ACM SIGPLAN International Symposium on Dynamic Languages, October 19, 2021, Arjun Guha (Ed.). ACM, 1–11. https://doi.org/10.1145/3486602.3486767
[11]
Hannah Gommerstadt, Limin Jia, and Frank Pfenning. 2022. Session-typed concurrent contracts. J. Log. Algebraic Methods Program., 124 (2022), 100731. https://doi.org/10.1016/J.JLAMP.2021.100731
[12]
Dries Harnie, Christophe Scholliers, and Wolfgang De Meuter. 2010. Ambient Contracts. Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 28 (2010), https://doi.org/10.14279/TUJ.ECEASST.28.397
[13]
Paul Harvey, Simon Fowler, Ornela Dardha, and Simon J. Gay. 2021. Multiparty Session Types for Safe Runtime Adaptation in an Actor Language. In 35th European Conference on Object-Oriented Programming, ECOOP 2021, July 11-17, 2021), Anders Møller and Manu Sridharan (Eds.) (LIPIcs, Vol. 194). 10:1–10:30. https://doi.org/10.4230/LIPICS.ECOOP.2021.10
[14]
Kohei Honda, Nobuko Yoshida, and Marco Carbone. 2008. Multiparty asynchronous session types. In Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 273–284. https://doi.org/10.1145/1328438.1328472
[15]
Kohei Honda, Nobuko Yoshida, and Marco Carbone. 2016. Multiparty Asynchronous Session Types. J. ACM, 63, 1 (2016), 9:1–9:67. https://doi.org/10.1145/1328438.1328472
[16]
Limin Jia, Hannah Gommerstadt, and Frank Pfenning. 2016. Monitors and blame assignment for higher-order session types. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, January 20 - 22, 2016, Rastislav Bodík and Rupak Majumdar (Eds.). ACM, 582–594. https://doi.org/10.1145/2837614.2837662
[17]
Casey Klein, John Clements, Christos Dimoulas, Carl Eastlund, Matthias Felleisen, Matthew Flatt, Jay A. McCarthy, Jon Rafkind, Sam Tobin-Hochstadt, and Robert Bruce Findler. 2012. Run your research: on the effectiveness of lightweight mechanization. In Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, January 22-28, 2012, John Field and Michael Hicks (Eds.). ACM, 285–296. https://doi.org/10.1145/2103656.2103691
[18]
Roland Kuhn, Brian Hanafee, and Jamie Allen. 2017. Reactive Design Patterns (1st ed.). Manning Publications Co., USA. isbn:9781617291807
[19]
Tanakorn Leesatapornwongsa, Jeffrey F. Lukman, Shan Lu, and Haryadi S. Gunawi. 2016. TaxDC: A Taxonomy of Non-Deterministic Concurrency Bugs in Datacenter Distributed Systems. In Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2016, April 2-6, 2016, Tom Conte and Yuanyuan Zhou (Eds.). ACM, 517–530. https://doi.org/10.1145/2872362.2872374
[20]
Hernán C. Melgratti and Luca Padovani. 2017. Chaperone contracts for higher-order sessions. Proc. ACM Program. Lang., 1, ICFP (2017), 35:1–35:29. https://doi.org/10.1145/2384616.2384685
[21]
Bertrand Meyer. 1998. Design by Contract: The Eiffel Method. In TOOLS 1998: 26th International Conference on Technology of Object-Oriented Languages and Systems. IEEE Computer Society, 446. https://doi.org/10.1109/TOOLS.1998.711043
[22]
Robin Milner. 1999. Communicating and mobile systems - the Pi-calculus. Cambridge university press. isbn:978-0-521-65869-0
[23]
Rumyana Neykova and Nobuko Yoshida. 2017. Multiparty Session Actors. Log. Methods Comput. Sci., 13, 1 (2017), https://doi.org/10.23638/LMCS-13(1:17)2017
[24]
Christophe Scholliers, Éric Tanter, and Wolfgang De Meuter. 2015. Computational contracts. Sci. Comput. Program., 98 (2015), 360–375. https://doi.org/10.1016/J.SCICO.2013.09.005
[25]
T. Stephen Strickland, Sam Tobin-Hochstadt, Robert Bruce Findler, and Matthew Flatt. 2012. Chaperones and impersonators: run-time support for reasonable interposition. In Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2012, part of SPLASH 2012, October 21-25, 2012, Gary T. Leavens and Matthew B. Dwyer (Eds.). ACM, 943–962. https://doi.org/10.1145/2384616.2384685
[26]
Bram Vandenbogaerde, Quentin Stiévenart, and Coen De Roover. 2024. Blame-Correct Support for Receiver Properties in Recursively-Structured Actor Contracts (Artifact). https://doi.org/10.5281/zenodo.12659179
[27]
Lucas Waye, Stephen Chong, and Christos Dimoulas. 2017. Whip: higher-order contracts for modern services. Proc. ACM Program. Lang., 1, ICFP (2017), 36:1–36:28. https://doi.org/10.1145/3110280
Index Terms
- Blame-Correct Support for Receiver Properties in Recursively-Structured Actor Contracts
Recommendations
Soft Verification for Actor Contract Systems
ISSTA 2024: Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and AnalysisDesign-by-contract is a software engineering practice where programmers annotate program elements with contract specifications that make expectations towards the user and supplier of the program element explicit. This practice has been applied in various ...
Correct blame for contracts: no more scapegoating
POPL '11: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesBehavioral software contracts supplement interface information with logical assertions. A rigorous enforcement of contracts provides useful feedback to developers if it signals contract violations as soon as they occur and if it assigns blame to ...
Correct blame for contracts: no more scapegoating
POPL '11Behavioral software contracts supplement interface information with logical assertions. A rigorous enforcement of contracts provides useful feedback to developers if it signals contract violations as soon as they occur and if it assigns blame to ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
August 2024
1031 pages
Copyright © 2024 Owner/Author.
This work is licensed under a Creative Commons Attribution-NoDerivs International 4.0 License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 15 August 2024
Published in PACMPL Volume 8, Issue ICFP
Check for updates
Badges
Author Tags
Qualifiers
- Research-article
Funding Sources
- FWO
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 120Total Downloads
- Downloads (Last 12 months)120
- Downloads (Last 6 weeks)26
Reflects downloads up to 25 Feb 2025
Other Metrics
Citations
Cited By
View allView Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in