SLAS is an Aurora collaboration project involving
- the Cash team
-
Software Engineering (SE) research group at the Dept. of Computing, Mathematics and Physics, Western Norway University of Applied Sciences (HVL) — Bergen
Main participants: Violet Ka I Pun, Einar Broch Johnsen, Ludovic Henrio
Scientific description:
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, depending on their typing discipline. 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.
Different approaches have been proposed and discussed to combine the two families of futures. For exam- ple, the work in [4] observes that the synchronisation of implicit futures and explicit is based on dataflow and control-flow, respectively, and introduces a new kind of futures that are explicit but with dataflow synchronisa- tion. A more complete characterisation of the differences between dataflow futures and control-flow futures is described in [3] that also proposes a model which integrates these two types of futures.
The global objective of this project is to combine our competencies in the formal specification of futures and actors and the recent advances of the participants in the domain of dataflow and control flow futures to further study dataflow aspects in programming languages, in particular, the unification of futures, asynchronous actors, and synchronous languages.
To reach this global objective, the 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 specification can be developed in terms of a formalisation based on symbolic trace semantics, in the style of earlier work [2] from the Norwegian side, which proposes a locally abstract, globally concrete (LAGC) semantics for concurrent programming. 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.
In this project, we extend the framework of symbolic trace semantics to study dataflow synchronisation on futures. In practice, we will 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 synchronisa- tion 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 also be the perfect context to start the study of another important aspect of sym- bolic semantics: How is this new form of semantics adapted to study race-conditions and non-determinism? The new notion of traces will require us to study how interleaving between different threads is revealed in the context of our new semantics. We believe that the notion of symbolic traces should be a good setting to reason about race-conditions and data-races, and further research on this issue will be conducted in the project. Thus, the global objective can be achieved by the following three technical objectives:
1. To formalise the semantics that captures dataflow synchronisation on futures;
2. to develop an executable prototype to experiment with the proposed formalism; and 3. to study the broader domain regarding dataflow aspects of programming languages.
On a more practical side, our goal is to bring contribution to programming languages and their implementations. The long term objective is the unification of notions that exist in actor languages, in dataflow languages, and in synchronous languages. While such an objective is ambitious and should be achieved in a context of a much larger project, we will investigate in this bilateral project the possibility to use dataflow futures in synchronous and dataflow languages. Next steps that could be investigated at the end of the project and could lead to further developments would be to introduce rich synchronisation primitives inspired by those coming from the active object languages (e.g., ParT, streaming futures). On a longer term, this research direction will allow us to integrate notions taken from dataflow languages, synchronous languages, and actor languages in a common framework and use it to implement efficient coupling between software entities, either at a low level for the synchronisation of dataflow kernels in the Cash team, or at a high level for the scheduling of actors running on a Cloud on the HVL side.
Clearly, the extension of symbolic trace semantics will also contribute to a better understanding of the relationship between these different programming paradigms, giving a practical application to the theoretical contributions of the project.