Commit ba5030c5 authored by Simcha van Collem's avatar Simcha van Collem
Browse files

tex: Improve proof of example

parent ca96e88e
......@@ -105,30 +105,30 @@ This makes it possible to call $\signalName$ and $\waitName$ on the returned bar
\RES{x \mapsto \False} \\
\COMMENT{Allocate $x$} \\
\CODE{\Let b = \newbarrier{\TT} in} \\
\COMMENT{Use \ruleref{New Barrier-Spec} with $P \eqdef \Exists b'. b' \in \Bool \ast x \mapsto b'$} \\
\RES{x \mapsto \False \ast \send{b}{\Exists b'. b' \in \Bool \ast x \mapsto b'} \ast \recv{b}{\Exists b'. b' \in \Bool \ast x \mapsto b'}} \\
\COMMENT{Use \ruleref{New Barrier-Spec} with $P \eqdef \Exists b' \in \Bool. x \mapsto b'$} \\
\RES{x \mapsto \False \ast \send{b}{\Exists b' \in \Bool. x \mapsto b'} \ast \recv{b}{\Exists b' \in \Bool. x \mapsto b'}} \\
\COMMENT{Give points-to and $\sendName$ predicate to left thread, $\recvName$ predicate to right thread} \\
x \mapsto \False \\
\quad\ast\spac \send{b}{\Exists b'. b' \in \Bool \ast x \mapsto b'}
\quad\ast\spac \send{b}{\Exists b' \in \Bool. x \mapsto b'}
\end{array}} \\
\CODE{x \gets \expensiveBoolName\spac \TT;} \\
\COMMENT{Specification of $\expensiveBoolName$} \\
b' \in \Bool \ast x \mapsto b' \\
\quad\ast\spac \send{b}{\Exists b'. b' \in \Bool \ast x \mapsto b'}
\quad\ast\spac \send{b}{\Exists b' \in \Bool. x \mapsto b'}
\end{array}} \\
\CODE{\signal{b}} \\
\COMMENT{Use \ruleref{Signal-Spec}} \\
\RES{\Ret v. v = \TT}
\end{array} &
\RES{\recv{b}{\Exists b'. b' \in \Bool \ast x \mapsto b'}} \\
\RES{\recv{b}{\Exists b' \in \Bool. x \mapsto b'}} \\
\CODE{\Let n = \expensiveIntName\spac \TT in} \\
\COMMENT{Specification of $\expensiveIntName$} \\
\RES{n \in \Z \ast \recv{b}{\Exists b'. b' \in \Bool \ast x \mapsto b'}} \\
\RES{n \in \Z \ast \recv{b}{\Exists b' \in \Bool. x \mapsto b'}} \\
\CODE{\wait{b}} \\
\COMMENT{Use \ruleref{Wait-Spec}} \\
\RES{n \in \Z \ast b' \in \Bool \ast x \mapsto b'} \\
......@@ -165,7 +165,7 @@ Before we can use \ruleref{New Barrier-Spec}, we should decide which resource we
We can see that the right thread needs access to the points-to predicate of $x$ and that a boolean should be stored.
We will thus use the following as our resource:
\Exists b'. b' \in \Bool \ast x \mapsto b'
\Exists b' \in \Bool. x \mapsto b'
We can now create a new barrier. We give the points-to and $\sendName$ predicates to the left thread and the $\recvName$ predicate to the right.
In the left thread we first compute $\expensiveBoolName$ and store it in $x$.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment