% -*- Mode: LaTeX -*-

\section{Dynamic Semantics of a Mini-Language with ``Close''}
\label{sec:dynamic-semantics}
\subsection{Syntax}
The expression syntax of our mini-language is given below. For
simplicity, the language provides ML-like references \cite{SML90} as
the only means of creating mutable data structures.  A brief
description of possible extensions to other data structures is given
in a later section.
\begin{center}
\begin{tabular}{l@{\hmmmm}rcl@{\hmm}l}
\cbx{expressions:} & $a$ &
    ::=         & $c$           & constant                 \\
& & $\mid$      & $x$           & identifier               \\
& & $\mid$      & $f\;\tbx{where}\;f(x)=a$ & recursive function    \\
& & $\mid$      & $a_{1}\;a_{2}$& application              \\
& & $\mid$      & \tbx{let} $x=a_{1}$ \tbx{in} $a_{2}$ & \tbx{let} binding \\
& & $\mid$      & $\tbx{close}\;a$ & \tbx{close} expression
\end{tabular}
\end{center}
The set of constants include the usual arithmetic primitive functions
$(+,-,\ldots)$, and functions to allocate, read and write locations
(\tbx{ref,!,:=}). We define $\fvar{a}$ to be the set of free
identifiers of the expression $a$. 

Entities used in the dynamic semantics are defined as follows:
\begin{center}
\begin{tabular}{l@{\hmmmm}rcl@{\hmm}l}
\cbx{values:} & $v$ & 
    ::=         & $c$                   & constant \\
& & $\mid$      & \cval{f,x,a,e}         & function closure  \\
& & $\mid$      & $l$                   & store location \\
\cbx{environments:} & $e$ & ::= & \cbx{identifiers} $\rightarrow$ \cbx{values} \\
\cbx{stores:} & $s$ & ::= & \cbx{locations} $\rightarrow$ \cbx{values}
$\times$ \cbx{tag}\\ 
\end{tabular}
\end{center}
Each location in a store has a tag, $\rw$ or $\ro$, indicating that
the location has read/write or read-only semantics. This is useful in
modeling the dynamic semantics of the \tbx{close} operation where the
tag of a location is explicitly changed from $\rw$ to $\ro$. We assume
functions $\fn{value}{s,l}$ and $\fn{tag}{s,l}$ that read the value
and tag respectively from a location.

For a value $v$, we define $\lvar{v}$ to be the set of locations
directly contained in the value $v$. This is defined structurally as
follows: $\lvar{c}=\phi$, $\lvar{l}=\{l\}$, and
$\lvar{\cval{f,x,a,e}}=\lvar{e}$. For an environment
$e=\{x_{1}\mapsto{}v_{1},\ldots,x_{n}\mapsto{}v_{n}\}$, we define
$\lvar{e}=\bigcup_{1\leq{}i\leq{}n}\lvar{v_{i}}$.

We also define \fn{Reachable}{v,s} to be the set of all locations
within the domain of store $s$ that are either directly contained
within the value $v$ or transitively contained in a value stored at
such a location \via the store $s$. This extends naturally (pointwise)
to values present in an environment $e$. 

\subsection{Evaluation Rules}
\begin{myfig}{fig:dynamic}{The Dynamic Semantics of the Mini-Language.}
\begin{center}
\begin{tabular}{l@{\hmmmm}c}
\cbx{const:} &
\stmt{e\vdash c/s \Rightarrow c/s} \\ \\
\cbx{ident:} &
\inference{\stmt{x\in\fn{Dom}{e}}}%
          {\stmt{e\vdash x/s \Rightarrow e(x)/s}} \\ \\
\cbx{abs:} &
\inference{\stmt{Y=\fvar{f\;\tbx{where}\;f(x)=a}}}%
          {\stmt{e\vdash (f\;\tbx{where}\;f(x)=a)/s 
           \Rightarrow \cval{f,x,a,e\mid_{Y}}/s}} \\ \\
\cbx{app:} &
\inference{\stmt{e\vdash a_{1}/s \Rightarrow\cval{f,x,a_{0},e_{0}}/s_{1}} \\
           \stmt{e\vdash a_{2}/s_{1} \Rightarrow v_{2}/s_{2}} \\
           \stmt{e_{0}+\{f\mapsto\cval{f,x,a_{0},e_{0}}, x \mapsto v_{2}\} 
                 \vdash a_{0}/s_{2} \Rightarrow v/s_{3}}}%
          {\stmt{e\vdash (a_{1}\; a_{2})/s \Rightarrow v/s_{3}}} \\ \\
\cbx{let:} &
\inference{\stmt{e\vdash a_{1}/s \Rightarrow v_{1}/s_{1}} \hmm
           \stmt{e+\{x \mapsto v_{1}\} \vdash a_{2}/s_{1} \Rightarrow v_{2}/s_{2}}}%
          {\stmt{e\vdash (\tbx{let}\;x=a_{1}\;\tbx{in}\;a_{2})/s
                 \Rightarrow v_{2}/s_{2}}} \\ \\
\cbx{alloc:} &
\inference{\stmt{e\vdash a/s \Rightarrow v/s_{1}}\hmm
           \stmt{l\not\in\fn{Dom}{s_{1}}}}%
          {\stmt{e\vdash \tbx{ref}(a)/s \Rightarrow
                 l/(s_{1}+\{l\mapsto v,\/\rw\})}} \\ \\
\cbx{deref:} &
\inference{\stmt{e\vdash a/s \Rightarrow l/s_{1}}\hmm
           \stmt{l\in\fn{Dom}{s_{1}}\hmm \fn{value}{s_{1},l}=v}}%
          {\stmt{e\vdash \tbx{!}a/s \Rightarrow v/s_{1}}} \\ \\
\cbx{assign:} &
\inference{\stmt{e\vdash a/s \Rightarrow (l,v)/s_{1}}\hmm
           \stmt{l\in\fn{Dom}{s_{1}}\hmm \fn{tag}{s_{1},l}=\rw}}%
          {\stmt{e\vdash \tbx{:=}(a)/s \Rightarrow 
                 \tbx{()}/(s_{1}+\{l\mapsto v,\/\rw\})}} \\ \\
\cbx{close:} &
\inference{\stmt{e\vdash a/s \Rightarrow l/s_{1}} \hmm
           \stmt{s_{1}(l)=v,\/\rw} \\
           \stmt{L=\fn{Reachable}{l,s_{1}}\cup\fn{Reachable}{e,s_{1}}\cup
                 \bigcup_{l'\in\fn{Dom}{s}}\fn{Reachable}{l',s_{1}}}}%
          {\stmt{e\vdash (\tbx{close}\;a)/s \Rightarrow 
                 l/(s_{1}\mid_{L}+\{l\mapsto v,\/\ro\})}}
\end{tabular}
\end{center}
\end{myfig}

\fig{dynamic} shows the axioms and inference rules for establishing
\cbx{evaluation judgments} of the form
$e\vdash{}a/s\Rightarrow{}v/s'$.  We do not provide ``error'' rules
explicitly; a dynamic type-error occurs when the evaluation becomes
``stuck''.  Most of the rules are fairly standard and
self-explanatory. The rules for primitive reference operators are
handled as special cases of the general \cbx{app} rule.  The
\cbx{assign} rule makes sure that the location being written carries a
read/write tag.

The \cbx{close} rule is the only place where the read/write tag of a
location is explicitly changed to a read-only tag. This causes a
dynamic ``close-error'' to be generated if that location is
subsequently assigned. Ultimately, we would like to detect such
dynamic errors at compile-time using the type system.  We also
restrict the domain of the final store in the \cbx{close} rule to the
reachable locations of the location being closed, the current
environment and the locations of the initial store. This operation
``cleans'' the store by removing spurious unreachable handles from its
domain that point to the location being closed.\footnote{This
restriction is only necessary to simplify our soundness proof.}

Although the rules given in \fig{dynamic} provide a
strict, sequential, call-by-value semantics for the mini-language, our
technique does not rely on preserving the sequentiality or the
determinism of evaluation.  This is seen from the fact that even if we
make the language non-deterministic by adding an additional \cbx{app}
rule which interchanges the order in which the function and the
argument are evaluated, our results on \tbx{close} still
hold.\footnote{Using a truly ``parallel'' semantics would be a more
convincing argument, but we are not aware of a relational style
semantics which captures parallelism. Adapting our system to a
``parallel'' semantics is a topic for future research.}
