Mungo and StMungo: Tools for Typechecking Protocols in Java

Abstract

Modern computing is dominated by communication, at every level from manycore architectures through multithreaded programs to large-scale distributed systems; this contrasts with the original emphasis on data processing. Early recognition of the importance of structured data meant that high-level programming languages have always incorporated data types and supported programmers through the techniques of static and dynamic typechecking. The foundational status of structured data was explicitly recognised in the title of Wirth’s classic 1976 text Algorithms + Data Structures = Programs, but a more appropriate modern slogan would be Programs + Communication Structures = Systems. The new reality of communication-based software development needs to be supported by programming tools based on structuring principles and high-level abstractions. Given the success of data types, it is natural to apply type-theoretic techniques to the specification and verification of communication-based code. During the last twenty years, this goal has been pursued by the expanding and increasingly active research community on session types [13, 14, 25]. A session type is a formal structured description of a communication protocol, specifying the type, sequence and direction of messages. By embedding this description in the type system of a programming language, adherence to the protocol can be verified by static typechecking; if desired, dynamic monitoring can be introduced into the runtime system. Several researchers have worked towards making typechecked communication structures available for mainstream software development, by transferring session types from their original setting of pi-calculus to functional and object-oriented languages [3, 5, 6, 7, 9, 16, 18, 20]. Gay et al. [10] proposed an integration of session types and object-oriented programming through the more general concept of typestate [23], in which methods are constrained to be called only in particular sequences. They defined a translation from the session types of communication channels into typestate specifications that constrained the use of send and receive methods on channel objects. Their notation for typestate specifications was itself inspired by the syntax of session types. We (the first four authors of the present chapter) extended that work and implemented it as Mungo [17], a front-end typechecking tool for Java. We also generalised the translation from session types to typestate specifications, so that it handles multiparty [12] instead of binary session types, and made it concrete by implementing StMungo [17], a translator from the Scribble [21, 26] protocol description language into Mungo specifications. The Scribble description of a protocol is translated into an API with which to program implementations of protocol roles; the typestate specification associated with the API permits static checking of the correctness of the implementation. Our previous paper [17] illustrated the use of Mungo and StMungo with a substantial case study based on the SMTP protocol [22], including the low-level implementation details necessary to enable communication with standard SMTP servers. This achieved the long-standing goal of using session types to specify and verify implementations of real internet protocols. The present chapter describes Mungo and StMungo in relation to three examples. The first, in Section 1.2.1, illustrates Mungo by defining and checking a typestate specification for an iterator. The second, in Section 1.3, is a simple multiparty scenario based on a travel agency. Finally, in Section 1.4, we show how Mungo and StMungo can be used to typecheck a client for the POP3 protocol [19].