Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Rice Wine
Iris
Commits
83979416
Commit
83979416
authored
Feb 01, 2016
by
Ralf Jung
Browse files
move \text... to their respective sections; get rid of \fork
parent
b45812dd
Changes
3
Hide whitespace changes
Inline
Side-by-side
docs/logic.tex
View file @
83979416
...
...
@@ -2,14 +2,14 @@
\section
{
Parameters to the logic
}
\begin{itemize}
\item
A set
\textdom
{
Exp
}
of
\emph
{
expressions
}
(metavariable
$
\expr
$
) with a
subset
\textdom
{
Val
}
of values (
$
\val
$
). We assume that if
$
\expr
$
is an
expression then so is
$
\fork
{
\expr
}$
. We moreover assume a value
\textsf
{
fRet
}
(giving the intended return value of a fork), and we assume that
\begin{align*}
\fork
{
\expr
}
&
\notin
\textdom
{
Val
}
\\
\fork
{
\expr
_
1
}
=
\fork
{
\expr
_
2
}
&
\implies
\expr
_
1 =
\expr
_
2
\end{align*}
%
\item A set \textdom{Exp} of \emph{expressions} (metavariable $\expr$) with a
%
subset \textdom{Val} of values ($\val$). We assume that if $\expr$ is an
%
expression then so is $\fork{\expr}$. We moreover assume a value
%
\textsf{fRet} (giving the intended return value of a fork), and we assume that
%
\begin{align*}
%
\fork{\expr} &\notin \textdom{Val} \\
%
\fork{\expr_1} = \fork{\expr_2} &\implies \expr_1 = \expr_2
%
\end{align*}
\item
A set
$
\textdom
{
Ectx
}$
of
\emph
{
evaluation contexts
}
(
$
\ectx
$
) that includes the empty context
$
[
\;
]
$
,
a plugging operation
$
\ectx
[
\expr
]
$
that produces an expression, and context composition
$
\circ
$
satisfying the following axioms:
...
...
@@ -20,7 +20,7 @@
\ectx
[\expr_1]
=
\ectx
[\expr_2]
&
\implies
\expr
_
1 =
\expr
_
2
\\
\ectx
_
1
\circ
\ectx
_
2 = [
\;
]
&
\implies
\ectx
_
1 =
\ectx
_
2 = [
\;
]
\\
\ectx
[\expr]
\in
\textdom
{
Val
}
&
\implies
\ectx
= [
\;
]
\\
\ectx
[\expr]
=
\fork
{
\expr
'
}
&
\implies
\ectx
= [
\;
]
%
\ectx[\expr] = \fork{\expr'} &\implies \ectx = [\;]
\end{align*}
\item
A set
\textdom
{
State
}
of shared machine states (
\eg
heaps), metavariable
$
\state
$
.
...
...
@@ -34,14 +34,14 @@ and notions of an expression to be \emph{reducible} or \emph{stuck}, such that
\lnot
\textlog
{
reducible
}
(
\expr
')
\end{align*}
and the following hold
\begin{align*}
&
\textlog
{
stuck
}
(
\fork
{
\expr
}
)
&
\\
&
\textlog
{
stuck
}
(
\val
)
&
\\
&
\ectx
[\expr]
=
\ectx
'[
\expr
']
\implies
\textlog
{
reducible
}
(
\expr
')
\implies
\expr
\notin
\textdom
{
Val
}
\implies
\Exists
\ectx
''.
\ectx
' =
\ectx
\circ
\ectx
''
&
\mbox
{
(step-by-value)
}
\\
&
\ectx
[\expr]
=
\ectx
'[
\fork
{
\expr
'
}
]
\implies
\expr
\notin
\textdom
{
Val
}
\implies
\Exists
\ectx
''.
\ectx
' =
\ectx
\circ
\ectx
''
&
\mbox
{
(fork-by-value)
}
\\
\end{align*}
%
\begin{align*}
%
&\textlog{stuck}(\fork{\expr})& \\
%
&\textlog{stuck}(\val)&\\
%
&\ectx[\expr] = \ectx'[\expr'] \implies \textlog{reducible}(\expr') \implies
%
\expr \notin \textdom{Val} \implies \Exists \ectx''. \ectx' = \ectx \circ \ectx'' &\mbox{(step-by-value)} \\
%
&\ectx[\expr] = \ectx'[\fork{\expr'}] \implies
%
\expr \notin \textdom{Val} \implies \Exists \ectx''. \ectx' = \ectx \circ \ectx'' &\mbox{(fork-by-value)} \\
%
\end{align*}
\item
A predicate
\textlog
{
atomic
}
on expressions satisfying
\begin{align*}
...
...
@@ -78,11 +78,11 @@ Let $\mcarp{M} \eqdef |\monoid| \setminus \{\mzero\}$.
{
\cfg
{
\state
}{
\expr
}
\step
\cfg
{
\state
'
}{
\expr
'
}}
{
\cfg
{
\state
}{
\tpool
[i
\mapsto
\ectx
[\expr]
]
}
\step
\cfg
{
\state
'
}{
\tpool
[i
\mapsto
\ectx
[\expr']
]
}}
\and
\infer
{}
{
\cfg
{
\state
}{
\tpool
[i
\mapsto
\ectx
[\fork{\expr}]
]
}
\step
\cfg
{
\state
}{
\tpool
[i
\mapsto
\ectx
[\textsf{fRet}]
] [j
\mapsto
\expr
]
}}
%
\and
%
\infer
%
{}
%
{\cfg{\state}{\tpool [i \mapsto \ectx[\fork{\expr}]]} \step
%
\cfg{\state}{\tpool [i \mapsto \ectx[\textsf{fRet}]] [j \mapsto \expr]}}
\end{mathpar}
\section
{
Syntax
}
...
...
@@ -567,10 +567,10 @@ We write $\provesalways$ to denote judgments that can only be extended with a bo
{
\hoare
{
\prop
}{
\expr
}{
\Ret\val
.
\propB
}
[
\mask
]
\and
\text
{$
\expr
$
not a value
}
}
{
\hoare
{
\prop
*
\later\propC
}{
\expr
}{
\Ret\val
.
\propB
*
\propC
}
[
\mask
\uplus
\mask
']
}
\and
\inferH
{
Fork
}
{
\hoare
{
\prop
}{
\expr
}{
\Ret\any
.
\TRUE
}
[
\top
]
}
{
\hoare
{
\later\prop
*
\later\propB
}{
\fork
{
\expr
}}{
\Ret\val
.
\val
=
\textsf
{
fRet
}
\land
\propB
}
[
\mask
]
}
%
\and
%
\inferH{Fork}
%
{\hoare{\prop}{\expr}{\Ret\any. \TRUE}[\top]}
%
{\hoare{\later\prop * \later\propB}{\fork{\expr}}{\Ret\val. \val = \textsf{fRet} \land \propB}[\mask]}
\and
\inferH
{
ACsq
}
{
\prop
\vs
[\mask \uplus \mask'][\mask]
\prop
'
\\
...
...
docs/model.tex
View file @
83979416
...
...
@@ -389,28 +389,28 @@ $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land
\typedsection
{
Weakest precondition
}{
\mathit
{
wp
}
:
\Delta
(
\pset
{
\mathbb
{
N
}}
)
\times
\Delta
(
\textdom
{
Exp
}
)
\times
(
\Delta
(
\textdom
{
Val
}
)
\to
\textdom
{
Prop
}
)
\to
\textdom
{
Prop
}
\in
{
\cal
U
}}
\begin{align*}
\mathit
{
wp
}_
\mask
(
\expr
, q)
&
\eqdef
\Lam
W.
\begin{aligned}
[t]
\{\,
(n,
\rs
)
&
\mid
\All
W
_
F
\geq
W; k
\leq
n;
\rs
_
F;
\state
;
\mask
_
F
\sep
\mask
. k > 0
\land
k
\in
(
\fullSat
{
\state
}{
\mask
\cup
\mask
_
F
}{
\rs
\rtimes
\rs
_
F
}{
W
_
F
}
)
\implies
{}
\\
&
\qquad
(
\expr
\in
\textdom
{
Val
}
\implies
\Exists
W'
\geq
W
_
F.
\Exists
\rs
'.
\\
&
\qquad\qquad
k
\in
(
\fullSat
{
\state
}{
\mask
\cup
\mask
_
F
}{
\rs
'
\rtimes
\rs
_
F
}{
W'
}
)
\land
(k,
\rs
')
\in
q(
\expr
)(W'))~
\land
\\
&
\qquad
(
\All\ectx
,
\expr
_
0,
\expr
'
_
0,
\state
'.
\expr
=
\ectx
[\expr_0]
\land
\cfg
{
\state
}{
\expr
_
0
}
\step
\cfg
{
\state
'
}{
\expr
'
_
0
}
\implies
\Exists
W'
\geq
W
_
F.
\Exists
\rs
'.
\\
&
\qquad\qquad
k - 1
\in
(
\fullSat
{
\state
'
}{
\mask
\cup
\mask
_
F
}{
\rs
'
\rtimes
\rs
_
F
}{
W'
}
)
\land
(k-1,
\rs
')
\in
wp
_
\mask
(
\ectx
[\expr_0']
, q)(W'))~
\land
\\
&
\qquad
(
\All\ectx
,
\expr
'.
\expr
=
\ectx
[\fork{\expr'}]
\implies
\Exists
W'
\geq
W
_
F.
\Exists
\rs
',
\rs
_
1',
\rs
_
2'.
\\
&
\qquad\qquad
k - 1
\in
(
\fullSat
{
\state
}{
\mask
\cup
\mask
_
F
}{
\rs
'
\rtimes
\rs
_
F
}{
W'
}
)
\land
\rs
' =
\rs
_
1'
\rtimes
\rs
_
2'~
\land
\\
&
\qquad\qquad
(k-1,
\rs
_
1')
\in
\mathit
{
wp
}_
\mask
(
\ectx
[\textsf{fRet}]
, q)(W')
\land
(k-1,
\rs
_
2')
\in
\mathit
{
wp
}_
\top
(
\expr
',
\Lam\any
.
\top
)(W'))
\,\}
\end{aligned}
\end{align*}
%
\begin{align*}
%
\mathit{wp}_\mask(\expr, q) &\eqdef \Lam W.
%
\begin{aligned}[t]
%
\{\, (n, \rs) &\mid \All W_F \geq W; k \leq n; \rs_F; \state; \mask_F \sep \mask. k > 0 \land k \in (\fullSat{\state}{\mask \cup \mask_F}{\rs \rtimes \rs_F}{W_F}) \implies{}\\
%
&\qquad
%
(\expr \in \textdom{Val} \implies \Exists W' \geq W_F. \Exists \rs'. \\
%
&\qquad\qquad
%
k \in (\fullSat{\state}{\mask \cup \mask_F}{\rs' \rtimes \rs_F}{W'}) \land (k, \rs') \in q(\expr)(W'))~\land \\
%
&\qquad
%
(\All\ectx,\expr_0,\expr'_0,\state'. \expr = \ectx[\expr_0] \land \cfg{\state}{\expr_0} \step \cfg{\state'}{\expr'_0} \implies \Exists W' \geq W_F. \Exists \rs'. \\
%
&\qquad\qquad
%
k - 1 \in (\fullSat{\state'}{\mask \cup \mask_F}{\rs' \rtimes \rs_F}{W'}) \land (k-1, \rs') \in wp_\mask(\ectx[\expr_0'], q)(W'))~\land \\
%
&\qquad
%
(\All\ectx,\expr'. \expr = \ectx[\fork{\expr'}] \implies \Exists W' \geq W_F. \Exists \rs', \rs_1', \rs_2'. \\
%
&\qquad\qquad
%
k - 1 \in (\fullSat{\state}{\mask \cup \mask_F}{\rs' \rtimes \rs_F}{W'}) \land \rs' = \rs_1' \rtimes \rs_2'~\land \\
%
&\qquad\qquad
%
(k-1, \rs_1') \in \mathit{wp}_\mask(\ectx[\textsf{fRet}], q)(W') \land
%
(k-1, \rs_2') \in \mathit{wp}_\top(\expr', \Lam\any. \top)(W'))
%
\,\}
%
\end{aligned}
%
\end{align*}
\begin{lem}
$
\mathit
{
wp
}$
is well-defined:
$
\mathit
{
wp
}_{
\mask
}
(
\expr
, q
)
$
is a valid proposition, and
$
\mathit
{
wp
}$
is a non-expansive map. Besides, the dependency on the recursive occurrence is contractive, so
$
\mathit
{
wp
}$
has a fixed-point.
\end{lem}
...
...
docs/setup.tex
View file @
83979416
...
...
@@ -34,6 +34,7 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% SETUP
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\SetSymbolFont
{
stmry
}{
bold
}{
U
}{
stmry
}{
m
}{
n
}
% this fixes warnings when \boldsymbol is used with stmaryrd included
\extrarowheight
=
\jot
% else, arrays are scrunched compared to, say, aligned
\newcolumntype
{
.
}{
@
{}}
...
...
@@ -84,17 +85,6 @@
\newtheorem
{
thm
}{
Theorem
}
\newtheorem
{
exercise
}{
Exercise
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% FONTS & FORMATTING
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\SetSymbolFont
{
stmry
}{
bold
}{
U
}{
stmry
}{
m
}{
n
}
% this fixes warnings when \boldsymbol is used with stmaryrd included
\newcommand
{
\textdom
}
[1]
{
\textit
{
#1
}}
\newcommand
{
\textlog
}
[1]
{
\textsf
{
#1
}}
\newcommand
{
\textsort
}
[1]
{
\textlog
{
#1
}}
\newcommand
{
\textlang
}
[1]
{
\texttt
{
#1
}}
\newcommand
{
\textmon
}
[1]
{
\textsc
{
#1
}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% GENERIC MACROS
...
...
@@ -217,6 +207,8 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% CMRA (RESOURCE ALGEBRA) SYMBOLS & NOTATION & IDENTIFIERS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand
{
\textmon
}
[1]
{
\textsc
{
#1
}}
\newcommand
{
\monoid
}{
M
}
\newcommand
{
\melt
}{
a
}
...
...
@@ -238,6 +230,7 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% MODEL-SPECIFIC SYMBOLS & NOTATION & IDENTIFIERS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand
{
\textdom
}
[1]
{
\textit
{
#1
}}
\newcommand
{
\wIso
}{
\xi
}
...
...
@@ -245,7 +238,7 @@
\newcommand
{
\rsB
}{
s
}
\newcommand
{
\pres
}{
\pi
}
\newcommand
{
\wld
}{
w
}
\newcommand
{
\ghostRes
}{
g
}
%% Various pieces of syntax
...
...
@@ -276,6 +269,8 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% LOGIC SYMBOLS & NOTATION & IDENTIFIERS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand
{
\textlog
}
[1]
{
\textsf
{
#1
}}
\newcommand
{
\textsort
}
[1]
{
\textlog
{
#1
}}
\newcommand
{
\Sig
}{
\mathcal
{
S
}}
\newcommand
{
\SigType
}{
\mathcal
{
T
}}
...
...
@@ -421,7 +416,7 @@
\newcommand
{
\FALSE
}{
\textlog
{
False
}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% LANGUAGE
-LEVEL
SYNTAX AND SEMANTICS
% LANGUAGE SYNTAX AND SEMANTICS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand
{
\expr
}{
e
}
\newcommand
{
\val
}{
v
}
...
...
@@ -433,7 +428,6 @@
\newcommand
{
\tpool
}{
T
}
\newcommand
{
\cfg
}
[2]
{{
#1
}
;
{
#2
}}
\newcommand
{
\fork
}
[1]
{
\textlang
{
fork
}
\;
{
#1
}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% DERIVED CONSTRUCTIONS
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment