Dimitrios Kouzapas
ABSTRACT
We report on two tools that extend Java with support for static type-checking of communication protocols. Our Mungo tool extends Java with typestate definitions, which allow classes to be associated with state machines defining permitted sequences of method calls. A complementary tool, StMungo, takes a communication protocol specified in the Scribble protocol description language, and generates a typestate specification for each endpoint, capturing the permitted sequences of messages along that channel. Endpoint implementations can be validated by Mungo against their typestate definitions and then compiled as usual with javac. We formalise Mungo's typestate inference system and demonstrate the Scribble, Mungo and StMungo toolchain via a typechecked SMTP client that can communicate with a real-world SMTP server.
- Mungo Webpage. http://www.dcs.gla.ac.uk/research/mungo/.Google Scholar
- Jonathan Aldrich, Joshua Sunshine, Darpan Saini, and Zachary Sparks. Typestate-oriented programming. In OOPSLA '09, pages 1015--1022. ACM Press, 2009. Google ScholarDigital Library
- Chris Allan, Pavel Avgustinov, Aske Simon Christensen, Laurie J. Hendren, Sascha Kuzins, Ondrej Lhoták, Oege de Moor, Damien Sereni, Ganesh Sittampalam, and Julian Tibble. Adding trace matching with free variables to Aspect J. In OOPSLA '05, pages 345--364. ACM Press, 2005. Google ScholarDigital Library
- Nels E. Beckman, Kevin Bierhoff, and Jonathan Aldrich. Verifying correct usage of atomic blocks and typestate. In OOPSLA '08, pages 227--244. ACM Press, 2008. Google ScholarDigital Library
- Kevin Bierhoff and Jonathan Aldrich. Modular typestate checking of aliased objects. In OOPSLA '07, pages 301--320. ACM Press, 2007. Google ScholarDigital Library
- Kevin Bierhoff, Nels E. Beckman, and Jonathan Aldrich. Practical API protocol checking with access permissions. In ECOOP '09, volume 5653 of Springer LNCS, pages 195--219, 2009. Google ScholarDigital Library
- Eric Bodden and Laurie J. Hendren. The Clara framework for hybrid typestate analysis. Software Tools for Technology Transfer, 14(3):307--326, 2012.Google ScholarDigital Library
- Viviana Bono, Chiara Messa, and Luca Padovani. Typing copyless message passing. In ESOP '11, volume 6602 of Springer LNCS, pages 57--76, 2011. Google ScholarDigital Library
- Sara Capecchi, Mario Coppo, Mariangiola Dezani-Ciancaglini, Sophia Drossopoulou, and Elena Giachino. Amalgamating sessions and methods in object-oriented languages with generics. Theoret. Comp. Sci., 410:142--167, 2009. Google ScholarDigital Library
- Marco Carbone, Kohei Honda, and Nobuko Yoshida. Structured interactional exceptions in session types. In CONCUR'08, volume 5201 of Springer LNCS, pages 402--417, 2008. Google ScholarDigital Library
- Silvia Crafa and Luca Padovani. The chemical approach to typestate-oriented programming. In OOPSLA '15, pages 917--934. ACM Press, 2015. Google ScholarDigital Library
- Robert DeLine and Manuel Fähndrich. Enforcing high-level protocols in low-level software. In PLDI '01, pages 59--69. ACM Press, 2001. Google ScholarDigital Library
- Robert DeLine and Manuel Fähndrich. Typestates for objects. In ECOOP '04, volume 3086 of Springer LNCS, pages 465--490, 2004.Google Scholar
- Mariangiola Dezani-Ciancaglini, Sophia Drossopoulou, Dimitris Mostrous, and Nobuko Yoshida. Objects and session types. Information and Computation, 207(5):595--641, 2009. Google ScholarDigital Library
- Mariangiola Dezani-Ciancaglini, Elena Giachino, Sophia Drossopoulou, and Nobuko Yoshida. Bounded session types for object oriented languages. In FMCO '06, volume 4709 of Springer LNCS, pages 207--245, 2006. Google ScholarDigital Library
- Mariangiola Dezani-Ciancaglini, Dimitris Mostrous, Nobuko Yoshida, and Sophia Drossopolou. Session types for object-oriented languages. In ECOOP '06, volume 4067 of Springer LNCS, pages 328--352, 2006. Google ScholarDigital Library
- Mariangiola Dezani-Ciancaglini, Nobuko Yoshida, Alexander Ahern, and Sophia Drossopolou. A distributed object-oriented language with session types. In TGC '05, volume 3705 of Springer LNCS, pages 299--318, 2005. Google ScholarDigital Library
- Manuel Fähndrich, Mark Aiken, Chris Hawblitzel, Orion Hodson, Galen Hunt, James R. Larus, and Steven Levi. Language support for fast and reliable message-based communication in Singularity OS. In EuroSys '06, pages 177--190. ACM Press, 2006.Google ScholarDigital Library
- Manuel Fähndrich and Robert DeLine. Adoption and focus: Practical linear types for imperative programming. In PLDI '02, pages 13--24. ACM Press, 2002. Google ScholarDigital Library
- Ronald Garcia, Éric Tanter, Roger Wolff, and Jonathan Aldrich. Foundations of typestate-oriented programming. ACM Trans. Program. Lang. Syst., 36(4):12:1--12:44, 2014. Google ScholarDigital Library
- Simon J. Gay and Malcolm J. Hole. Subtyping for session types in the pi calculus. Acta Informatica, 42(2/3):191--225, 2005.Google ScholarCross Ref
- Simon J. Gay and Vasco T. Vasconcelos. Linear type theory for asynchronous session types. Journal of Functional Programming, 20(1):19--50, 2010. Google ScholarDigital Library
- Simon J. Gay, Vasco T. Vasconcelos, António Ravara, Nils Gesbert, and Alexandre Z. Caldeira. Modular session types for distributed object-oriented programming. In POPL '10, pages 299--312. ACM Press, 2010. Google ScholarDigital Library
- Görel Hedin. An introductory tutorial on Jast Add attribute grammars. In Generative and Transformational Techniques in Software Engineering III, volume 6491 of Springer LNCS, pages 166--200, 2011. Google ScholarDigital Library
- K. Honda, N. Yoshida, and M. Carbone. Multiparty asynchronous session types. In POPL '08, pages 273--284. ACM Press, 2008. Google ScholarDigital Library
- Raymond Hu, Dimitrios Kouzapas, Olivier Pernet, Nobuko Yoshida, and Kohei Honda. Type-safe eventful sessions in Java. In ECOOP '10, volume 6183 of Springer LNCS, pages 329--353, 2010. Google ScholarDigital Library
- Raymond Hu and Nobuko Yoshida. Hybrid session verification through endpoint API generation. In FASE '16, volume 9633 of Springer LNCS, pages 401--418, 2016.Google Scholar
- Raymond Hu, Nobuko Yoshida, and Kohei Honda. Session-based distributed programming in Java. In ECOOP '08, volume 5142 of Springer LNCS, pages 516--541, 2008. Google ScholarDigital Library
- Idris language homepage. www.idris-lang.org.Google Scholar
- Dimitrios Kouzapas, Ornela Dardha, Roly Perera, and Simon J. Gay. Typechecking protocols with Mungo and StMungo (long version). http://www.dcs.gla.ac.uk/research/mungo/papers/mungo.pdf.Google Scholar
- Message Passing Forum. MPI: A message-passing interface standard. Technical report, University of Tennessee, 1994. Google ScholarDigital Library
- Filipe Militão, Jonathan Aldrich, and Luís Caires. Aliasing control with view-based typestate. In FTfJP '10. ACM Press, 2010.Google Scholar
- Matthias Neubauer and Peter Thiemann. An implementation of session types. In PADL '04, volume 3057 of Springer LNCS, pages 56--70, 2004.Google Scholar
- Rumyana Neykova and Nobuko Yoshida. Multiparty session actors. In COORDINATION '14, volume 8459 of Springer LNCS, pages 131--146, 2014. Google ScholarDigital Library
- Rumyana Neykova, Nobuko Yoshida, and Raymond Hu. SPY: local verification of global protocols. In RV '13, volume 8174 of Springer LNCS, pages 358--363, 2013.Google Scholar
- Nicholas Ng, José Gabriel de Figueiredo Coutinho, and Nobuko Yoshida. Protocols by default - safe MPI code generation based on session types. In CC '15, volume 9031 of Springer LNCS, pages 212--232, 2015.Google Scholar
- Nicholas Ng, Nobuko Yoshida, and Kohei Honda. Multiparty session C: safe parallel programming with message optimisation. In TOOLS '12, volume 7304 of Springer LNCS, pages 202--218, 2012. Google ScholarDigital Library
- Nicholas Ng, Nobuko Yoshida, Olivier Pernet, Raymond Hu, and Yiannos Kryftis. Safe parallel programming with Session Java. In COORDINATION '11, volume 6721 of Springer LNCS, pages 110--126, 2011. Google ScholarDigital Library
- Riccardo Pucella and Jesse A. Tov. Haskell session types with (almost) no class. In Proceedings of the 1st ACM SIGPLAN Symposium on Haskell, pages 25--36. ACM Press, 2008. Google ScholarDigital Library
- Rust language homepage. www.rust-lang.org.Google Scholar
- Scribble project homepage. www.scribble.org.Google Scholar
- Extended simple mail transfer protocol, RFC 5321. https://tools.ietf.org/html/rfc5321.Google Scholar
- Robert E. Strom and Shaula Yemini. Typestate: A programming language concept for enhancing software reliability. IEEE Trans. Softw. Eng., 12(1):157--171, 1986. Google ScholarDigital Library
- Joshua Sunshine, Karl Naden, Sven Stork, Jonathan Aldrich, and Éric Tanter. First-class state change in Plaid. In OOPSLA '11, pages 713--732. ACM Press, 2011. Google ScholarDigital Library
- Roger Wolff, Ronald Garcia, Eric Tanter, and Jonathan Aldrich. Gradual typestate. In ECOOP '11, volume 6813 of Springer LNCS, pages 459--483, 2011. Google ScholarDigital Library
- Nobuko Yoshida, Raymond Hu, Rumyana Neykova, and Nicholas Ng. The Scribble protocol language. In TGC '13, volume 8358 of Springer LNCS, pages 22--41, 2013.Google Scholar
Index Terms
- Typechecking protocols with Mungo and StMungo
Recommendations
Typechecking Java Protocols with [St]Mungo
Formal Techniques for Distributed Objects, Components, and SystemsAbstractThis is a tutorial paper on [St]Mungo, a toolchain based on multiparty session types and their connection to typestates for safe distributed programming in Java language.
The StMungo (“Scribble-to-Mungo”) tool is a bridge between multiparty session ...
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 ...
Typestate-like analysis of multiple interacting objects
This 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 ...
Comments