In the world of concurrent programs, futures are often used to synchronise asynchronous operations. In general, futures can be categorised as either implicit or explicit. With implicit futures, it is in general not possible to decide if a variable holds a future value or a concrete value in program codes, and the synchronisation points are implicit and hidden from the programmers. On the contrary, explicit futures use a future type to explicitly indicate the use of a future in the program, and the synchronisation points are explicit and controlled by the programmers. It is observed that the synchronisation of implicit futures and explicit futures is based on dataflow and control-flow, respectively.
This project plans to lift the integration of dataflow and control-flow futures to the level of programming language semantics by developing a formal specification format to allow a seamless transition from control-flow driven programming to dataflow oriented. Such a specification can be developed in terms of a formalisation based on symbolic trace semantics. Symbolic trace semantics is more expressive than traditional state-based semantics; it relies on symbolic traces and is thus more convenient to reason about the behaviour of programs in a symbolic and compositional way.
It is challenging to achieve such an integration: In practice, we need a symbolic trace semantics in which synchronisation triggers an unbounded number of communication events. In the trace, we will have the choice between showing a single synchronisation step, which facilitates reasoning about the program but is more difficult to write, or exposing intermediate steps which bring complementary properties: it is more precise but does not correspond to the programmer's perspective. This project will therefore focus on these chagllenges, and a successful result of this project will form a basis for the unification of futures, asynchronous actors, and synchronous languages.