Article

Typechecking Java Protocols with [St]Mungo

Authors:

A. Laura Voinea,

Simon J. GayAuthors Info & Claims

Formal Techniques for Distributed Objects, Components, and Systems: 40th IFIP WG 6.1 International Conference, FORTE 2020, Held as Part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Valletta, Malta, June 15–19, 2020, Proceedings

Pages 208 - 224

https://doi.org/10.1007/978-3-030-50086-3_12

Published: 15 June 2020 Publication History

Abstract

This 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 types and typestates. StMungo translates a communication protocol, namely a sequence of sends and receives of messages, given as a multiparty session type in the Scribble language, into a typestate specification and a Java API skeleton. The generated API skeleton is then further extended with the necessary logic, and finally typechecked by Mungo. The Mungo tool extends Java with (optional) typestate specifications. A typestate is a state machine specifying a Java object protocol, namely the permitted sequence of method calls of that object. Mungo statically typechecks that method calls follow the object’s protocol, as defined by its typestate specification. Finally, if no errors are reported, the code is compiled with javac and run as standard Java code.

In this tutorial paper we give an overview of the stages of the [St]Mungo toolchain, starting from Scribble communication protocols, translating to Java classes with typestates, and finally to typechecking method calls with Mungo. We illustrate the [St]Mungo toolchain via a real-world case study, the HTTP client-server request-response protocol over TCP. During the tutorial session, we will apply [St]Mungo to a range of examples having increasing complexity, with HTTP being one of them.

References

[1]

Mungo Repository. https://bitbucket.org/abcd-glasgow/mungo-tools/src/master/

[2]

Mungo Webpage. http://www.dcs.gla.ac.uk/research/mungo/

[3]

Aldrich, J., Sunshine, J., Saini, D., Sparks, Z.: Typestate-oriented programming. In: OOPSLA Companion, pp. 1015–1022. ACM (2009). 10.1145/1639950.1640073

[4]

Allan, C., et al.: Adding trace matching with free variables to AspectJ. In: OOPSLA, pp. 345–364. ACM (2005). 10.1145/1094811.1094839

[5]

Ancona D et al. Behavioral types in programming languages Found. Trends Program. Lang. 2016 3 2–3 95-230

[6]

ANTLR Project Homepage. www.antlr.org

[7]

Balzer S, Toninho B, and Pfenning F Caires L Manifest deadlock-freedom for shared session types Programming Languages and Systems 2019 Cham Springer 611-639

[8]

Beckman, N.E., Bierhoff, K., Aldrich, J.: Verifying correct usage of atomic blocks and typestate. In: OOPSLA, pp. 227–244. ACM (2008). 10.1145/1449764.1449783

[9]

Bierhoff, K., Aldrich, J.: Modular typestate checking of aliased objects. In: OOPSLA, pp. 301–320. ACM (2007). 10.1145/1297027.1297050

[10]

Bierhoff K, Beckman NE, and Aldrich J Drossopoulou S Practical API protocol checking with access permissions ECOOP 2009 – Object-Oriented Programming 2009 Heidelberg Springer 195-219

[11]

Bodden E and Hendren LJ The clara framework for hybrid typestate analysis STTT 2012 14 3 307-326

[12]

Bono V, Messa C, and Padovani L Barthe G Typing copyless message passing Programming Languages and Systems 2011 Heidelberg Springer 57-76

[13]

Capecchi S, Castellani I, and Dezani-Ciancaglini MInformation flow safety in multiparty sessionsMath. Struct. Comput. Sci.20162681352-139435701121362.68204

[14]

Carbone M, Honda K, and Yoshida N van Breugel F and Chechik M Structured interactional exceptions in session types CONCUR 2008 - Concurrency Theory 2008 Heidelberg Springer 402-417

[15]

Castro-Perez D, Hu R, Jongmans S, Ng N, and Yoshida N Distributed programming using role-parametric session types in go: statically-typed endpoint APIs for dynamically-instantiated communication structures PACMPL 2019 3 POPL 29:1-29:30

[16]

Crafa, S., Padovani, L.: The chemical approach to typestate-oriented programming. In: OOPSLA, pp. 917–934. ACM (2015). 10.1145/2814270.2814287

[17]

Dardha, O., Gay, S.J., Kouzapas, D., Perera, R., Voinea, A.L., Weber, F.: Mungo and StMungo: tools for typechecking protocols in Java. In: Behavioural Types: From Theory to Tools. River Publishers (2017)

[18]

DeLine, R., Fähndrich, M.: Enforcing high-level protocols in low-level software. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 59–69. ACM (2001). 10.1145/378795.378811

[19]

DeLine R and Fähndrich M Odersky M Typestates for objects ECOOP 2004 – Object-Oriented Programming 2004 Heidelberg Springer 465-490

[20]

Fähndrich, M., et al.: Language support for fast and reliable message-based communication in singularity OS. In: EuroSys, pp. 177–190. ACM (2006). 10.1145/1217935.1217953

[21]

Fähndrich, M., DeLine, R.: Adoption and focus: practical linear types for imperative programming. In: PLDI, pp. 13–24. ACM (2002). 10.1145/512529.512532

[22]

Fielding, R.T., Reschke, J.F.: Hypertext transfer protocol (HTTP/1.1): message syntax and routing. RFC 7230, pp. 1–89 (2014)

[23]

Garcia R, Tanter É, Wolff R, and Aldrich J Foundations of typestate-oriented programming ACM Trans. Program. Lang. Syst. 2014 36 4 12:1-12:44

[24]

Gay SJ and Ravara A Behavioural Types: From Theory to Tools 2017 Denmark River Publishers

[25]

Hedin G Fernandes JM, Lämmel R, Visser J, and Saraiva J An introductory tutorial on JastAdd attribute grammars Generative and Transformational Techniques in Software Engineering III 2011 Heidelberg Springer 166-200

[26]

Honda K Best E Types for dyadic interaction CONCUR 1993 1993 Heidelberg Springer 509-523

[27]

Honda K, Mukhamedov A, Brown G, Chen T-C, and Yoshida N Natarajan R and Ojo A Scribbling interactions with a formal foundation Distributed Computing and Internet Technology 2011 Heidelberg Springer 55-75

[28]

Honda K, Vasconcelos VT, and Kubo M Hankin C Language primitives and type discipline for structured communication-based programming Programming Languages and Systems 1998 Heidelberg Springer 122-138

[29]

Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: POPL, pp. 273–284. ACM (2008). 10.1145/1328438.1328472

[30]

Honda K, Yoshida N, and Carbone MMultiparty asynchronous session typesJ. ACM20166319:1-9:6734902361426.68047

[31]

Hu, R.: Distributed programming using Java APIs generated from session types. Behavioural Types: from Theory to Tools, pp. 287–308 (2017)

[32]

Hu R and Yoshida N Stevens P and Wąsowski A Hybrid session verification through endpoint API generation Fundamental Approaches to Software Engineering 2016 Heidelberg Springer 401-418

[33]

Hüttel H et al. Foundations of session types and behavioural contracts ACM Comput. Surv. 2016 49 1 3:1-3:36

[34]

Kouzapas, D., Dardha, O., Perera, R., Gay, S.J.: Typechecking protocols with mungo and StMungo. In: PPDP, pp. 146–159. ACM (2016). 10.1145/2967973.2968595

[35]

Kouzapas D, Dardha O, Perera R, and Gay SJ Typechecking protocols with Mungo and StMungo: a session type toolchain for java Sci. Comput. Program. 2018 155 52-75

[36]

Militão, F., Aldrich, J., Caires, L.: Aliasing control with view-based typestate. In: FTfJP@ECOOP, pp. 7:1–7:7. ACM (2010). 10.1145/1924520.1924527

[37]

Neykova, R., Hu, R., Yoshida, N., Abdeljallal, F.: A session type provider: compile-time API generation of distributed protocols with refinements in F#. In: CC, pp. 128–138. ACM (2018). 10.1145/3178372.3179495

[38]

Öqvist, J.: ExtendJ: extensible java compiler. In: Programming, pp. 234–235. ACM (2018). 10.1145/3191697.3213798

[39]

Padovani LA simple library implementation of binary sessionsJ. Funct. Program.201727e435934981418.68036

[40]

Padovani L Deadlock-free typestate-oriented programming Program. J. 2018 2 3 15

[41]

Scribble Project Homepage. www.scribble.org

[42]

Strom RE and Yemini STypestate: a programming language concept for enhancing software reliabilityIEEE Trans. Softw. Eng.1986121157-1710575.68036

[43]

Sunshine, J., Naden, K., Stork, S., Aldrich, J., Tanter, É.: First-class state change in Plaid. In: OOPSLA, pp. 713–732 (2011). 10.1145/2048066.2048122

[44]

Takeuchi K, Honda K, and Kubo M Halatsis C, Maritsas D, Philokyprou G, and Theodoridis S An interaction-based language and its typing system PARLE 1994 Parallel Architectures and Languages Europe 1994 Heidelberg Springer 398-413

[45]

Wolff R, Garcia R, Tanter É, and Aldrich J Mezini M Gradual typestate ECOOP 2011 – Object-Oriented Programming 2011 Heidelberg Springer 459-483

Cited By

Giallorenzo SMontesi FPeressotti M(2024)Choral: Object-oriented Choreographic ProgrammingACM Transactions on Programming Languages and Systems10.1145/363239846:1(1-59)Online publication date: 16-Jan-2024
https://dl.acm.org/doi/10.1145/3632398
de Ferro CCogumbreiro TMartins F(2023)Shelley: A Framework for Model Checking Call Ordering on Hierarchical SystemsCoordination Models and Languages10.1007/978-3-031-35361-1_5(93-114)Online publication date: 19-Jun-2023
https://dl.acm.org/doi/10.1007/978-3-031-35361-1_5
Jongmans SProença J(2022)ST4MP: A Blueprint of Multiparty Session Typing for Multilingual ProgrammingLeveraging Applications of Formal Methods, Verification and Validation. Verification Principles10.1007/978-3-031-19849-6_26(460-478)Online publication date: 22-Oct-2022
https://dl.acm.org/doi/10.1007/978-3-031-19849-6_26
Show More Cited By

Index Terms

Typechecking Java Protocols with [St]Mungo
1. Software and its engineering
2. Theory of computation
  1. Semantics and reasoning

Index terms have been assigned to the content through auto-classification.

Recommendations

Typechecking protocols with Mungo and StMungo
PPDP '16: Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming

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 ...
A decentralized analysis of multiparty protocols
Abstract
Protocols provide the unifying glue in concurrent and distributed software today; verifying that message-passing programs conform to such governing protocols is important but difficult. Static approaches based on multiparty session ...
Highlights
- A new analysis of multiparty protocols expressed as Multiparty Session Types (MPST).
Polymorphic Typestate for Session Types
PPDP '23: Proceedings of the 25th International Symposium on Principles and Practice of Declarative Programming

Session types provide a principled approach to typed communication protocols that guarantee type safety and protocol fidelity. Formalizations of session-typed communication are typically based on process calculi, concurrent lambda calculi, or linear ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

Formal Techniques for Distributed Objects, Components, and Systems: 40th IFIP WG 6.1 International Conference, FORTE 2020, Held as Part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Valletta, Malta, June 15–19, 2020, Proceedings

Jun 2020

242 pages

ISBN:978-3-030-50085-6

DOI:10.1007/978-3-030-50086-3

Editors:
Alexey Gotsman
IMDEA Software Institute, Pozuelo de Alarcón, Spain
,
Ana Sokolova
University of Salzburg, Salzburg, Austria

© IFIP International Federation for Information Processing 2020.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 15 June 2020

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 30 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Giallorenzo SMontesi FPeressotti M(2024)Choral: Object-oriented Choreographic ProgrammingACM Transactions on Programming Languages and Systems10.1145/363239846:1(1-59)Online publication date: 16-Jan-2024
https://dl.acm.org/doi/10.1145/3632398
de Ferro CCogumbreiro TMartins F(2023)Shelley: A Framework for Model Checking Call Ordering on Hierarchical SystemsCoordination Models and Languages10.1007/978-3-031-35361-1_5(93-114)Online publication date: 19-Jun-2023
https://dl.acm.org/doi/10.1007/978-3-031-35361-1_5
Jongmans SProença J(2022)ST4MP: A Blueprint of Multiparty Session Typing for Multilingual ProgrammingLeveraging Applications of Formal Methods, Verification and Validation. Verification Principles10.1007/978-3-031-19849-6_26(460-478)Online publication date: 22-Oct-2022
https://dl.acm.org/doi/10.1007/978-3-031-19849-6_26
Jakobsen MRavier ADardha O(2021)Papaya: Global Typestate Analysis of Aliased ObjectsProceedings of the 23rd International Symposium on Principles and Practice of Declarative Programming10.1145/3479394.3479414(1-13)Online publication date: 6-Sep-2021
https://dl.acm.org/doi/10.1145/3479394.3479414
Yoshida NZhou FFerreira F(2021)Communicating Finite State Machines and an Extensible Toolchain for Multiparty Session TypesFundamentals of Computation Theory10.1007/978-3-030-86593-1_2(18-35)Online publication date: 12-Sep-2021
https://dl.acm.org/doi/10.1007/978-3-030-86593-1_2
Bravetti MFrancalanza AGolovanov IHüttel HJakobsen MKettunen MRavara A(2020)Behavioural Types for Memory and Method Safety in a Core Object-Oriented LanguageProgramming Languages and Systems10.1007/978-3-030-64437-6_6(105-124)Online publication date: 30-Nov-2020
https://dl.acm.org/doi/10.1007/978-3-030-64437-6_6

View Options

View options

Get Access

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

Media

Figures

Other

Tables

View Table of Contents