From 1fedc0b668f14ae3acfebf877ad9e909ed78420e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9ophile=20Bastian?= <contact@tobast.fr>
Date: Sat, 20 Aug 2016 20:00:32 +0200
Subject: [PATCH] Nearly final version
---
report.tex | 198 ++++++++++++++++++++++++++++++++++++++++-------------
1 file changed, 151 insertions(+), 47 deletions(-)
diff --git a/report.tex b/report.tex
index 8664571..f601a48 100644
--- a/report.tex
+++ b/report.tex
@@ -173,15 +173,18 @@ considered ``failed'' without reducing to $0$ (in case of deadlock).
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 a new channel $a$ on which two
-processes can be synchronized. Here, the ``synchronization'' simply means that
-a call to the channel is blocking until its other end has been called as well.
+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.
+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*}
@@ -238,12 +241,12 @@ 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 types since $a$ and
-$\bar{a}$ are not consumed. Our semantics would then not satisfy subject
-reduction.
+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 much problems, while
+\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}
@@ -252,8 +255,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 only $\proc$ and
-$\chan$.
+the typing rules). In particular, the only base types are $\proc$ and $\chan$.
\begin{figure}[h]
\begin{minipage}[t]{0.55\textwidth}
@@ -274,9 +276,16 @@ $\chan$.
\caption{Linear \lcalc{} terms and types}\label{fig:llam:syntax}
\end{figure}
-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.
+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*}
@@ -313,7 +322,21 @@ To lift the operational semantics to \llccs, we only need to add one rule:
\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 \todo{More examples?}
+ \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}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -328,10 +351,10 @@ the often-used tree-like games.
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 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
+$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}
@@ -346,9 +369,9 @@ game tree
\]
This can of course be used to describe much larger games, and is often useful
-to reason concurrently, since the causal histories appear 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, 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
@@ -371,7 +394,7 @@ before Player can play $C$. The corresponding tree-like game would be
\]
This goes even worse with less structure: since there is $n!$ % chktex 40
-permutations for $n$ elements, the tree can grow way bigger.
+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
@@ -476,7 +499,27 @@ 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}[Process game]
+\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}
@@ -489,11 +532,14 @@ 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}$
- means that a process cannot finish \emph{before} it is called.
+ 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$, $\sigma: A$, is an ESP such that
+ 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)$;
@@ -501,6 +547,9 @@ drink.
\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
@@ -524,7 +573,26 @@ drink.
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.
+ 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
@@ -552,7 +620,8 @@ unrealistic. We then have to restrict pre-strategies to \emph{strategies}:
(\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.
+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
@@ -574,10 +643,10 @@ 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.
+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]
+\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
@@ -589,7 +658,9 @@ $B$ and $C$ denotes games, $\sigma: A$ and $\tau: B$ denotes 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.
+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
@@ -597,7 +668,7 @@ 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]
+\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.
@@ -606,7 +677,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$.
+ 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
@@ -623,13 +694,14 @@ causal loop).
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
-objective here is to \emph{compose} strategies: indeed, a strategy on $A^\perp
+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$.
+C$ (as one would compose two mathematical functions $f$ and $g$ into $g \circ
+f$).
-\begin{definition}[Compositional interaction]
+\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
@@ -637,7 +709,9 @@ C$.
\end{definition}
The idea is to put in correspondence the ``middle'' states (those of $B$) while
-adding ``neutral'' states for $A$ and $C$.
+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$.
$\tau \strInteract \sigma$ is an \emph{event structure} (\ie, without
polarities): indeed, the two strategies disagree on the polarities of the
@@ -647,7 +721,7 @@ over $\set{+,-,?}$.
From this point, the notion of composition we sought is only a matter of
``hiding'' the middle part:
-\begin{definition}[Strategies composition]
+\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
@@ -656,9 +730,11 @@ From this point, the notion of composition we sought is only a matter of
\end{definition}
It is then useful to consider an identity strategy \wrt{} the composition
-operator. This identity is called the \emph{copycat} strategy:
+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]
+\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}
@@ -696,10 +772,14 @@ $\sigma : A$, $\sigma$ is a strategy $\iff$ $\cc_A \strComp \sigma = \sigma$.
(12) edge (11)
(22) edge (21)
(31) edge (32)
- (31) edge (11)
+% (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}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -837,17 +917,17 @@ games, in this order.
We will now prove the major result of this study, the \emph{adequacy} of the
game semantics.
-\begin{theorem}[Adequacy]
+\begin{theorem}[adequacy]
The previous interpretation is \emph{adequate} with the operational
semantics, that is
- \[ \forall P \textit{ st. } \vdash P : \proc,~
+ \[ \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]
+\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$.
@@ -880,10 +960,13 @@ required.
\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}$,
+ $\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$;
@@ -924,9 +1007,15 @@ 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). \todo{?}
+ \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}
@@ -953,6 +1042,21 @@ 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
@@ -976,7 +1080,7 @@ isomorphism) of $\parallel$, but in the code, each use of the associativity
must be explicit, leading to a large amount of code.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\section*{Conclusion}
+\section{Conclusion}
During this internship, I have established deterministic game semantics for a
simple concurrent language. Although the language is fairly simple, it should