From e659c053a45f18c28c5bc78a1ed3f47663041e07 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9ophile=20Bastian?= Date: Tue, 9 Aug 2016 18:40:25 +0100 Subject: [PATCH] Redacted introduction --- concurgames.sty | 3 ++ report.tex | 74 ++++++++++++++++++++++++++++++++++++++++++------- 2 files changed, 67 insertions(+), 10 deletions(-) diff --git a/concurgames.sty b/concurgames.sty index 0ae1207..250690b 100644 --- a/concurgames.sty +++ b/concurgames.sty @@ -9,6 +9,8 @@ \usetikzlibrary{shapes,arrows} +\newcommand{\fname}[1]{\textsc{#1}} + \newcommand{\con}{\operatorname{Con}} \newcommand{\confl}{\raisebox{0.5em}{\uwave{\hspace{2em}}}} @@ -35,6 +37,7 @@ % LCCS \newcommand{\lccs}{$\lambda$CCS} +\newcommand{\llccs}{$\lambda$CCS$_\linarrow$} \newcommand{\proc}{\mathbb{P}} \newcommand{\chan}{\mathbb{C}} diff --git a/report.tex b/report.tex index 80f58cc..eb7e076 100644 --- a/report.tex +++ b/report.tex @@ -36,20 +36,20 @@ \section{Introduction} -Game semantics are a kind of operational semantics in which a program's -behaviour 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). +\paragraph{Game semantics} are a kind of operational 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 additional +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 @@ -58,7 +58,61 @@ 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. \qtodo{why?} +\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 +$\lambda$-calculus 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} laid the first stone +by defining game semantics for a fine-grained concurrent language including +parallel execution of ``threads'' and low-level semaphores. + +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 is 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, these approaches often introduce non-determinism in the strategies: if +two moves are available to a player, the model often states that she makes 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 that purpose as well. +Yet, these techniques do not adapt well to interleavings game semantics. + +\paragraph{The purpose of this internship} was to try to take a first step +towards the reunification of those two approaches. 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 +\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 ---, we 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{Existing work}