language.tex 3.52 KB
Newer Older
1
2
3
\section{Language}
\label{sec:language}

4
A \emph{language} $\Lang$ consists of a set \Expr{} of \emph{expressions} (metavariable $\expr$), a set \Val{} of \emph{values} (metavariable $\val$), and a nonempty set $\State$ of \emph{states} (metavariable $\state$) such that
Ralf Jung's avatar
Ralf Jung committed
5
\begin{itemize}[itemsep=0pt]
6
7
8
9
\item There exist functions $\ofval : \Val \to \Expr$ and $\toval : \Expr \pfn \Val$ (notice the latter is partial), such that
\begin{mathpar}
{\All \expr, \val. \toval(\expr) = \val \Ra \ofval(\val) = \expr} \and
{\All\val. \toval(\ofval(\val)) = \val} 
10
\end{mathpar}
11
\item There exists a \emph{primitive reduction relation} \[(-,- \step -,-,-) \subseteq \Expr \times \State \times \Expr \times \State \times \List(\Expr)\]
12
13
14
15
16
17
18
19
  A reduction $\expr_1, \state_1 \step \expr_2, \state_2, \overline\expr$ indicates that, when $\expr_1$ reduces to $\expr_2$, the new threads in the list $\overline\expr$ is forked off.
  We will write $\expr_1, \state_1 \step \expr_2, \state_2$ for $\expr_1, \state_1 \step \expr_2, \state_2, ()$, \ie when no threads are forked off. \\
\item All values are stuck:
\[ \expr, \_ \step  \_, \_, \_ \Ra \toval(\expr) = \bot \]
\end{itemize}

\begin{defn}
  An expression $\expr$ and state $\state$ are \emph{reducible} (written $\red(\expr, \state)$) if
20
  \[ \Exists \expr_2, \state_2, \vec\expr. \expr,\state \step \expr_2,\state_2,\vec\expr \]
21
22
23
\end{defn}

\begin{defn}
Ralf Jung's avatar
Ralf Jung committed
24
25
26
27
  An expression $\expr$ is \emph{weakly atomic} if it reduces in one step to something irreducible:
  \[ \atomic(\expr) \eqdef \All\state_1, \expr_2, \state_2, \vec\expr. \expr, \state_1 \step \expr_2, \state_2, \vec\expr \Ra \lnot \red(\expr_2, \state_2) \]
  It is \emph{strongly atomic} if it reduces in one step to a value:
  \[ \stronglyAtomic(\expr) \eqdef \All\state_1, \expr_2, \state_2, \vec\expr. \expr, \state_1 \step \expr_2, \state_2, \vec\expr \Ra \toval(\expr_2) \neq \bot \]
28
\end{defn}
Ralf Jung's avatar
Ralf Jung committed
29
30
31
We need two notions of atomicity to accommodate both kinds of weakest preconditions that we will define later:
If the weakest precondition ensures that the program cannot get stuck, weak atomicity is sufficient.
Otherwise, we need strong atomicity.
32
33

\begin{defn}[Context]
34
  A function $\lctx : \Expr \to \Expr$ is a \emph{context} if the following conditions are satisfied:
35
36
37
38
  \begin{enumerate}[itemsep=0pt]
  \item $\lctx$ does not turn non-values into values:\\
    $\All\expr. \toval(\expr) = \bot \Ra \toval(\lctx(\expr)) = \bot $
  \item One can perform reductions below $\lctx$:\\
39
    $\All \expr_1, \state_1, \expr_2, \state_2, \vec\expr. \expr_1, \state_1 \step \expr_2,\state_2,\vec\expr \Ra \lctx(\expr_1), \state_1 \step \lctx(\expr_2),\state_2,\vec\expr $
40
  \item Reductions stay below $\lctx$ until there is a value in the hole:\\
41
    $\All \expr_1', \state_1, \expr_2, \state_2, \vec\expr. \toval(\expr_1') = \bot \land \lctx(\expr_1'), \state_1 \step \expr_2,\state_2,\vec\expr \Ra \Exists\expr_2'. \expr_2 = \lctx(\expr_2') \land \expr_1', \state_1 \step \expr_2',\state_2,\vec\expr $
42
43
44
  \end{enumerate}
\end{defn}

Ralf Jung's avatar
Ralf Jung committed
45
\subsection{Concurrent Language}
46
47
48
49
50

For any language $\Lang$, we define the corresponding thread-pool semantics.

\paragraph{Machine syntax}
\[
51
	\tpool \in \ThreadPool \eqdef \List(\Expr)
52
53
54
55
56
57
\]

\judgment[Machine reduction]{\cfg{\tpool}{\state} \step
  \cfg{\tpool'}{\state'}}
\begin{mathpar}
\infer
58
  {\expr_1, \state_1 \step \expr_2, \state_2, \vec\expr}
59
  {\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state_1} \step
60
     \cfg{\tpool \dplus [\expr_2] \dplus \tpool' \dplus \vec\expr}{\state_2}}
61
62
\end{mathpar}

Ralf Jung's avatar
Ralf Jung committed
63
64
65
66
67

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "iris"
%%% End: