From 4ffb48b42f15c50a03656065b7d4bebb2372e26d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9ophile=20Bastian?= Date: Tue, 30 Aug 2016 16:49:49 +0200 Subject: [PATCH] Final version of the report --- report/README.md => README.md | 0 report/biblio.bib | 4 +- report/report.tex | 191 +++++++++++++++++++--------------- 3 files changed, 111 insertions(+), 84 deletions(-) rename report/README.md => README.md (100%) diff --git a/report/README.md b/README.md similarity index 100% rename from report/README.md rename to README.md diff --git a/report/biblio.bib b/report/biblio.bib index 1a39f45..6707bad 100644 --- a/report/biblio.bib +++ b/report/biblio.bib @@ -34,7 +34,7 @@ } @article{abramsky2000pcf, - title={Full abstraction for PCF}, + title={{Full abstraction for PCF}}, author={Abramsky, Samson and Jagadeesan, Radha and Malacaria, Pasquale}, journal={Information and Computation}, volume={163}, @@ -82,7 +82,7 @@ } @article{laird2001game, - title={A game semantics of Idealized CSP}, + title={{A game semantics of Idealized CSP}}, author={Laird, James}, journal={Electronic Notes in Theoretical Computer Science}, volume={45}, diff --git a/report/report.tex b/report/report.tex index 41dbbbc..31dd517 100644 --- a/report/report.tex +++ b/report/report.tex @@ -83,14 +83,13 @@ 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 +focus at some point on modelling concurrency. The problem was first 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. +communication on channels. \fname{Ghica} and \fname{Murawski} then simplified +\textsc{Laird}'s approach, and gave a fully abstract model for a slightly more +realistic concurrent programming language with shared memory +in~\cite{ghica2004angelic}. 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 @@ -105,15 +104,15 @@ 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. +non-deterministic uniform choice. Yet, even for concurrent programs it is +often a desirable property that they should behave consistently with the +environment, meaning that they are deterministic up to the choice of the +scheduler. Such determinism can be ensured statically, via typing. 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 @@ -142,7 +141,7 @@ 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. +determinism requirements through the banning of interference. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \subsection{A linear variant of CCS~: \linccs} @@ -231,7 +230,7 @@ where $a$ denotes a channel and $x$ denotes any possible label. \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}) + {(\nu a)P \redarrow{x} (\nu a)P'} & (x \not\in \set{a,\tau_a}) \end{align*} \caption{\linccs{} operational semantics}\label{fig:lccs:opsem} \end{figure} @@ -245,11 +244,7 @@ necessary. Consider the reduction of $(\nu a) (a \cdot 1 \parallel \bar{a} 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. +subject reduction for $\tau$-reductions. \subsection{Lifting to the higher order: linear \lcalc} @@ -257,7 +252,7 @@ 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$. +the typing rules). \begin{figure}[h] \begin{minipage}[t]{0.55\textwidth} @@ -338,15 +333,17 @@ To lift the operational semantics to \llccs, we only need to add one rule: \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. + channels are dual or not, that is, its declaration ignores duality + relations between its parameters. In practice, it means that no + synchronization can happen before the term is $\beta$-reduced. \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. +Our goal is now to give a deterministic 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} @@ -371,9 +368,9 @@ corresponds to the game tree \] 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. +to reason concurrently. The different configurations of the game that can be +reached are quite easily read: one only has to concatenate the events found +along path starting at 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 @@ -395,10 +392,14 @@ before Player can play $C$. The corresponding tree-like game would be \end{tikzpicture} \] -This goes even worse with less structure: since there is $n!$ % chktex 40 +This goes even worse with less structure: since there are $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 +The previous example also points out a kind of \textit{obfuscation} of the +causal histories: reading the diagram above does not make it obvious to the +reader that $A$ and $B$ must be played before $C$. + +This problem can be solved by using \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. @@ -433,7 +434,9 @@ look like \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$. + over $E$ that is defined as the transitive reduction of $\leq_E$, \ie{} the + minimal subset of $\leq_E$ such that the transitive closures of $\leq_E$ + and $\edgeArrow$ are the same. \end{definition} In this context, the right intuition of event structures is a set of events @@ -442,7 +445,7 @@ 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$. +reduction of $\leq_E$ (\ie{} $\edgeArrow_E$). \begin{definition}[event structure with polarities] An \emph{event structure with polarities} (\textit{ESP}) is an event @@ -485,8 +488,9 @@ 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$. + is used to mean that the standard union ($\cup$) is disjoint. It is also + possible to write $x \forkover{e}$, stating that $x \sqcup \set{e} \in + \config(A)$, or $x \fork y$. \end{notation} %%%%% @@ -534,7 +538,7 @@ drink. \] 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}$ + finished, if it ever does. The relation $\texttt{call} \leq \texttt{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. @@ -544,7 +548,8 @@ drink. A \emph{pre-strategy} on the game $A$, written $\sigma: A$, is an ESP such that \begin{enumerate}[(i)] - \item $\sigma \subseteq A$; + \item $\sigma \subseteq A$ (inclusion over set of events, not including + the order); \item $\config(\sigma) \subseteq \config(A)$; \item $\forall s \in \sigma, \rho_A(s) = \rho_\sigma(s)$ \end{enumerate} @@ -600,23 +605,26 @@ int main() { 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}: +$\text{call}_0 \leq \text{call}_1$ on a variant of the above strategy would be +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$; + \textit{receptive}: $\forall x \in \config(\sigma), x \sqcup + \set{e} \in \config(A) \land \rho(e) = \ominus \implies x \sqcup + \set{e} \in \config(\sigma)$ + \item\label{def:courteous} - \textit{courteous}: $\forall x \edgeArrow_\sigma x' \in \sigma$, - $(\rho(x),\rho(x')) \neq (-,+) \implies - x \edgeArrow_A x'$. + \textit{courteous}: $\forall e \edgeArrow_\sigma e' \in \sigma$, + $(\rho(e),\rho(e')) \neq (-,+) \implies + e \edgeArrow_A e'$. \end{enumerate} \end{definition} @@ -634,8 +642,8 @@ 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$. +$e$ then $e'$, it is undefined whether Opponent will receive $e$ then $e'$ or +$e'$ then $e$. %%%%% \subsubsection{Operations on games and strategies}\label{sssec:es_operations} @@ -680,7 +688,7 @@ one strategy plays against the other''. ${(\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. + contained in such loops from $\sigma \cap \tau$, yielding a partial order. \end{definition} \textit{This construction is a simplified version of the analogous one @@ -707,8 +715,8 @@ 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. + \sigma$ is an event structure defined as $(\sigma \parallel C^\perp) \wedge + (A \parallel \tau)$, where $A$ and $C^\perp$ are seen as strategies. \end{definition} The idea is to put in correspondence the ``middle'' states (those of $B$) while @@ -746,7 +754,8 @@ the other player from each board on the other. 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$. +$\sigma : A$, $\sigma$ is a strategy $\iff$ $\cc_A \strComp \sigma = +\sigma$~\cite{rideau2011concurrent}. \begin{example}[copycat] If we consider the following game $A$ @@ -808,8 +817,7 @@ language as strategies as defined in figure~\ref{fig:llccs:interp}. \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) + (0) edge [bend right] (2) edge [bend right] (4) (2) edge (3) (4) edge (5) @@ -832,8 +840,7 @@ language as strategies as defined in figure~\ref{fig:llccs:interp}. \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) + (0) edge [bend right] (4) (2) edge (3) (4) edge (5) (3) edge [bend right] (1) @@ -855,8 +862,7 @@ language as strategies as defined in figure~\ref{fig:llccs:interp}. \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) + (0) edge [bend right] (2) (2) edge (3) (4) edge (5) (3) edge (4) @@ -878,8 +884,7 @@ language as strategies as defined in figure~\ref{fig:llccs:interp}. \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) + (0) edge [bend right] (2) (2) edge (3) (3) edge [bend right] (1) (4) edge (5) @@ -892,10 +897,21 @@ language as strategies as defined in figure~\ref{fig:llccs:interp}. \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. +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. + +The $\seman{-}$ operator always sends a term $x_1 : A_1, \ldots, x_p : A_p +\vdash t : B$ to a strategy $\seman{t} : \seman{A_1}^\perp \parallel \ldots +\parallel \seman{A_p}^\perp \parallel \seman{B}$. For brevity purposes, the +associativity and commutativity steps ---~up to isomorphism~--- will be kept +implicit here, although those are handled very formally in the implementation. + +A lot of these interpretations is what was expected: $\proc$ has the same +interpretation as presented before, and that of $\chan$ is set to the same, $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$. @@ -908,21 +924,15 @@ 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. +We will now describe the main steps of the proof of 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 + The previous interpretation is \emph{adequate} with respect to 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} @@ -946,6 +956,10 @@ required. \item $\forall a : \chan,~a \in l \implies \bar{a} \not\in l$. \end{enumerate} + where $\freevars(P)$ denotes the set of free variables of $P$, defined as + usual by induction over the syntax as the set of variables unbound in the + term. + \end{definition} \begin{lemma} @@ -1010,7 +1024,10 @@ The theorem is mostly a consequence of the following lemma: 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 + \not\longrightarrow_\beta$, because we can always do every + $\beta$-reduction before any other $\tau$-reduction, and because the + $\beta$-reduced term corresponding to a counter-example is a + counter-example as well; thus the terms are in \linccs): for each syntactic construction, we prove that under the induction hypotheses, there is such a $Q$. \end{proof} @@ -1023,10 +1040,13 @@ 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}} + {\includegraphics[height=2em]{tryme32.png}~\raisebox{0.5em}{Try + online\footnotemark}} + \footnotetext{\url{{https://tobast.fr/l3/demo.html}}} \qquad \href{https://github.com/tobast/cam-strategies/} {\includegraphics[height=2em]{github32.png}~\raisebox{0.5em}{Github - repository}} + repository\footnotemark}} + \footnotetext{\url{https://github.com/tobast/cam-strategies/}} \vspace{1em} @@ -1095,9 +1115,9 @@ literature. 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$, +equivalent} if and only if their (denotational) semantics are also +observationally equivalent, 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 }\,:\, @@ -1105,7 +1125,14 @@ for all $P,Q$ two \llccs{} terms such that $\Gamma \vdash P,Q : A$, \calC[P] \Downarrow \iff \calC[Q] \Downarrow \right] \quad\iff\quad - \left( \seman{P} = \seman{Q} \right) + \left( \seman{P} \simeq \seman{Q} \right) +\] + +where $\simeq$ denotes the observational equivalence on strategies, that is, + +\[ + (\sigma : A) \simeq (\tau : A) \iff \forall (\alpha : A^\perp \parallel + \proc), \alpha \strComp \sigma = \alpha \strComp \tau \] Yet, by lack of time, I had to abandon this path. Indeed, this would have