language.tex 3.52 KB
 Robbert Krebbers committed Oct 17, 2016 1 2 3 \section{Language} \label{sec:language}  Ralf Jung committed Feb 02, 2017 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 committed Dec 12, 2016 5 \begin{itemize}[itemsep=0pt]  Robbert Krebbers committed Oct 17, 2016 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}  Robbert Krebbers committed Oct 17, 2016 10 \end{mathpar}  Robbert Krebbers committed Oct 17, 2016 11 \item There exists a \emph{primitive reduction relation} $(-,- \step -,-,-) \subseteq \Expr \times \State \times \Expr \times \State \times \List(\Expr)$  Robbert Krebbers committed Oct 17, 2016 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  Robbert Krebbers committed Oct 17, 2016 20  $\Exists \expr_2, \state_2, \vec\expr. \expr,\state \step \expr_2,\state_2,\vec\expr$  Robbert Krebbers committed Oct 17, 2016 21 22 23 \end{defn} \begin{defn}  Ralf Jung committed Dec 12, 2017 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$  Robbert Krebbers committed Oct 17, 2016 28 \end{defn}  Ralf Jung committed Dec 12, 2017 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.  Robbert Krebbers committed Oct 17, 2016 32 33  \begin{defn}[Context]  Robbert Krebbers committed Oct 17, 2016 34  A function $\lctx : \Expr \to \Expr$ is a \emph{context} if the following conditions are satisfied:  Robbert Krebbers committed Oct 17, 2016 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$:\\  Robbert Krebbers committed Oct 17, 2016 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$  Robbert Krebbers committed Oct 17, 2016 40  \item Reductions stay below $\lctx$ until there is a value in the hole:\\  Robbert Krebbers committed Oct 17, 2016 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$  Robbert Krebbers committed Oct 17, 2016 42 43 44  \end{enumerate} \end{defn}  Ralf Jung committed Dec 10, 2017 45 \subsection{Concurrent Language}  Robbert Krebbers committed Oct 17, 2016 46 47 48 49 50  For any language $\Lang$, we define the corresponding thread-pool semantics. \paragraph{Machine syntax} $ Robbert Krebbers committed Oct 17, 2016 51  \tpool \in \ThreadPool \eqdef \List(\Expr)  Robbert Krebbers committed Oct 17, 2016 52 53 54 55 56 57 $ \judgment[Machine reduction]{\cfg{\tpool}{\state} \step \cfg{\tpool'}{\state'}} \begin{mathpar} \infer  Robbert Krebbers committed Oct 17, 2016 58  {\expr_1, \state_1 \step \expr_2, \state_2, \vec\expr}  Robbert Krebbers committed Oct 17, 2016 59  {\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state_1} \step  Robbert Krebbers committed Oct 17, 2016 60  \cfg{\tpool \dplus [\expr_2] \dplus \tpool' \dplus \vec\expr}{\state_2}}  Robbert Krebbers committed Oct 17, 2016 61 62 \end{mathpar}  Ralf Jung committed Dec 12, 2016 63 64 65 66 67  %%% Local Variables: %%% mode: latex %%% TeX-master: "iris" %%% End: