$\llbracket\texttt{assume}(\mathcal{S})\rrbracket(s)\overset{\mathrm{def}}{=}\left\\{\begin{array}[]{ll}\\{s\\}&\textrm{if}~{}s\in\mathcal{S}\\\
\emptyset&\textrm{Otherwise}\end{array}\right.$
$\llbracket{\mathsf{while}\;(e)\;C}\rrbracket\overset{\mathrm{def}}{=}\left(\mathsf{assume}(e);C\right)^{*};(\mathsf{assume}(\lnot
e));$ $\displaystyle\displaystyle{\hbox{\hskip
31.94461pt\vbox{\hbox{\hskip-31.9446pt\hbox{\hbox{$\displaystyle\displaystyle\\{P\\}\cap\\{\lceil\mathcal{S}\rceil\\}\sqsubseteq\\{Q\\}$}}}\vbox{}}}\over\hbox{\hskip
30.65224pt\vbox{\vbox{}\hbox{\hskip-30.65222pt\hbox{\hbox{$\displaystyle\displaystyle\\{P\\}\texttt{assume}\left(b\right)\\{Q\\}$}}}}}}$
where  $\lceil\mathcal{S}\rceil=\\{m|\lfloor
m\rfloor\cap\mathcal{S}\neq\emptyset\\}$

Figure 15: Encoding of assume(b)

The framework also describes a useful concept called the view shift operator
$\subseteq$, that describes a way to reinterpret a set of instrumented states
as a new set of instrumented states. This operator enables us to define an
abstract notion of executing a small step of the program. We express the step
from $p$ to $q$ with action $\alpha$ ensuring that the operation
interpretation of the action satisfies the specification:$p\sqsubseteq
q\stackrel{{\scriptstyle def}}{{=}}\forall m\in\mathcal{M}\ldotp\lfloor
p*\\{m\\}\rfloor\subseteq\lfloor q*\mathcal{R}(\\{m\\})\rfloor$. Because the
Views framework handles soundness for the structural rules (sequencing,
parallel composition, etc.), there are really only three types of proof
obligations for us to prove. First, we must prove that the non-trivial command
translations (i.e., for conditionals and while loops) embed correctly in the
Views logic, which is straightforward. Second, we must show that for our
environment subtyping, if $\Gamma<:\Gamma^{\prime}$, then
$\llbracket{\Gamma}\rrbracket\sqsubseteq\llbracket\Gamma^{\prime}\rrbracket$.
And finally, we must prove that each atomic action’s type rule corresponds to
a valid semantic judgment in the Views Framework:

$\forall
m\ldotp\llbracket\alpha\rrbracket(\lfloor\llbracket\Gamma_{1}\rrbracket_{tid}*\\{m\\}\rfloor)\subseteq\lfloor\llbracket\Gamma_{2}\rrbracket_{tid}*\mathcal{R}(\\{m\\})\rfloor$

The use of $*$ validates the frame rule and makes this obligation akin to an
interference-tolerant version of the small footprint property from traditional
separation logics [34, 5].

######  Lemma 9 (Axiom of Soundness for Atoms)

For each axiom, $\Gamma_{1}\vdash_{\textsf{RMO}}\alpha\dashv\Gamma_{2}$, we
must show

$\forall
m\ldotp\llbracket\alpha\rrbracket(\lfloor\llbracket\Gamma_{1}\rrbracket_{tid}*\\{m\\}\rfloor)\subseteq\lfloor\llbracket\Gamma_{2}\rrbracket_{tid}*\mathcal{R}(\\{m\\})\rfloor$

###### Proof

By case analysis on the atomic action $\alpha$ followed by inversion on typing
derivation. All the cases proved as different lemmas in Section 0.A.3.

Type soundness proceeds according to the requirements of the Views Framework,
primarily embedding each type judgment into the Views logic:

######  Lemma 10 (Views Embedding for Read-Side)

$\forall\Gamma,C,\Gamma^{\prime},\mathit{t}\ldotp\Gamma\vdash_{R}C\dashv\Gamma^{\prime}\Rightarrow\llbracket\Gamma\rrbracket_{\mathit{t}}\cap\llbracket{R}\rrbracket_{t}\vdash\llbracket
C\rrbracket_{\mathit{t}}\dashv\llbracket\Gamma^{\prime}\rrbracket_{\mathit{t}}\cap\llbracket{R}\rrbracket_{t}$

###### Proof

Proof is similar to the one for Lemma 11 except the denotation for type system
definition is $\llbracket R\rrbracket_{t}=\\{\\{((s,h,l,rt,R,B),O,U,T,F)|t\in
R\\}$ which shrinks down the set of all logical states to the one that can
only be defined by types(rcuItr) in read type system.

######  Lemma 11 (Views Embedding for Write-Side)

$\forall\Gamma,C,\Gamma^{\prime},\mathit{t}\ldotp\Gamma\vdash_{M}C\dashv\Gamma^{\prime}\Rightarrow\llbracket\Gamma\rrbracket_{\mathit{t}}\cap\llbracket{M}\rrbracket_{t}\vdash\llbracket
C\rrbracket_{\mathit{t}}\dashv\llbracket\Gamma^{\prime}\rrbracket_{\mathit{t}}\cap\llbracket{M}\rrbracket_{t}$

###### Proof

Induction on derivation of $\Gamma\vdash_{M}C\dashv\Gamma^{\prime}$ and then
inducting on the type of first element of the environment. For the nonempty
case, $\Gamma^{\prime\prime},x:T$ we do case analysis on $T$. Type environment
for write-side actions includes only: $\textsf{rcuItr}\,\rho\,\mathcal{N}$,
undef, rcuFresh, unlinked and freeable. Denotations of these types include the
constraint $t=l$ and other constraints specific to the type’s denotation. The
set of logical state defined by the denotation of the type is _subset_ of
intersection of the set of logical states defined by $\llbracket
M\rrbracket_{t}\cap\llbracket x:T\rrbracket_{t}$ which shrinks down the
logical states defined by $\llbracket
M\rrbracket_{t}=\\{((s,h,l,rt,R,B),O,U,T,F)|t=l\\}$ to the set of logical
states defined by denotation $\llbracket x:T\rrbracket_{t}$.

Because the intersection of the environment denotation with the denotations
for the different critical sections remains a valid view, the Views Framework
provides most of this proof for free, given corresponding lemmas for the
_atomic actions_ $\alpha$:

$\begin{array}[]{l}\forall\alpha,\Gamma_{1},\Gamma_{2}\ldotp\Gamma_{1}\vdash_{R}\alpha\dashv\Gamma_{2}\Rightarrow\\\
\quad\forall
m\ldotp\llbracket\alpha\rrbracket(\lfloor\llbracket\Gamma_{1}\rrbracket_{\textsf{R},tid}*\\{m\\}\rfloor)\subseteq\lfloor\llbracket\Gamma_{2}\rrbracket_{\textsf{R},tid}*\mathcal{R}(\\{m\\})\rfloor\end{array}$
$\begin{array}[]{l}\forall\alpha,\Gamma_{1},\Gamma_{2}\ldotp\Gamma_{1}\vdash_{M}\alpha\dashv\Gamma_{2}\Rightarrow\\\
\quad\forall
m\ldotp\llbracket\alpha\rrbracket(\lfloor\llbracket\Gamma_{1}\rrbracket_{\textsf{M},tid}*\\{m\\}\rfloor)\subseteq\lfloor\llbracket\Gamma_{2}\rrbracket_{\textsf{M},tid}*\mathcal{R}(\\{m\\})\rfloor\end{array}$

$\alpha$ ranges over any atomic command, such as a field access or variable
assignment.

Denoting a type environment $\llbracket\Gamma\rrbracket_{\mathsf{M},tid}$,
unfolding the definition one step, is merely
$\llbracket\Gamma\rrbracket_{tid}\cap\llbracket\mathsf{M}\rrbracket_{tid}$. In
the type system for write-side critical sections, this introduces extra
boilerplate reasoning to prove that each action preserves lock ownership. To
simplify later cases of the proof, we first prove this convenient lemma.

######  Lemma 12 (Write-Side Critical Section Lifting)

For each $\alpha$ whose semantics does not affect the write lock, if

$\forall
m\ldotp\llbracket\alpha\rrbracket(\lfloor\llbracket\Gamma_{1}\rrbracket_{tid}*\\{m\\}\rfloor)\subseteq\lfloor\llbracket\Gamma_{2}\rrbracket_{tid}*\mathcal{R}(\\{m\\})\rfloor$

then

$\forall
m\ldotp\llbracket\alpha\rrbracket(\lfloor\llbracket\Gamma_{1}\rrbracket_{\textsf{M},tid}*\\{m\\}\rfloor)\subseteq\lfloor\llbracket\Gamma_{2}\rrbracket_{\textsf{M},tid}*\mathcal{R}(\\{m\\})\rfloor$

###### Proof

Each of these shared actions $\alpha$ preserves the lock component of the
physical state, the only component constrained by
$\llbracket-\rrbracket_{M,tid}$ beyond $\llbracket-\rrbracket_{tid}$. For the
read case, we must prove from the assumed subset relationship that for an
aritrary $m$:

$\llbracket\alpha\rrbracket(\lfloor\llbracket\Gamma_{1}\rrbracket_{tid}\cap\llbracket\textsf{M}\rrbracket_{tid}*\\{m\\}\rfloor)\subseteq\lfloor\llbracket\Gamma_{2}\rrbracket_{tid}\cap\llbracket\textsf{M}\rrbracket_{tid}*\mathcal{R}(\\{m\\})\rfloor$

By assumption, transitivity of $\subseteq$, and the semantics for the possible
$\alpha$s, the left side of this containment is already a subset of

$\lfloor\llbracket\Gamma_{2}\rrbracket_{tid}*\mathcal{R}(\\{m\\})\rfloor$

What remains is to show that the intersection with
$\llbracket\mathsf{M}\rrbracket_{tid}$ is preserved by the atomic action. This
follows from the fact that none of the possible $\alpha$s modifies the global
lock.

###  0.A.2 Complete Memory Axioms

  1. 1.

Ownership invariant in Figure 16 invariant asserts that none of the heap nodes
can be observed as undefined by any of those threads.

$\textbf{OW}(\sigma,O,U,T,F)=\left\\{\begin{array}[]{ll}&\forall_{o,o^{\prime}f,f^{\prime}}\ldotp\sigma.h(o,f)=v\land\sigma.h(o^{\prime},f^{\prime})=v\\\
&\land v\in\textsf{OID}\land\textsf{FType}(f)=\textsf{RCU}\implies\\\
&\left\\{\begin{array}[]{cl}&o=o^{\prime}\land f=f^{\prime}\\\
&\lor\textsf{unlinked}\in O(o)\\\ &\lor\textsf{unlinked}\in O(o^{\prime})\\\
&\lor\textsf{freeable}\in O(o)\\\ &\lor\textsf{freeable}\in O(o^{\prime})\\\
&\lor\textsf{fresh}\in O(o))\\\ &\lor\textsf{fresh}\in
O(o^{\prime})\end{array}\right.\end{array}\right.$
Figure 16: Ownership

  2. 2.

Reader-Writer-Iterators-CoExistence invariant in Figure 17 asserts that if a
heap location is not undefined then all reader threads and the writer thread
can observe the heap location as iterator or the writer thread can observe
heap as fresh, unlinked or freeable.

$\textbf{RWOW}(\sigma,O,U,T,F)=\left\\{\begin{array}[]{ll}\forall
x,tid,o\ldotp\sigma.s(x,tid)=o\land(x,tid)\notin U\implies\\\
\left\\{\begin{array}[]{ll}&\textsf{iterator }\,tid\in O(o)\\\
&\lor(\sigma.l=tid\land(\textsf{unlinked}\in O(o))\\\
&\lor(\sigma.l=tid\land\textsf{freeable}\in O(o)))\\\
&\lor(\sigma.l=tid\land\textsf{fresh}\in
O(o))\end{array}\right.\end{array}\right.$
Figure 17: Reader-Writer-Iterator-Coexistence-Ownership

  3. 3.

Alias-With-Root invariant in Figure 18 asserts that the unique root location
can only be aliased with thread local references through which the unique root
location is observed as iterator.

$\textbf{AWRT}(\sigma,O,U,T,F)=\left\\{(\forall_{y,tid}\ldotp
h^{*}(\sigma.rt,\epsilon)=s(y,tid)\implies\textsf{iterator}\,tid\in
O(s(y,tid)))\right.$
Figure 18: Alias with Unique Root

  4. 4.

Iterators-Free-List invariant in Figure 19 asserts that if a heap location is
observed as iterator and it is the free list then the observer thread is in
the set of bounding threads.

$\textbf{IFL}(\sigma,O,U,T,F)=\left\\{\forall
tid,o\ldotp\textsf{iterator}\,tid\in O(o)\land\forall_{T^{\prime}\subseteq
T}\ldotp\sigma.F([o\mapsto T^{\prime}])\implies tid\in T^{\prime}\right.$
Figure 19: Iterators-Free-List

  5. 5.

Unlinked-Reachability invariant in Figure 20 asserts that if a heap node is
observed as unlinked then all heap locations from which you can reach to the
unlinked one are also unlinked or in the free list.

$\textbf{ULKR}(\sigma,O,U,T,F)=\left\\{\begin{array}[]{ll}\forall
o\ldotp\textsf{unlinked}\in O(o)\implies\\\ \left\\{\begin{array}[]{cl}\forall
o^{\prime},f^{\prime}\ldotp\sigma.h(o^{\prime},f^{\prime})=o\implies\\\
\left\\{\begin{array}[]{cl}&\textsf{unlinked}\in O(o^{\prime})\lor\\\
&\textsf{freeable}\in
O(o^{\prime})\end{array}\right.\end{array}\right.\end{array}\right.$
Figure 20: Unlinked-Reachability

  6. 6.

Free-List-Reachability invariant in Figure 21 asserts that if a heap location
is in the free list then all heap locations from which you can reach to the
one in the free list are also in the free list.

$\textbf{FLR}(\sigma,O,U,T,F)=\left\\{\begin{array}[]{ll}\forall o\ldotp
F([o\mapsto T])\implies\\\ \left\\{\begin{array}[]{cl}\forall
o^{\prime},f^{\prime}\ldotp\sigma.h(o^{\prime},f^{\prime})=o\implies\\\
\left\\{\begin{array}[]{cl}&\exists_{T^{\prime}\subseteq T}\ldotp
F([o^{\prime}\mapsto
T^{\prime}])\end{array}\right.\end{array}\right.\end{array}\right.$
Figure 21: Free-List-Reachability

  7. 7.

Writer-Unlink invariant in Figure 22 asserts that the writer thread cannot
observe a heap location as unlinked.

$\textbf{WULK}(\sigma,O,U,T,F)=\left\\{\begin{array}[]{ll}\forall
o\ldotp\textsf{iterator}\,\sigma.l\in O(o)\implies\textsf{unlinked}\notin
O(o)\land\textsf{freeable}\notin O(o)\land\textsf{undef}\notin
O(o)\end{array}\right.$
Figure 22: Writer-Unlink

  8. 8.

Fresh-Reachable invariant in Figure 23 asserts that there exists no heap
location that can reach to a freshly allocated heap location together with
fact on nonexistence of aliases to it.

$\textbf{FR}(\sigma,O,U,T,F)=\begin{array}[]{ll}\forall_{tid,x,o}\ldotp(\sigma.s(x,tid)=o\land\textsf{fresh}\in
O(o))\implies\\\
\left\\{\begin{array}[]{cl}(\forall_{y,o^{\prime},f^{\prime},tid^{\prime}}.(h(o^{\prime},f^{\prime})\neq
o)\lor(s(y,tid)\neq o\\\ \lor(tid^{\prime}\neq tid\implies
s(y,tid^{\prime})\neq o))\end{array}\right\\}\end{array}$ Figure 23: Fresh-
Reachable

  9. 9.

Fresh-Writer invariant in Figure 24 asserts that heap allocation can be done
only by writer thread.

$\textbf{WF}(\sigma,O,U,T,F)=\forall_{tid,x,o}\ldotp(\sigma.s(x,tid)=o\land\textsf{fresh}\in
O(o))\implies tid=\sigma.l$ Figure 24: Fresh-Writer

  10. 10.

Fresh-Not-Reader invariant in Figure 25 asserts that a heap location allocated
freshly cannot be observed as unlinked or iterator.

$\textbf{FNR}(\sigma,O,U,T,F)=\forall_{o}\ldotp(\textsf{fresh}\in
O(o))\implies(\forall_{x,tid}\ldotp\textsf{iterator}\,tid\notin
O(o))\land\textsf{unlinked}\notin O(o)$
Figure 25: Fresh-Not-Reader

  11. 11.

Fresh-Points-Iterator invariant in Figure 26 states that any field of fresh
allocated object can only be set to point heap node which can be observed as
iterator (not unlinked or freeable). This invariant captures the fact
$\mathcal{N}=\mathcal{N}^{\prime}$ asserted in the type rule for fresh node
linking(T-Replace).

$\textbf{FPI}(\sigma,O,U,T,F)=\forall_{o}\ldotp(\textsf{fresh}\in
O(o)\land\exists_{f,o^{\prime}}\ldotp
h(o,f)=o^{\prime})\implies(\forall_{tid}\ldotp\textsf{iterator}\,tid\in
O(o^{\prime}))$ Figure 26: Fresh-Points-Iterator

  12. 12.

Writer-Not-Reader invariant in Figure 27 asserts that a writer thread
identifier can not be a reader thread identifier.

$\textbf{WNR}(\sigma,O,U,T,F)=\left\\{\begin{array}[]{ll}\sigma.l\notin\sigma.R\end{array}\right.$
Figure 27: Writer-Not-Reader

  13. 13.

Readers-Iterator-Only invariant in the Figure 28 asserts that a reader threads
can only make iterator observation on a heap location.

$\textbf{RITR}(\sigma,O,U,T,F)=\left\\{\begin{array}[]{ll}\forall_{tid\in\sigma.R,o}\ldotp\textsf{iterator}\,tid\in
O(o)\end{array}\right.$
Figure 28: Readers-Iterator-Only

  14. 14.

Readers-In-Free-List invariant in Figure 29 asserts that for any mapping from
a location to a set of threads in the free list we know the fact that this set
of threads is a subset of bounding threads( which itself is subset of reader
threads).

$\textbf{RINFL}(\sigma,O,U,T,F)=\left\\{\begin{array}[]{ll}\forall_{o}\ldotp
F([o\mapsto T])\implies T\subseteq\sigma.B\end{array}\right.$
Figure 29: Readers-In-Free-List

  15. 15.

Heap-Domain invariant in the Figure 30 defines the domain of the heap.

$\textbf{HD}(\sigma,O,U,T,F)=\forall_{o,f^{\prime},o^{\prime}}\ldotp\sigma.h(o,f)=o^{\prime}\implies
o^{\prime}\in dom(\sigma.h)$ Figure 30: Heap-Domain

  16. 16.

Unique-Root invariant in Figure 31 asserts that a heap location which is
observed as root has no incoming edges from any nodes in the domain of the
heap and all nodes accessible from root is is observed as iterator. This
invariant is part of enforcement for _acyclicity_.

$\textbf{UNQRT}(\sigma,O,U,T,F)=\left\\{\begin{array}[]{ll}\forall_{\rho\neq\epsilon}\ldotp\textsf{iterator}\,tid\in
O(h^{*}(\sigma.rt,\rho)\\\
\land\lnot(\exists_{f^{\prime}}\ldotp\sigma.rt=h(h^{*}(\sigma.rt,\rho),f^{\prime}))\end{array}\right\\}$
Figure 31: Unique-Root

  17. 17.

Unique-Reachable invariant in Figure 32 asserts that every node is reachable
from root node with an unique path. This invariant is a part of
acyclicity(tree structure) enforcement on the heap layout of the data
structure.

$\textbf{UNQR}(\sigma,O,U,T,F)=\left\\{\begin{array}[]{ll}\forall_{\rho,\rho^{\prime}}\ldotp
h^{*}(\sigma.rt,\rho)\neq
h^{*}(\sigma.rt,\rho^{\prime})\implies\rho\neq\rho^{\prime}\end{array}\right.$
Figure 32: Unique-Reachable

Each of these memory invariants captures different aspects of validity of the
memory under RCU setting, $\textsf{WellFormed}(\sigma,O,U,T,F)$, is defined as
conjunction of all memory axioms.

###  0.A.3 Soundness Proof of Atoms

In this section, we do proofs to show the soundness of each type rule for each
atomic actions.

######  Lemma 13 (Unlink)

$\displaystyle\llbracket
x.f_{1}:=r\rrbracket(\lfloor\llbracket\Gamma,\,x:\mathsf{rcuItr}\,\rho\,\mathcal{N}([f_{1}\rightharpoonup
z]),z:\mathsf{rcuItr}\,\rho^{\prime}\,\mathcal{N}^{\prime}([f_{2}\rightharpoonup
r]),\;r:\mathsf{rcuItr}\,\rho^{\prime\prime}\,\mathcal{N}^{\prime\prime}\rrbracket_{M,tid}*\\{m\\}\rfloor)\subseteq$
$\displaystyle\lfloor\llbracket\Gamma,\,x:\mathsf{rcuItr}\,\rho\,\mathcal{N}(f_{1}\rightharpoonup
z\setminus
r),\;z:\mathsf{unlinked},\;r:\mathsf{rcuItr}\,\rho^{\prime}\,\mathcal{N}^{\prime\prime}\rrbracket*\mathcal{R}(\\{m\\})\rfloor$

###### Proof

We assume

$\displaystyle\begin{aligned}
(\sigma,O,U,T,F)\,\in&\llbracket\Gamma,\,x:\mathsf{rcuItr}\,\rho\,\mathcal{N},\,z:\mathsf{rcuItr}\,\rho^{\prime}\,\mathcal{N}^{\prime},\\\
&r:\mathsf{rcuItr}\,\rho^{\prime\prime}\,\mathcal{N}^{\prime\prime}\rrbracket_{M,tid}*\\{m\\}\end{aligned}$
(1) $\displaystyle\textsf{WellFormed}(\sigma,O,U,T,F)$ (2)

From assumptions in the type rule of T-UnlinkH we assume that

$\displaystyle\rho.f_{1}=\rho^{\prime}\text{ and
}\rho^{\prime}.f_{2}=\rho^{\prime\prime}\text{ and }\mathcal{N}(f_{1})=z\text{
and }\mathcal{N}^{\prime}(f_{2})=r$ (3) $\displaystyle\forall_{f\in
dom(\mathcal{N}^{\prime})}\ldotp f\neq
f_{2}\implies\mathcal{N}^{\prime}(f)=\textsf{null}$ (4)
$\displaystyle\begin{array}[]{l}\footnotesize\forall_{n\in\Gamma,m,\mathcal{N}^{\prime\prime\prime},p^{\prime\prime\prime},f}\ldotp
n:\textsf{rcuItr}\,\rho^{\prime\prime\prime}\,\mathcal{N}^{\prime\prime\prime}([f\rightharpoonup
m])\implies\left\\{\begin{array}[]{l}((\neg\mathsf{MayAlias}(\rho^{\prime\prime\prime},\\{\rho,\rho^{\prime},\rho^{\prime\prime}\\}))\@arraycr\land(m\not\in\\{z,r\\}))\@arraycr\land(\forall_{\rho^{\prime\prime\prime\prime}\neq\epsilon}\ldotp\neg\mathsf{MayAlias}(\rho^{\prime\prime\prime},\rho^{\prime\prime}.\rho^{\prime\prime\prime\prime}))\end{array}\right.\end{array}$
(7)

We split the composition in 1 as

$\displaystyle\begin{aligned}
(\sigma_{1},O_{1},U_{1},T_{1},F_{1})\in&\llbracket\Gamma,\,x:\mathsf{rcuItr}\,\rho\,\mathcal{N},\,z:\mathsf{rcuItr}\,\rho^{\prime}\,\mathcal{N}^{\prime},\\\
&r:\mathsf{rcuItr}\,\rho^{\prime\prime}\,\mathcal{N}^{\prime\prime}\rrbracket_{M,tid}\end{aligned}$
(8) $\displaystyle(\sigma_{2},O_{2},U_{2},T_{2},F_{2})=m$ (9)
$\displaystyle\sigma_{1}\bullet_{s}\sigma_{2}=\sigma$ (10) $\displaystyle
O_{1}\bullet_{O}O_{2}=O$ (11) $\displaystyle U_{1}\cup U_{2}=U$ (12)
$\displaystyle T_{1}\cup T_{2}=T$ (13) $\displaystyle F_{1}\uplus F_{2}=F$
(14) $\displaystyle\textsf{WellFormed}(\sigma_{1},O_{1},U_{1},T_{1},F_{1})$
(15) $\displaystyle\textsf{WellFormed}(\sigma_{2},O_{2},U_{2},T_{2},F_{2})$
(16)

We must show
$\exists_{\sigma^{\prime}_{1},\sigma^{\prime}_{2},O^{\prime}_{1},O^{\prime}_{2},U^{\prime}_{1},U^{\prime}_{2},T^{\prime}_{1},T^{\prime}_{2},F^{\prime}_{1},F^{\prime}_{2}}$
such that

$\displaystyle\begin{aligned}
(\sigma_{1}^{\prime},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})\in\llbracket\Gamma,\,x:\mathsf{rcuItr}\,\rho\,\mathcal{N}([f_{1}\rightharpoonup
r]),\,z:\mathsf{unlinked},r:\mathsf{rcuItr}\,\rho^{\prime}\,\mathcal{N}^{\prime\prime}\rrbracket_{M,tid}\end{aligned}$
(17) $\displaystyle\mathcal{N}(f_{1})=r$ (19)
$\displaystyle(\sigma_{2}^{\prime},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})\in\mathcal{R}(\\{m\\})$
(20)
$\displaystyle\sigma^{\prime}_{1}\bullet_{s}\sigma^{\prime}_{2}=\sigma^{\prime}$
(21) $\displaystyle O^{\prime}_{1}\bullet_{O}O^{\prime}_{2}=O^{\prime}$ (22)
$\displaystyle U^{\prime}_{1}\cup U^{\prime}_{2}=U^{\prime}$ (23)
$\displaystyle T^{\prime}_{1}\cup T^{\prime}_{2}=T^{\prime}$ (24)
$\displaystyle F^{\prime}_{1}\uplus F^{\prime}_{2}=F^{\prime}$ (25)
$\displaystyle\textsf{WellFormed}(\sigma_{1}^{\prime},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})$
(26)
$\displaystyle\textsf{WellFormed}(\sigma_{2}^{\prime},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$
(27)

We also know from operational semantics that the machine state has changed as

$\displaystyle\sigma_{1}^{\prime}=\sigma_{1}[h(s(x,tid),f_{1})\mapsto
s(r,tid)]$ (28)

and 28 is determined by operational semantics.

The only change in the observation map is on $s(y,tid)$ from
$\textsf{iterator}\;tid$ to unliked

$\displaystyle
O^{\prime}_{1}=O_{1}(s(y,tid))[\textsf{iterator}\;tid\mapsto\textsf{unlinked}]$
(29)

30 follows from 1

$\displaystyle T_{1}=\\{tid\\}\text{ and }tid=\sigma.l$ (30)

$\sigma^{\prime}_{1}$ is determined by operational semantics. The undefined
map, free list and $T_{1}$ need not change so we can pick $U^{\prime}_{1}$ as
$U_{1}$, $T^{\prime}_{1}$ as $T_{1}$ and $F^{\prime}_{1}$ as $F_{1}$. Assuming
8 and choices on maps makes
$(\sigma_{1}^{\prime},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})$
in denotation

$\llbracket\Gamma,\,x:\mathsf{rcuItr}\,\rho\,\mathcal{N}([f\rightharpoonup
r]),z:\mathsf{unlinked},r:\mathsf{rcuItr}\,\rho^{\prime}\,\mathcal{N}^{\prime\prime}\rrbracket_{M,tid}$

In the rest of the proof, we prove 26, 27 and show the composition of
$(\sigma^{\prime}_{1},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})$
and
$(\sigma^{\prime}_{2},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$.
To prove 26, we need to show that each of the memory axioms in Section 0.A.2
holds for the state
$(\sigma^{\prime},O^{\prime}_{1},U_{1}^{\prime},T_{1}^{\prime},F^{\prime}_{1})$.

Let $o_{x}$ be $\sigma.s(x,tid)$, $o_{y}$ be $\sigma.s(y,tid)$ and $o_{z}$ be
$\sigma.s(z,tid)$.

###### Case 4

\- UNQR 31 and 32 follow from framing assumption(3-7), denotations of the
precondition(8) and 15.UNQR

$\displaystyle\rho\neq\rho^{\prime}\neq\rho^{\prime\prime}$ (31)

and

$\displaystyle o_{x}\neq o_{y}\neq o_{z}$ (32)

where $o_{x}$, $o_{y}$ and $o_{z}$ are equal to
$\sigma.h^{*}(\sigma.rt,\rho)$, $\sigma.h^{*}(\sigma.rt,\rho,f_{1})$ and
$\sigma.h^{*}(\sigma.rt,\rho.f_{1}.f_{2})$ respectively and
they($o_{x},o_{y},o_{z}$ and $\rho,\rho^{\prime}$) are unique.

We must prove

$\displaystyle h^{\prime*}(\sigma.rt,\rho)\neq
h^{\prime*}(\sigma.rt,\rho.f_{1})\implies\rho\neq\rho.f_{1}$ (33)

to show that uniqueness is preserved.

We know from operational semantics that root has not changed so

$\sigma.rt=\sigma^{\prime}.rt$

From denotations (17) we know that all heap locations reached by following
$\rho$ and $\rho.f_{1}$ are observed as $\textsf{iterator}\,tid$ including the
final reached heap locations($\textsf{iterator}\,tid\in
O^{\prime}_{1}(\sigma^{\prime}.h^{*}(\sigma.rt,\rho))$ and
$\textsf{iterator}\,tid\in
O_{1}^{\prime}(\sigma^{\prime}.h^{*}(\sigma.rt,\rho.f_{1}))$). 19 is
determined directly by operational semantics.

$\textsf{unlinked}\in O^{\prime}_{1}(o_{y})$ follows from 29 and 28 which
makes path $\rho.f_{1}.f_{2}$ invalid(from denotation(17), all heap locations
reaching to $O_{1}^{\prime}(o_{r})$ from root($\sigma.rt$) are observed as
$\textsf{iterator}\,tid$ so this proves that $\textsf{unlinked}\in
O^{\prime}_{1}(o_{y})$) cannot be observed on the path to the $o_{r}$ which
implies that $f_{2}$ cannot be part of the path and uniqueness of the paths to
$o_{x}$ and $o_{r}$ is preserved. So we conclude 34 and 35

$\displaystyle\rho\neq\rho^{\prime}$ (34) $\displaystyle o_{x}\neq o_{y}\neq
o_{z}$ (35)

from which 33 follows.

###### Case 5

\- OW By 15.OW, 28, 29.

###### Case 6

\- RWOW By 15.RWOW, 28 and 29.

###### Case 7

\- IFL By 15.WULK, 15.RINFL, 15.IFL, 29 and choice of $F^{\prime}_{1}$.

###### Case 8

\- FLR By choice of $F^{\prime}_{1}$ and 15.

###### Case 9

\- WULK By 17, 29 and 30.

###### Case 10

\- WF, FPI and FR Trivial.

###### Case 11

\- AWRT By 17.

###### Case 12

\- HD By 26.OW(proved), 15.HD and 28.

###### Case 13

\- WNR By 15.WNR, 28, 29 and 30.

###### Case 14

\- RINFL By 17, 15.RINFL, choice of $F^{\prime}_{1}$ and 28.

###### Case 15

\- ULKR We must prove 36

$\displaystyle\begin{aligned}
\forall_{o^{\prime},f^{\prime}}\ldotp\sigma^{\prime}.h(o^{\prime},f^{\prime})=o_{y}\implies&\textsf{unlinked}\in
O^{\prime}_{1}(o^{\prime})\\\ &\lor(\textsf{freeable}\in
O^{\prime}_{1}(o^{\prime}))\end{aligned}$ (36)

which follows from 17, 15.OW, operational semantics(28) and 29. If
$o^{\prime}$ were observed as iterator then that would conflict with 26.UNQR.

###### Case 16

\- UNQRT: By 15.UNQRT, 29 and 28.

To prove 20 we need to show interference relation

$(\sigma,O_{2},U_{2},T_{2},F_{2})\mathcal{R}(\sigma^{\prime},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$

which by definition means that we must show

$\displaystyle\sigma_{2}.l\in
T_{2}\rightarrow(\sigma_{2}.h=\sigma^{\prime}_{2}.h\land\sigma_{2}.l=\sigma^{\prime}_{2}.l)$
(37) $\displaystyle l\in T_{2}\rightarrow F_{2}=F_{2}^{\prime}$ (38)
$\displaystyle\forall tid,o\ldotp\textsf{iterator}\,tid\in O_{2}(o)\rightarrow
o\in dom(\sigma_{2}.h)$ (39) $\displaystyle\forall
tid,o\ldotp\textsf{iterator}\,tid\in O_{2}(o)\rightarrow o\in
dom(\sigma^{\prime}_{2}.h)$ (40) $\displaystyle O_{2}=O_{2}^{\prime}\land
U_{2}=U_{2}^{\prime}\land
T_{2}=T_{2}^{\prime}\land\sigma_{2}.R=\sigma^{\prime}_{2}.R\land\sigma_{2}.rt=\sigma^{\prime}_{2}.rt$
(41) $\displaystyle\forall x,t\in
T_{2}\ldotp\sigma_{2}.s(x,t)=\sigma^{\prime}_{2}.s(x,t)$ (42)
$\displaystyle\forall tid,o\ldotp\textsf{root}\,tid\in O(o)\rightarrow o\in
dom(h)$ (43) $\displaystyle\forall tid,o\ldotp\textsf{root}\,tid\in
O(o)\rightarrow o\in dom(h^{\prime})$ (44)

To prove all relations (37-42) we assume 30 which is to assume $T_{2}$ as
subset of reader threads. Let $\sigma^{\prime}_{2}$ be $\sigma_{2}$. $O_{2}$
need not change so we pick $O^{\prime}_{2}$ as $O_{2}$. Since $T_{2}$ is
subset of reader threads, we pick $T_{2}$ as $T^{\prime}_{2}$. We pick
$F^{\prime}_{2}$ as $F_{2}$.

37 and 38 follow from 30 and choice of $F_{2}^{\prime}$. 43, 44 and 41 are
determined by choice of $\sigma^{\prime}_{2}$, operational semantic and
choices made on maps related to the assertions.

By assuming 16 we show 27. 39 and 40 follow trivially. 42 follows from choice
of $\sigma^{\prime}_{2}$, 28 and 30.

To prove 22 consider two cases: $O^{\prime}_{1}\cap O^{\prime}_{2}=\emptyset$
and $O^{\prime}_{1}\cap O^{\prime}_{2}\neq\emptyset$. The first case is
trivial. The second case is where we consider

$\textsf{iterator}\,tid\in O^{\prime}_{2}(o_{y})$

We also know from 29 that

$\textsf{unliked}\in O^{\prime}_{1}(o_{y})$

Both together with 11 and 17 proves 22.

To show 21 we consider two cases:
$\sigma^{\prime}_{1}.h\cap\sigma^{\prime}_{2}.h=\emptyset$ and
$\sigma^{\prime}_{1}.h\cap\sigma^{\prime}_{2}.h\neq\emptyset$. First is
trivial. Second follows from 26.OW-HD and 27.OW-HD. 23, 24 and 25 are trivial
by choices on related maps and semantics of composition operations on them.
All compositions shown let us to derive conclusion for
$(\sigma^{\prime}_{1},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})\bullet(\sigma^{\prime}_{2},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$.

######  Lemma 14 (Replace)

$\displaystyle\llbracket
p.f:=n\rrbracket(\lfloor\llbracket\Gamma,\,p:\textsf{rcuItr}\,\rho\,\mathcal{N}\,,r:\textsf{rcuItr}\,\rho^{\prime}\,\mathcal{N}^{\prime}\,,n:\textsf{rcuFresh}\,\mathcal{N}^{\prime\prime}\rrbracket_{M,tid}*\\{m\\}\rfloor)\subseteq$
$\displaystyle\lfloor\llbracket\Gamma\,,p:\textsf{rcuItr}\,\rho\,\mathcal{N}([f\rightharpoonup
r\setminus
n])\,,n:\textsf{rcuItr}\,\rho^{\prime}\,\mathcal{N}^{\prime\prime}\,,r:\textsf{unlinked}\rrbracket*\mathcal{R}(\\{m\\})\rfloor$

###### Proof

We assume

$\displaystyle\begin{aligned}
(\sigma,O,U,T,F)\,\in&\llbracket\Gamma,\,p:\textsf{rcuItr}\,\rho\,\mathcal{N}\,,r:\textsf{rcuItr}\,\rho^{\prime}\,\mathcal{N}^{\prime}\,,n:\textsf{rcuFresh}\,\mathcal{N}^{\prime\prime}\rrbracket_{M,tid}*\\{m\\}\end{aligned}$
(45) $\displaystyle\textsf{WellFormed}(\sigma,O,U,T,F)$ (46)

From assumptions in the type rule of T-Replace we assume that

$\displaystyle\textsf{FV}(\Gamma)\cap\\{p,r,n\\}=\emptyset$ (47)
$\displaystyle\rho.f=\rho^{\prime}\text{ and }\mathcal{N}(f)=r$ (48)
$\displaystyle\mathcal{N}^{\prime}=\mathcal{N}^{\prime\prime}$ (49)
$\displaystyle\begin{aligned}
\forall_{x\in\Gamma,\mathcal{N}^{\prime\prime\prime},\rho^{\prime\prime},f^{\prime},y}\ldotp(x:\textsf{rcuItr}\,\rho^{\prime\prime}\,\mathcal{N}^{\prime\prime\prime}([f^{\prime}\rightharpoonup
y]))\implies(\neg\mathsf{MayAlias}(\rho^{\prime\prime},\\{\rho,\rho^{\prime}\\})\land(y\neq
o))\end{aligned}$ (50)

We split the composition in 45 as

$\displaystyle\begin{aligned}
(\sigma_{1},O_{1},U_{1},T_{1},F_{1})\in&\llbracket\Gamma,\,p:\textsf{rcuItr}\,\rho\,\mathcal{N}\,,r:\textsf{rcuItr}\,\rho^{\prime}\,\mathcal{N}^{\prime}\,,n:\textsf{rcuFresh}\,\mathcal{N}^{\prime\prime}\rrbracket_{M,tid}\end{aligned}$
(51) $\displaystyle(\sigma_{2},O_{2},U_{2},T_{2},F_{2})=m$ (52) $\displaystyle
O_{1}\bullet_{O}O_{2}=O$ (53)
$\displaystyle\sigma_{1}\bullet_{s}\sigma_{2}=\sigma$ (54) $\displaystyle
U_{1}\cup U_{2}=U$ (55) $\displaystyle T_{1}\cup T_{2}=T$ (56) $\displaystyle
F_{1}\uplus F_{2}=F$ (57)
$\displaystyle\textsf{WellFormed}(\sigma_{1},O_{1},U_{1},T_{1},F_{1})$ (58)
$\displaystyle\textsf{WellFormed}(\sigma_{2},O_{2},U_{2},T_{2},F_{2})$ (59)

We must show
$\exists_{\sigma^{\prime}_{1},\sigma^{\prime}_{2},O^{\prime}_{1},O^{\prime}_{2},U^{\prime}_{1},U^{\prime}_{2},T^{\prime}_{1},T^{\prime}_{2},F^{\prime}_{1},F^{\prime}_{2}}$
such that

$\displaystyle\begin{aligned}
(\sigma_{1}^{\prime},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})\in\llbracket
p:\textsf{rcuItr}\,\rho\,\mathcal{N}\,,n:\textsf{rcuItr}\,\rho^{\prime}\,\mathcal{N}^{\prime\prime}\,,r:\textsf{unlinked}\,,\Gamma\rrbracket_{M,tid}\end{aligned}$
(60) $\displaystyle\mathcal{N}(f)=n$ (61)
$\displaystyle(\sigma_{2}^{\prime},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})\in\mathcal{R}(\\{m\\})$
(62) $\displaystyle O^{\prime}_{1}\bullet_{O}O^{\prime}_{2}=O^{\prime}$ (63)
$\displaystyle\sigma^{\prime}_{1}\bullet_{s}\sigma^{\prime}_{2}=\sigma^{\prime}$
(64) $\displaystyle U^{\prime}_{1}\cup U^{\prime}_{2}=U^{\prime}$ (65)
$\displaystyle T^{\prime}_{1}\cup T^{\prime}_{2}=T^{\prime}$ (66)
$\displaystyle F^{\prime}_{1}\uplus F^{\prime}_{2}=F^{\prime}$ (67)
$\displaystyle\textsf{WellFormed}(\sigma_{1}^{\prime},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})$
(68)
$\displaystyle\textsf{WellFormed}(\sigma_{2}^{\prime},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$
(69)

We also know from operational semantics that the machine state has changed as

$\displaystyle\sigma_{1}^{\prime}=\sigma_{1}[h(s(p,tid),f)\mapsto s(n,tid)]$
(70)

61 is determined directly from operational semantics.

We know that changes in observation map are

$\displaystyle
O^{\prime}_{1}=O_{1}(s(r,tid))[\textsf{iterator}\;tid\mapsto\textsf{unlinked}]$
(71)

and

$\displaystyle
O^{\prime}_{1}=O_{1}(s(n,tid))[\textsf{fresh}\mapsto\textsf{iterator}\,tid]$
(72)

73 follows from 45

$\displaystyle T_{1}=\\{tid\\}\text{ and }tid=\sigma.l$ (73)

Let $T^{\prime}_{1}$ be $T_{1}$, $F^{\prime}_{1}$ be $F_{1}$ and
$\sigma^{\prime}_{1}$ be determined by operational semantics. The undefined
map need not change so we can pick $U^{\prime}_{1}$ as $U_{1}$. Assuming 51
and choices on maps makes
$(\sigma_{1}^{\prime},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1})$ in
denotation

$\llbracket p:\textsf{rcuItr}\,\rho\,\mathcal{N}(f\rightharpoonup r\setminus
n)\,,n:\textsf{rcuItr}\,\rho^{\prime}\,\mathcal{N}^{\prime\prime}\,,r:\textsf{unlinked}\,,\Gamma\rrbracket_{M,tid}$

In the rest of the proof, we prove 68, 69 and show the composition of
$(\sigma^{\prime}_{1},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})$
and
$(\sigma^{\prime}_{2},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$.
To prove 68, we need to show that each of the memory axioms in Section 0.A.2
holds for the state
$(\sigma^{\prime},O^{\prime}_{1},U_{1}^{\prime},T_{1}^{\prime},F^{\prime}_{1})$.

###### Case 17

\- UNQR Let $o_{p}$ be $\sigma.s(p,tid)$, $o_{r}$ be $\sigma.s(r,tid)$ and
$o_{n}$ be $\sigma.s(n,tid)$. 73 and 75 follow from framing assumption(47-50),
denotations of the precondition(51), 15.FR and 58.UNQR

$\displaystyle\rho\neq\rho.f\neq\forall_{\mathcal{N}^{\prime}([f_{i}\rightharpoonup
x_{i}])}\ldotp\rho.f.f_{i}$ (74)

and

$\displaystyle o_{p}\neq o_{r}\neq o_{n}\neq o_{i}\text{ where
}o_{i}=h(o_{r},f_{i})$ (75)

where $o_{p}$, $o_{r}$ are $\sigma.h^{*}(\sigma.rt,\rho)$,
$\sigma.h^{*}(\sigma.rt,\rho.f)$ respectively and they(heap locations in 75
and paths in 74) are unique(From 58.FR, we assume that there exists no field
alias/path alias to heap location freshly allocated $o_{n}$).

We must prove

$\displaystyle\rho\neq\rho.f\neq\rho.f.f_{i}\iff\sigma^{\prime}.h^{*}(\sigma.rt,\rho)\neq\sigma^{\prime}.h^{*}(\sigma.rt,\rho.f))\neq\sigma^{\prime}.h^{*}(\sigma.rt,\rho.f.f_{i}))$
(76)

We know from operational semantics that root has not changed so

$\sigma.rt=\sigma^{\prime}.rt$

From denotations (60) we know that all heap locations reached by following
$\rho$ and $\rho.f$ are observed as $\textsf{iteartor}\,tid$ including the
final reached heap locations($\textsf{iterator}\,tid\in
O^{\prime}_{1}(\sigma^{\prime}.h^{*}(\sigma.rt,\rho))$,
$\textsf{iterator}\,tid\in
O^{\prime}_{1}(\sigma^{\prime}.h^{*}(\sigma.rt,\rho.f))$ and
$\textsf{iterator}\,tid\in
O^{\prime}_{1}(\sigma^{\prime}.h^{*}(\sigma.rt,\rho.f.f_{i}))$). The
preservation of uniqueness follows from 71, 72, 70 and 58.FR.

from which we conclude 77 and 78

$\displaystyle\rho\neq\rho.f\neq\rho.f.f_{i}$ (77) $\displaystyle o_{p}\neq
o_{n}\neq o_{r}$ (78)

from which 76 follows.

###### Case 18

\- OW By 58.OW, 70, 71 and 72.

###### Case 19

\- RWOW By 58.RWOW, 70, 71 and 72

###### Case 20

\- AWRT Trivial.

###### Case 21

\- IFL By 58.WULK, 71, 72 choice of $F^{\prime}_{1}$ and operational
semantics.

###### Case 22

\- FLR By choice of $F^{\prime}_{1}$ and 58.

###### Case 23

\- FPI By 60.

###### Case 24

\- WULK Determined by operational semantics By 58.WULK, 71, 72 and operational
semantics.

###### Case 25

\- WF and FR Trivial.

###### Case 26

\- HD

###### Case 27

\- WNR By 73 and operational semantics.

###### Case 28

\- RINFL Determined by operational semantics(70) and 58.RINFL.

###### Case 29

\- ULKR We must prove

$\displaystyle\begin{aligned}
\forall_{o^{\prime},f^{\prime}}\ldotp\sigma^{\prime}.h(o^{\prime},f^{\prime})=o_{r}\implies&\textsf{unlinked}\in
O^{\prime}_{1}(o^{\prime})\\\ &\textsf{freeable}\in
O^{\prime}_{1}(o^{\prime})\end{aligned}$ (79)

which follows from 60, 58.OW and determined by operational semantics(70), 71,
72. If $o^{\prime}$ were observed as iterator then that would conflict with
68.UNQR.

###### Case 30

\- UNQRT By 58.UNQRT, 71, 72 and 70.

To prove 62, we need to show interference relation

$(\sigma,O_{2},U_{2},T_{2},F_{2})\mathcal{R}(\sigma^{\prime},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$

which by definition means that we must show

$\displaystyle\sigma_{2}.l\in
T_{2}\rightarrow(\sigma_{2}.h=\sigma^{\prime}_{2}.h\land\sigma_{2}.l=\sigma^{\prime}_{2}.l)$
(80) $\displaystyle l\in T_{2}\rightarrow F_{2}=F_{2}^{\prime}$ (81)
$\displaystyle\forall tid,o\ldotp\textsf{iterator}\,tid\in O_{2}(o)\rightarrow
o\in dom(\sigma_{2}.h)$ (82) $\displaystyle\forall
tid,o\ldotp\textsf{iterator}\,tid\in O_{2}(o)\rightarrow o\in
dom(\sigma^{\prime}_{2}.h)$ (83) $\displaystyle O_{2}=O_{2}^{\prime}\land
U_{2}=U_{2}^{\prime}\land
T_{2}=T_{2}^{\prime}\land\sigma_{2}.R=\sigma^{\prime}_{2}.R\land\sigma_{2}.rt=\sigma^{\prime}_{2}.rt$
(84) $\displaystyle\forall x,t\in
T_{2}\ldotp\sigma_{2}.s(x,t)=\sigma^{\prime}_{2}.s(x,t)$ (85)
$\displaystyle\forall tid,o\ldotp\textsf{root}\,tid\in O(o)\rightarrow o\in
dom(h)$ (86) $\displaystyle\forall tid,o\ldotp\textsf{root}\,tid\in
O(o)\rightarrow o\in dom(h^{\prime})$ (87)

To prove all relations (80-85) we assume 73 which is to assume $T_{2}$ as
subset of reader threads. Let $\sigma^{\prime}_{2}$ be $\sigma_{2}$,
$F^{\prime}_{2}$ be $F_{2}$. $O_{2}$ need not change so we pick
$O^{\prime}_{2}$ as $O_{2}$. Since $T_{2}$ is subset of reader threads, we
pick $T_{2}$ as $T^{\prime}_{2}$. By assuming 59 we show 69. 82 and 83 follow
trivially. 85 follows from choice of $\sigma^{\prime}_{2}$, 70 and 73.

80 and 81 follow from 73 and choice of $F_{2}^{\prime}$. 84, 86 and 87 are
determined by choice of $\sigma^{\prime}_{2}$, operational semantics and
choices made on maps related to the assertions.

To prove 63 consider two cases: $O^{\prime}_{1}\cap O^{\prime}_{2}=\emptyset$
and $O^{\prime}_{1}\cap O^{\prime}_{2}\neq\emptyset$. The first case is
trivial. The second case is where we consider 88 and 89

$\displaystyle\textsf{iterator}\,tid\in O^{\prime}_{2}(o_{r})$ (88)

From 71 we know that

$\textsf{unliked}\in O^{\prime}_{1}(o_{r})$

Both together with 53 and 60 proves 63.

For case 89

$\displaystyle\textsf{fresh}\in O_{2}(o_{n})$ (89)

From 72 we know that

$\textsf{iterator}\,tid\in O^{\prime}_{1}(o_{n})$

Both together with 53 and 60 proves 63.

To show 64 we consider two cases:
$\sigma^{\prime}_{1}\cap\sigma^{\prime}_{2}=\emptyset$ and
$\sigma^{\prime}_{1}\cap\sigma^{\prime}_{2}\neq\emptyset$. First is trivial.
Second follows from 68.OW-HD and 69.OW-HD. 65, 67 and 66 are trivial by
choices on related maps and semantics of the composition operators for these
maps. All compositions shown let us to derive conclusion for
$(\sigma^{\prime}_{1},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})\bullet(\sigma^{\prime}_{2},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$.

######  Lemma 15 (Insert)

$\displaystyle\llbracket
p.f:=n\rrbracket(\lfloor\llbracket\Gamma,\,p:\textsf{rcuItr}\,\rho\,\mathcal{N}\,,r:\textsf{rcuItr}\,\rho_{1}\,\mathcal{N}_{2}\,,n:\textsf{rcuFresh}\,\mathcal{N}_{1}\rrbracket_{M,tid}*\\{m\\}\rfloor)\subseteq$
$\displaystyle\lfloor\llbracket\Gamma\,,p:\textsf{rcuItr}\,\rho\,\mathcal{N}([f\rightharpoonup
r\setminus
n])\,,n:\textsf{rcuItr}\,\rho_{1}\,\mathcal{N}_{1}\,,r:\textsf{rcuItr}\,\rho_{2}\,\mathcal{N}_{2}\rrbracket*\mathcal{R}(\\{m\\})\rfloor$

###### Proof

We assume

$\displaystyle\begin{aligned}
(\sigma,O,U,T,F)\,\in&\llbracket\Gamma,\,p:\textsf{rcuItr}\,\rho\,\mathcal{N}\,,r:\textsf{rcuItr}\,\rho_{1}\,\mathcal{N}_{2}\,,n:\textsf{rcuFresh}\,\mathcal{N}_{1}\rrbracket_{M,tid}*\\{m\\}\end{aligned}$
(90) $\displaystyle\textsf{WellFormed}(\sigma,O,U,T,F)$ (91)

From assumptions in the type rule of T-Insert we assume that

$\displaystyle\textsf{FV}(\Gamma)\cap\\{p,r,n\\}=\emptyset$ (92)
$\displaystyle\rho.f=\rho_{1}\text{ and }\rho.f_{4}=\rho_{2}\text{ and
}\mathcal{N}(f)=r$ (93)
$\displaystyle\mathcal{N}(f)=\mathcal{N}_{1}(f_{4})\text{ and
}\forall_{f_{2}\in dom(\mathcal{N}_{1})}\ldotp f_{4}\neq
f_{2}\implies\mathcal{N}_{1}(f_{2})=\textsf{null}$ (94)
$\displaystyle\begin{aligned}
\forall_{x\in\Gamma,\mathcal{N}_{3},\rho_{3},f_{1},y}\ldotp(x:\textsf{rcuItr}\,\rho_{3}\,\mathcal{N}_{3}([f_{1}\rightharpoonup
y]))\implies(\forall_{\rho_{4}\neq\epsilon}\ldotp\neg\mathsf{MayAlias}(\rho_{3},\rho.\rho_{4}))\end{aligned}$
(95)

We split the composition in 90 as

$\displaystyle\begin{aligned}
(\sigma_{1},O_{1},U_{1},T_{1},F_{1})\in&\llbracket\Gamma,\,p:\textsf{rcuItr}\,\rho\,\mathcal{N}\,,r:\textsf{rcuItr}\,\rho_{1}\,\mathcal{N}_{2}\,,n:\textsf{rcuFresh}\,\mathcal{N}_{1}\rrbracket_{M,tid}\end{aligned}$
(96) $\displaystyle(\sigma_{2},O_{2},U_{2},T_{2},F_{2})=m$ (97) $\displaystyle
O_{1}\bullet_{O}O_{2}=O$ (98)
$\displaystyle\sigma_{1}\bullet_{s}\sigma_{2}=\sigma$ (99) $\displaystyle
U_{1}\cup U_{2}=U$ (100) $\displaystyle T_{1}\cup T_{2}=T$ (101)
$\displaystyle F_{1}\uplus F_{2}=F$ (102)
$\displaystyle\textsf{WellFormed}(\sigma_{1},O_{1},U_{1},T_{1},F_{1})$ (103)
$\displaystyle\textsf{WellFormed}(\sigma_{2},O_{2},U_{2},T_{2},F_{2})$ (104)

We must show
$\exists_{\sigma^{\prime}_{1},\sigma^{\prime}_{2},O^{\prime}_{1},O^{\prime}_{2},U^{\prime}_{1},U^{\prime}_{2},T^{\prime}_{1},T^{\prime}_{2},F^{\prime}_{1},F^{\prime}_{2}}$
such that

$\displaystyle\begin{aligned}
(\sigma_{1}^{\prime},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})\in\llbracket
p:\textsf{rcuItr}\,\rho\,\mathcal{N}([f\rightharpoonup r\setminus
n])\,,n:\textsf{rcuItr}\,\rho_{1}\,\mathcal{N}_{1}\,,r:\textsf{rcuItr}\,\rho_{2}\,\mathcal{N}_{2}\,,\Gamma\rrbracket_{M,tid}\end{aligned}$
(105)
$\displaystyle(\sigma_{2}^{\prime},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})\in\mathcal{R}(\\{m\\})$
(106) $\displaystyle O^{\prime}_{1}\bullet_{O}O^{\prime}_{2}=O^{\prime}$ (107)
$\displaystyle\sigma^{\prime}_{1}\bullet_{s}\sigma^{\prime}_{2}=\sigma^{\prime}$
(108) $\displaystyle U^{\prime}_{1}\cup U^{\prime}_{2}=U^{\prime}$ (109)
$\displaystyle T^{\prime}_{1}\cup T^{\prime}_{2}=T^{\prime}$ (110)
$\displaystyle F^{\prime}_{1}\uplus F^{\prime}_{2}=F^{\prime}$ (111)
$\displaystyle\textsf{WellFormed}(\sigma_{1}^{\prime},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})$
(112)
$\displaystyle\textsf{WellFormed}(\sigma_{2}^{\prime},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$
(113)

We also know from operational semantics that the machine state has changed as

$\displaystyle\sigma_{1}^{\prime}=\sigma_{1}[h(s(p,tid),f)\mapsto s(n,tid)]$
(114)

We know that changes in observation map are

$\displaystyle
O^{\prime}_{1}=O_{1}(s(n,tid))[\textsf{fresh}\mapsto\textsf{iterator}\;tid]$
(115)

116 follows from 90

$\displaystyle T_{1}=\\{tid\\}\text{ and }tid=\sigma.l$ (116)

Let $T^{\prime}_{1}$ be $T_{1}$, $F^{\prime}_{1}$ be $F_{1}$ and
$\sigma^{\prime}_{1}$ be determined by operational semantics. The undefined
map need not change so we can pick $U^{\prime}_{1}$ as $U_{1}$. Assuming 96
and choices on maps makes
$(\sigma_{1}^{\prime},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1})$ in
denotation

$\llbracket p:\textsf{rcuItr}\,\rho\,\mathcal{N}(f\rightharpoonup r\setminus
n)\,,n:\textsf{rcuItr}\,\rho_{1}\,\mathcal{N}_{1}\,,r:\textsf{rcuItr}\,\rho_{2}\,\mathcal{N}_{2}\,,\Gamma\rrbracket_{M,tid}$

In the rest of the proof, we prove 112, 113 and show the composition of
$(\sigma^{\prime}_{1},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})$
and
$(\sigma^{\prime}_{2},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$.
To prove 112, we need to show that each of the memory axioms in Section 0.A.2
holds for the state
$(\sigma^{\prime},O^{\prime}_{1},U_{1}^{\prime},T_{1}^{\prime},F^{\prime}_{1})$.

Proofs for OW, RWOW, AWRT, IFL, WULK, FLR, FPI, WF, FR, HD, WNR, RINFL and
ULKR. The proof of UNQR is similar to the ones we did for Lemma 14 and Lemma
13 with a simpler fact to prove: we assume framing conditions 92-95 together
with the 103.UNQR and 103.FR which makes 112UNQR trivial.

To prove 106, we need to show interference relation

$(\sigma,O_{2},U_{2},T_{2},F_{2})\mathcal{R}(\sigma^{\prime},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$

which by definition means that we must show

$\displaystyle\sigma_{2}.l\in
T_{2}\rightarrow(\sigma_{2}.h=\sigma^{\prime}_{2}.h\land\sigma_{2}.l=\sigma^{\prime}_{2}.l)$
(117) $\displaystyle l\in T_{2}\rightarrow F_{2}=F_{2}^{\prime}$ (118)
$\displaystyle\forall tid,o\ldotp\textsf{iterator}\,tid\in O_{2}(o)\rightarrow
o\in dom(\sigma_{2}.h)$ (119) $\displaystyle\forall
tid,o\ldotp\textsf{iterator}\,tid\in O_{2}(o)\rightarrow o\in
dom(\sigma^{\prime}_{2}.h)$ (120) $\displaystyle O_{2}=O_{2}^{\prime}\land
U_{2}=U_{2}^{\prime}\land
T_{2}=T_{2}^{\prime}\land\sigma_{2}.R=\sigma^{\prime}_{2}.R\land\sigma_{2}.rt=\sigma^{\prime}_{2}.rt$
(121) $\displaystyle\forall x,t\in
T_{2}\ldotp\sigma_{2}.s(x,t)=\sigma^{\prime}_{2}.s(x,t)$ (122)
$\displaystyle\forall tid,o\ldotp\textsf{root}\,tid\in O(o)\rightarrow o\in
dom(h)$ (123) $\displaystyle\forall tid,o\ldotp\textsf{root}\,tid\in
O(o)\rightarrow o\in dom(h^{\prime})$ (124)

To prove all relations (80-85) we assume 116 which is to assume $T_{2}$ as
subset of reader threads. Let $\sigma^{\prime}_{2}$ be $\sigma_{2}$,
$F^{\prime}_{2}$ be $F_{2}$. $O_{2}$ need not change so we pick
$O^{\prime}_{2}$ as $O_{2}$. Since $T_{2}$ is subset of reader threads, we
pick $T_{2}$ as $T^{\prime}_{2}$. By assuming 104 we show 113. 119 and 120
follow trivially. 122 follows from choice of $\sigma^{\prime}_{2}$ and 116.

117 and 118 follow from 116 and choice of $F_{2}^{\prime}$. 121, 123 and 124
are determined by choice of $\sigma^{\prime}_{2}$, operational semantics and
choices made on maps related to the assertions.

107 follows from assumptions 115, 98 and choice of $O^{\prime}_{2}$ as
$O_{2}$.

To show 108 we consider two cases:
$\sigma^{\prime}_{1}\cap\sigma^{\prime}_{2}=\emptyset$ and
$\sigma^{\prime}_{1}\cap\sigma^{\prime}_{2}\neq\emptyset$. First is trivial.
Second follows from 112.OW-HD and 113.OW-HD. 109, 111 and 110 are trivial by
choices on related maps and semantics of the composition operators for these
maps. All compositions shown let us to derive conclusion for
$(\sigma^{\prime}_{1},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})\bullet(\sigma^{\prime}_{2},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$.

######  Lemma 16 (ReadStack)

$\displaystyle\llbracket
z:=x\rrbracket(\lfloor\llbracket\Gamma\,,z:\\_\,,x:\textsf{rcuItr}\;\;\rho\;\;\mathcal{N}\rrbracket_{M,tid}*\\{m\\}\rfloor)\subseteq$
$\displaystyle\lfloor\llbracket\Gamma\,,x:\textsf{rcuItr}\;\;\rho\;\;\mathcal{N}\,,z:\textsf{rcuItr}\;\;\rho\;\;\mathcal{N}\rrbracket*\mathcal{R}(\\{m\\})\rfloor$

###### Proof

We assume

$\displaystyle\begin{aligned}
(\sigma,O,U,T,F)\,\in&\llbracket\Gamma\,,z:\\_\,,x:\textsf{rcuItr}\;\;\rho\;\;\mathcal{N}\rrbracket_{M,tid}*\\{m\\}\end{aligned}$
(125) $\displaystyle\textsf{WellFormed}(\sigma,O,U,T,F)$ (126)

From the assumption in the type rule of T-ReadS we assume that

$\displaystyle\textsf{FV}(\Gamma)\cap\\{z\\}=\emptyset$ (127)

We split the composition in 125 as

$\displaystyle\begin{aligned}
(\sigma,O_{1},U_{1},T_{1},F_{1})\in&\llbracket\Gamma\,,z:\\_\,,x:\textsf{rcuItr}\;\;\rho\;\;\mathcal{N}\rrbracket_{M,tid}\end{aligned}$
(128) $\displaystyle(\sigma,O_{2},U_{2},T_{2},F_{2})=m$ (129)
$\displaystyle\sigma_{1}\bullet\sigma_{2}=\sigma$ (130) $\displaystyle
O_{1}\bullet_{O}O_{2}=O$ (131) $\displaystyle U_{1}\cup U_{2}=U$ (132)
$\displaystyle T_{1}\cup T_{2}=T$ (133) $\displaystyle F_{1}\uplus F_{2}=F$
(134) $\displaystyle\textsf{WellFormed}(\sigma_{1},O_{1},U_{1},T_{1},F_{1})$
(135) $\displaystyle\textsf{WellFormed}(\sigma_{2},O_{2},U_{2},T_{2},F_{2})$
(136)

We must show
$\exists_{\sigma^{\prime}_{1},\sigma^{\prime}_{2},O^{\prime}_{1},O^{\prime}_{2},U^{\prime}_{1},U^{\prime}_{2},T^{\prime}_{1},T^{\prime}_{2},F^{\prime}_{1},F^{\prime}_{2}}$
such that

$\displaystyle\begin{aligned}
(\sigma^{\prime},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})\in\llbracket\Gamma\,,x:\textsf{rcuItr}\;\;\rho\;\;\mathcal{N}\,,z:\textsf{rcuItr}\;\;\rho\;\;\mathcal{N}\rrbracket_{M,tid}\end{aligned}$
(137)
$\displaystyle(\sigma^{\prime},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})\in\mathcal{R}(\\{m\\})$
(138)
$\displaystyle\sigma^{\prime}_{1}\bullet\sigma^{\prime}_{2}=\sigma^{\prime}$
(139) $\displaystyle O^{\prime}_{1}\bullet_{O}O^{\prime}_{2}=O^{\prime}$ (140)
$\displaystyle U^{\prime}_{1}\cup U^{\prime}_{2}=U^{\prime}$ (141)
$\displaystyle T^{\prime}_{1}\cup T^{\prime}_{2}=T^{\prime}$ (142)
$\displaystyle F^{\prime}_{1}\uplus F^{\prime}_{2}=F^{\prime}$ (143)
$\displaystyle\textsf{WellFormed}(\sigma_{1}^{\prime},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})$
(144)
$\displaystyle\textsf{WellFormed}(\sigma_{2}^{\prime},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$
(145)

Let $s(x,tid)$ be $o_{x}$. We also know from operational semantics that the
machine state has changed as

$\displaystyle\sigma^{\prime}=\sigma[s(z,tid)\mapsto o_{x}]$ (146)

We know that there exists no change in the observation of heap locations

$\displaystyle O^{\prime}_{1}=O_{1}$ (147)

148 follows from 125

$\displaystyle T_{1}=\\{tid\\}\text{ and }tid=\sigma.l$ (148)

$\sigma^{\prime}_{1}$ is determined by operational semantics. The undefined
map, $T_{1}$ and free list need not change so we can pick $U^{\prime}_{1}$ as
$U_{1}$, $T^{\prime}_{1}$ as $T_{1}$ and $F^{\prime}_{1}$ as $F_{1}$. Assuming
128 and choices on maps makes
$(\sigma_{1}^{\prime},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})$
in denotation

$\llbracket\Gamma\,,x:\textsf{rcuItr}\;\;\rho\;\;\mathcal{N}\,,z:\textsf{rcuItr}\;\;\rho\;\;\mathcal{N}\rrbracket_{M,tid}$

In the rest of the proof, we prove 144, 145 and show the composition of
$(\sigma^{\prime}_{1},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})$
and
$(\sigma^{\prime}_{2},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$.
144 follows from 135 trivially.

To prove 138, we need to show interference relation

$(\sigma,O_{2},U_{2},T_{2},F_{2})\mathcal{R}(\sigma^{\prime},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$

which by definition means that we must show

$\displaystyle\sigma_{2}.l\in
T_{2}\rightarrow(\sigma_{2}.h=\sigma^{\prime}_{2}.h\land\sigma_{2}.l=\sigma^{\prime}_{2}.l)$
(149) $\displaystyle l\in T_{2}\rightarrow F_{2}=F_{2}^{\prime}$ (150)
$\displaystyle\forall tid,o\ldotp\textsf{iterator}\,tid\in O_{2}(o)\rightarrow
o\in dom(\sigma_{2}.h)$ (151) $\displaystyle\forall
tid,o\ldotp\textsf{iterator}\,tid\in O_{2}(o)\rightarrow o\in
dom(\sigma^{\prime}_{2}.h)$ (152) $\displaystyle O_{2}=O_{2}^{\prime}\land
U_{2}=U_{2}^{\prime}\land
T_{2}=T_{2}^{\prime}\land\sigma_{2}.R_{2}=\sigma_{2}^{\prime}.R_{2}\land\sigma_{2}.rt=\sigma^{\prime}_{2}.rt$
(153) $\displaystyle\forall x,t\in
T_{2}\ldotp\sigma_{2}.s(x,t)=\sigma^{\prime}_{2}.s(x,t)$ (154)
$\displaystyle\forall tid,o\ldotp\textsf{root}\,tid\in O(o)\rightarrow o\in
dom(h)$ (155) $\displaystyle\forall tid,o\ldotp\textsf{root}\,tid\in
O(o)\rightarrow o\in dom(h^{\prime})$ (156)

To prove all relations (149-154) we assume 148 which is to assume $T_{2}$ as
subset of reader threads. Let $\sigma^{\prime}_{2}$ be $\sigma_{2}$. $O_{2}$
need not change so we pick $O^{\prime}_{2}$ as $O_{2}$. We pick
$F^{\prime}_{2}$ as $F_{2}$. Since $T_{2}$ is subset of reader threads, we
pick $T_{2}$ as $T^{\prime}_{2}$. By assuming 136 we show 145. 151, 152, 155
and 156 follow trivially. 154 follows from choice of $\sigma^{\prime}_{2}$ and
146(determined by operational semantics).

149 and 150 follow from 148 and choice of $F_{2}^{\prime}$. 153, 155 and 156
are determined by choice of $\sigma^{\prime}_{2}$, operational semantics and
choices made on maps related to the assertions.

140-143 are trivial by choices on related maps and semantics of the
composition operators for these maps. 139 follows trivially from 130. All
compositions shown let us to derive conclusion for
$(\sigma^{\prime}_{1},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})\bullet(\sigma^{\prime}_{2},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$
trivial.

######  Lemma 17 (ReadHeap)

$\displaystyle\llbracket
z:=x.f\rrbracket(\lfloor\llbracket\Gamma\,,z:\\_\,,x:\textsf{rcuItr}\,\rho\,\mathcal{N}\rrbracket_{M,tid}*\\{m\\}\rfloor)\subseteq$
$\displaystyle\lfloor\llbracket\Gamma\,,x:\textsf{rcuItr}\,\rho\,\mathcal{N}[f\mapsto
z]\,,z:\textsf{rcuItr}\,\rho^{\prime}\,\mathcal{N}_{\emptyset}\rrbracket*\mathcal{R}(\\{m\\})\rfloor$

###### Proof

We assume

$\displaystyle\begin{aligned}
(\sigma,O,U,T,F)\,\in&\llbracket\Gamma\,,z:\textsf{rcuItr}\,\\_\,,x:\textsf{rcuItr}\;\;\rho\;\;\mathcal{N}\rrbracket_{M,tid}*\\{m\\}\end{aligned}$
(157) $\displaystyle\textsf{WellFormed}(\sigma,O,U,T,F)$ (158)

From the assumption in the type rule of T-ReadH we assume that

$\displaystyle\textsf{FV}(\Gamma)\cap\\{z\\}=\emptyset$ (159)
$\displaystyle\rho.f=\rho^{\prime}$ (160)

We split the composition in 157 as

$\displaystyle\begin{aligned}
(\sigma_{1},O_{1},U_{1},T_{1},F_{1})\in&\llbracket\Gamma\,,z:\textsf{rcuItr}\,\\_\,,x:\textsf{rcuItr}\;\;\rho\;\;\mathcal{N}\rrbracket_{M,tid}\end{aligned}$
(162) $\displaystyle(\sigma_{2},O_{2},U_{2},T_{2},F_{2})=m$ (163)
$\displaystyle\sigma_{1}\bullet\sigma_{2}=\sigma$ (164) $\displaystyle
O_{1}\bullet_{O}O_{2}=O$ (165) $\displaystyle U_{1}\cup U_{2}=U$ (166)
$\displaystyle T_{1}\cup T_{2}=T$ (167) $\displaystyle F_{1}\uplus F_{2}=F$
(168) $\displaystyle\textsf{WellFormed}(\sigma_{1},O_{1},U_{1},T_{1})$ (169)
$\displaystyle\textsf{WellFormed}(\sigma_{2},O_{2},U_{2},T_{2})$ (170)

We must show
$\exists_{\sigma^{\prime}_{1},\sigma^{\prime}_{2},O^{\prime}_{1},O^{\prime}_{2},U^{\prime}_{1},U^{\prime}_{2},T^{\prime}_{1},T^{\prime}_{2},F^{\prime}_{1},F^{\prime}_{2}}$
such that

$\displaystyle\begin{aligned}
(\sigma^{\prime},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F_{1})\in\llbracket\Gamma\,,x:\textsf{rcuItr}\,\rho\,\mathcal{N}[f\mapsto
z]\,,z:\textsf{rcuItr}\,\rho^{\prime}\,\mathcal{N}_{\emptyset}\rrbracket_{M,tid}\end{aligned}$
(171) $\displaystyle\mathcal{N}(f)=z$ (172)
$\displaystyle(\sigma^{\prime},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F_{2})\in\mathcal{R}(\\{m\\})$
(173)
$\displaystyle\sigma^{\prime}_{1}\bullet\sigma^{\prime}_{2}=\sigma^{\prime}$
(174) $\displaystyle O^{\prime}_{1}\bullet_{O}O^{\prime}_{2}=O^{\prime}$ (175)
$\displaystyle U^{\prime}_{1}\cup U^{\prime}_{2}=U^{\prime}$ (176)
$\displaystyle T^{\prime}_{1}\cup T^{\prime}_{2}=T^{\prime}$ (177)
$\displaystyle F^{\prime}_{1}\uplus F^{\prime}_{2}=F^{\prime}$ (178)
$\displaystyle\textsf{WellFormed}(\sigma_{1}^{\prime},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})$
(179)
$\displaystyle\textsf{WellFormed}(\sigma_{2}^{\prime},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$
(180)

Let $h(s(z,tid),f)$ be $o_{z}$. We also know from operational semantics that
the machine state has changed as

$\displaystyle\sigma_{1}^{\prime}=\sigma_{1}[s(x,tid)\mapsto o_{z}]$ (181)

172 is determined directly from operational semantics.

We know that there exists no change in the observation of heap locations

$\displaystyle O^{\prime}_{1}=O_{1}$ (182)

183 follows from 157

$\displaystyle T_{1}=\\{tid\\}\text{ and }tid=\sigma.l$ (183)

$\sigma^{\prime}_{1}$ is determined by operational semantics. The undefined
map, free list and $T_{1}$ need not change so we can pick $U^{\prime}_{1}$ as
$U_{1}$, $F^{\prime}_{1}$ as $F_{1}$ and $T^{\prime}_{1}$ and $T_{1}$.
Assuming 162 and choices on maps makes
$(\sigma_{1}^{\prime},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})$
in denotation

$\llbracket\Gamma\,,x:\textsf{rcuItr}\,\rho\,\mathcal{N}[f\mapsto
z]\,,z:\textsf{rcuItr}\,\rho^{\prime}\,\mathcal{N}_{\emptyset}\rrbracket_{M,tid}$

In the rest of the proof, we prove 179, 180 and show the composition of
$(\sigma^{\prime}_{1},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})$
and
$(\sigma^{\prime}_{2},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$.

To prove 173, we need to show that each of the memory axioms in Section 0.A.2
holds for the state
$(\sigma^{\prime},O^{\prime}_{1},U_{1}^{\prime},T_{1}^{\prime},F^{\prime}_{1})$.

###### Case 31

\- UNQR By 181, 169.UNQR and $\sigma.rt=\sigma.rt^{\prime}$.

###### Case 32

\- OW By 181, 182 and 169.OW

###### Case 33

\- RWOW By 181, 182 and 169.RWOW

###### Case 34

\- AWRT Trivial.

###### Case 35

\- IFL By 171, 169.WULK, 182, choice of $F^{\prime}_{1}$ and operational
semantics.

###### Case 36

\- FLR By operational semantics(181), choice for $F^{\prime}_{1}$ and 169.

###### Case 37

\- WULK By 169.WULK, 182 and operational
semantics($\sigma.l=\sigma.l^{\prime}$).

###### Case 38

\- WF, FNR, FPI and FR Trivial.

###### Case 39

\- HD

###### Case 40

\- WNR By 183 and operational semantics($\sigma.l=\sigma.l^{\prime}$).

###### Case 41

\- RINFL By operational semantics(181) bounding threads have not changed. We
choose $F^{\prime}_{1}$ as $F_{1}$. These two together with 169 shows RINFL.

###### Case 42

\- ULKR Trivial.

###### Case 43

\- UNQRT By 169.UNQRT, 182 and 181.

To prove 173, we need to show interference relation

$(\sigma,O_{2},U_{2},T_{2},F_{2})\mathcal{R}(\sigma^{\prime},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$

which by definition means that we must show

$\displaystyle\sigma_{2}.l\in
T_{2}\rightarrow(\sigma_{2}.h=\sigma^{\prime}_{2}.h\land\sigma_{2}.l=\sigma^{\prime}_{2}.l)$
(184) $\displaystyle l\in T_{2}\rightarrow F_{2}=F_{2}^{\prime}$ (185)
$\displaystyle\forall tid,o\ldotp\textsf{iterator}\,tid\in O_{2}(o)\rightarrow
o\in dom(\sigma_{2}.h)$ (186) $\displaystyle\forall
tid,o\ldotp\textsf{iterator}\,tid\in O_{2}(o)\rightarrow o\in
dom(\sigma^{\prime}_{2}.h)$ (187) $\displaystyle O_{2}=O_{2}^{\prime}\land
U_{2}=U_{2}^{\prime}\land
T_{2}=T_{2}^{\prime}\land\sigma_{2}.R_{2}=\sigma_{2}^{\prime}.R_{2}\land\sigma_{2}.rt=\sigma^{\prime}_{2}.rt$
(188) $\displaystyle\forall x,t\in
T_{2}\ldotp\sigma_{2}.s(x,t)=\sigma^{\prime}_{2}.s(x,t)$ (189)
$\displaystyle\forall tid,o\ldotp\textsf{root}\,tid\in O(o)\rightarrow o\in
dom(h)$ (190) $\displaystyle\forall tid,o\ldotp\textsf{root}\,tid\in
O(o)\rightarrow o\in dom(h^{\prime})$ (191)

To prove all relations (184-189) we assume 183 which is to assume $T_{2}$ as
subset of reader threads. Let $\sigma^{\prime}_{2}$ be $\sigma_{2}$ and
$F^{\prime}_{2}$ be $F_{2}$. $O_{2}$ need not change so we pick
$O^{\prime}_{2}$ as $O_{2}$. Since $T_{2}$ is subset of reader threads, we
pick $T_{2}$ as $T^{\prime}_{2}$. By assuming 170 we show 180. 186 and 187
follows trivially. 189 follows from choice of $\sigma^{\prime}_{2}$ and
181(determined by operational semantics).

184 and 185 follow from 183 and choice of $F_{2}^{\prime}$.188, 190 and 191
are determined by choice of $\sigma^{\prime}_{2}$, operational semantics and
choices made on maps related to the assertions.

175-178 are trivial by choices on related maps and semantics of the
composition operators for these maps. 174 follows trivially from 164. All
compositions shown let us to derive conclusion for
$(\sigma^{\prime}_{1},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})\bullet(\sigma^{\prime}_{2},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$.

######  Lemma 18 (WriteFreshField)

$\displaystyle\llbracket
p.f:=z\rrbracket(\lfloor\llbracket\Gamma,p:\textsf{rcuFresh}\,\mathcal{N}^{\prime}_{f,\emptyset},\;x:\textsf{rcuItr}\;\;\rho\;\;\mathcal{N}\rrbracket_{M,tid}*\\{m\\}\rfloor)\subseteq$
$\displaystyle\lfloor\llbracket\Gamma\,,p:\textsf{rcuFresh}\;\;\mathcal{N}(\cup_{f\rightharpoonup
z})\,,x:\textsf{rcuItr}\,\rho\,\mathcal{N}([f\rightharpoonup
z])\rrbracket*\mathcal{R}(\\{m\\})\rfloor$

###### Proof

We assume

$\displaystyle\begin{aligned}
(\sigma,O,U,T,F)\,\in&\llbracket\Gamma,p:\textsf{rcuFresh}\,\mathcal{N}^{\prime}_{f,\emptyset},\;x:\textsf{rcuItr}\;\;\rho\;\;\mathcal{N}\rrbracket_{M,tid}*\\{m\\}\end{aligned}$
(192) $\displaystyle\textsf{WellFormed}(\sigma,O,U,T,F)$ (193)

From the assumption in the type rule of T-WriteFH we assume that

$\displaystyle z:\textsf{rcuItr}\,\rho.f\,\\_\text{ and
}\mathcal{N}(f)=z\text{ and }f\notin dom(\mathcal{N}^{\prime})$ (194)

We split the composition in 192 as

$\displaystyle\begin{aligned}
(\sigma,O_{1},U_{1},T_{1},F_{1})\in&\llbracket\Gamma,p:\textsf{rcuFresh}\,\mathcal{N}^{\prime}_{f,\emptyset},\;x:\textsf{rcuItr}\;\;\rho\;\;\mathcal{N}\rrbracket_{M,tid}\end{aligned}$
(195) $\displaystyle(\sigma,O_{2},U_{2},T_{2},F_{2})=m$ (196)
$\displaystyle\sigma_{1}\bullet\sigma_{2}=\sigma$ (197) $\displaystyle
O_{1}\bullet_{O}O_{2}=O$ (198) $\displaystyle U_{1}\cup U_{2}=U$ (199)
$\displaystyle T_{1}\cup T_{2}=T$ (200) $\displaystyle F_{1}\uplus F_{2}=F$
(201) $\displaystyle\textsf{WellFormed}(\sigma_{1},O_{1},U_{1},T_{1},F_{1})$
(202) $\displaystyle\textsf{WellFormed}(\sigma_{2},O_{2},U_{2},T_{2},F_{2})$
(203)

We must show
$\exists_{\sigma^{\prime}_{1},\sigma^{\prime}_{2},O^{\prime}_{1},O^{\prime}_{2},U^{\prime}_{1},U^{\prime}_{2},T^{\prime}_{1},T^{\prime}_{2},F^{\prime}_{1},F^{\prime}_{2}}$
such that

$\displaystyle\begin{aligned}
(\sigma^{\prime},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})\in\llbracket\Gamma\,,p:\textsf{rcuFresh}\;\;\mathcal{N}(\cup_{f\rightharpoonup
z})\,,x:\textsf{rcuItr}\,\rho\,\mathcal{N}([f\rightharpoonup
z])\rrbracket_{M,tid}\end{aligned}$ (204)
$\displaystyle\mathcal{N}(f)=z\land\mathcal{N}^{\prime}(f)=z$ (205)
$\displaystyle(\sigma^{\prime},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})\in\mathcal{R}(\\{m\\})$
(206)
$\displaystyle\sigma^{\prime}_{1}\bullet\sigma^{\prime}_{2}=\sigma^{\prime}$
(207) $\displaystyle O^{\prime}_{1}\bullet_{O}O^{\prime}_{2}=O^{\prime}$ (208)
$\displaystyle U^{\prime}_{1}\cup U^{\prime}_{2}=U^{\prime}$ (209)
$\displaystyle T^{\prime}_{1}\cup T^{\prime}_{2}=T^{\prime}$ (210)
$\displaystyle F^{\prime}_{1}\uplus F^{\prime}_{2}=F^{\prime}$ (211)
$\displaystyle\textsf{WellFormed}(\sigma_{1}^{\prime},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})$
(212)
$\displaystyle\textsf{WellFormed}(\sigma_{2}^{\prime},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$
(213)

We also know from operational semantics that the machine state has changed as

$\displaystyle\sigma^{\prime}=\sigma[h(s(p,tid),f)\mapsto s(z,tid)]$ (214)

There exists no change in the observation of heap locations

$\displaystyle O^{\prime}_{1}=O_{1}$ (215)

216 follows from 192

$\displaystyle T_{1}=\\{tid\\}\text{ and }tid=\sigma.l$ (216)

$\sigma^{\prime}_{1}$ is determined by operational semantics. The undefined
map, free list, $T_{1}$ need not change so we can pick $U^{\prime}_{1}$ as
$U_{1}$, $T^{\prime}_{1}$ as $T_{1}$ and $F^{\prime}_{1}$ as $F_{1}$. Assuming
195 and choices on maps makes
$(\sigma_{1}^{\prime},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1})$ in
denotation

$\llbracket\Gamma\,,p:\textsf{rcuFresh}\;\;\mathcal{N}(\cup_{f\rightharpoonup
z})\,,x:\textsf{rcuItr}\,\rho\,\mathcal{N}([f\rightharpoonup
z])\rrbracket_{M,tid}$

In the rest of the proof, we prove 212 and 213 and show the composition of
$(\sigma^{\prime}_{1},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})$
and
$(\sigma^{\prime}_{2},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$.
To prove 212, we need to show that each of the memory axioms in Section 0.A.2
holds for the state
$(\sigma^{\prime},O^{\prime}_{1},U_{1}^{\prime},T_{1}^{\prime},F^{\prime}_{1})$.

###### Case 44

\- UNQR By 202.UNQR, 212.FR(proved) and $\sigma.rt=\sigma.rt^{\prime}$.

###### Case 45

\- OW By 214,215 and 202.OW

###### Case 46

\- RWOW By 214, 215 and 202.RWOW

###### Case 47

\- AWRT Trivial.

###### Case 48

\- IFL By 202.WULK, 215, choice of $F^{\prime}_{1}$ and operational semantics.

###### Case 49

\- FLR By operational semantics(214), choice of $F^{\prime}_{1}$ and 202.

###### Case 50

\- WULK By 202.WULK, 215 and operational
semantics($\sigma.l=\sigma.l^{\prime}$).

###### Case 51

\- WF By 202.WF, 216, 215 and operational semantics(214).

###### Case 52

\- FR By 202.FR, 216, 215 and operational semantics(214).

###### Case 53

\- FNR By 202.FNR, 216, 215 and operational semantics(214).

###### Case 54

\- FPI By 202.FPI, 195 and 194

###### Case 55

\- HD

###### Case 56

\- WNR By 216 and operational semantics($\sigma.l=\sigma.l^{\prime}$).

###### Case 57

\- RINFL By operational semantics(214 \- bounding threads have not changed),
choice of $F^{\prime}_{1}$ and 202.

###### Case 58

\- ULKR Trivial.

###### Case 59

\- UNQRT By 202.UNQRT, 215 and 214.

To prove 206, we need to show interference relation

$(\sigma,O_{2},U_{2},T_{2},F_{2})\mathcal{R}(\sigma^{\prime},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$

which by definition means that we must show

$\displaystyle\sigma_{2}.l\in
T_{2}\rightarrow(\sigma_{2}.h=\sigma^{\prime}_{2}.h\land\sigma_{2}.l=\sigma^{\prime}_{2}.l)$
(217) $\displaystyle l\in T_{2}\rightarrow F_{2}=F_{2}^{\prime}$ (218)
$\displaystyle\forall tid,o\ldotp\textsf{iterator}\,tid\in O_{2}(o)\rightarrow
o\in dom(\sigma_{2}.h)$ (219) $\displaystyle\forall
tid,o\ldotp\textsf{iterator}\,tid\in O_{2}(o)\rightarrow o\in
dom(\sigma^{\prime}_{2}.h)$ (220) $\displaystyle O_{2}=O_{2}^{\prime}\land
U_{2}=U_{2}^{\prime}\land
T_{2}=T_{2}^{\prime}\land\sigma_{2}.R=\sigma^{\prime}_{2}.R\land\sigma_{2}.rt=\sigma^{\prime}_{2}.rt$
(221) $\displaystyle\forall x,t\in
T_{2}\ldotp\sigma_{2}.s(x,t)=\sigma^{\prime}_{2}.s(x,t)$ (222)
$\displaystyle\forall tid,o\ldotp\textsf{root}\,tid\in O(o)\rightarrow o\in
dom(h)$ (223) $\displaystyle\forall tid,o\ldotp\textsf{root}\,tid\in
O(o)\rightarrow o\in dom(h^{\prime})$ (224)

To prove all relations (217-222) we assume 216 which is to assume $T_{2}$ as
subset of reader threads and 203. Let $\sigma^{\prime}_{2}$ be $\sigma_{2}$
and $F^{\prime}_{2}$ be $F_{2}$. $O_{2}$ need not change so we pick
$O^{\prime}_{2}$ as $O_{2}$. Since $T_{2}$ is subset of reader threads, we
pick $T_{2}$ as $T^{\prime}_{2}$. By assuming 203 we show 213. 219 and 220
follows trivially. 222 follows from choice of $\sigma^{\prime}_{2}$ and
214(determined by operational semantics).

217 and 218 follow from 216 and choice of $F_{2}^{\prime}$. 221 are determined
by operational semantics, choice of $\sigma^{\prime}_{2}$ and choices made on
maps related to the assertions.

209-211 are trivial by choices on related maps and semantics of the
composition operators for these maps. 223 and 224 follow from choice of
$\sigma^{\prime}_{2}$.

$O^{\prime}_{1}\bullet O^{\prime}_{2}$ follows from 198, 215 and choice of
$O_{2}$.

We assume $\sigma_{1}.h\bullet\sigma_{2}.h$. We know from 194 that $f\notin
dom(\mathcal{N}^{\prime})$. From 204, 212-213.FNR, 212-213.RITR and
212-213.WNR we show $\sigma^{\prime}_{1}.h\bullet\sigma^{\prime}_{2}.h$ (with
choices for other maps in the machine state we show 174). All compositions
shown let us to derive conclusion for
$(\sigma^{\prime}_{1},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})\bullet(\sigma^{\prime}_{2},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$.

######  Lemma 19 (Sycn)

$\displaystyle\llbracket\textsf{SyncStart};\textsf{SyncStop}\rrbracket(\lfloor\llbracket\Gamma\rrbracket_{M,tid}*\\{m\\}\rfloor)\subseteq$
$\displaystyle\lfloor\llbracket\Gamma[\overline{x:\textsf{freeable}/x:\textsf{unlinked}}]\rrbracket*\mathcal{R}(\\{m\\})\rfloor$

###### Proof

We assume

$\displaystyle\begin{aligned}
(\sigma,O,U,T,F)\,\in&\llbracket\Gamma\rrbracket_{M,tid}*\\{m\\}\end{aligned}$
(225) $\displaystyle\textsf{WellFormed}(\sigma,O,U,T,F)$ (226)

We split the composition in 225 as

$\displaystyle\begin{aligned}
(\sigma,O_{1},U_{1},T_{1},F_{1})\in&\llbracket\Gamma\rrbracket_{M,tid}\end{aligned}$
(227) $\displaystyle(\sigma,O_{2},U_{2},T_{2},F_{2})=m$ (228)
$\displaystyle\sigma_{1}\bullet\sigma_{2}=\sigma$ (229) $\displaystyle
O_{1}\bullet_{O}O_{2}=O$ (230) $\displaystyle U_{1}\cup U_{2}=U$ (231)
$\displaystyle T_{1}\cup T_{2}=T$ (232) $\displaystyle F_{1}\uplus F_{2}=F$
(233) $\displaystyle\textsf{WellFormed}(\sigma,O_{1},U_{1},T_{1},F_{1})$ (234)
$\displaystyle\textsf{WellFormed}(\sigma,O_{2},U_{2},T_{2},F_{2})$ (235)

We must show
$\exists_{\sigma^{\prime}_{1},\sigma^{\prime}_{2},O^{\prime}_{1},O^{\prime}_{2},U^{\prime}_{1},U^{\prime}_{2},T^{\prime}_{1},T^{\prime}_{2}},F^{\prime}_{1},F^{\prime}_{2}$
such that

$\displaystyle\begin{aligned}
(\sigma^{\prime},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})\in\llbracket\Gamma[\overline{x:\textsf{freeable}/x:\textsf{unlinked}}]\rrbracket_{M,tid}\end{aligned}$
(236)
$\displaystyle(\sigma^{\prime},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})\in\mathcal{R}(\\{m\\})$
(237)
$\displaystyle\sigma^{\prime}_{1}\bullet\sigma^{\prime}_{2}=\sigma^{\prime}$
(238) $\displaystyle O^{\prime}_{1}\bullet_{O}O^{\prime}_{2}=O^{\prime}$ (239)
$\displaystyle U^{\prime}_{1}\cup U^{\prime}_{2}=U^{\prime}$ (240)
$\displaystyle T^{\prime}_{1}\cup T^{\prime}_{2}=T^{\prime}$ (241)
$\displaystyle F^{\prime}_{1}\uplus F^{\prime}_{2}=F^{\prime}$ (243)
$\displaystyle\textsf{WellFormed}(\sigma^{\prime},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})$
(244)
$\displaystyle\textsf{WellFormed}(\sigma^{\prime},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$
(245)

We also know from operational semantics that SyncStart changes

$\displaystyle\sigma_{1}^{\prime}.B=\sigma_{1}.B[\emptyset\mapsto R]$ (246)

Then SyncStop changes it to $\emptyset$ so there exists no change in $B$ after
SyncStart;SyncStop. So there is no change in machine state.

$\displaystyle\sigma_{1}^{\prime}=\sigma_{1}$ (247)

There exists no change in the observation of heap locations

$\displaystyle O^{\prime}_{1}=O_{1}(\forall_{x\in\Gamma}\ldotp
s(x,tid))[\textsf{unlinked}\mapsto\textsf{freeable}]$ (248)

and we pick free list to be

$\displaystyle
F^{\prime}_{1}=F_{1}(\forall_{x:\textsf{unlinked}\in\Gamma,T\subseteq R}\ldotp
s(x,tid)[T\mapsto\\{\emptyset\\}])$ (249)

250 follows from 225

$\displaystyle T_{1}=\\{tid\\}\text{ and }tid=\sigma.l$ (250)

Let $T^{\prime}_{1}$ be $T_{1}$ and $\sigma^{\prime}_{1}$(not changed) be
determined by operational semantics. The undefined map need not change so we
can pick $U^{\prime}_{1}$ as $U_{1}$. Assuming 227 and choices on maps makes
$(\sigma_{1}^{\prime},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})$
in denotation

$\llbracket\Gamma[\overline{x:\textsf{freeable}/x:\textsf{unlinked}}]\rrbracket_{M,tid}$

In the rest of the proof, we prove 244 and 245 and show the composition of
$(\sigma^{\prime}_{1},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})$
and
$(\sigma^{\prime}_{2},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$.
To prove 244, we need to show that each of the memory axioms in Section 0.A.2
holds for the state
$(\sigma^{\prime},O^{\prime}_{1},U_{1}^{\prime},T_{1}^{\prime},F^{\prime}_{1})$
which is trivial by assuming 234. We also know 236(as we showed the support of
state to the denotation).

To prove 237, we need to show interference relation

$(\sigma,O_{2},U_{2},T_{2},F_{2})\mathcal{R}(\sigma^{\prime},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F_{2}^{\prime})$

which by definition means that we must show

$\displaystyle\sigma_{2}.l\in
T_{2}\rightarrow(\sigma_{2}.h=\sigma^{\prime}_{2}.h\land\sigma_{2}.l=\sigma^{\prime}_{2}.l)$
(251) $\displaystyle l\in T_{2}\rightarrow F_{2}=F_{2}^{\prime}$ (252)
$\displaystyle\forall tid,o\ldotp\textsf{iterator}\,tid\in O_{2}(o)\rightarrow
o\in dom(\sigma_{2}.h)$ (253) $\displaystyle\forall
tid,o\ldotp\textsf{iterator}\,tid\in O_{2}(o)\rightarrow o\in
dom(\sigma^{\prime}_{2}.h)$ (254) $\displaystyle O_{2}=O_{2}^{\prime}\land
U_{2}=U_{2}^{\prime}\land
T_{2}=T_{2}^{\prime}\land\sigma_{2}.R=\sigma^{\prime}_{2}.R\land\sigma_{2}.rt=\sigma^{\prime}_{2}.rt$
(255) $\displaystyle\forall x,t\in
T_{2}\ldotp\sigma_{2}.s(x,t)=\sigma^{\prime}_{2}.s(x,t)$ (256)
$\displaystyle\forall tid,o\ldotp\textsf{root}\,tid\in O(o)\rightarrow o\in
dom(h)$ (257) $\displaystyle\forall tid,o\ldotp\textsf{root}\,tid\in
O(o)\rightarrow o\in dom(h^{\prime})$ (258)

To prove all relations (251-256) we assume 250 which is to assume $T_{2}$ as
subset of reader threads and 235. Let $\sigma^{\prime}_{2}$ be $\sigma_{2}$.
$O_{2}$ need not change so we pick $O^{\prime}_{2}$ as $O_{2}$. Since $T_{2}$
is subset of reader threads, we pick $T_{2}$ as $T^{\prime}_{2}$. By assuming
235 we show 245. 253 and 254 follows trivially. 256 follows from choice of
$\sigma^{\prime}_{2}$ and 247(determined by operational semantics).

251 and 252 follow from 250. 255 are determined by choice of
$\sigma^{\prime}_{2}$ and operational semantics and choices made on maps
related to the assertions.

240-243 follow from 230-233 trivially by choices on maps of logical state and
semantics of composition operators. 238 follow from 229, 247-250 and choice of
$\sigma^{\prime}_{2}$. All compositions shown let us to derive conclusion for
$(\sigma^{\prime}_{1},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})\bullet(\sigma^{\prime}_{2},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$
.

######  Lemma 20 (Alloc)

$\displaystyle\llbracket
x:=new\rrbracket(\lfloor\llbracket\Gamma\,,x:\textsf{undef}\,\rrbracket_{M,tid}*\\{m\\}\rfloor)\subseteq$
$\displaystyle\lfloor\llbracket\Gamma\,,x:\textsf{rcuFresh}\,\mathcal{N}_{\emptyset}\rrbracket*\mathcal{R}(\\{m\\})\rfloor$

###### Proof

We assume

$\displaystyle\begin{aligned}
(\sigma,O,U,T,F)\,\in&\llbracket\Gamma\,,x:\textsf{undef}\,\rrbracket_{M,tid}*\\{m\\}\rfloor)\end{aligned}$
(259) $\displaystyle\textsf{WellFormed}(\sigma,O,U,T,F)$ (260)

We split the composition in 259 as

$\displaystyle\begin{aligned}
(\sigma,O_{1},U_{1},T_{1},F_{1})\in&\llbracket\Gamma\,,x:\textsf{undef}\,\rrbracket_{M,tid}\end{aligned}$
(261) $\displaystyle(\sigma,O_{2},U_{2},T_{2},F_{2})=m$ (262)
$\displaystyle\sigma_{1}\bullet\sigma_{2}=\sigma$ (263) $\displaystyle
O_{1}\bullet_{O}O_{2}=O$ (264) $\displaystyle U_{1}\cup U_{2}=U$ (265)
$\displaystyle T_{1}\cup T_{2}=T$ (266) $\displaystyle F_{1}\uplus F_{2}=F$
(267) $\displaystyle\textsf{WellFormed}(\sigma,O_{1},U_{1},T_{1},F_{1})$ (268)
$\displaystyle\textsf{WellFormed}(\sigma,O_{2},U_{2},T_{2},F_{2})$ (269)

We must show
$\exists_{O^{\prime}_{1},O^{\prime}_{2},U^{\prime}_{1},U^{\prime}_{2},T^{\prime}_{1},T^{\prime}_{2},F^{\prime}_{1},F^{\prime}_{2}}$
such that

$\displaystyle\begin{aligned}
(\sigma^{\prime},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})\in\llbracket\Gamma\,,x:\textsf{rcuFresh}\,\mathcal{N}_{\emptyset}\rrbracket\end{aligned}$
(270)
$\displaystyle(\sigma^{\prime},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})\in\mathcal{R}(\\{m\\})$
(271)
$\displaystyle\sigma^{\prime}_{1}\bullet\sigma^{\prime}_{2}=\sigma^{\prime}$
(272) $\displaystyle O^{\prime}_{1}\bullet_{O}O^{\prime}_{2}=O^{\prime}$ (273)
$\displaystyle U^{\prime}_{1}\cup U^{\prime}_{2}=U^{\prime}$ (274)
$\displaystyle T^{\prime}_{1}\cup T^{\prime}_{2}=T^{\prime}$ (275)
$\displaystyle F^{\prime}_{1}\uplus F^{\prime}_{2}=F^{\prime}$ (276)
$\displaystyle\textsf{WellFormed}(\sigma^{\prime},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1})$
(277)
$\displaystyle\textsf{WellFormed}(\sigma^{\prime},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2})$
(278)

From operational semantics we know that $s(y,tid)$ is $\ell$. We also know
from operational semantics that the machine state has changed as

$\displaystyle\sigma^{\prime}=\sigma[h(\ell)\mapsto\textsf{nullmap}]$ (279)

There exists no change in the observation of heap locations

$\displaystyle
O^{\prime}_{1}=O_{1}(\ell)[\textsf{undef}\mapsto\textsf{fresh}]$ (280)

281 follows from 259

$\displaystyle T_{1}=\\{tid\\}\text{ and }tid=\sigma.l$ (281)

Let $T^{\prime}_{1}$ to be $T_{1}$. Undefined map and free list need not
change so we can pick $U^{\prime}_{1}$ as $U_{1}$ and $F^{\prime}_{1}$ as
$F_{1}$ and show(270) that
$(\sigma^{\prime},O^{\prime}_{1},U_{1}^{\prime},T_{1}^{\prime},F^{\prime}_{1})$
is in denotation of

$\llbracket\Gamma\,,x:\textsf{rcuFresh}\,\mathcal{N}_{\emptyset}\rrbracket$

In the rest of the proof, we prove 277, 278 and
$(\sigma^{\prime}_{1},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})$
and
$(\sigma^{\prime}_{2},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$.
To prove 277, we need to show that each of the memory axioms in Section 0.A.2
holds for the state
$(\sigma^{\prime},O^{\prime}_{1},U_{1}^{\prime},T_{1}^{\prime},F^{\prime}_{1})$.

###### Case 60

\- UNQR Determined by 270 and operational semantics($\ell$ is fresh-unique).

###### Case 61

\- RWOW, OW By 270

###### Case 62

\- AWRT Determined by operational semantics($\ell$ is fresh-unique).

###### Case 63

\- IFL, ULKR, WULK, RINFL, UNQRT Trivial.

###### Case 64

\- FLR determined by operational semantics and 270.

###### Case 65

\- WF By 281, 270 and 280.

###### Case 66

\- FR Determined by operational semantics($\ell$ is fresh-unique).

###### Case 67

\- FNR By 270 and operational semantics($\ell$ is fresh-unique).

###### Case 68

\- FPI By 270 and $\mathcal{N}_{f,\emptyset}$.

###### Case 69

\- HD

###### Case 70

\- WNR By 281.

To prove 271, we need to show interference relation

$(\sigma,O_{2},U_{2},T_{2},F_{2})\mathcal{R}(\sigma^{\prime},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$

which by definition means that we must show

$\displaystyle\sigma_{2}.l\in
T_{2}\rightarrow(\sigma_{2}.h=\sigma^{\prime}_{2}.h\land\sigma_{2}.l=\sigma^{\prime}_{2}.l)$
(282) $\displaystyle l\in T_{2}\rightarrow F_{2}=F_{2}^{\prime}$ (283)
$\displaystyle\forall tid,o\ldotp\textsf{iterator}\,tid\in O_{2}(o)\rightarrow
o\in dom(\sigma_{2}.h)$ (284) $\displaystyle\forall
tid,o\ldotp\textsf{iterator}\,tid\in O_{2}(o)\rightarrow o\in
dom(\sigma^{\prime}_{2}.h)$ (285) $\displaystyle O_{2}=O_{2}^{\prime}\land
U_{2}=U_{2}^{\prime}\land
T_{2}=T_{2}^{\prime}\land\sigma_{2}.R=\sigma^{\prime}_{2}.R\land\sigma_{2}.rt=\sigma^{\prime}_{2}.rt$
(286) $\displaystyle\forall x,t\in
T\ldotp\sigma_{2}.s(x,t)=\sigma^{\prime}_{2}.s(x,t)$ (287)
$\displaystyle\forall tid,o\ldotp\textsf{root}\,tid\in O(o)\rightarrow o\in
dom(h)$ (288) $\displaystyle\forall tid,o\ldotp\textsf{root}\,tid\in
O(o)\rightarrow o\in dom(h^{\prime})$ (289)

To prove all relations (282-289) we assume 281 which is to assume $T_{2}$ as
subset of reader threads and 269. Let $\sigma^{\prime}_{2}$ be $\sigma_{2}$.
$F_{2}$ and $O_{2}$ need not change so we pick $O^{\prime}_{2}$ as $O_{2}$ and
$F^{\prime}_{2}$ as $F_{2}$. Since $T_{2}$ is subset of reader threads, we
pick $T_{2}$ as $T^{\prime}_{2}$. By assuming 269 and choices on maps we show
278. 284 and 285 follow trivially. 287 follows from choice of
$\sigma^{\prime}_{2}$ and 279(determined by operational semantics). 273-276
follow from 264-267, semantics of compositions operators and choices made for
maps of the logical state.

282 and 283 follow from 281 and choice on $F^{\prime}_{2}$. 286 are determined
by operational semantics, operational semantics and choices made on maps
related to the assertion.

$\sigma^{\prime}_{1}.h\cap\sigma^{\prime}_{2}.h=\emptyset$ is determined by
operational semantics($\ell$ is unique and fresh). So, 272 follows from 263
and choice of $\sigma^{\prime}_{2}$. All compositions shown let us to derive
conclusion for
$(\sigma^{\prime}_{1},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})\bullet(\sigma^{\prime}_{2},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$.

######  Lemma 21 (Free)

$\displaystyle\llbracket Free(x)\rrbracket(\lfloor\llbracket
x:\textsf{freeable}\rrbracket_{M,tid}*\\{m\\}\rfloor)\subseteq$
$\displaystyle\lfloor\llbracket
x:\textsf{undef}\rrbracket*\mathcal{R}(\\{m\\})\rfloor$

###### Proof

We assume

$\displaystyle\begin{aligned} (\sigma,O,U,T,F)\,\in&\llbracket
x:\textsf{freeable}\,\rrbracket_{M,tid}*\\{m\\}\rfloor)\end{aligned}$ (290)
$\displaystyle\textsf{WellFormed}(\sigma,O,U,T,F)$ (291)

We split the composition in 290 as

$\displaystyle\begin{aligned} (\sigma,O_{1},U_{1},T_{1},F_{1})\in&\llbracket
x:\textsf{freeable}\rrbracket_{M,tid}\end{aligned}$ (292)
$\displaystyle(\sigma,O_{2},U_{2},T_{2},F_{2})=m$ (293)
$\displaystyle\sigma_{1}\bullet\sigma_{2}=\sigma$ (294) $\displaystyle
O_{1}\bullet_{O}O_{2}=O$ (295) $\displaystyle U_{1}\cup U_{2}=U$ (296)
$\displaystyle T_{1}\cup T_{2}=T$ (297) $\displaystyle F_{1}\uplus F_{2}=F$
(298) $\displaystyle\textsf{WellFormed}(\sigma,O_{1},U_{1},T_{1},F_{1})$ (299)
$\displaystyle\textsf{WellFormed}(\sigma,O_{2},U_{2},T_{2},F_{2})$ (300)

We must show
$\exists_{O^{\prime}_{1},O^{\prime}_{2},U^{\prime}_{1},U^{\prime}_{2},T^{\prime}_{1},T^{\prime}_{2},F^{\prime}_{1},F^{\prime}_{2}}$
such that

$\displaystyle\begin{aligned}
(\sigma^{\prime},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})\in\llbracket
x:\textsf{undef}\rrbracket\end{aligned}$ (301)
$\displaystyle(\sigma^{\prime},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})\in\mathcal{R}(\\{m\\})$
(302)
$\displaystyle\sigma^{\prime}_{1}\bullet\sigma^{\prime}_{2}=\sigma^{\prime}$
(303) $\displaystyle O^{\prime}_{1}\bullet_{O}O^{\prime}_{2}=O^{\prime}$ (304)
$\displaystyle U^{\prime}_{1}\cup U^{\prime}_{2}=U^{\prime}$ (305)
$\displaystyle T^{\prime}_{1}\cup T^{\prime}_{2}=T^{\prime}$ (306)
$\displaystyle F^{\prime}_{1}\uplus F^{\prime}_{2}=F^{\prime}$ (307)
$\displaystyle\textsf{WellFormed}(\sigma^{\prime},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})$
(308)
$\displaystyle\textsf{WellFormed}(\sigma^{\prime},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$
(309)

From operational semantics we know that

$\displaystyle\forall_{f,o^{\prime}}\ldotp rt\neq s(x,tid)\land o^{\prime}\neq
s(x,tid)\implies
h(o^{\prime},f)=h^{\prime}(o^{\prime},f)\land\forall_{f}\ldotp
h^{\prime}(o,f)=\textsf{undef}$ (310)

$\displaystyle
O^{\prime}_{1}=O_{1}(s(x,tid))[\textsf{freeable}\mapsto\textsf{undef}]$ (311)

$\displaystyle
F^{\prime}_{1}=F_{1}\setminus\\{s(x,tid)\mapsto\\{\emptyset\\}\\}$ (312)

$\displaystyle U^{\prime}_{1}=U_{1}\cup\\{(x,tid)\\}$ (313)

314 follows from 290

$\displaystyle T_{1}=\\{tid\\}\text{ and }tid=\sigma.l$ (314)

Let $T^{\prime}_{1}$ to be $T_{1}$. All 310-313 show(301) that
$(\sigma^{\prime},O^{\prime}_{1},U_{1}^{\prime},T_{1}^{\prime},F^{\prime}_{1})$
is in denotation of

$\llbracket x:\textsf{undef}\rrbracket$

In the rest of the proof, we prove 308, 309 and show the composition of
$(\sigma^{\prime}_{1},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})$
and
$(\sigma^{\prime}_{2},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$..
To prove 308, we need to show that each of the memory axioms in Section 0.A.2
holds for the state
$(\sigma^{\prime},O^{\prime}_{1},U_{1}^{\prime},T_{1}^{\prime},F^{\prime}_{1})$
and it it trivial by 310-313 and 301.

To prove 302, we need to show interference relation

$(\sigma,O_{2},U_{2},T_{2},F_{2})\mathcal{R}(\sigma^{\prime},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$

which by definition means that we must show

$\displaystyle\sigma_{2}.l\in
T_{2}\rightarrow(\sigma_{2}.h=\sigma^{\prime}_{2}.h\land\sigma_{2}.l=\sigma^{\prime}_{2}.l)$
(315) $\displaystyle l\in T_{2}\rightarrow F_{2}=F_{2}^{\prime}$ (316)
$\displaystyle\forall tid,o\ldotp\textsf{iterator}\,tid\in O_{2}(o)\rightarrow
o\in dom(\sigma_{2}.h)$ (317) $\displaystyle\forall
tid,o\ldotp\textsf{iterator}\,tid\in O_{2}(o)\rightarrow o\in
dom(\sigma^{\prime}_{2}.h)$ (318) $\displaystyle O_{2}=O_{2}^{\prime}\land
U_{2}=U_{2}^{\prime}\land
T_{2}=T_{2}^{\prime}\land\sigma_{2}.R=\sigma^{\prime}_{2}.R\land\sigma_{2}.rt=\sigma^{\prime}_{2}.rt$
(319) $\displaystyle\forall x,t\in
T\ldotp\sigma_{2}.s(x,t)=\sigma^{\prime}_{2}.s(x,t)$ (320)
$\displaystyle\forall tid,o\ldotp\textsf{root}\,tid\in O(o)\rightarrow o\in
dom(h)$ (321) $\displaystyle\forall tid,o\ldotp\textsf{root}\,tid\in
O(o)\rightarrow o\in dom(h^{\prime})$ (322)

To prove all relations (315-322) we assume 314 which is to assume $T_{2}$ as
subset of reader threads and 269. Let $\sigma^{\prime}_{2}$ be $\sigma_{2}$.
$F_{2}$ and $O_{2}$ need not change so we pick $O^{\prime}_{2}$ as $O_{2}$ and
$F^{\prime}_{2}$ as $F_{2}$. Since $T_{2}$ is subset of reader threads, we
pick $T_{2}$ as $T^{\prime}_{2}$. By assuming 269 and choices on maps we show
309. 317 and 318 follow trivially. 320 follows from choice of
$\sigma^{\prime}_{2}$ and 310(determined by operational semantics). 304-307
follow from 296-298, semantics of composition operators and choices on related
maps.

315 and 316 follow from 314 and choice on $F^{\prime}_{2}$. 319 are determined
by operational semantics, choice of $\sigma^{\prime}_{2}$ and choices made on
maps related to the assertion.

Composition for heap for case
$\sigma^{\prime}_{1}.h\cap\sigma^{\prime}_{2}.h=\emptyset$ is trivial.
$\sigma^{\prime}_{1}.h\cap\sigma^{\prime}_{2}.h\neq\emptyset$ is determined by
semantics of heap composition operator $\bullet_{h}$( $v$ has precedence over
undef) and this makes showing 304 straightforward. Since other machine
components do not change(determined by operational semantics), 303 follows
from 294, 310 and choice of $\sigma^{\prime}_{2}$. All compositions shown let
us to derive conclusion for
$(\sigma^{\prime}_{1},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})\bullet(\sigma^{\prime}_{2},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$.

######  Lemma 22 (RReadStack)

$\displaystyle\llbracket
z:=x\rrbracket(\lfloor\llbracket\Gamma\,,z:\textsf{rcuItr}\,,x:\textsf{rcuItr}\rrbracket_{R,tid}*\\{m\\}\rfloor)\subseteq$
$\displaystyle\lfloor\llbracket\Gamma\,,x:\textsf{rcuItr}\,,z:\textsf{rcuItr}\rrbracket*\mathcal{R}(\\{m\\})\rfloor$

###### Proof

We assume

$\displaystyle\begin{aligned}
(\sigma,O,U,T,F)\,\in&\llbracket\Gamma\,,\Gamma\,,z:\textsf{rcuItr}\,,x:\textsf{rcuItr}\rrbracket_{R,tid}*\\{m\\}\end{aligned}$
(323) $\displaystyle\textsf{WellFormed}(\sigma,O,U,T,F)$ (324)

We split the composition in 323 as

$\displaystyle\begin{aligned}
(\sigma_{1},O_{1},U_{1},T_{1},F_{1})\in&\llbracket\Gamma\,,\Gamma\,,z:\textsf{rcuItr}\,,x:\textsf{rcuItr}\rrbracket_{R,tid}\end{aligned}$
(325) $\displaystyle(\sigma,O_{2},U_{2},T_{2},F_{2})=m$ (326) $\displaystyle
O_{1}\bullet_{O}O_{2}=O$ (327)
$\displaystyle\sigma_{1}\bullet\sigma_{2}=\sigma$ (328) $\displaystyle
U_{1}\cup U_{2}=U$ (329) $\displaystyle T_{1}\cup T_{2}=T$ (330)
$\displaystyle F_{1}\uplus F_{2}=F$ (331)
$\displaystyle\textsf{WellFormed}(\sigma,O_{1},U_{1},T_{1},F_{1})$ (332)
$\displaystyle\textsf{WellFormed}(\sigma,O_{2},U_{2},T_{2},F_{2})$ (333)

We must show
$\exists_{O^{\prime}_{1},O^{\prime}_{2},U^{\prime}_{1},U^{\prime}_{2},T^{\prime}_{1},T^{\prime}_{2},F^{\prime}_{1},F^{\prime}_{2}}$
such that

$\displaystyle\begin{aligned}
(\sigma^{\prime},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})\in\llbracket\Gamma\,,x:\textsf{rcuItr}\,,z:\textsf{rcuItr}\rrbracket_{R,tid}\end{aligned}$
(334)
$\displaystyle(\sigma^{\prime},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})\in\mathcal{R}(\\{m\\})$
(335) $\displaystyle O^{\prime}_{1}\bullet_{O}O^{\prime}_{2}=O^{\prime}$ (336)
$\displaystyle\sigma^{\prime}_{1}\bullet\sigma^{\prime}_{2}=\sigma^{\prime}$
(337) $\displaystyle U^{\prime}_{1}\cup U^{\prime}_{2}=U^{\prime}$ (338)
$\displaystyle T^{\prime}_{1}\cup T^{\prime}_{2}=T^{\prime}$ (339)
$\displaystyle F^{\prime}_{1}\uplus F^{\prime}_{2}=F^{\prime}$ (340)
$\displaystyle\textsf{WellFormed}(\sigma^{\prime},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})$
(341)
$\displaystyle\textsf{WellFormed}(\sigma^{\prime},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$
(342)

We also know from operational semantics that the machine state has changed as

$\displaystyle\sigma_{1}^{\prime}=\sigma_{1}$ (343)

There exists no change in the observation of heap locations

$\displaystyle O^{\prime}_{1}=O_{1}$ (344)

345 follows from 323

$\displaystyle T_{1}\subseteq R$ (345)

Let $T^{\prime}_{1}$ be $T_{1}$ and $\sigma^{\prime}_{1}$ be determined by
operational semantics as $\sigma_{1}$. The undefined map and free list need
not change so we can pick $U^{\prime}_{1}$ as $U_{1}$ and $F^{\prime}_{1}$ as
$F_{1}$. Assuming 325 and choices on maps makes
$(\sigma_{1}^{\prime},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})$
in denotation

$\llbracket\Gamma\,,x:\textsf{rcuItr}\,,z:\textsf{rcuItr}\rrbracket_{R,tid}$

In the rest of the proof, we prove 341, 34226, 27 and show the composition of
$(\sigma^{\prime}_{1},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})$
and
$(\sigma^{\prime}_{2},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$.
To prove 341, we need to show that each of the memory axioms in Section 0.A.2
holds for the state
$(\sigma^{\prime},O^{\prime}_{1},U_{1}^{\prime},T_{1}^{\prime},F^{\prime}_{1})$
which is trivial by assuming 332 and knowing 345, 344 and components of the
state determined by operational semantics.

To prove 342, we need to show that WellFormedness is preserved under
interference relation

$(\sigma,O_{2},U_{2},T_{2},F_{2})\mathcal{R}(\sigma^{\prime},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$

which by definition means that we must show

$\displaystyle\sigma_{2}.l\in
T_{2}\rightarrow(\sigma_{2}.h=\sigma^{\prime}_{2}.h\land\sigma_{2}.l=\sigma^{\prime}_{2}.l)$
(346) $\displaystyle l\in T_{2}\rightarrow F_{2}=F_{2}^{\prime}$ (347)
$\displaystyle\forall tid,o\ldotp\textsf{iterator}\,tid\in O_{2}(o)\rightarrow
o\in dom(\sigma_{2}.h)$ (348) $\displaystyle\forall
tid,o\ldotp\textsf{iterator}\,tid\in O_{2}(o)\rightarrow o\in
dom(\sigma^{\prime}_{2}.h)$ (349) $\displaystyle O_{2}=O_{2}^{\prime}\land
U_{2}=U_{2}^{\prime}\land
T_{2}=T_{2}^{\prime}\land\sigma_{2}.B=\sigma^{\prime}_{2}.B\land\sigma_{2}.rt=\sigma^{\prime}_{2}.rt$
(350) $\displaystyle\forall x,t\in
T_{2}\ldotp\sigma_{2}.s(x,t)=\sigma^{\prime}_{2}.s(x,t)$ (351)
$\displaystyle\forall tid,o\ldotp\textsf{root}\,tid\in O(o)\rightarrow o\in
dom(h)$ (352) $\displaystyle\forall tid,o\ldotp\textsf{root}\,tid\in
O(o)\rightarrow o\in dom(h^{\prime})$ (353)

$\sigma_{2}$, $O_{2}$, $U_{2}$ and $T_{2}$ need not change so that we choose
$\sigma^{\prime}_{2}$ to be $\sigma^{\prime}_{2}$, $O^{\prime}_{2}$ to be
$O_{2}$, $U^{\prime}_{2}$ to $U_{2}$ and $T^{\prime}_{2}$ to be $T_{2}$. Let
$F^{\prime}_{2}$ be $F_{2}$. These choices make proving 346-353 trivial and
336-339 follow from assumptions 327-331, choices made for related maps and
semantics of composition operations. All compositions shown let us derive
conclusion for
$(\sigma^{\prime}_{1},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})\bullet(\sigma^{\prime}_{2},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$.

######  Lemma 23 (RReadHeap)

$\displaystyle\llbracket
z:=x.f\rrbracket(\lfloor\llbracket\Gamma\,,z:\textsf{rcuItr}\,,x:\textsf{rcuItr}\rrbracket_{R,tid}*\\{m\\}\rfloor)\subseteq$
$\displaystyle\lfloor\llbracket\Gamma\,,x:\textsf{rcuItr}\,,z:\textsf{rcuItr}\rrbracket*\mathcal{R}(\\{m\\})\rfloor$

###### Proof

We assume

$\displaystyle\begin{aligned}
(\sigma,O,U,T,F)\,\in&\llbracket\Gamma\,,z:\textsf{rcuItr}\,,x:\textsf{rcuItr}\rrbracket_{R,tid}*\\{m\\}\rfloor)\end{aligned}$
(354) $\displaystyle\textsf{WellFormed}(\sigma,O,U,T,F)$ (355)

We split the composition in 354 as

$\displaystyle\begin{aligned}
(\sigma_{1},O_{1},U_{1},T_{1},F_{1})\in&\llbracket\Gamma\,,z:\textsf{rcuItr}\,,x:\textsf{rcuItr}\rrbracket_{R,tid}\end{aligned}$
(356) $\displaystyle(\sigma_{2},O_{2},U_{2},T_{2},F_{2})=m$ (357)
$\displaystyle\sigma_{1}\bullet\sigma_{2}=\sigma$ (358) $\displaystyle
O_{1}\bullet_{O}O_{2}=O$ (359) $\displaystyle U_{1}\cup U_{2}=U$ (360)
$\displaystyle T_{1}\cup T_{2}=T$ (361) $\displaystyle F_{1}\uplus F_{2}=F$
(362) $\displaystyle\textsf{WellFormed}(\sigma_{1},O_{1},U_{1},T_{1},F_{1})$
(363) $\displaystyle\textsf{WellFormed}(\sigma_{2},O_{2},U_{2},T_{2},F_{2})$
(364)

We must show
$\exists_{\sigma^{\prime}_{1},\sigma^{\prime}_{2},O^{\prime}_{1},O^{\prime}_{2},U^{\prime}_{1},U^{\prime}_{2},T^{\prime}_{1},T^{\prime}_{2},F^{\prime}_{1},F^{\prime}_{2}}$
such that

$\displaystyle\begin{aligned}
(\sigma_{1}^{\prime},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})\in\lfloor\llbracket\Gamma\,,x:\textsf{rcuItr}\,,z:\textsf{rcuItr}\rrbracket\end{aligned}$
(365)
$\displaystyle(\sigma_{2}^{\prime},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})\in\mathcal{R}(\\{m\\})$
(366)
$\displaystyle\sigma^{\prime}_{1}\bullet\sigma^{\prime}_{2}=\sigma^{\prime}$
(367) $\displaystyle O^{\prime}_{1}\bullet_{O}O^{\prime}_{2}=O^{\prime}$ (368)
$\displaystyle U^{\prime}_{1}\cup U^{\prime}_{2}=U^{\prime}$ (369)
$\displaystyle T^{\prime}_{1}\cup T^{\prime}_{2}=T^{\prime}$ (370)
$\displaystyle\textsf{WellFormed}(\sigma_{1}^{\prime},O^{\prime}_{1},U^{\prime}_{1},T^{\prime}_{1},F^{\prime}_{1})$
(371)
$\displaystyle\textsf{WellFormed}(\sigma_{2}^{\prime},O^{\prime}_{2},U^{\prime}_{2},T^{\prime}_{2},F^{\prime}_{2})$
(372)

Let $h(s(x,tid),f)$ be $o_{x}$. We also know from operational semantics that
the machine state has changed as

$\displaystyle\sigma_{1}^{\prime}=\sigma_{1}[s(z,tid)\mapsto o_{x}]$ (373)

There exists no change in the observation of heap locations

$\displaystyle O^{\prime}_{1}=O_{1}$ (374)

375 follows from 354

$\displaystyle T_{1}\subseteq R$ (375)

Proof is similar to Lemma 22.

###  0.A.4 Soundness Proof of Structural Program Actions

In this section, we introduce soundness Theorem 0.A.1 for structural rules of
the type system. We consider the cases of the induction on derivation of
$\Gamma\vdash C\dashv\Gamma$ for all type systems,$R,M$.

Although we have proofs for read-side structural rules, we only present proofs
for write-side structural type rules in this section as read-side rules are
simple versions of write-side rules and proofs for them are trivial and
already captured by proofs for write-side structural rools.

######  Theorem 0.A.1 (Type System Soundness)

$\forall_{\Gamma,\Gamma^{\prime},C}\ldotp\Gamma\vdash
C\dashv\Gamma^{\prime}\implies\llbracket\Gamma\vdash
C\dashv\Gamma^{\prime}\rrbracket$

###### Proof

Induction on derivation of $\Gamma\vdash_{M}C\dashv\Gamma$.

###### Case 71

-M: consequence where $C$ has the form $\Gamma\vdash_{M}C\dashv\Gamma^{\prime\prime\prime}$. We know

$\displaystyle\Gamma^{\prime}\vdash_{M}C\dashv\Gamma^{\prime\prime}$ (376)
$\displaystyle\Gamma\prec:\Gamma^{\prime}$ (377)
$\displaystyle\Gamma^{\prime\prime}\prec:\Gamma^{\prime\prime\prime}$ (378)
$\displaystyle\\{\llbracket\Gamma^{\prime}\rrbracket_{M,tid}\\}C\\{\llbracket\Gamma^{\prime\prime}\rrbracket_{M,tid}\\}$
(379)

We need to show

$\displaystyle\\{\llbracket\Gamma\rrbracket_{M,tid}\\}C\\{\llbracket\Gamma^{\prime\prime\prime}\rrbracket_{M,tid}\\}$
(380)

The $\prec:$ relation translated to entailment relation in Views Logic. The
relation is established over the action judgement for identity
label/transition

From 377 and Lemma 24 we know

$\displaystyle\llbracket\Gamma\rrbracket_{M,tid}\sqsubseteq\llbracket\Gamma^{\prime}\rrbracket_{M,tid}$
(381)

From 378 and 24 we know

$\displaystyle\llbracket\Gamma^{\prime\prime}\rrbracket_{M,tid}\sqsubseteq\llbracket\Gamma^{\prime\prime\prime}\rrbracket_{M,tid}$
(382)

By using 381, 382 and 379 as antecedentes of Views Logic’s consequence rule,
we conclude 380.

###### Case 72

-M: where $C$ is sequence statement. $C$ has the form $C_{1};C_{2}$. Our goal is to prove

$\displaystyle\\{\llbracket\Gamma\rrbracket_{M,tid}\\}\vdash_{M}C_{1};C_{2}\dashv\\{\llbracket\Gamma^{\prime\prime}\rrbracket_{M,tid}\\}$
(383)

We know

$\displaystyle\Gamma\vdash_{M}C_{1}\dashv\Gamma^{\prime}$ (384)
$\displaystyle\Gamma^{\prime}\vdash_{M}C_{2}\dashv\Gamma^{\prime\prime}$ (385)
$\displaystyle\\{\llbracket\Gamma\rrbracket_{M,tid}\\}C_{1}\\{\llbracket\Gamma^{\prime}\rrbracket_{M,tid}\\}$
(386)
$\displaystyle\\{\llbracket\Gamma^{\prime}\rrbracket_{M,tid}\\}C_{2}\\{\llbracket\Gamma^{\prime\prime}\rrbracket_{M,tid}\\}$
(387)

By using 386 and 387 as the antecedents for the Views sequencing rule, we can
derive the conclusion for 383.

###### Case 73

-M: where $C$ is loop statement. $C$ has the form $while\left(x\right)\\{C\\}$.

$\displaystyle\Gamma\vdash_{M}C\dashv\Gamma$ (388)
$\displaystyle\Gamma(x)=\textsf{bool}$ (389)
$\displaystyle\\{\llbracket\Gamma\rrbracket_{M,tid}\\}C\\{\llbracket\Gamma\rrbracket_{M,tid}\\}$
(390)

Our goal is to prove

$\displaystyle\\{\llbracket\Gamma\rrbracket_{M,tid}\\}\left(assume\left(x\right);C\right)^{*};assume(\lnot
x)\\{\llbracket\Gamma\rrbracket_{M,tid}\\}$ (391)

We prove 391 by from the consequence rule, based on the proofs of the
following 392 and 393

$\displaystyle\\{\llbracket\Gamma\rrbracket_{M,tid}\\}\left(assume\left(x\right);C\right)^{*}\\{\llbracket\Gamma\rrbracket_{M,tid}\\}$
(392) $\displaystyle\\{\llbracket\Gamma\rrbracket_{M,tid}\\}assume\left(\lnot
x\right)\\{\llbracket\Gamma\rrbracket_{M,tid}\\}$ (393)

The poof of 392 follows from Views Logic’s proof rule for assume construct by
using

$\\{\llbracket\Gamma\rrbracket_{M,tid}\\}assume\left(x\right)\\{\llbracket\Gamma\rrbracket_{M,tid}\\}$

as antecedent. We can use this antecedent together with the antecedent we know
from 390

$\\{\llbracket\Gamma\rrbracket_{M,tid}\\}C\\{\llbracket\Gamma\rrbracket_{M,tid}\\}$

as antecedents to the Views Logic’s proof rule for sequencing. Then we use the
antecedent

$\\{\llbracket\Gamma\rrbracket_{M,tid}\\}assume\left(x\right);C\\{\llbracket\Gamma\rrbracket_{M,tid}\\}$

to the proof rule for nondeterministic looping.

The proof of 393 follows from Views Logic’s proof rule for assume construct by
using the

$\\{\llbracket\Gamma\rrbracket_{M,tid}\\}assume\left(\lnot
x\right)\\{\llbracket\Gamma\rrbracket_{M,tid}\\}$

as the antecedent.

###### Case 74

-M: where $C$ is a loop statement. $C$ has the form $while(x.f\neq\texttt{null})\\{C\\}$ Proof is similar to the one for T-Loop1.

###### Case 75

-M: case where $C$ is branch statement. $C$ has the form $if\left(e\right)then\\{C_{1}\\}else\\{C_{2}\\}$.

$\displaystyle\Gamma,x:\textsf{rcuItr}\;\rho\;\mathcal{N}([f_{1}\rightharpoonup
z])\vdash_{M}C_{1}\dashv\Gamma^{\prime}$ (394)
$\displaystyle\Gamma,x:\textsf{rcuItr}\;\rho\;\mathcal{N}([f_{2}\rightharpoonup
z])\vdash_{M}C_{2}\dashv\Gamma^{\prime}$ (395)
$\displaystyle\\{\llbracket\Gamma,\,x:\textsf{rcuItr}\;\rho\;\mathcal{N}([f_{1}\rightharpoonup
z])\rrbracket_{M,tid}\\}C_{1}\\{\llbracket\Gamma^{\prime}\rrbracket_{M,tid}\\}$
(396)
$\displaystyle\\{\llbracket\Gamma,\,x:\textsf{rcuItr}\;\rho\;\mathcal{N}([f_{2}\rightharpoonup
z])\rrbracket_{M,tid}\\}C_{2}\\{\llbracket\Gamma^{\prime}\rrbracket_{M,tid}\\}$
(397)

Our goal is to prove

$\displaystyle\begin{array}[]{l}\\{\llbracket\Gamma,x:\textsf{rcuItr}\;\rho\;\mathcal{N}([f_{1}|f_{2}\rightharpoonup
z])\rrbracket_{M,tid}\\}\\\
y=x.f_{1};\left(assume\left(z=y\right);C_{1}\right)+\left(assume\left(y\neq
z\right);C_{2}\right)\\\
\\{\llbracket\Gamma^{\prime}\rrbracket_{M,tid}\\}\end{array}$ (401)

where the desugared form includes a fresh variable y. We use fresh variables
just for desugaring and they are not included in any type context. We prove401
from the consequence rule of Views Logic based on the proofs of the following
405 and 409

$\displaystyle\begin{array}[]{l}\\{\llbracket\Gamma,x:\textsf{rcuItr}\;\rho\;\mathcal{N}([f_{1}|f_{2}\rightharpoonup
z])\rrbracket_{M,tid}\\}\\\
\left(assume\left(z=y\right);C_{1}\right)+\left(assume\left(y\neq
z\right);C_{2}\right)\\\
\\{\llbracket\Gamma^{\prime}\rrbracket_{M,tid}\\}\end{array}$ (405)

and

$\displaystyle\begin{array}[]{l}\\{\llbracket\Gamma,x:\textsf{rcuItr}\;\rho\;\mathcal{N}[f_{1}|f_{2}\rightharpoonup
z]\rrbracket_{M,tid}\\}\\\ y=x.f_{1}\\\
\\{\llbracket\Gamma,x:\textsf{rcuItr}\;\rho\;\mathcal{N}([f_{1}|f_{2}\rightharpoonup
z])\llbracket_{M,tid}\cap\llbracket
x:\textsf{rcuItr}\;\rho\;\mathcal{N}([f_{1}\rightharpoonup
y])\rrbracket_{M,tid}\\}\end{array}$ (409)

409 is trivial from the fact that y is a fresh variable and it is not included
in any type context and just used for desugaring.

We prove 405 from the branch rule of Views Logic based on the proofs of the
following 414 and 419

$\displaystyle\begin{array}[]{l}\\{\llbracket\Gamma,x:\textsf{rcuItr}\;\rho\;\mathcal{N}([f_{1}|f_{2}\rightharpoonup
z])\rrbracket_{M,tid}\cap\\\ \llbracket
x:\textsf{rcuItr}\;\rho\;\mathcal{N}([f_{1}\rightharpoonup
y])\rrbracket_{M,tid}\\}\\\ \left(assume\left(z=y\right);C_{1}\right)\\\
\\{\llbracket\Gamma^{\prime}\rrbracket_{M,tid}\\}\end{array}$ (414)

and

$\displaystyle\begin{array}[]{l}\\{\llbracket\Gamma,x:\textsf{rcuItr}\;\rho\;\mathcal{N}([f_{1}|f_{2}\rightharpoonup
z])\rrbracket_{M,tid}\cap\\\ \llbracket
x:\textsf{rcuItr}\;\rho\;\mathcal{N}([f_{1}\rightharpoonup
y])\rrbracket_{M,tid}\\}\\\ \left(assume\left(z\neq y\right);C_{2}\right)\\\
\llbracket\Gamma^{\prime}\rrbracket_{M,tid}\\}\end{array}$ (419)

We show 414 from Views Logic’s proof rule for the assume construct by using

$\begin{array}[]{l}\\{\llbracket\Gamma,x:\textsf{rcuItr}\;\rho\;\mathcal{N}([f_{1}|f_{2}\rightharpoonup
z])\rrbracket_{M,tid}\cap\\\ \llbracket
x:\textsf{rcuItr}\;\rho\;\mathcal{N}([f_{1}\rightharpoonup
y])\rrbracket_{M,tid}\\}\\\ assume\left(y=z\right)\\\
\\{\llbracket\Gamma,x:\textsf{rcuItr}\;\rho\;\mathcal{N}([f_{1}\rightharpoonup
z])\rrbracket_{M,tid}\\}\end{array}$

as the antecedent. We can use this antecedent together with

$\\{\llbracket\Gamma,x:\textsf{rcuItr}\rho\mathcal{N}([f_{1}\rightharpoonup
z])\rrbracket_{M,tid}\\}C_{1}\\{\llbracket\Gamma^{\prime}\rrbracket_{M,tid}\\}$

as antecedents to the View’s Logic’s proof rule for sequencing.

We show 419 from Views Logic’s proof rule for the assume construct by using

$\begin{array}[]{l}\\{\llbracket\Gamma,x:\textsf{rcuItr}\;\rho\;\mathcal{N}([f_{1}|f_{2}\rightharpoonup
z])\cap\\\ x:\textsf{rcuItr}\;\rho\;\mathcal{N}([f_{1}\rightharpoonup
y])\rrbracket_{M,tid}\\}\\\ assume(x\neq y)\\\
\\{\llbracket\Gamma,x:\textsf{rcuItr}\;\rho\;\mathcal{N}([f_{2}\rightharpoonup
z])\rrbracket_{M,tid}\\}\end{array}$

as the antecedent. We can use this antecedent together with

$\\{\llbracket\Gamma,x:\textsf{rcuItr}\rho\mathcal{N}([f_{2}\rightharpoonup
z])\rrbracket_{M,tid}\\}C_{2}\\{\llbracket\Gamma^{\prime}\rrbracket_{M,tid}\\}$

as antecedents to the Views Logic’s proof rule for sequencing.

###### Case 76

-M: case where $C$ is branch statement. $C$ has the form $if(x.f==\texttt{null})then\\{C_{1}\\}else\\{C_{2}\\}$. Proof is similar to one for T-Branch1.

###### Case 77

-O: parallel where $C$ has the form $\Gamma_{1},\Gamma_{2}\vdash_{O}C_{1}||C_{2}\dashv\Gamma^{\prime}_{1},\Gamma^{\prime}_{2}$ We know

$\displaystyle\Gamma_{1}\vdash C_{1}\dashv\Gamma^{\prime}_{1}$ (420)
$\displaystyle\Gamma_{2}\vdash C_{2}\dashv\Gamma^{\prime}_{2}$ (421)
$\displaystyle\\{\llbracket\Gamma_{1}\rrbracket\\}C_{1}\\{\llbracket\Gamma^{\prime}_{1}\rrbracket\\}$
(422)
$\displaystyle\\{\llbracket\Gamma_{2}\rrbracket\\}C_{2}\\{\llbracket\Gamma^{\prime}_{2}\rrbracket\\}$
(423)

We need to show

$\displaystyle\\{\llbracket\Gamma_{1},\Gamma_{2}\rrbracket\\}C_{1}||C_{2}\\{\llbracket\Gamma^{\prime}_{1},\Gamma^{\prime}_{2}\rrbracket\\}$
(424)

By using 422 and 423 as antecedents to Views Logic’s parallel rule, we can
draw conclusion for 425

$\displaystyle\\{\llbracket\Gamma_{1}\rrbracket*\llbracket\Gamma_{2}\rrbracket\\}C_{1}||C_{2}\\{\llbracket\Gamma^{\prime}_{1}\rrbracket*\llbracket\Gamma^{\prime}_{2}\rrbracket\\}$
(425)

Showing 424 requires showing

$\displaystyle\llbracket\Gamma_{1},\Gamma_{2}\rrbracket\sqsubseteq\llbracket\Gamma_{1}\rrbracket*\llbracket\Gamma_{2}\rrbracket$
(426)

$\displaystyle\llbracket\Gamma^{\prime}_{1}\rrbracket*\llbracket\Gamma^{\prime}_{2}\rrbracket\sqsubseteq\llbracket\Gamma^{\prime}_{1},\Gamma^{\prime}_{2}\rrbracket$
(427)

By using 426 and 427(trivial to show as ”,” and ”*” for denotation of type
contexts are both semantically equivalent to $\cap$) as antecedents to Views
Logic’s consequence rule, we can conclude 424.

###### Case 78

-M where C has form $\textsf{RCUWrite}\,x.f\text{ as }y\text{ in }C$ which desugars into

$\textsf{WriteBegin};x.f:=y;C;\textsf{WriteEnd}$

We assume from the rule ToRCUWrite

$\displaystyle\Gamma,y:\textsf{rcuItr}\;\\_\vdash_{M}C\dashv\Gamma^{\prime}$
(428) $\displaystyle\textsf{FType}(f)=\textsf{RCU}$ (429)
$\displaystyle\textsf{NoFresh}(\Gamma^{\prime})$ (430)
$\displaystyle\textsf{NoFreeable}(\Gamma^{\prime})$ (431)
$\displaystyle\textsf{NoUnlinked}(\Gamma^{\prime})$ (432)
$\displaystyle\\{\llbracket\Gamma\,,y:\textsf{rcuItr}\;\\_\rrbracket_{M,tid}\\}C\\{\llbracket\Gamma^{\prime}\rrbracket_{M,tid}\\}$
(433)

Our goal is to prove

$\displaystyle\begin{array}[]{l}\\{\llbracket\Gamma\rrbracket_{M,tid}\\}\textsf{WriteBegin};C;\textsf{WriteEnd}\\{\llbracket\Gamma^{\prime}\rrbracket_{M,tid}\\}\end{array}$
(435)

Any case of $C$ does not change the state(no heap update) by assumptions
430-432 therefore 435 follows from assumptions 428-433 trivially.

######  Lemma 24 (Context-SubTyping-M)

$\Gamma\prec:\Gamma^{\prime}\implies\llbracket\Gamma\rrbracket_{M,tid}\sqsubseteq\llbracket\Gamma^{\prime}\rrbracket_{M,tid}$

###### Proof

Induction on the subtyping derivation. Then inducting on the first entry in
the non-empty context(empty case is trivial) which follows from 26.

######  Lemma 25 (Context-SubTyping-R)

$\Gamma\prec:\Gamma^{\prime}\implies\llbracket\Gamma\rrbracket_{R,tid}\sqsubseteq\llbracket\Gamma^{\prime}\rrbracket_{R,tid}$

###### Proof

Induction on the subtyping derivation. Then inducting on the first entry in
the non-empty context(empty case is trivial) which follows from 27.

######  Lemma 26 (Singleton-SubTyping-M)

$x:T\prec:x:T^{\prime}\implies\llbracket
x:T\rrbracket_{M,tid}\sqsubseteq\llbracket x:T^{\prime}\rrbracket_{R,tid}$

###### Proof

Proof by case analysis on structure of $T^{\prime}$ and $T$. Important case
includes the subtyping relation is defined over components of rcuItr type.
$T^{\prime}$ including approximation on the path component

$\rho.f_{1}\prec:\rho.f_{1}|f_{2}$

together with the approximation on the field map

$\mathcal{N}([f_{1}\rightharpoonup\\_])\prec:\mathcal{N}([f_{1}|f_{2}\rightharpoonup\\_])$

lead to subset inclusion in between a set of states defined by denotation of
the $x:T^{\prime}$ the set of states defined by denotation of the $x:T$(which
is also obvious for T-Sub). Reflexive relations and relations capturing base
cases in subtyping are trivial to show.

######  Lemma 27 (Singleton-SubTyping-R)

$x:T\prec:x:T^{\prime}\implies\llbracket
x:T\rrbracket_{M,tid}\sqsubseteq\llbracket x:T^{\prime}\rrbracket_{M,tid}$

###### Proof

Proof is similar to 26 with a single trivial reflexive derivation relation
(T-TSub2)

$\textsf{rcuItr}\prec:\textsf{rcuItr}$

##  Appendix 0.B RCU BST Delete

$\small\begin{array}[]{@{}l@{}}void\;delete(\;\texttt{int}\;data)\;\\{\\\
\;\;WriteBegin;\\\ \;\;\text{// Find data in the tree}\\\ \;\;\text{// Root is
never empty and its value is unique id}\\\
\;\;BinaryTreeNode\;current,\;parent=root;\\\
\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{parent:rcuItr\;\epsilon\;\\{\\}\right\\}}\\\
\;\;current=parent.Right;\\\
\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{parent:rcuItr\;\epsilon\;\\{Right\mapsto
current\\}\right\\}}\\\
\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:rcuItr\;Right\;\\{\\}\right\\}}\\\
\;\;while\;(current!=null\&\&current.data!=data)\\\ \;\;\\{\\\
\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{parent:rcuItr\;(Left|Right)^{k}\;\\{(Left|Right)\mapsto
current\\}\right\\}}\\\
\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:rcuItr\;(Left|Right)^{k}.(Left|Right)\;\\{\\}\right\\}}\\\
\;\;\;\;if\;(current.data>data)\\\ \;\;\;\;\\{\\\ \;\;\;\;\;\;\text{//if data
exists it's in the left subtree}\\\ \;\;\;\;\;\;parent=current;\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{parent:rcuItr\;(Left|Right)^{k}\;\\{\\}\right\\}}\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:rcuItr\;(Left|Right)^{k}\;\\{\\}\right\\}}\\\
\;\;\;\;\;\;current=parent.Left;\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{parent:rcuItr\;(Left|Right)^{k}\;\\{Left\mapsto
current\\}\right\\}}\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:rcuItr\;(Left|Right)^{k}.Left\;\\{\\}\right\\}}\\\
\;\;\;\;\\}\\\ \;\;\;\;else\;if\;(current.data<data)\\\ \;\;\;\;\\{\\\
\;\;\;\;\;\;\text{//if data exists it's in the right subtree}\\\
\;\;\;\;\;\;parent=current;\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{parent:rcuItr\;(Left|Right)^{k}\;\\{\\}\right\\}}\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:rcuItr\;(Left|right)^{k}\;\\{\\}\right\\}}\\\
\;\;\;\;\;\;current=current.Right;\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{parent:rcuItr\;(Left|Right)^{k}\;\\{Right\mapsto
current\\}\right\\}}\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:rcuItr\;(Left|Right)^{k}.Right\;\\{\\}\right\\}}\\\
\;\;\;\;\\}\\\ \;\;\\}\\\
\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{parent:rcuItr\;(Left|Right)^{k}\;\\{(Left|Right)\mapsto
current\\}\right\\}}\\\
\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:rcuItr\;(Left|Right)^{k}.(Left|Right)\;\\{\\}\right\\}}\\\
\;\;\text{// At this point, we've found the node to remove}\\\
\;\;BinaryTreeNode\;lmParent=current.Right;\\\
\;\;BinaryTreeNode\;currentL=current.Left;\\\
\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:rcuItr(Left|Right)^{k}.(Left|Right)\\{Left\mapsto
currentL,Right\mapsto lmParent\\}\right\\}}\\\
\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{currentL:rcuItr\;(Left|Right)^{k}.(Left|Right).Left\;\\{\\}\right\\}}\\\
\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{lmParent:rcuItr\;Left|Right)^{k}.(Left|Right).Right\;\\{\\}\right\\}}\\\
\end{array}$ $\small\begin{array}[]{@{}l@{}}\;\;\text{// We now need to
"rethread" the tree}\\\ \;\;\text{// CASE 1: If current has no right child,
then current's left child becomes}\\\ \;\;\text{// the node pointed to by the
parent}\\\ \;\;if\;(current.Right==null)\\\ \;\;\\{\\\
\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{parent:rcuItr\;(Left|Right)^{k}\;\\{(Left|Right)\mapsto
current\\}\right\\}}\\\
\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:rcuItr\;(Left|Right)^{k}.(Left|Right)\;\\{Left\mapsto
currentL,Right\mapsto null\\}\right\\}}\\\
\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{currentL:rcuItr\;(Left|Right)^{k}.(Left|Right).Left\;\\{\\}\right\\}}\\\
\;\;\;\;if\;(parent.Left==current)\\\ \;\;\;\;\;\;\text{// parent.Value is
greater than current.Value}\\\ \;\;\;\;\;\;\text{// so make current's left
child a left child of parent}\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{parent:rcuItr\;(Left|Right)^{k}\;\\{Left\mapsto
current\\}\right\\}}\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:rcuItr\;(Left|Right)^{k}.Left\;\\{Left\mapsto
currentL,Right\mapsto null\\}\right\\}}\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{currentL:rcuItr\;(Left|Right)^{k}.Left.Left\;\\{\\}\right\\}}\\\
\;\;\;\;\;\;parent.Left=currentL;\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{parent:rcuItr\;(Left|Right)^{k}\;\\{Left\mapsto
current\\}\right\\}}\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:unlinked\right\\}}\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{currentL:rcuItr\;(Left|Right)^{k}.Left\;\\{\\}\right\\}}\\\
\;\;\;\;else\\\ \;\;\;\;\;\;\text{// parent.Value is less than
current.Value}\\\ \;\;\;\;\;\;\text{// so make current's left child a right
child of parent}\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{parent:rcuItr\;(Left|Right)^{k}\;\\{Right\mapsto
current\\}\right\\}}\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:rcuItr\;(Left|Right)^{k}.Right\;\\{Left\mapsto
currentL,Right\mapsto null\\}\right\\}}\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{currentL:rcuItr\;(Left|Right)^{k}.Right.Left\;\\{\\}\right\\}}\\\
\;\;\;\;\;\;parent.Right=currentL;\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{parent:rcuItr\;(Left|Right)^{k}\;\\{Right\mapsto
current\\}\right\\}}\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{currentL:rcuItr\;(Left|Right)^{k}.Right\;\\{\\}\right\\}}\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:unlinked\right\\}}\\\
\;\;\;\;\;\;SyncStart;\\\ \;\;\;\;\;\;SyncStop;\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:freeable\right\\}}\\\
\;\;\;\;\;\;Free(current);\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:undef\right\\}}\\\
\;\;\\}\\\ \end{array}$

$\small\begin{array}[]{@{}l@{}}\;\;\text{// CASE 2: If current's right child
has no left child, then current's right child}\\\ \;\;\text{ // replaces
current in the tree}\\\ \;\;else\;if\;(current.Left==null)\\\ \;\;\\{\\\
\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{parent:rcuItr\;(Left|Right)^{k}\;\\{(Left|Right)\mapsto
current\\}\right\\}}\\\
\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:rcuItr\;(Left|Right)^{k}.(Left|Right)\;\\{Left\mapsto
null,Right\mapsto lmParent\\}\right\\}}\\\
\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{currentL:rcuItr\;(Left|Right)^{k}.(Left|Right).Left\;\\{\\}\right\\}}\\\
\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{lmParent:rcuItr\;(Left|Right)^{k}.(Left|Right).Right\;\\{\\}\right\\}}\\\
\;\;\;\;if\;(parent.Left==current)\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{parent:rcuItr\;(Left|Right)^{k}\;\\{Left\mapsto
current\\}\right\\}}\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:rcuItr\;(Left|Right)^{k}.Left\;\\{Left\mapsto
null,Right\mapsto lmParent\\}\right\\}}\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{lmParent:rcuItr\;(Left|Right)^{k}.Left.Right\;\\{\\}\right\\}}\\\
\;\;\;\;\;\;\text{// parent.Value is greater than current.Value}\\\
\;\;\;\;\;\;\text{// so make current's right child a left child of parent}\\\
\;\;\;\;\;\;parent.Left=lmParent;\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{parent:rcuItr\;(Left|Right)^{k}\;\\{Left\mapsto
lmParent\\}\right\\}}\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:unlinked\right\\}}\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{lmParent:rcuItr\;(Left|Right)^{k}.Left\;\\{\\}\right\\}}\\\
\;\;\;\;else\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{parent:rcuItr\;(Left|Right)^{k}\;\\{Right\mapsto
current\\}\right\\}}\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:rcuItr\;(Left|Right)^{k}.Right\;\\{Left\mapsto
null,Right\mapsto lmParent\\}\right\\}}\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{lmParent:rcuItr\;(Left|Right)^{k}.Right.Right\;\\{\\}\right\\}}\\\
\;\;\;\;\;\;\text{// parent.Value is less than current.Value}\\\
\;\;\;\;\;\;\text{// so make current's right child a right child of parent}\\\
\;\;\;\;\;\;parent.Right=lmParent;\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{parent:rcuItr\;(Left|Right)^{k}\;\\{Right\mapsto
lmParent\\}\right\\}}\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{lmParent:rcuItr\;(Left|Right)^{k}.Right\;\\{\\}\right\\}}\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:unlinked\right\\}}\\\
\;\;\;\;\;\;SyncStart;\\\ \;\;\;\;\;\;SyncStop;\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:freeable\right\\}}\\\
\;\;\;\;\;\;Free(current);\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:undef\right\\}}\\\
\;\;\\}\\\ \end{array}$ $\small\begin{array}[]{@{}l@{}}\;\;\text{// CASE 3: If
current's right child has a left child, replace current with current's}\\\
\;\;\text{// right child's left-most descendent}\\\ \;\;else\\\ \;\;\\{\\\
\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{parent:rcuItr\;(Left|Right)^{k}\;\\{(Left|Right)\mapsto
current\\}\right\\}}\\\
\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:rcuItr\;(Left|Right)^{k}.(Left|Right)\;\\{Right\mapsto
lmParent,Left\mapsto currentL\\}\right\\}}\\\
\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{lmParent:rcuItr\;(Left|Right)^{k}.(Left|Right).Right\;\\{\\}\right\\}}\\\
\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{currentL:rcuItr\;(Left|Right)^{k}.(Left|Right).Left\;\\{\\}\right\\}}\\\
\;\;\;\;\text{// We first need to find the right node's left-most child}\\\
\;\;\;\;BinaryTreeNode\;currentF=new;\\\
\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{currentF:rcuFresh\right\\}}\\\
\;\;\;\;currentF.Right=lmParent;\\\
\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{currentF:rcuFresh\;\\{Right\mapsto
lmParent\\}\right\\}}\\\ \;\;\;\;currentF.Left=currentL;\\\
\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{currentF:rcuFresh\;\\{Right\mapsto
lmParent,Left\mapsto currentL\\}\right\\}}\\\
\;\;\;\;BinaryTreeNode\;leftmost=lmParent.Left;\\\
\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{lmParent:rcuItr\;(Left|Right)^{k}.(Left|Right).Right\;\\{Left\mapsto
leftmost\\}\right\\}}\\\
\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{leftmost:rcuItr\;(Left|Right)^{k}.(Left|Right).Right.Left\;\\{\\}\right\\}}\\\
\;\;\;\;if\;(lmParent.Left==null)\\{\\\
\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{lmParent:rcuItr\;(Left|Right)^{k}.(Left|Right).Right\;\\{Left\mapsto
null\\}\right\\}}\\\ \;\;\;\;\;\;currentF.data=lmParent.data;\\\
\;\;\;\;\;\;if\;(parent.Left==current)\\{\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{parent:rcuItr\;(Left|Right)^{k}\;\\{Left\mapsto
current\\}\right\\}}\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:rcuItr\;(Left|Right)^{k}.Left\;\\{Right\mapsto
lmParent,Left\mapsto currentL\\}\right\\}}\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{currentF:rcuFresh\;\\{Right\mapsto
lmParent,Left\mapsto currentL\\}\right\\}}\\\
\;\;\;\;\;\;\;\;\text{//current's right child a left child of parent}\\\
\;\;\;\;\;\;\;\;parent.Left=currentF;\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{parent:rcuItr\;(Left|Right)^{k}\;\\{Left\mapsto
currentF\\}\right\\}}\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:unlinked\right\\}}\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{currentF:rcuItr\;(Left|Right)^{k}.Left\;\\{Right\mapsto
lmParent,Left\mapsto currentL\\}\right\\}}\\\ \;\;\;\;\;\;\;\;SyncStart;\\\
\;\;\;\;\;\;\;\;SyncStop;\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:freeable\right\\}}\\\
\;\;\;\;\;\;\;\;Free(current);\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:undef\right\\}}\\\
\;\;\;\;\;\;\\}\\\ \;\;\;\;\;\;else\\{\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{parent:rcuItr\;(Left|Right)^{k}\;\\{Right\mapsto
current\\}\right\\}}\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:rcuItr\;(Left|Right)^{k}.Right\;\\{Right\mapsto
lmParent,Left\mapsto currentL\\}\right\\}}\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{currentF:rcuFresh\;\\{Right\mapsto
lmParent,Left\mapsto currentL\\}\right\\}}\\\
\;\;\;\;\;\;\;\;\text{//current's right child a right child of parent}\\\
\;\;\;\;\;\;\;\;parent.Right=currentF;\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{parent:rcuItr\;(Left|Right)^{k}\;\\{Right\mapsto
currentF\\}\right\\}}\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:unlinked\right\\}}\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{currentF:rcuItr\;(Left|Right)^{k}.Right\;\\{Right\mapsto
lmParent,Left\mapsto currentL\\}\right\\}}\\\ \;\;\;\;\;\;\;\;SyncStart;\\\
\;\;\;\;\;\;\;\;SyncStop;\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:freeable\right\\}}\\\
\;\;\;\;\;\;\;\;Free(current);\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:undef\right\\}}\\\
\;\;\;\;\;\;\\}\\\ \;\;\;\;\\}\end{array}$

$\small\begin{array}[]{@{}l@{}}\;\;\;\;else\\{\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{lmParent:rcuItr\;(Left|Right)^{k}.(Left|Right).Right\;\\{Left\mapsto
leftmost\\}\right\\}}\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{leftmost:rcuItr\;(Left|Right)^{k}.(Left|Right).Right.Left\;\\{\\}\right\\}}\\\
\;\;\;\;\;\;while\;(leftmost.Left!=null)\\\ \;\;\;\;\;\;\\{\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{lmParent:rcuItr\;(Left|Right)^{k}.(Left|Right).Right.Left(Left)^{l}\;\\{Left\mapsto
leftmost\\}\right\\}}\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{leftmost:rcuItr\;(Left|Right)^{k}.(Left|Right).Right.Left(Left)^{l}.Left\;\\{\\}\right\\}}\\\
\;\;\;\;\;\;\;\;lmParent=leftmost;\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{lmParent:rcuItr\;(Left|Right)^{k}.(Left|Right).Right.Left(Left)^{l}.Left\;\\{\\}\right\\}}\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{leftmost:rcuItr\;(Left|Right)^{k}.(Left|Right).Right.Left(Left)^{l}.Left\;\\{\\}\right\\}}\\\
\;\;\;\;\;\;\;\;leftmost=lmParent.Left;\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{lmParent:rcuItr\;(Left|Right)^{k}.(Left|Right).Right.Left(Left)^{l}.Left\;\\{Left\mapsto
leftmost\\}\right\\}}\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{leftmost:rcuItr\;(Left|Right)^{k}.(Left|Right).Right.Left(Left)^{l}.Left.Left\;\\{\\}\right\\}}\\\
\;\;\;\;\;\;\\}\\\ \;\;\;\;\;\;currentF.data=leftmost.data;\\\
\;\;\;\;\;\;if\;(parent.Left==current)\\{\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{parent:rcuItr\;(Left|Right)^{k}\;\\{Left\mapsto
current\\}\right\\}}\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:rcuItr\;(Left|Right)^{k}.Left\;\\{Right\mapsto
lmParent,Left\mapsto currentL\\}\right\\}}\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{currentF:rcuFresh\;\\{Right\mapsto
lmParent,Left\mapsto currentL\\}\right\\}}\\\
\;\;\;\;\;\;\;\;\text{//current's right child a left child of parent}\\\
\;\;\;\;\;\;\;\;parent.Left=currentF;\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{parent:rcuItr\;(Left|Right)^{k}\;\\{Left\mapsto
currentF\\}\right\\}}\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:unlinked\right\\}}\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{currentF:rcuItr\;(Left|Right)^{k}.Left\;\\{Right\mapsto
lmParent,Left\mapsto currentL\\}\right\\}}\\\ \;\;\;\;\;\;\;\;SyncStart;\\\
\;\;\;\;\;\;\;\;SyncStop;\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:freeable\right\\}}\\\
\;\;\;\;\;\;\;\;Free(current);\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:undef\right\\}}\\\
\;\;\;\;\;\;\\}\\\ \;\;\;\;\;\;else\\{\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{parent:rcuItr\;(Left|Right)^{k}\;\\{Right\mapsto
current\\}\right\\}}\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:rcuItr\;(Left|Right)^{k}.Right\;\\{Right\mapsto
lmParent,Left\mapsto currentL\\}\right\\}}\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{currentF:rcuFresh\;\\{Right\mapsto
lmParent,Left\mapsto currentL\\}\right\\}}\\\
\;\;\;\;\;\;\;\;\text{//current's right child a right child of parent}\\\
\;\;\;\;\;\;\;\;parent.Right=currentF;\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{parent:rcuItr\;(Left|Right)^{k}\;\\{Right\mapsto
currentF\\}\right\\}}\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:unlinked\right\\}}\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{currentF:rcuItr\;(Left|Right)^{k}.Right\;\\{Right\mapsto
lmParent,Left\mapsto currentL\\}\right\\}}\\\ \;\;\;\;\;\;\;\;SyncStart;\\\
\;\;\;\;\;\;\;\;SyncStop;\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:freeable\right\\}}\\\
\;\;\;\;\;\;\;\;Free(current);\\\
\;\;\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{current:undef\right\\}}\\\
\;\;\;\;\;\;\\}\\\ \end{array}$
$\small\begin{array}[]{@{}l@{}}\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{lmParent:rcuItr\;(Left|Right)^{k}.(Left|Right).Right.Left(Left)^{l}\;\\{Left\mapsto
leftmost\\}\right\\}}\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{leftmost:rcuItr\;(Left|Right)^{k}.(Left|Right).Right.Left(Left)^{l}.Left\;\\{Left\mapsto
null\\}\right\\}}\\\ \;\;\;\;\;\;BinaryTreeNode\;leftmostR=leftmost.Right;\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{leftmost:rcuItr\;(Left|Right)^{k}.(Left|Right).Right.Left(Left)^{l}.Left\;\left\\{\begin{array}[]{ll}Left\mapsto
null,\\\ Right\mapsto leftmostR\end{array}\right\\}\right\\}}\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{lmParent:rcuItr\;(Left|Right)^{k}.(Left|Right).Right.Left(Left)^{l}\;\\{Left\mapsto
leftmost\\}\right\\}}\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{leftmostR:rcuItr\;(Left|Right)^{k}.(Left|Right).Right.Left(Left)^{l}.Left.Right\;\\{\\}\right\\}}\\\
\;\;\;\;\;\;\text{// the parent's left subtree becomes the leftmost's right
subtree}\\\ \;\;\;\;\;\;lmParent.Left=leftmostR;\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{leftmost:unlinked\right\\}}\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{lmParent:rcuItr\;(Left|Right)^{k}.(Left|Right).Right.Left(Left)^{l}\;\\{Left\mapsto
leftmostR\\}\right\\}}\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{leftmostR:rcuItr\;(Left|Right)^{k}.(Left|Right).Right.Left(Left)^{l}.Left\;\\{\\}\right\\}}\\\
\;\;\;\;\;\;SyncStart;\\\ \;\;\;\;\;\;SyncStop;\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{leftmost:freeable\right\\}}\\\
\;\;\;\;\;\;Free(leftmost);\\\
\;\;\;\;\;\;{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\left\\{leftmost:undef\right\\}}\\\