Aliasing Control in an Object-Oriented Programming Language with Typestate Annotations

When writing stateful programs, an order of operation is often expected, even though the order itself is only informally denied, if denied at all. We call the order of operations a protocol. For small protocols, an informal specification may be manageable for the programmer to navigate. However, as the protocols become increasingly complex, it can become difficult for the programmer to ensure that operations are performed in the correct order. Multiple approaches have been proposed to integrate such protocols into programming languages, typestates being a key one. While a type describes all available operations allowed on data of that type, a typestate takes into consideration the context of the operations, hence only allows a subset of all operations, for a given point in the program. We can view the typestate of an object as a state machine for that particular object, where each state has a distinct set of operations available. A related problem to protocol checking is that of ensuring correct communication between processes. For this problem, which has been studied extensively, we employ session types to describe the types of data that will be sent through communication channels. Although session types were originally defined for small calculi, such as the pi-calculus, session types have also been applied to other settings. One such example is the introduction of channels and session types to an object oriented programming language, where a global session type is defined for a class, and the logic for conforming to the session type could be distributed over multiple methods. As a result of the relation between the two problems, the amalgamation of session types and typestate declarations for object oriented programming languages was studied by Dardha and co-authors and resulted in the tools Mungo and StMungo. In Mungo, a Java class is annotated with a typestate declaration, denoting the available set of method calls during the lifetime of the object. As Mungo employ typestate tracking, aliasing of objects must be controlled, to track where an object is updated. Mungo employs a linear typing approach, where only a single reference to an object is available at a given time. This is a common approach to typing communication and is often seen for session types and typestate based languages. The reasoning for enforcing linearity is that when we are working with behavioral types, we expect them to evolve during the lifetime of an object. In Mungo, for example, we expect the typestate of an object to be changed after performing a method call. If we allow unlimited aliasing of object references, changes performed by one alias are not reflected at the other aliases, even if the underlying object has changed. Linear typing sidesteps the issue, by not allowing these aliases to coexist. While such a restriction makes reasoning about types easier, it is very inflexible to program in an object-oriented language that disallows aliasing. During his PhD, Mathias will explore the linearity constraints in the Mungo formal framework and tool implementation, with the aim of relaxing these constraints for more expressive programming with typestates while still preserving the desired soundness and safety properties. The proposed methodology for loosening linearity constraints is alias control. To further the relevance and robustness of Mungo, his PhD also will focus on typestate inference (not present in Mungo so far) as well as the integration of Mungo with mainstream IDEs, making Mungo an applicable and industry-ready tool.