Mathias Jakobsen
ABSTRACT
Typestates are state machines used in object-oriented programming to specify and verify correct order of method calls on an object. To avoid inconsistent object states, typestates enforce linear typing, which eliminates—or at best limits—aliasing. However, aliasing is an important feature in programming, and the state-of-the-art on typestates is too restrictive if we want typestates to be adopted in real-world software systems.
In this paper, we present a type system for an object-oriented language with typestate annotations, which allows for unrestricted aliasing, and as opposed to previous approaches it does not require linearity constraints. The typestate analysis is global and tracks objects throughout the entire program graph, which ensures that well-typed programs conform and complete the declared protocols. We implement our framework in the Scala programming language and illustrate our approach using a running example that shows the interplay between typestates and aliases.
- Jonathan Aldrich, Joshua Sunshine, Darpan Saini, and Zachary Sparks. 2009. Typestate-oriented programming. (2009), 1015–1022. https://doi.org/10.1145/1639950.1640073Google Scholar
Digital Library
- Kevin Bierhoff and Jonathan Aldrich. 2007. Modular typestate checking of aliased objects. ACM SIGPLAN Notices 42, 10 (2007), 301–319. https://doi.org/10.1145/1297105.1297050Google ScholarDigital Library
- Mario Bravetti, Adrian Francalanza, Iaroslav Golovanov, Hans Hüttel, Mathias S Jakobsen, Mikkel K Kettunen, and António Ravara. 2020. Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language. In Programming Languages and Systems, Bruno C d. S Oliveira (Ed.). Springer International Publishing, Cham, 105–124.Google Scholar
- Luís Caires and João C. Seco. 2013. The type discipline of behavioral separation. ACM SIGPLAN Notices 48, 1 (2013), 275–286. https://doi.org/10.1145/2480359.2429103Google ScholarDigital Library
- Silvia Crafa and Luca Padovani. 2017. The chemical approach to typestate-oriented programming. ACM Transactions on Programming Languages and Systems 39, 3 (2017), 917–934. https://doi.org/10.1145/3064849Google ScholarDigital Library
- Ornela Dardha, Simon J. Gay, Dimitrios Kouzapas, Roly Perera, A. Laura Voinea, and Florian Weber. 2017. Mungo and StMungo: tools for typechecking protocols in Java. In Behavioural Types: from Theory to Tools, Simon Gay and Antonio Ravara (Eds.). River Publishers, 309–328. http://eprints.gla.ac.uk/146891/Google Scholar
- Robert DeLine and Manuel Fahndrich. 2001. Enforcing high-level protocols in low-level software. In Proc. of PLDI pages(2001), 59–69.Google ScholarDigital Library
- Robert DeLine and Manuel Fähndrich. 2004. The Fugue protocol checker: Is your software Baroque?Technical Report January. Microsoft Research. http://research.microsoft.com/apps/pubs/default.aspx?id=67458%5Cnhttp://research.microsoft.com/en-us/projects/fugue/Google Scholar
- Robert Deline and Manuel Fähndrich. 2004. Typestates for Objects. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 3086 (2004), 465–490. https://doi.org/10.1007/978-3-540-24851-4_21Google ScholarCross Ref
- Mariangiola Dezani-Ciancaglini, Dimitris Mostrous, Nobuko Yoshida, and Sophia Drossopoulou. 2006. Session types for object-oriented languages. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 4067 LNCS (2006), 328–352. https://doi.org/10.1007/11785477_20Google ScholarDigital Library
- Manuel Fähndrich and Robert DeLine. 2002. Adoption and Focus: Practical Linear Types for Imperative Programming. In Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Berlin, Germany, June 17-19, 2002, Jens Knoop and Laurie J. Hendren (Eds.). ACM, 13–24. https://doi.org/10.1145/512529.512532Google ScholarDigital Library
- Stephen J. Fink, Eran Yahav, Nurit Dor, G. Ramalingam, and Emmanuel Geay. 2008. Effective typestate verification in the presence of aliasing. ACM Trans. Softw. Eng. Methodol. 17, 2 (2008), 9:1–9:34. https://doi.org/10.1145/1348250.1348255Google ScholarDigital Library
- Simon J. Gay, Nils Gesbert, António Ravara, and Vasco T. Vasconcelos. 2015. Modular session types for objects. Logical Methods in Computer Science 11, 4 (2015), 1–76. https://doi.org/10.2168/LMCS-11(4:12)2015Google ScholarCross Ref
- Simon J. Gay, Vasco Thudichum Vasconcelos, António Ravara, Nils Gesbert, and Alexandre Z. Caldeira. 2010. Modular session types for distributed object-oriented programming. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010, Manuel V. Hermenegildo and Jens Palsberg (Eds.). ACM, 299–312. https://doi.org/10.1145/1706299.1706335Google ScholarDigital Library
- Iaroslav Golovanov, Hans Hüttel, Mathias Steen Jakobsen, and Mikkel Klinke Kettunen. 2021. Behavioural Separation with Parallel Usages. In Proceedings of the 23rd ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs (Virtual, Denmark) (FTfJP 2021). Association for Computing Machinery, New York, NY, USA.Google ScholarDigital Library
- Kohei Honda. 1993. Types for Dyadic Interaction. In CONCUR ’93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993, Proceedings(Lecture Notes in Computer Science, Vol. 715), Eike Best(Ed.). Springer, 509–523. https://doi.org/10.1007/3-540-57208-2_35Google Scholar
- Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. 1998. Language primitives and type discipline for structured communication-based programming. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 1381 (1998), 122–138. https://doi.org/10.1007/bfb0053567Google Scholar
- Kohei Honda, Nobuko Yoshida, and Marco Carbone. 2008. Multiparty asynchronous session types. In Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, George C. Necula and Philip Wadler (Eds.). ACM, 273–284. https://doi.org/10.1145/1328438.1328472Google ScholarDigital Library
- Mathias Jakobsen, Alice Ravier, and Ornela Dardha. 2021. Papaya: Global Typestate Analysis of Aliased Objects Extended Version. CoRR abs/2107.13101(2021). arxiv:2107.13101https://arxiv.org/abs/2107.13101Google Scholar
- Mathias Steen Jakobsen, Mikkel Klinke Kettunen, and Iaroslav Golovanov. 2020. Behavioural Separation with Parallel Usages for a Core Object-Oriented Language.Google Scholar
- Dimitrios Kouzapas, Ornela Dardha, Roly Perera, and Simon J. Gay. 2016. Typechecking protocols with Mungo and StMungo. In Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, Edinburgh, United Kingdom, September 5-7, 2016, James Cheney and Germán Vidal (Eds.). ACM, 146–159. https://doi.org/10.1145/2967973.2968595Google ScholarDigital Library
- Dimitrios Kouzapas, Ornela Dardha, Roly Perera, and Simon J. Gay. 2018. Typechecking protocols with Mungo and StMungo: A session type toolchain for Java. Science of Computer Programming 155 (2018), 52–75. https://doi.org/10.1016/j.scico.2017.10.006Google ScholarCross Ref
- Microsoft. 2020. Common Language Runtime (CLR) overview -.NET. https://docs.microsoft.com/en-us/dotnet/standard/clrGoogle Scholar
- Filipe Militão, Jonathan Aldrich, and Luís Caires. 2010. Aliasing control with view-based typestate. In Proceedings of the 12th Workshop on Formal Techniques for Java-Like Programs, FTFJP 2010, Maribor, Slovenia, June 22, 2010. ACM, 7:1–7:7. https://doi.org/10.1145/1924520.1924527Google ScholarDigital Library
- João Mota. 2021. Coping with the reality: adding crucial features to a typestate-oriented language.Google Scholar
- João Mota, Marco Giunti, and António Ravara. 2021. Java Typestate Checker. In Coordination Models and Languages - 23rd IFIP WG 6.1 International Conference, COORDINATION 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, June 14-18, 2021, Proceedings(Lecture Notes in Computer Science, Vol. 12717), Ferruccio Damiani and Ornela Dardha (Eds.). Springer, 121–133. https://doi.org/10.1007/978-3-030-78142-2_8Google ScholarDigital Library
- Mungo project. 2021. Mungo. http://www.dcs.gla.ac.uk/research/mungo/Google Scholar
- Martin Odersky, Philippe Altherr, Vincent Cremet, Gilles Dubochet, Burak Emir, Philipp Haller, Stéphane Micheloud, Nikolay Mihaylov, Adriaan Moors, Lukas Rytz, Michel Schinz, Erik Stenman, and Matthias Zenger. 2021. Scala Language Specification. https://scala-lang.org/files/archive/spec/2.13/Google Scholar
- Luca Padovani. 2018. Deadlock-Free Typestate-Oriented Programming. Art Sci. Eng. Program. 2, 3 (2018), 15. https://doi.org/10.22152/programming-journal.org/2018/2/15Google ScholarCross Ref
- Alice Ravier. 2021. Scala-Mungo. https://github.com/Aliceravier/Scala-MungoGoogle Scholar
- Alceste Scalas, Ornela Dardha, Raymond Hu, and Nobuko Yoshida. 2017. A linear decomposition of multiparty sessions for safe distributed programming. Leibniz International Proceedings in Informatics, LIPIcs 74, March(2017), 241–2431. https://doi.org/10.4230/LIPIcs.ECOOP.2017.24Google Scholar
- Alceste Scalas and Nobuko Yoshida. 2016. Lightweight Session Programming in Scala. In Proceedings of the 30th European Conference on Object-Oriented Programming, ECOOP(LIPIcs, Vol. 56). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 21:1–21:28. https://doi.org/10.4230/LIPIcs.ECOOP.2016.21Google Scholar
- Robert E. Strom and Shaula Yemini. 1986. Typestate: A Programming Language Concept for Enhancing Software Reliability., 157–171 pages. https://doi.org/10.1109/TSE.1986.6312929Google ScholarDigital Library
- Joshua Sunshine, Karl Naden, Sven Stork, Jonathan Aldrich, and Eric Tanter. 2011. First-class state change in plaid. ACM SIGPLAN Notices 46, 10 (2011), 713–732. https://doi.org/10.1145/2076021.2048122Google ScholarDigital Library
- Vasco T. Vasconcelos. 2011. Sessions, from Types to Programming Languages. Bull. EATCS 103(2011), 53–73. http://eatcs.org/beatcs/index.php/beatcs/article/view/136Google Scholar
- Vasco T. Vasconcelos, Simon J. Gay, António Ravara, Nils Gesbert, and Alexandre Z. Caldiera. 2009. Dynamic interfaces. In 2009 International Workshop on Foundations of Object-Oriented Languages (FOOL’09).Google Scholar
- A. Laura Voinea, Ornela Dardha, and Simon J. Gay. 2020. Typechecking Java Protocols with [St]Mungo. In Proceedings of the International Conference on Formal Techniques for Distributed Objects, Components, and Systems - 40th IFIP WG 6.1, FORTE(Lecture Notes in Computer Science, Vol. 12136). Springer, 208–224. https://doi.org/10.1007/978-3-030-50086-3_12Google ScholarDigital Library
Index Terms
- Papaya: Global Typestate Analysis of Aliased Objects
Index terms have been assigned to the content through auto-classification.
Recommendations
Typestate-like analysis of multiple interacting objects
OOPSLA '08: Proceedings of the 23rd ACM SIGPLAN conference on Object-oriented programming systems languages and applicationsThis paper presents a static analysis of typestate-like temporal specifications of groups of interacting objects, which are expressed using tracematches. Whereas typestate expresses a temporal specification of one object, a tracematch state may change ...
Foundations of Typestate-Oriented Programming
Typestate reflects how the legal operations on imperative objects can change at runtime as their internal state changes. A typestate checker can statically ensure, for instance, that an object method is only called when the object is in a state for which ...
Modular typestate checking of aliased objects
OOPSLA '07: Proceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems, languages and applicationsObjects often define usage protocols that clients must follow inorder for these objects to work properly. Aliasing makes itnotoriously difficult to check whether clients and implementations are compliant with such protocols. Accordingly, existing ...
Comments