tobast/L3-internship-report
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Nearly final version

Browse source
This commit is contained in:
Théophile Bastian 2016-08-20 20:00:32 +02:00
parent 4bcd8dba6f
commit 1fedc0b668
1 changed files with 151 additions and 47 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

198
report.tex
View file

@ -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