SLAS: Synchronous Languages meet Asynchronous Semantics

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.



CAPESA is an Inria “Associated Team”,

  • Principal investigator (Inria): Laure Gonnord, CASH.
  • Principal investigator (Partner institution): Sébastien Mosser, Département d’informatique, UQAM (Canada)
  • Other participants:] Ludovic Henrio (CNRS, CASH, LIP), Matthieu Moy (University Claude Bernard Lyon 1, CASH, LIP), Jean Privat (UQAM, Canada)
  • Research Project

    In this project we propose to study code transformation in terms of
    “semantic diff”. This notion will be defined thanks to code
    intermediate representations such as Abstract Syntax Trees (AST) or
    the control flow graph, not by textual representation. The objective
    is not only to compute but also to manipulate these “diffs” in several
    contexts: being able to reapply a diff on another program than the one
    it comes from, quantify the interference between two diffs, and more
    generally to study the composability of several diffs. The approach
    will be experimentally validated on problems coming from the domain of
    expertise of both teams of the cooperation: compiler pass analyses
    (expertise of CASH), and git commits (expertise of UQAM). The
    complementarity of the analysis and compilation approaches of the CASH
    team and the expertise on software engineering of the UQAM member will
    ensure the success and the originality of the project.


    static analysis, compilation, software engineering, software
    evolution, code transformation, semantics


(funded by the National French Agency, 2018-2022, PI: Laure Gonnord)

The context of the proposal is the increasing need for methods and tools that are able to deal with the massive parallelism now faced by the programmers. So far, methods and tools based on the polyhedral model (a powerful representation for capturing the flow and the data of a program at the same time) suffer from their lack of expressivity.

The objective of the proposal is to invent a way to reason about more general programs and data structures (e.g., trees). We will explore adapting and extending the existing efficient scheduling techniques that have
been developed since the advent of the polyhedral model. The ambition is to develop a new framework with new ideas that may come from other communities such as abstract interpretation, and rewriting systems.

The website of the project is: