The concurrent games abstract machine
Pierre Clairambault
LIP, ÉNS Lyon
http://perso.ens-lyon.fr/pierre.clairambault/
Date(s) : 24/06/2021 iCal
10h30 - 11h30
In this talk, I will introduce the concurrent games abstract machine: a multi-token machine for Idealized Parallel Algol (IPA), a higher-order concurrent programming language with shared state and semaphores. The abstract machine takes the shape of a compositional interpretation of terms as « Petri structures », certain coloured Petri nets.
For the purely functional fragment, the machine is conceptually close to Geometry of Interaction token machines, originating from Linear Logic and presenting higher-order computation as the low-level process of a token walking through a graph (a proof net) representing the term. This is paired here with folklore ideas on the representation of first-order imperative concurrent programs as coloured Petri nets.
To prove our machine correct, we follow game semantics and represent types as certain games specifying dependencies and conflict between computational events. We define Petri strategies as those Petri structures obeying the rules of the game. In turn, we show how Petri strategies unfold to concurrent strategies in the sense of concurrent games on event structures. This not only entails correctness and adequacy of our machine, but also lets us generate operationally a causal description of the behaviour of programs at higher-order types.
This is (almost finished) joint work with Simon Castellan.
https://arxiv.org/abs/2103.15453
Catégories
