×

zbMATH — the first resource for mathematics

A type checking algorithm for concurrent object protocols. (English) Zbl 1400.68141
Summary: Concurrent objects can be accessed and possibly modified concurrently by several running processes. It is notoriously difficult to make sure that such objects are consistent with – and are used according to – their intended protocol. In this paper we detail a type checking algorithm for concurrent objects protocols that provides automated support for this verification task. We model concurrent objects in the Objective Join Calculus and specify protocols using terms of a Commutative Kleene Algebra. The presented results are an essential first step towards the application of this static analysis technique to real-world programs.

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Software:
z3; Mungo; LASH; session-ocaml
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Agha, Gul, Actors: A model of concurrent computation in distributed systems, (1986), MIT Press
[2] Aldrich, Jonathan; Sunshine, Joshua; Saini, Darpan; Sparks, Zachary, Typestate-oriented programming, (Companion to the 24th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA’09, (2009), ACM), 1015-1022
[3] Ancona, Davide; Bono, Viviana; Bravetti, Mario; Campos, Joana; Castagna, Giuseppe; Deniélou, Pierre-Malo; Gay, Simon J.; Gesbert, Nils; Giachino, Elena; Hu, Raymond; Johnsen, Einar Broch; Martins, Francisco; Mascardi, Viviana; Montesi, Fabrizio; Neykova, Rumyana; Ng, Nicholas; Padovani, Luca; Vasconcelos, Vasco T.; Yoshida, Nobuko, Behavioral types in programming languages, Found. Trends Program. Lang., 3, 95-230, (2016)
[4] Armstrong, Joe, Erlang, Commun. ACM, 53, 9, 68-75, (2010)
[5] Berry, Gérard; Boudol, Gérard, The chemical abstract machine, Theor. Comput. Sci., 96, 1, 217-248, (1992) · Zbl 0747.68013
[6] Boigelot, Bernard, The liège automata-based symbolic handler (LASH), (August 2017)
[7] Brzozowski, Janusz A., Derivatives of regular expressions, J. ACM, 11, 4, 481-494, (1964) · Zbl 0225.94044
[8] Castagna, Giuseppe; Dezani-Ciancaglini, Mariangiola; Padovani, Luca, On global types and multi-party sessions, Log. Methods Comput. Sci., 8, 1-45, (2012) · Zbl 1238.68026
[9] Colaço, Jean-Luis; Pantel, Marc; Dagnat, Fabien; Sallé, Patrick, Static safety analysis for non-uniform service availability in actors, (Proceedings of the 3rd International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS’99, IFIP Conference Proceedings, vol. 139, (1999), Kluwer) · Zbl 0928.68048
[10] Conway, John, Regular algebra and finite machines, (1971), William Clowes & Sons Ltd · Zbl 0231.94041
[11] Courcelle, Bruno, Fundamental properties of infinite trees, Theor. Comput. Sci., 25, 95-169, (1983) · Zbl 0521.68013
[12] Crafa, Silvia; Padovani, Luca, The chemical approach to typestate-oriented programming, ACM Trans. Program. Lang. Syst., 39, 13:1-13:45, (2017)
[13] de’Liguoro, Ugo; Padovani, Luca, Mailbox types for unordered interactions, (Proceedings of the 32nd European Conference on Object-Oriented Programming, ECOOP’18, LIPIcs, vol. 109, (2018), Schloss Dagstuhl)
[14] Esparza, Javier; Kiefer, Stefan; Luttenberger, Michael, Newtonian program analysis, J. ACM, 57, 6, 33:1-33:47, (November 2010)
[15] Fournet, Cédric; Gonthier, Georges, The reflexive CHAM and the join-calculus, (Proceedings of POPL’96, (1996), ACM), 372-385
[16] Fournet, Cédric; Laneve, Cosimo; Maranget, Luc; Rémy, Didier, Inheritance in the join calculus, J. Log. Algebraic Program., 57, 1-2, 23-69, (2003) · Zbl 1035.03011
[17] Garcia, Ronald; Tanter, Éric; Wolff, Roger; Aldrich, Jonathan, Foundations of typestate-oriented programming, ACM Trans. Program. Lang. Syst., 36, 4, 12, (2014)
[18] Haase, Christoph; Hofman, Piotr, Tightening the complexity of equivalence problems for commutative grammars, (Proceedings of STACS’16, LIPIcs, vol. 47, (2016)), 41:1-41:14 · Zbl 1388.68154
[19] Haller, Philipp; Sommers, Frank, Actors in scala, Concurrent Programming for the Multi-core Era, (2011), Artima
[20] Hewitt, Carl; Bishop, Peter; Steiger, Richard, A universal modular ACTOR formalism for artificial intelligence, (Proceedings of IJCAI’73, (1973), William Kaufmann), 235-245
[21] Hoare, C. A.R.; Möller, Bernhard; Struth, Georg; Wehrman, Ian, Concurrent Kleene algebra, (Proceedings of CONCUR’09, LNCS, vol. 5710, (2009), Springer), 399-414 · Zbl 1254.68172
[22] Honda, Kohei, Types for dyadic interaction, (Proceedings of CONCUR’93, LNCS, vol. 715, (1993), Springer), 509-523 · Zbl 0939.68642
[23] Honda, Kohei; Yoshida, Nobuko; Carbone, Marco, Multiparty asynchronous session types, J. ACM, 63, 1, 9, (2016) · Zbl 1426.68047
[24] Hopkins, Mark W.; Kozen, Dexter, Parikh’s theorem in commutative Kleene algebra, (Proceedings of LICS’99, (1999), IEEE), 394-401
[25] Hüttel, Hans; Lanese, Ivan; Vasconcelos, Vasco T.; Caires, Luís; Carbone, Marco; Deniélou, Pierre-Malo; Mostrous, Dimitris; Padovani, Luca; Ravara, António; Tuosto, Emilio; Vieira, Hugo Torres; Zavattaro, Gianluigi, Foundations of session types and behavioural contracts, ACM Comput. Surv., 49, 1, 3:1-3:36, (2016)
[26] Huynh, Dung T., The complexity of equivalence problems for commutative grammars, Inf. Control, 66, 1/2, 103-121, (1985) · Zbl 0601.68048
[27] Imai, Keigo; Yoshida, Nobuko; Yuen, Shoji, Session-ocaml: a session-based library with polarities and lenses, (Proceedings of COORDINATION’17, LNCS, vol. 10319, (2017), Springer), 99-118
[28] Kouzapas, Dimitrios; Dardha, Ornela; Perera, Roly; Gay, Simon J., Typechecking protocols with mungo and stmungo: a session type toolchain for Java, Sci. Comput. Program., 155, 52-75, (2018)
[29] Padovani, Luca, On projecting processes into session types, Math. Struct. Comput. Sci., 22, 237-289, (2012) · Zbl 1277.68199
[30] Padovani, Luca, \(\mathsf{Cobalt} \mathbf{Blue}\) - behavioral type checking for concurrent objects, (August 2017)
[31] Padovani, Luca, A simple library implementation of binary sessions, J. Funct. Program., 27, (2017) · Zbl 1418.68036
[32] Padovani, Luca, Deadlock-free typestate-oriented programming, Program. J., 2, 3, (2018)
[33] Puntigam, Franz, State inference for dynamically changing interfaces, Comput. Lang., 27, 4, 163-202, (2001) · Zbl 0997.68016
[34] The Z3 theorem prover, (August 2017), Microsoft Research
[35] Vasconcelos, Vasco Thudichum, Typed concurrent objects, (Proceedings of the 8th European Conference on Object-Oriented Programming, ECOOP’94, LNCS, vol. 821, (1994), Springer), 100-117
[36] Wolper, Pierre; Boigelot, Bernard, On the construction of automata from linear arithmetic constraints, (Proceedings of TACAS’00, LNCS, vol. 1785, (2000), Springer), 1-19 · Zbl 0964.68082
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.