Top

Published in:

2020 | OriginalPaper | Chapter

Typechecking Java Protocols with [St]Mungo

Authors : A. Laura Voinea, Ornela Dardha, Simon J. Gay

Published in: Formal Techniques for Distributed Objects, Components, and Systems

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Tutorial: Parameterized Verification with Byzantine Model Checker

next chapter Towards a Hybrid Verification Methodology for Communication Protocols (Short Paper)

COST Action IC1201: Behavioural Types for Reliable Large-Scale Software Systems (BETTY), www.behavioural-types.eu.

EPSRC EP/K034413/1 From Data Types to Session Types: A Basis for Concurrency and Distribution (ABCD), groups.inf.ed.ac.uk/abcd/.

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

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

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

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

Ancona, D., et al.: Behavioral types in programming languages. Found. Trends Program. Lang. 3(2–3), 95–230 (2016). https://doi.org/10.1561/2500000031CrossRef

ANTLR Project Homepage. www.antlr.org

Balzer, S., Toninho, B., Pfenning, F.: Manifest deadlock-freedom for shared session types. In: Caires, L. (ed.) ESOP 2019. LNCS, vol. 11423, pp. 611–639. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17184-1_22CrossRef

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

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

10.

Bierhoff, K., Beckman, N.E., Aldrich, J.: Practical API protocol checking with access permissions. In: Drossopoulou, S. (ed.) ECOOP 2009. LNCS, vol. 5653, pp. 195–219. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03013-0_10CrossRef

11.

Bodden, E., Hendren, L.J.: The clara framework for hybrid typestate analysis. STTT 14(3), 307–326 (2012). https://doi.org/10.1007/s10009-010-0183-5CrossRef

12.

Bono, V., Messa, C., Padovani, L.: Typing copyless message passing. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 57–76. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19718-5_4CrossRef

13.

Capecchi, S., Castellani, I., Dezani-Ciancaglini, M.: Information flow safety in multiparty sessions. Math. Struct. Comput. Sci. 26(8), 1352–1394 (2016). https://doi.org/10.1017/S0960129514000619MathSciNetCrossRefMATH

14.

Carbone, M., Honda, K., Yoshida, N.: Structured interactional exceptions in session types. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 402–417. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-85361-9_32CrossRef

15.

Castro-Perez, D., Hu, R., Jongmans, S., Ng, N., Yoshida, N.: Distributed programming using role-parametric session types in go: statically-typed endpoint APIs for dynamically-instantiated communication structures. PACMPL 3(POPL), 29:1–29:30 (2019). https://doi.org/10.1145/3290342CrossRef

16.

Crafa, S., Padovani, L.: The chemical approach to typestate-oriented programming. In: OOPSLA, pp. 917–934. ACM (2015). https://doi.org/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). https://doi.org/10.1145/378795.378811

19.

DeLine, R., Fähndrich, M.: Typestates for objects. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 465–490. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24851-4_21CrossRef

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). https://doi.org/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). https://doi.org/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., Aldrich, J.: Foundations of typestate-oriented programming. ACM Trans. Program. Lang. Syst. 36(4), 12:1–12:44 (2014). https://doi.org/10.1145/2629609CrossRef

24.

Gay, S.J., Ravara, A. (eds.): Behavioural Types: From Theory to Tools. River Publishers, Denmark (2017)

25.

Hedin, G.: An introductory tutorial on JastAdd attribute grammars. In: Fernandes, J.M., Lämmel, R., Visser, J., Saraiva, J. (eds.) GTTSE 2009. LNCS, vol. 6491, pp. 166–200. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-18023-1_4CrossRef

26.

Honda, K.: Types for dyadic interaction. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 509–523. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-57208-2_35CrossRef

27.

Honda, K., Mukhamedov, A., Brown, G., Chen, T.-C., Yoshida, N.: Scribbling interactions with a formal foundation. In: Natarajan, R., Ojo, A. (eds.) ICDCIT 2011. LNCS, vol. 6536, pp. 55–75. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19056-8_4CrossRef

28.

Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 122–138. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0053567CrossRef

29.

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

30.

Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. J. ACM 63(1), 9:1–9:67 (2016). https://doi.org/10.1145/2827695MathSciNetCrossRefMATH

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., Yoshida, N.: Hybrid session verification through endpoint API generation. In: Stevens, P., Wąsowski, A. (eds.) FASE 2016. LNCS, vol. 9633, pp. 401–418. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49665-7_24CrossRef

33.

Hüttel, H., et al.: Foundations of session types and behavioural contracts. ACM Comput. Surv. 49(1), 3:1–3:36 (2016). https://doi.org/10.1145/2873052CrossRef

34.

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

35.

Kouzapas, D., Dardha, O., Perera, R., Gay, S.J.: Typechecking protocols with Mungo and StMungo: a session type toolchain for java. Sci. Comput. Program. 155, 52–75 (2018). https://doi.org/10.1016/j.scico.2017.10.006CrossRef

36.

Militão, F., Aldrich, J., Caires, L.: Aliasing control with view-based typestate. In: FTfJP@ECOOP, pp. 7:1–7:7. ACM (2010). https://doi.org/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). https://doi.org/10.1145/3178372.3179495

38.

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

39.

Padovani, L.: A simple library implementation of binary sessions. J. Funct. Program. 27, e4 (2017). https://doi.org/10.1017/S0956796816000289MathSciNetCrossRefMATH

40.

Padovani, L.: Deadlock-free typestate-oriented programming. Program. J. 2(3), 15 (2018). https://doi.org/10.22152/programming-journal.org/2018/2/15CrossRef

41.

Scribble Project Homepage. www.scribble.org

42.

Strom, R.E., Yemini, S.: Typestate: a programming language concept for enhancing software reliability. IEEE Trans. Softw. Eng. 12(1), 157–171 (1986). https://doi.org/10.1109/TSE.1986.6312929CrossRefMATH

43.

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

44.

Takeuchi, K., Honda, K., Kubo, M.: An interaction-based language and its typing system. In: Halatsis, C., Maritsas, D., Philokyprou, G., Theodoridis, S. (eds.) PARLE 1994. LNCS, vol. 817, pp. 398–413. Springer, Heidelberg (1994). https://doi.org/10.1007/3-540-58184-7_118CrossRef

45.

Wolff, R., Garcia, R., Tanter, É., Aldrich, J.: Gradual typestate. In: Mezini, M. (ed.) ECOOP 2011. LNCS, vol. 6813, pp. 459–483. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22655-7_22CrossRef

Title: Typechecking Java Protocols with [St]Mungo
Authors: A. Laura Voinea
Ornela Dardha
Simon J. Gay
Publisher: Springer International Publishing
Book: Formal Techniques for Distributed Objects, Components, and Systems
Print ISBN: 978-3-030-50085-6

Electronic ISBN: 978-3-030-50086-3

Copyright Year: 2020
DOI: https://doi.org/10.1007/978-3-030-50086-3_12

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner