Cash seminars and reading groups: October

Cash seminars have started again, they are now coordinated by Yannick and Ludovic. October seminars were:

SEM 14/10 : Ludo    Phs Thesis of Pierre Leca “Combining active object and BSP programs”

Reading group 21/10 : Christophe “La compilation polyédrique en 30 minutes”

SEM 28/10 :    

  • Ludo (+ Laure): petit topo informel de 15 min sur le nouveau GdT CLAP dans le GdR GPL (avec explication des acronymes)    
  • Yannick (15 minutes) : tour haut niveau du projet Vellvm — principe, objectifs, challenges et sous-projets en cours et futurs

Reading group 04/11 : Laure    Interprétation abstraite 101 (30 min)

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.

14th Cash reading group

14th edition of CASH reading group will be on

25/3 at 14:00 in room 316
This will be a special session where I will speak about communication timing based on an old article:

Synchronous, asynchronous, and causally ordered communication
Bernadette Charron–Bost, Friedemann Mattern, Gerard Tel
Program: 10 minutes brief introduction of the paper followed by details on the results and formalisation and discussion for those who want to stay after the introduction
Presentation will be based on slides of a former course I used to give in Nice

8th edition of CASH reading group

8th edition of CASH reading group will be on
Oct 2 at 15:45

Salle 316


  • Christophe ALIAS: mini-survey of single assignment languages
  • Laure Gonnord and Ludovic Henrio:

    Albert Cohen, Léonard Gérard, and Marc Pouzet. Programming parallelism with futures in Lustre. In ACM International Conference on Embedded Software (EM- SOFT’12), Tampere, Finland, October 7-12 2012. ACM. Best paper award.

7th Cash reading group: 10/4 at 9:30

7th edition of CASH paper presentation will be on
April 10 at 9:30
Salle de réunion M7 3ème étage


  • Laure Gonnord: “Relational Program Reasoning” based on:
    • Relational Program Reasoning Using Compiler IR VSTTE 2016, Moritz
      Kiefer, Vladimir Klebanov, Mattias Ulbrich
    • De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.:
      Relational verification through Horn clause transformation., SAS 2016
    • (opt) Beckert, B., Bormer, T., Gocht, S., Herda, M., Lentzsch, D.,
      Ulbrich, M.: Sem-slice: Exploiting relational verification for
      automatic program slicing. Tool paper IFM 2017
  • Paul Iannetta: “Tiramisu: A Polyhedral Compiler for Expressing Fast and Portable Code”Riyadh Baghdadi, Jessica Ray, Malek Ben Romdhane, Emanuele Del Sozzo, Abdurrahman Akkas, Yunming Zhang, Patricia Suriana, Shoaib Kamil, and Saman Amarasinghe. 2019.  International Symposium on Code Generation and Optimization (CGO 2019).