EasyJoin – Concurrent Typestate-Oriented Programming in Java

Overview

TypeState-Oriented Programming (TSOP) [AldrichEtAl09] is a programming methodology for implementing objects with a state-sensitive public interface. Common examples of such objects are iterators, files, and containers. Concurrent TSOP [CrafaPadovani17] is an extension of TSOP to concurrent objects such as locks, future variables, barriers, and the like. EasyJoin [GerboPadovani19] is a code generator that allows Java programmers to use concurrent TSOP when implementing and using object with state-sensitive interfaces. Below is an example of Java class for future variables written using concurrent TSOP and EasyJoin.

@Protocol("*get·(EMPTY·put + FULL)")
class Future<A> {
    @State     private void EMPTY();
    @State     private void FULL(A x);
    @Operation public  A    get();
    @Operation public  void put(A x);
    @Reaction  private void when_EMPTY_put(A x) { this.FULL(x); }
    @Reaction  private A    when_FULL_get(A x) { this.FULL(x); return x; }
    public Future() { this.EMPTY(); }
}

The states of an object are represented as methods with a @State annotation. In the example, the EMPTY state represents an empty variable (one which has not been resolved yet) and the FULL state represents a resolved variable. State methods always have void return type but may have argument representing data that is meaningful when the object is in that particular state. In the example, the FULL method has an argument x containing the current value of the future variable. Invoking a state method means changing the state of the object to the one represented by the method. For example, the constructor initializes the future variable is state EMPTY.

The operations of an object that depend on (and may affect) its state are represented as methods with an @Operation annotation. In the example, the put operation is used to resolve a future variable and the get operation is used to retrieve the content of a future variable. Operation methods may have arguments and possibly return results. In the example, the put method has an argument x representing the value with which the future variable is resolved, whereas the return type of the get method corresponds to that of the value stored in the future variable.

The body of state and operation methods is not provided by programmer, but is generated automatically by EasyJoin. The actual behavior of the object to different combinations of state and operations is specified by reactions, represented as methods with a @Reaction annotation. The two reactions in the example specify that the put operation invoked on an EMPTY variable resolves the variable by changing its state to FULL, whereas the get operation invoked on a FULL variable leaves the variable in that state and returns the current value of the variable. In general, a reaction combines exactly one operation and zero or more states. The synchronization logic that detects the moment when a reaction fires is automatically generated by EasyJoin.

Object Protocols

There are no reactions specifying the effect of a get operation on an EMPTY variable and the effect of a put operation on a FULL variable. In fact, get has an effect only when the variable is FULL and put has an effect only when the variable is EMPTY. However, there is a difference between the two cases: a process trying to read the content of an EMPTY future variable is not doing anything wrong. It simply means that the process will be suspended until the variable is resolved. On the contrary, a process trying to resolve a FULL future variable is violating the protocol of the future variable, because a future variable is meant to be resolved only once. To distinguish the two possibilities, the programmer specifies the protocol of the class using a @Protocol annotation. The value of the annotation is a behavioral type indicating, in this case, that EMPTY and FULL are mutually exclusive states, that get can be invoked any number of times regardless of the state of the future variable, and that put can only be invoked once when the variable is EMPTY. The code generated by EasyJoin includes runtime checks verifying whether an object is used according to its protocol. In case it's not, a suitable exception is thrown.

The general syntax and meaning of types is the following:

• a type m, where m is either a state or an operation, means that it is legal to invoke method m on the object once;

• a type *m means that it is legal to invoke method m on the object any number of times, possibly by concurrent processes;

• a type T·S means that the object must be used as specified by both T and S. For example, EMPTY·put means that both methods EMPTY and put must be invoked (once) on the object;

• a type T + S means that the object must be used either as specified by T or as specified by S. For example, EMPTY·put + FULL means that either the EMPTY method is invoked (in combination with put) or the FULL method is invoked, imposing that the state of a future variable is either EMPTY or FULL. Trying to invoke both EMPTY and FULL will cause an exception.

A formal semantics of object protocols is given in [CrafaPadovani17].

Installation instructions

You need GHC to compile EasyJoin and, optionally, Graphviz to visualize matching automata. Use of the Haskell Platform (full version) and Cabal is recommended. After unpacking the archive, just run make to create the EasyJoin code generator. The examples folder contains a few examples of (concurrent) TSOP in Java using EasyJoin. Running make in there will generate all classes and the corresponding matching automata (dot is necessary to produce the PDFs of the automata).

References

[AldrichEtAl09]: Jonathan Aldrich, Joshua Sunshine, Darpan Saini and Zachary Sparks: Typestate-Oriented Programming, Proceedings of OOPSLA, 2009.

[CrafaPadovani17]: Silvia Crafa and Luca Padovani: The Chemical Approach to Typestate-Oriented Programming, ACM Transactions on Programming Languages and Systems, 2017.

[GerboPadovani19]: Rosita Gerbo and Luca Padovani: Concurrent Typestate-Oriented Programming in Java, Proceedings of PLACES, 2019.