\documentclass[11pt,a4paper]{article} \usepackage[utf8]{inputenc} \usepackage[T1]{fontenc} \usepackage{amsmath} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{graphicx} \usepackage{indentfirst} \usepackage{enumerate} \usepackage{cite} \usepackage{caption} \usepackage[left=2cm,right=2cm,top=2cm,bottom=2cm]{geometry} \usepackage{todo} % Custom packages \usepackage{leftrule_theorems} \usepackage{my_listings} \usepackage{my_hyperref} \usepackage{math} \usepackage{concurgames} \newcommand{\qtodo}[1]{\colorbox{orange}{\textcolor{blue}{#1}}} \newcommand{\todo}[1]{\colorbox{orange}{\qtodo{\textbf{TODO:} #1}}} \newcommand{\qnote}[1]{\colorbox{Cerulean}{\textcolor{Sepia}{[#1]}}} \newcommand{\note}[1]{\qnote{\textbf{NOTE:} #1}} \author{Théophile \textsc{Bastian}, supervised by Glynn \textsc{Winskel} and Pierre \textsc{Clairambault} \\ \begin{small}Cambridge University\end{small}} \title{Internship report\\Concurrent games as event structures} \date{June-July 2016} \begin{document} \maketitle \begin{abstract} During my internship, I have worked on a \emph{deterministic} game semantics model for a minimalistic \emph{concurrent} language, described using the \emph{games as event structures} formalism. I have proved the \emph{adequacy} of this model with the operational semantics of the language modelled; and I have implemented this model, allowing one to input an expression of the language and getting its representation as Dot graph. This implementation also supports basic operations on event structures, which could be useful to other people working in this domain. \end{abstract} \tableofcontents %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \section{Introduction} \paragraph{Game semantics} are a kind of denotational semantics in which a program's behavior is abstracted as a two-players game, in which Player plays for the program and Opponent plays for the environment of the program (the user, the operating system, \ldots). The execution of a program, in this formalism, is then represented as a succession of moves. For instance, the user pressing a key on the keyboard would be a move of Opponent, to which Player could react by triggering the corresponding action (\eg{} adding the corresponding letter in a text field). Game semantics emerged mostly with~\cite{hyland2000pcf} and~\cite{abramsky2000pcf}, independently establishing a fully-abstract model for PCF using game semantics, while ``classic'' semantics had failed to provide a fully-abstract, reasonable and satisfying model. But this field mostly gained in notoriety with the development of techniques to capture imperative programming languages constructions, among which references handling~\cite{abramsky1996linearity}, followed by higher-order references~\cite{abramsky1998references}, allowing to model languages with side effects; or exception handling~\cite{laird2001exceptions}. Since then, the field has been deeply explored, providing a wide range of such constructions in the literature. A success of game semantics is to provide \emph{compositional} and \emph{syntax-free} semantics. Syntax-free, because representing a program as a strategy on a game totally abstracts it from the original syntax of the programming language, representing only the behavior of a program reacting to its execution environment, which is often desirable in semantics. Compositional, because game semantics are usually defined by induction over the syntax, thus easily composed. For instance, it is worth noting that the application of one term to another is represented as the \emph{composition} of the two strategies. \paragraph{Concurrency in game semantics.} In the continuity of the efforts put forward to model imperative primitives in game semantics, it was natural to focus at some point on modelling concurrency. The problem was tackled by \fname{Laird}~\cite{laird2001game}, introducing game semantics for a \lcalc{} with a few additions, as well as a \emph{parallel execution} operator and communication on channels. It is often considered, though, that \fname{Ghica} and \fname{Murawski}~\cite{ghica2004angelic} really took the fundamental step by defining game semantics for a fine-grained concurrent language including parallel execution of ``threads'' and low-level semaphores --- a way more realistic approach to the problem. However, both of these constructions are based on \emph{interleavings}. That is, they model programs on \emph{tree-like games}, games in which the moves that a player is allowed to play at a given point are represented as a tree (\eg, in a state $A$, Player can play the move $x$ by following an edge of the tree starting from $A$, thus reaching $B$ and allowing Opponent to play a given set of moves --- the outgoing edges of $B$). The concurrency is then represented as the \emph{interleaving} of all possible sequences of moves, in order to reach a game tree in which every possible ``unordered'' (\ie, that is not enclosed in any kind of synchronisation block, as with semaphores) combination of moves is a valid path. However, this approach introduces non-determinism in the strategies: if two moves are available to a player, the model states that they make a non-deterministic uniform choice. Yet, one could reasonably argue that a program should behave consistently with the environment, which would mean that the semantics of a program --- even a concurrent one --- should still be deterministic. This idea was explored outside of the game semantics context, for instance by~\cite{reynolds1978syntactic}, establishing a type-checking system to restrict concurrent programs to deterministic ones. Some recent work makes use of linear logic~\cite{caires2010session} for similar purposes as well. Yet, the interleavings game semantics of these languages remains non-deterministic. \paragraph{The purpose of this internship} was to try to take a first step towards the reunification of those two developments. For that purpose, my objective was to give a \emph{deterministic} game semantics to a linear lambda-calculus enriched with parallel and sequential execution operators, as well as synchronization on channels. In order to model this, I used the games as \emph{event structures} formalism, described later on and introduced in~\cite{rideau2011concurrent} by S. \fname{Rideau} and G. \fname{Winskel}. Roughly, event structures represent a strategy as a \emph{partial order} on the moves, stating that move $x$ can only be played after move $y$, which is more flexible than tree-like game approaches. Although a full-abstraction result could not be reached --- but is not so far away ---, I have proved the \emph{adequacy} of the operational and denotational semantics, and have obtained an implementation of the (denotational) game semantics, that is, code that translates a term of the language into its corresponding strategy. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \section{A linear \lcalc{} with concurrency primitives: \llccs} The language on which my internship was focused was meant to be simple, easy to parse and easy to work on both in theory and on the implementation. It should of course include concurrency primitives. For these reasons, we chose to consider a variant of CCS~\cite{milner1980ccs} --- a simple standard language including parallel and sequential execution primitives, as well as synchronization of processes through \emph{channels} ---, lifted up to the higher order through a \lcalc. The language was then restricted to a \emph{linear} one --- that is, each identifier declared must be referred to exactly once ---, partly to keep the model simple, partly to meet the determinism requirements. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \subsection{A linear variant of CCS~: \linccs} The variant of CCS we chose to use has two base types: \emph{processes}~($\proc$) and \emph{channels}~($\chan$). It has two base processes, $0$ (failure) and $1$ (success), although a process can be considered ``failed'' without reducing to $0$ (in case of deadlock). \begin{figure}[h] \begin{minipage}[t]{0.60\textwidth} \begin{center}Terms\end{center}\vspace{-1em} \begin{align*} t,u,\ldots ::=~&1 & \text{(success)}\\ \vert~&0 & \text{(error)}\\ \vert~&t \parallel u & \text{(parallel)}\\ \vert~&t \cdot u & \text{(sequential)}\\ \vert~&(\nu a) t & \text{(new channel)} \end{align*} \end{minipage} \hfill \begin{minipage}[t]{0.35\textwidth} \begin{center}Types\end{center}\vspace{-1em} \begin{align*} A,B,\ldots ::=~&\proc & \text{(process)} \\ \vert~&\chan & \text{(channel)} \end{align*} \end{minipage} \caption{\linccs{} terms and types}\label{fig:lccs:def} \end{figure} The syntax is pretty straightforward to understand: $0$ and $1$ are base processes; $\parallel$ executes in parallel its two operands; $\cdot$ executes sequentially its two operands (or synchronizes on a channel if its left-hand operand is a channel); $(\nu a)$ creates two new channels, $a$ and $\bar{a}$, on which two processes can be synchronized. Here, the ``synchronization'' simply means that a call to the channel is blocking until its dual channel has been called as well. The language is simply typed as in figure~\ref{fig:lccs:typing}. Note that binary operators split their environment between their two operands, ensuring that each identifier is used at most once, and that no rules (in particular the axiom rules) ``forget'' any part of the environment, ensuring that each identifier is used at least once. For instance, in $\Gamma = \left[p:\proc,\,q:\proc\right]$, $0$ cannot be typed (\ie{} $\overline{\Gamma \vdash 0 : \proc}$ is not a valid rule). \begin{figure}[h] \begin{align*} \frac{~}{\,\vdash 0:\proc} & (\textit{Ax}_0) & \frac{~}{\,\vdash 1:\proc} & (\textit{Ax}_1) & \frac{~}{t:A \vdash t:A} & (\textit{Ax}) & \frac{\Gamma, a:\chan, \bar{a}:\chan \vdash P : \proc} {\Gamma \vdash (\nu a) P : \proc} & (\nu) \end{align*}\vspace{-1.5em}\begin{align*} \frac{\Gamma \vdash P : \proc \quad \Delta \vdash Q : \proc} {\Gamma,\Delta \vdash P \parallel Q : \proc} & (\parallel) & \frac{\Gamma \vdash P : \proc \quad \Delta \vdash Q : \proc} {\Gamma,\Delta \vdash P \cdot Q : \proc} & (\cdot_\proc) & \frac{\Gamma \vdash P : \proc} {\Gamma,a:\chan \vdash a \cdot P: \proc} & (\cdot_\chan) \end{align*} \vspace{-1.5em} \caption{\linccs{} typing rules}\label{fig:lccs:typing} \end{figure} We also equip this language with operational semantics, in the form of a labeled transition system (LTS), as described in figure~\ref{fig:lccs:opsem}, where $a$ denotes a channel and $x$ denotes any possible label. \begin{figure}[h] \begin{align*} \frac{~}{a \cdot P \redarrow{a} P} & & \frac{~}{1 \parallel P \redarrow{\tau} P} & & \frac{~}{1 \cdot P \redarrow{\tau} P} & & \frac{P \redarrow{\tau_c} Q} {(\nu a) P \redarrow{\tau} Q} & (c \in \set{a,\bar{a}})& \frac{P \redarrow{a} P'\quad Q \redarrow{\bar{a}} Q'} {P \parallel Q \redarrow{\tau_a} P' \parallel Q'} \end{align*}\begin{align*} \frac{P \redarrow{x} P'} {P \parallel Q \redarrow{x} P' \parallel Q} & & \frac{Q \redarrow{x} Q'} {P \parallel Q \redarrow{x} P \parallel Q'} & & \frac{P \redarrow{x} P'} {P \cdot Q \redarrow{x} P' \cdot Q} & & \frac{P \redarrow{x} P'} {(\nu a)P \redarrow{x} (\nu a)P'} & (a \not\in \set{x,\tau_a}) \end{align*} \caption{\linccs{} operational semantics}\label{fig:lccs:opsem} \end{figure} We consider that a term $P$ \emph{converges} whenever $P \redarrow{\tau}^\ast 1$, and we write $P \Downarrow$. The $\tau_a$ reduction scheme may sound a bit unusual. It is, however, necessary. Consider the reduction of $(\nu a) (a \cdot 1 \parallel \bar{a} \cdot 1)$: the inner term $\tau_a$-reduces to $1$, thus allowing the whole term to reduce to $1$; but if we replaced that $\tau_a$ with a $\tau$, the whole term would reduce to $(\nu a) 1$, which has no valid type since $a$ and $\bar{a}$ are not consumed (linearity). Our semantics would then not satisfy subject reduction. Switching to an \emph{affine} \linccs{} while keeping it wrapped in a \emph{linear} \lcalc{} was considered, but yielded way too many problems, while switching to a fully-affine model would have modified the problem too deeply. \subsection{Lifting to the higher order: linear \lcalc} In order to reach the studied language, \llccs, we have to lift up \linccs{} to a \lcalc. To do so, we add to the language the constructions of figure~\ref{fig:llam:syntax}, which are basically the usual \lcalc{} constructions slightly transformed to be linear (which is mostly reflected by the typing rules). In particular, the only base types are $\proc$ and $\chan$. \begin{figure}[h] \begin{minipage}[t]{0.55\textwidth} \begin{center}Terms\end{center}\vspace{-1em} \begin{align*} t,u,\ldots ::=~&x \in \mathbb{V} & \text{(variable)}\\ \vert~&t~u & \text{(application)}\\ \vert~&\lambda x^A \cdot t & \text{(abstraction)}\\ \vert~&\text{\linccs}\textit{ constructions} & \end{align*} \end{minipage} \hfill \begin{minipage}[t]{0.40\textwidth} \begin{center}Types\end{center}\vspace{-1em} \begin{align*} A,B,\ldots ::=~&A \linarrow B & \text{(linear arrow)}\\ \vert~&\proc~\vert~\chan & \text{(\linccs)} \end{align*} \end{minipage} \caption{Linear \lcalc{} terms and types}\label{fig:llam:syntax} \end{figure} To keep the language simple and ease the implementation, the $\lambda$-abstractions are annotated with the type of their abstracted variable. The usual $\rightarrow$ symbol was also changed to $\linarrow$, to clearly remind that the terms are \emph{linear}. \smallskip In order to enforce the linearity, the only typing rules of the usual \lcalc{} that have to be changed are the $(\textit{Ax})$ and $(\textit{App})$ presented in figure~\ref{fig:llam:typing}. The $(\textit{Abs})$ rule is the usual one. \begin{figure}[h] \begin{align*} \frac{~}{x : A \vdash x : A} & (\textit{Ax}) & \frac{\Gamma \vdash t : A \linarrow B \quad \Delta \vdash u : A} {\Gamma,\Delta \vdash t~u : B} & (\textit{App}) & \frac{\Gamma, x : A \vdash t : B} {\Gamma \vdash \lambda x^{A} \cdot t : A \linarrow B} & (Abs) \end{align*} \caption{Linear \lcalc{} typing rules}\label{fig:llam:typing} \end{figure} The linearity is here guaranteed: in the (\textit{Ax}) rule, the environment must be $x:A$ instead of the usual $\Gamma, x:A$, ensuring that each variable is used \emph{at least once}; while the environment split in the binary operators' rules ensures that each variable is used \emph{at most once} (implicitly, $\Gamma \cap \Delta = \emptyset$). To lift the operational semantics to \llccs, we only need to add one rule: \[ \frac{P \longrightarrow_\beta P'}{P \redarrow{\tau} P'} \] %%%%%%%%%%%%%%%%%%%%% \subsection{Examples} \begin{itemize} \item Simple channel usage: $T_1 \eqdef \newch{a} (a \cdot 1 \parallel \bar{a} \cdot 1)$. This term converges: $\left(a \cdot 1 \parallel \bar{a} \cdot 1 \right) \redarrow{\tau_a} 1 \parallel 1$, thus $T_1 \redarrow{\tau} \left(1 \parallel 1\right) \redarrow{\tau} 1$. \item Deadlock: $T_2 \eqdef \newch{a} (a \cdot \bar{a} \cdot 1)$. This term does not reduce at all: no reduction is possible under the $\nu$. \item Simple function call: $T_3 \eqdef ((\lambda x^P \cdot x) 1) \parallel 1$ reduces to $1 \parallel 1$. \item Channel passing: $T_4 \eqdef \newch{f}\newch{g} \left(f \cdot 1 \parallel \left(\left( \lambda a^C \cdot \lambda b^C \cdot \lambda c^C \cdot \left(\left(a \cdot 1\right) \cdot \left(b \cdot 1\right)\right) \parallel \left(c \cdot 1\right)\right)\,\bar{f}\,\bar{g}\,g\right)\right)$, which $\beta$-reduces (and thus $\tau$-reduces) to $\newch{f}\newch{g} \left(\left(f\cdot1\right) \parallel \left(\left(\left(\bar{f} \cdot 1\right) \cdot \left(\bar{g} \cdot 1\right)\right) \parallel \left(g \cdot 1\right) \right)\right)$. Note that the function has no idea whether two channels are dual or not. \end{itemize} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \section{A games model} Our goal is now to give a games model for the above language. For that purpose, we will use \emph{event structures}, providing an alternative formalism to the often-used tree-like games. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \subsection{The event structures framework} The traditional approach to concurrent games is to represent them as \emph{tree-like games}. If the considered game consists in three moves, namely $A$, $B$ and $C$, where $A$ can be played by Opponent and either one of the others by Player \emph{after} Opponent has played $A$, that means that the states of the game will be $\epsilon$, $A$, $A \cdot B$ and $A \cdot C$, which corresponds to the game tree \[ \begin{tikzpicture} \node (1) at (0.5,1.2) {A} ; \node (2) at (0,0) {B}; \node (3) at (1,0) {C}; \path [->] (1) edge (2) edge (3); \end{tikzpicture} \] This can of course be used to describe much larger games, and is often useful to reason concurrently, since the causal histories appears clearly: the possible states of the game can be read easily by concatenating the events found along a path from the root of the tree. But it also has the major drawback of growing exponentially in size: let us consider a game in which Opponent must play $A$ and $B$ in no particular order before Player can play $C$. The corresponding tree-like game would be \[ \begin{tikzpicture} \node (11) {$A_1$}; \node (21) [below of=11] {$B_1$}; \node (31) [below of=21] {$C_1$}; \node (22) [right of=11] {$B_2$}; \node (12) [below of=22] {$A_2$}; \node (32) [below of=12] {$C_2$}; \path [->] (11) edge (21) (21) edge (31) (22) edge (12) (12) edge (32); \end{tikzpicture} \] This goes even worse with less structure: since there is $n!$ % chktex 40 permutations for $n$ elements, the tree can grow way larger. This problem motivated the use of \emph{event structures} as a formalism to describe such games~\cite{rideau2011concurrent}. Informally, an event structure is a partial order $\leq$ on \emph{events} (here, the game's moves), alongside with a \emph{consistency} relation. The purpose of the consistency relation is to describe non-determinism, in which we are not interested here, since we seek a deterministic model: in all the following constructions, I will omit the consistency set. The original constructions including it can be found for instance in~\cite{castellan2016concurrent,winskel1986event}. The partial order $e_1 \leq e_2$ means that $e_1$ must have been played before $e_2$ can be played. For instance, the Hasse diagram of the previous game would look like \[ \begin{tikzpicture} \node (1) {A}; \node (2) [right of=1] {B}; \node (3) [below left of=1, below right of=2] {C}; \path[->] (1) edge (3) (2) edge (3); \end{tikzpicture} \] %%%%% \subsubsection{Event structures} \begin{definition}[event structure] An \emph{event structure}~\cite{winskel1986event} is a poset $(E, \leq_E)$, where $E$ is a set of \emph{events} and $\leq_E$ is a partial order on $E$ such that for all $e \in E$, $\downclose{e} \eqdef \set{e' \in E~\vert~e' \leq_E e}$ is finite. The partial order $\leq_E$ naturally induces a binary relation $\edgeArrow$ over $E$ that is defined as the transitive reduction of $\leq_E$. \end{definition} In this context, the right intuition of event structures is a set of events that can occur, the players' moves, alongside with a partial order stating that a given move cannot occur before another move. Event structures are often represented as a directed acyclic graph (DAG) where the vertices are the elements of $E$ and the edges are the transitive reduction of $\leq_E$. \begin{definition}[event structure with polarities] An \emph{event structure with polarities} (\textit{ESP}) is an event structure $(E, \leq_E, \rho)$, where $\rho : E \to \set{+,-}$ is a function associating a \emph{polarity} to each event. \end{definition} In order to model games, this is used to represent whether a move is to be played by Player or Opponent. To represent polarities, we will often use colors instead of $+$ and $-$ signs: a red-circled event will have a negative polarity, \ie{} will be played by Opponent, while a green-circled one will have a positive polarity. The ESP of the previous example would then be \[ \begin{tikzpicture} \node (1) at (0,1.6) [draw=red, ellipse] {A}; \node (2) at (1,1.6) [draw=red, ellipse] {B}; \node (3) at (0.6,0) [draw=green, ellipse] {C}; \path[->] (1) edge (3) (2) edge (3); \end{tikzpicture} \] \begin{definition}[configuration] A \emph{configuration} of an ESP $A$ is a finite subset $X \subseteq A$ that is \emph{down-closed}, \ie{} \vspace{-0.5em} \[ {\forall x \in X}, {\forall e \in A}, {e \leq_A x} \implies {e \in X}.\] We write $\config(A)$ the set of configurations of $A$. \end{definition} A configuration can thus be seen as a valid state of the game. The set $\config(A)$ plays a major role in definitions and proofs on games and strategies. \begin{notation} For $x,y \in \config(A)$, $x \forkover{e} y$ states that $y = x \sqcup \set{e}$ (and that both are valid configurations), where $\sqcup$ denotes the disjoint union. It is also possible to write $x \forkover{e}$, stating that $x \sqcup \set{e} \in \config(A)$, or $x \fork y$. \end{notation} %%%%% \subsubsection{Concurrent games} \begin{definition}[game] A \emph{game} $A$ is an event structure with polarities. \\ The dual game $A^\perp$ is the game $A$ where all the polarities in $\rho$ have been reversed. \end{definition} For instance, one could imagine a game modeling the user interface of a coffee machine: Player is the coffee machine, while Opponent is a user coming to buy a drink. \begin{example}[coffee machine] A game describing a coffee machine could be the following one: \[ \begin{tikzpicture} \node (1) at (2,1.5) [draw=red, ellipse] {coin}; \node (2) at (-1,1.5) [draw=red, ellipse] {getCoffee}; \node (3) at (5,1.5) [draw=red, ellipse] {getTea}; \node (4) at (0,0) [draw=green, ellipse] {giveCoffee}; \node (5) at (4,0) [draw=green, ellipse] {giveTea}; \end{tikzpicture} \] Note that there are no edges at all. Indeed, we are here describing the \emph{game}, that is, giving a structure on which we can model any software that would run on the hardware of the coffee machine. Nothing is hardwired that would make it mandatory to insert a coin before getting a coffee: the \emph{software} decides that, it is thus up to the \emph{strategy} --- of which we will talk later on --- to impose such constraints. \end{example} \begin{example}[process game] We can represent a process by the following game: \[ \begin{tikzpicture} \node (1) at (0,0) [draw=red,ellipse] {call}; \node (2) at (2,0) [draw=green,ellipse] {done}; \path[->] (1) edge (2); \end{tikzpicture} \] The ``call'' event will be triggered by Opponent (the system) when the process is started, and Player will play ``done'' when the process has finished, if it ever does. The relation $\text{call} \leq \text{done}$ means that a process cannot finish \emph{before} it is called: unlike what happened in the previous example, it is here a ``hardwired'' relation that the software cannot bypass. \end{example} \begin{definition}[pre-strategy] A \emph{pre-strategy} on the game $A$, written $\sigma: A$, is an ESP such that \begin{enumerate}[(i)] \item $\sigma \subseteq A$; \item $\config(\sigma) \subseteq \config(A)$; \item $\forall s \in \sigma, \rho_A(s) = \rho_\sigma(s)$ \end{enumerate} \end{definition} In particular, (ii) imposes that $\leq_A$ restrained to $\sigma$ is included in $\leq_\sigma$. \begin{example}[processes, cont.] A possible \emph{pre-strategy} for the game consisting in two processes put side by side (in which the game's events are annotated with a number to distinguish the elements of the two processes) would be \[ \begin{tikzpicture} \node (1) at (0,1.2) [draw=red,ellipse] {call$_0$}; \node (2) at (0,0) [draw=green,ellipse] {done$_0$}; \node (3) at (2,1.2) [draw=red,ellipse] {call$_1$}; \path[->] (1) edge (2) (3) edge (2); \end{tikzpicture} \] This pre-strategy is valid: it is a subset of the game that does not include $\text{call}_1$, but it does include both $\text{call}_0$ and $\text{done}_0$ and inherits the game's partial order. This would describe two processes working in parallel. The process $0$ waits before the process $1$ is called to terminate, and the process $1$ never returns. Assuming that \lstc{called} is an initially false boolean shared between the two processes, this could for instance be written \begin{minipage}[T]{0.45\textwidth} \begin{center}\textit{Process 0}\end{center} \begin{lstlisting}[language=C++] int main() { while(!called) {} return 0; }\end{lstlisting} \end{minipage} \begin{minipage}[T]{0.45\textwidth} \begin{center}\textit{Process 1}\end{center} \begin{lstlisting}[language=C++] int main() { called=true; while(true) {} // never returns. }\end{lstlisting} \end{minipage} \end{example} But as it is defined, a pre-strategy does not exactly capture what we expect of a \emph{strategy}: it is too expressive. For instance, the relation $\text{call}_0 \leq \text{call}_1$ on the above strategy is allowed, stating that the operating system cannot decide to start the process $1$ before the process $0$. It is not up to the program to decide that, this strategy is thus unrealistic. We then have to restrict pre-strategies to \emph{strategies}: \begin{definition}[strategy] A \emph{strategy} is a pre-strategy $\sigma : A$ that ``behaves well'', \ie{} that is \begin{enumerate}[(i)] \item\label{def:receptive} \textit{receptive}: for all $x \in \config(A)$ \st{} $x \forkover{e^-}$, $e \in \sigma$; \item\label{def:courteous} \textit{courteous}: $\forall x \edgeArrow_\sigma x' \in \sigma$, $(\rho(x),\rho(x')) \neq (-,+) \implies x \edgeArrow_A x'$. \end{enumerate} \end{definition} (\ref{def:receptive}) captures the idea that we cannot prevent Opponent from playing one of its moves. Indeed, not including an event in a strategy means that this event \emph{will not} be played. It is unreasonable to consider that a strategy could forbid Opponent to play a given move, unless the game itself forbids that as well. (\ref{def:courteous}) states that unless a dependency relation is imposed by the games' rules, one can only make one of its moves depend on an Opponent move, \ie{} every direct arrow in the partial order that is not inherited from the game should be ${\ominus \edgeArrow \oplus}$. Clearly, it is unreasonable to consider an arrow ${\ostar \edgeArrow \ominus}$, which would mean forcing Opponent to wait for a move (either from Player or Opponent) before playing their move; but ${\oplus \edgeArrow \oplus}$ is also unreasonable, since we're working in a concurrent context. Intuitively, one could think that when playing $x$ then $y$, it is undefined whether Opponent will receive $x$ then $y$ or $y$ then $x$. %%%%% \subsubsection{Operations on games and strategies}\label{sssec:es_operations} In order to manipulate strategies and define them by induction over the syntax, the following operations will be extensively used. It may also be worth noting that in the original formalism~\cite{castellan2016concurrent}, games, strategies and maps between them form a bicategory in which these operations play special roles. In this whole section, unless stated otherwise, $E$ and $F$ denotes ESPs; $A$, $B$ and $C$ denotes games; $\sigma: A$ and $\tau: B$ denotes strategies. \begin{definition}[parallel composition] The \emph{parallel composition} $E \parallel F$ of two ESPs is an ESP whose events are $\left(\set{0} \times E\right) \sqcup \left(\set{1} \times F\right)$ (the disjoint tagged union of the events of $E$ and $F$), and whose partial order is $\leq_E$ on $E$ and $\leq_F$ on $F$, with no relation between elements of $E$ and $F$. One can then naturally expand this definition to games (by preserving polarities) and to strategies. \end{definition} In the example before, when talking of ``two processes side by side'', we actually referred formally to the parallel composition of two processes, in which we took the liberty of renaming the events for more clarity (which we will often do). \smallskip Given two strategies on dual games $A$ and $A^\perp$, it is natural and interesting to compute their \emph{interaction}, that is, ``what will happen if one strategy plays against the other''. \begin{definition}[closed interaction] Given two strategies $\sigma : A$ and $\tau : A^\perp$, their \emph{interaction} $\sigma \wedge \tau$ is the ESP $\sigma \cap \tau \subseteq A$ from which causal loops have been removed. More precisely, $\sigma \cap \tau$ is a set adjoined with a \emph{preorder} ${(\leq_\sigma \cup \leq_\tau)}^\ast$ (transitive closure) that may not respect antisymmetry, that is, may have causal loops. The event structure $\sigma \wedge \tau$ is then obtained by removing all the elements contained in such loops from $\sigma \cap \tau$, yielding a regular order. \end{definition} \textit{This construction is a simplified version of the analogous one from~\cite{castellan2016concurrent} (the pullback), taking advantage of the fact that our event structures are deterministic --- that is, without a consistency set.} This indeed captures what we wanted: $\sigma \wedge \tau$ contains the moves that both $\sigma$ and $\tau$ are ready to play, including both orders, except for the events that can never be played because of a ``deadlock'' (\ie{} a causal loop). \smallskip We might now try to generalize that to an \emph{open} case, where both strategies don't play on the same games, but only have a common part. Our goal here is to \emph{compose} strategies: indeed, a strategy on $A^\perp \parallel B$ can be seen as a strategy \emph{from $A$ to $B$}, playing as Opponent on a board $A$ and as Player on a board $B$. This somehow looks like a function, that could be composed with another strategy on $B^\perp \parallel C$ (as one would compose two mathematical functions $f$ and $g$ into $g \circ f$). \begin{definition}[compositional interaction] Given two strategies $\sigma : A^\perp \parallel B$ and $\tau : B^\perp \parallel C$, their \emph{compositional interaction} $\tau \strInteract \sigma$ is an event structure defined as $(\sigma \parallel C) \wedge (A^\perp \parallel \tau)$, where $A^\perp$ and $C$ are seen as strategies. \end{definition} The idea is to put in correspondence the ``middle'' states (those of $B$) while adding ``neutral'' states for $A$ and $C$, which gives us two strategies playing on the same game (if we ignore polarities), $A \parallel B \parallel C$. Here, we define $\tau \strInteract \sigma$ as an \emph{event structure} (\ie, without polarities): indeed, the two strategies disagree on the polarities of the middle part. Alternatively, it can be seen as an ESP with a polarity function over $\set{+,-,?}$. From this point, the notion of composition we sought is only a matter of ``hiding'' the middle part: \begin{definition}[strategies composition] Given two strategies $\sigma : A^\perp \parallel B$ and $\tau : B^\perp \parallel C$, their \emph{composition} $\tau \strComp \sigma$ is the ESP $(\tau \strInteract \sigma) \cap (A^\perp \parallel C)$, on which the partial order is the restriction of $\leq_{\tau \strInteract \sigma}$ and the polarities those of $\sigma$ and $\tau$. \end{definition} It is then useful to consider an identity strategy \wrt{} the composition operator. This identity is called the \emph{copycat} strategy: on a game $A$, the copycat strategy playing on $A^\perp \parallel A$ replicates the moves the other player from each board on the other. \begin{definition}[copycat] The \emph{copycat strategy} of a game $A$, $\cc_A$, is the strategy on the game $A^\perp \parallel A$ whose events are $A^\perp \parallel A$ wholly, on which the order is the transitive closure of $\leq_{A^\perp \parallel A} \cup \set{ (1-i, e) \leq (i, e) \vert e \in A~\&~\rho((i,e)) = \oplus}$. \end{definition} The copycat strategy of a game is indeed an identity for the composition of \emph{strategies}. In fact, it even holds that for a \emph{pre-}strategy $\sigma : A$, $\sigma$ is a strategy $\iff$ $\cc_A \strComp \sigma = \sigma$. \begin{example}[copycat] If we consider the following game $A$ \[ \begin{tikzpicture} \node (1) [draw=red,ellipse] {A}; \node (3) [draw=green,ellipse,right of=1] {C}; \node (2) [draw=red,ellipse,right of=3] {B}; \path[->] (3) edge (1); \end{tikzpicture} \] its copycat strategy $\cc_A$ is \[ \begin{tikzpicture} \node (01) {($A^\perp$)}; \node (02) [below of=01] {($A$)}; \node (11) [draw=green,ellipse,right of=01] {A}; \node (31) [draw=red,ellipse,right of=11] {C}; \node (21) [draw=green,ellipse,right of=31] {B}; \node (12) [draw=red,ellipse,right of=02] {A}; \node (32) [draw=green,ellipse,right of=12] {C}; \node (22) [draw=red,ellipse,right of=32] {B}; \path[->] (12) edge (11) (22) edge (21) (31) edge (32) % (31) edge (11) (32) edge (12); \end{tikzpicture} \] Note that the edge $C \rightarrow A$ in the upper row is no longer needed, since it can be obtained transitively and we only represent the transitive reduction of the partial order. \end{example} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \subsection{Interpretation of \llccs}\label{ssec:llccs_interp} We can now equip \llccs{} with denotational semantics, interpreting the language as strategies as defined in figure~\ref{fig:llccs:interp}. \begin{figure}[h] \begin{align*} \seman{x^A} &\eqdef \cc_{\seman{A}} & \seman{A \linarrow B} &\eqdef \seman{A}^\perp \parallel \seman{B} \\ \seman{t^{A \linarrow B}~u^{A}} &\eqdef \cc_{A \linarrow B} \strComp \left( \seman{t} \parallel \seman{u} \right) \\ \seman{\lambda x^A \cdot t} &\eqdef \seman{t} \\ \seman{P \parallel Q} &\eqdef \left( \begin{tikzpicture}[baseline, scale=0.8] \node (4) at (0,0.65) [draw=green,ellipse] {call $P$}; \node (5) at (0,-0.65) [draw=red,ellipse] {done $P$}; \node (2) at (2.5,0.65) [draw=green,ellipse] {call $Q$}; \node (3) at (2.5,-0.65) [draw=red,ellipse] {done $Q$}; \node (0) at (5,0.65) [draw=red,ellipse] {call}; \node (1) at (5,-0.65) [draw=green,ellipse] {done}; \path[->] (0) edge (1) edge [bend right] (2) edge [bend right] (4) (2) edge (3) (4) edge (5) (3) edge [bend right] (1) (5) edge [bend right] (1); \end{tikzpicture} \right) \strComp \left(\seman{P} \parallel \seman{Q}\right) & \seman{\proc} = \seman{\chan} &\eqdef \begin{tikzpicture}[baseline] \node (1) at (0,0.5) [draw=red,ellipse] {call}; \node (2) at (0,-0.5) [draw=green,ellipse] {done}; \draw [->] (1) -- (2); \end{tikzpicture} \\ %%%%%%%%%%%%%%%%%%%%%%%%% \seman{P \cdot Q} &\eqdef \left( \begin{tikzpicture}[baseline,scale=0.8] \node (4) at (0,0.65) [draw=green,ellipse] {call $P$}; \node (5) at (0,-0.65) [draw=red,ellipse] {done $P$}; \node (2) at (2.5,0.65) [draw=green,ellipse] {call $Q$}; \node (3) at (2.5,-0.65) [draw=red,ellipse] {done $Q$}; \node (0) at (5,0.65) [draw=red,ellipse] {call}; \node (1) at (5,-0.65) [draw=green,ellipse] {done}; \path[->] (0) edge (1) edge [bend right] (4) (2) edge (3) (4) edge (5) (3) edge [bend right] (1) (5) edge (2); \end{tikzpicture} \right) \strComp \left(\seman{P} \parallel \seman{Q}\right) & \seman{1} &\eqdef \begin{tikzpicture}[baseline] \node (1) at (0,0.5) [draw=red,ellipse] {call}; \node (2) at (0,-0.5) [draw=green,ellipse] {done}; \draw [->] (1) -- (2); \end{tikzpicture} \\ %%%%%%%%%%%%%%%%%%%%%%%%% \seman{(a : \chan) \cdot P} &\eqdef \left( \begin{tikzpicture}[baseline,scale=0.8] \node (4) at (0,0.65) [draw=green,ellipse] {call $P$}; \node (5) at (0,-0.65) [draw=red,ellipse] {done $P$}; \node (2) at (2.5,0.65) [draw=green,ellipse] {call $a$}; \node (3) at (2.5,-0.65) [draw=red,ellipse] {done $a$}; \node (0) at (5,0.65) [draw=red,ellipse] {call}; \node (1) at (5,-0.65) [draw=green,ellipse] {done}; \path[->] (0) edge (1) edge [bend right] (2) (2) edge (3) (4) edge (5) (3) edge (4) (5) edge [bend right] (1); \end{tikzpicture} \right) \strComp \left(\seman{P} \parallel \seman{a}\right) & \seman{0} &\eqdef \begin{tikzpicture}[baseline] \node (1) at (0,0.2) [draw=red,ellipse] {call}; \end{tikzpicture} \\ %%%%%%%%%%%%%%%%%%%%%%%%% \seman{(\nu a) P} &\eqdef \left( \begin{tikzpicture}[baseline,scale=0.8] \node (6) at (0,0.65) [draw=green,ellipse] {call $a$}; \node (7) at (0,-0.65) [draw=red,ellipse] {done $a$}; \node (4) at (2.5,0.65) [draw=green,ellipse] {call $\bar{a}$}; \node (5) at (2.5,-0.65) [draw=red,ellipse] {done $\bar{a}$}; \node (2) at (5,0.65) [draw=green,ellipse] {call $P$}; \node (3) at (5,-0.65) [draw=red,ellipse] {done $P$}; \node (0) at (7.5,0.65) [draw=red,ellipse] {call}; \node (1) at (7.5,-0.65) [draw=green,ellipse] {done}; \path[->] (0) edge (1) edge [bend right] (2) (2) edge (3) (3) edge [bend right] (1) (4) edge (5) edge (7) (6) edge (7) edge (5); \end{tikzpicture} \right) \strComp \seman{P} & \end{align*} \caption{\llccs{} interpretation as strategies}\label{fig:llccs:interp} \end{figure} A lot of these interpretations is what was expected: $\proc$ and $\chan$ have the same interpretation as presented before, $1$ is interpreted as the game playing \textit{done} while $0$ does not, the arrow is the type introduced for functions. A variable is represented by a \emph{copycat} of its type, to keep a version of the variable in the environment, reflecting the judgement $x:A \vdash x:A$. Same goes for the abstraction: the typing rule states that given a term verifying $\Gamma, x:A \vdash t:B$, we should obtain a term verifying $\Gamma \vdash \lambda x^A \cdot t : A \linarrow B$. The only thing we have to do is to ``move'' $x$ from the environment to the term, which is transcribed by the associativity of $\parallel$. In the application, one can notice that the copycat wires up perfectly $\seman{t} \parallel \seman{u}$: the version of $x$ from the environment of $t$ is connected to $u$, and the output of $t$ is connected to the output of the term. In the representation above, the drawn strategies are organized in columns: for instance, the strategy involved in $\seman{P \parallel Q}$ has type $P^\perp \parallel P^\perp \parallel P$. Each column of events stands for one of those games, in this order. %%%%%%%%%%%%%%%%%%%%% \subsection{Adequacy} We will now prove the major result of this study, the \emph{adequacy} of the game semantics. \begin{theorem}[adequacy] The previous interpretation is \emph{adequate} with the operational semantics, that is \[ \forall P \textit{ st. } \left(\vdash P : \proc\right),~ \left(P \Downarrow\right) \iff \left(\seman{P} = \seman{1}\right) \] \end{theorem} In order to prove the theorem, a few intermediary definitions and results are required. \begin{definition}[evaluation in a context] For $l$ a list of channels and $P$ a term, the evaluation of $P$ in the context $l$, $\seman{P}_l$, is defined by induction by $\seman{P}_{[]} \eqdef \seman{P}$ and $\seman{P}_{h::t} \eqdef \seman{(\nu h)P}_t$. \end{definition} \begin{definition}[valid contexts] The \emph{valid contexts} for a reduction $P \redarrow{x} Q$, $\validctx_{P \redarrow{x} Q}$, is the set of (ordered) lists of channels $l$ such that \begin{enumerate}[(i)] \item $\forall a:\chan \in \freevars(P)~\st~\bar{a} \in \freevars(P),~ a \in l \text{ or } \bar{a} \in l$; \item if $x = a : \chan$, $a \not\in l$; \item $\forall a : \chan,~a \in l \implies \bar{a} \not\in l$. \end{enumerate} \end{definition} \begin{lemma} For all $a: \chan$, $P, Q, R : \proc$, the following properties hold: \begin{enumerate}[(i)] \item $\newch{a} (P \parallel Q) = \left(\newch{a} P\right) \parallel Q$ when $a,\bar{a} \not\in \freevars{Q}$; \item $\newch{a} (P \parallel Q) = P \parallel \left(\newch{a} Q\right)$ when $a,\bar{a} \not\in \freevars{P}$; \item $\newch{a} \left(P\cdot Q\right) = \left(\newch{a} P\right) \cdot Q$ when $a,\bar{a} \not\in \freevars{Q}$; \item $\seman{\parallel}_l$ is associative, that is, for all $l$, $\seman{(A \parallel B) \parallel C}_l = \seman{A \parallel (B \parallel C)}_l$. \end{enumerate} \end{lemma} The previous lemma's proof mostly consists in technical, formal reasoning on event structures, but it is essentially intuitive. The theorem is mostly a consequence of the following lemma: \begin{lemma} $\forall P \redarrow{x} Q,~\forall l \in \validctx_{P \redarrow{x} Q}$, \begin{enumerate}[(i)] \item if $x = \tau$, then $\seman{P}_l = \seman{Q}_l$; \item if $x = a: \chan$, then $\seman{P}_l = \seman{a \cdot Q}_l$; \item if $x = \tau_a$ ($a : \chan$), then $\seman{P}_{a::l} = \seman{Q}_l$. \end{enumerate} \end{lemma} \begin{proof} We prove this by induction over the rules of the operational semantics of \llccs. Most of the cases are straightforward, thus, we will only sketch the proof for a few of those cases. \begin{itemize} \item The basic rules (for $\parallel$, $\cdot$, \ldots) are working thanks to the previous lemma. \item $\dfrac{P \redarrow{a} P'\quad Q \redarrow{\bar{a}} Q'} {P \parallel Q \redarrow{\tau_a} P' \parallel Q'}$: for all $l$, by (ii), $\seman{P}_l = \seman{a \cdot P'}_l$ and $\seman{Q} = \seman{\bar{a} \cdot Q'}$, thus $\seman{(\nu a)(P \parallel Q)}_l = \seman{\newch{a}(a \cdot P' \parallel \bar{a} \cdot Q')}$ (inline replacement of terms, permitted by the previous lemma), thus $\seman{\newch{a} (P \parallel Q)}_l = \seman{P' \parallel Q'}_l$. \item $\dfrac{P \redarrow{\tau_c} Q}{\newch{a} P \redarrow{\tau} Q} (c \in \set{a,\bar{a}})$ clearly works thanks to (iii). \end{itemize} \end{proof} \begin{proof}[Proof: theorem] \emph{Forwards implication}: $\left(P \Downarrow\right) \implies \left(\seman{P} = \seman{1}\right)$. Proof by induction over the derivation of $P \redarrow{\tau}^\ast 1$, by iterating the previous lemma. \emph{Backwards implication}: $\left(\seman{P} = \seman{1}\right) \implies \left(P \Downarrow\right)$. We prove its contrapositive judgement, $P \neq 1\,\&\,\seman{P} = \seman{1} \implies \exists Q\,:\,P \redarrow{\tau} Q$ by induction over the syntax of \linccs{} (\wlogen, we can assume that $P \not\longrightarrow_\beta$, thus the terms are in \linccs): for each syntactic construction, we prove that under the induction hypotheses, there is such a $Q$. \end{proof} This proves the adequacy of our semantics, giving some credit to the game semantics we provided: indeed, in order to decide whether a term converges, we can compute its associated strategy and check whether it is $\seman{1}$. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \section{Implementation of deterministic concurrent games} \hfill\href{https://tobast.fr/l3/demo.html} {\includegraphics[height=2em]{tryme32.png}~\raisebox{0.5em}{Try online}} \qquad \href{https://github.com/tobast/cam-strategies/} {\includegraphics[height=2em]{github32.png}~\raisebox{0.5em}{Github repository}} \vspace{1em} One of the goals of my internship was also to implement the operations on games and strategies described in §\ref{sssec:es_operations}, and to use them to provide a convenient Dot representation of the operational semantics of \llccs{} described in §\ref{ssec:llccs_interp}. \subsection{Structures} The implementation aims to stay as close as possible to the mathematical model, while still providing quite efficient operations. As we do not handle non-determinism, an event structure can be easily represented as a DAG in memory. The actual representation that was chosen is a set of nodes, each containing (as well as a few other information) a list of incoming and outgoing edges. \subsection{Generic operations} The software --- apart from a few convenience functions used to input and output games and strategies, as well as the \llccs{} handling --- mostly consists in graph handling functions (mostly used internally) and the implementation of the operations on games and strategies previously described. This allows to compute the result of any operation on a deterministic strategy, and is modular enough to make it possible to implement non-determinism on the top of it later on (even without having to understand the whole codebase). Those operations can be used directly from the OCaml toplevel, conveniently initialized with the correct modules loaded with \lstbash{make toplevel}; but it is mostly intended to be a backend for higher level interfaces, such as the \llccs{} interface. \subsection{Modelling \llccs} The modelling of \llccs{} required to implement a lexer/parser for the language and a function transforming \llccs{} terms into strategies, as well as a rendering backend, displaying a strategy as a Dot graph. This could then just be plugged into an HTML/Javascript frontend using \texttt{js\_of\_ocaml}; this frontend is linked above in the document. The major difficulty came from the necessity to massively reorder the sub-terms of the strategies on the go: indeed, in order to know how to compose two strategies $\sigma$ and $\tau$, the implementation keeps track of the parallel compositions that were taken to get both strategies. For instance, if $\sigma$ was obtained by putting in parallel strategies so that the game is $(A \parallel B^\perp) \parallel C^\perp$, and $\tau$ was obtained the same way, reaching a game $(B \parallel C) \parallel D$, the implementation would refuse to compute $\tau \strComp \sigma$, because it would try to match games $C^\perp$ and $(B \parallel C)$. The theoretical construction extensively uses the associativity (up to isomorphism) of $\parallel$, but in the code, each use of the associativity must be explicit, leading to a large amount of code. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \section{Conclusion} During this internship, I have established deterministic game semantics for a simple concurrent language. Although the language is fairly simple, it should not be too hard to lift it to a language closer to real-world programming languages, through the inclusion of the imperative primitives found in the literature. \medskip I also explored the possibility to reach a full-abstraction result. The full-abstraction property states that two terms are \emph{observationally equivalent} if and only if their (denotational) semantics are equal, that is, in this context, for all $P,Q$ two \llccs{} terms such that $\Gamma \vdash P,Q : A$, \[ \left[ \forall \calC[-] \text{ a context }\,:\, \left( \vdash \calC[P] : \proc \right),~ \calC[P] \Downarrow \iff \calC[Q] \Downarrow \right] \quad\iff\quad \left( \seman{P} = \seman{Q} \right) \] Yet, by lack of time, I had to abandon this path. Indeed, this would have required either to modify \llccs{} or to restrict the authorized strategies, because of the following legal strategy, which cannot be expressed as the semantics of a term in \llccs{}: \[ \begin{tikzpicture} \node (0P) at (2,2) {$\proc$}; \node (0C) at (0,2) {$\chan$}; \node (1) at (0,1) [draw=red, ellipse] {call}; \node (2) at (0,0) [draw=green, ellipse] {done}; \node (3) at (2,1) [draw=red, ellipse] {call}; \node (4) at (2,0) [draw=green, ellipse] {done}; \path[->] (1) edge (2) (3) edge (4) edge (1); \end{tikzpicture} \] This strategy behaves like a ``forget'' strategy: its effect is to call one end of a channel, and then to resume the execution of the term without waiting for the other end to be called. If we integrate this operator to the language as $(f\,a)$ for any channel $a$, this construction can discriminate terms that would not have been discriminated before. For instance $\lambda x^{\chan \linarrow \proc} \cdot \newch{a} ((x a) \cdot \bar{a} \cdot 1)$ and $\lambda x^{\chan \linarrow \proc} \cdot \newch{a} ((x a) \cdot \bar{a} \cdot 0)$ can be discriminated by the context $\calC[X] = X (\lambda a^\chan \cdot (f a))$. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \bibliography{biblio} \bibliographystyle{alpha} \end{document}