Interaction trees and compositional linearizability

Guarded interaction trees

For $E:{\mathcal{U}}_i\to {\mathcal{U}}_i$ and $R:{\mathcal{U}}_i$, the complete constructor rules used in chapter 86 are

$\mathrm{\Gamma }⊢r:R$

$\mathrm{\Gamma }⊢\mathsf{Ret}(r):\mathsf{ITree}(E,R)$

$\mathrm{\Gamma }⊢t:\mathsf{ITree}(E,R)$

$\mathrm{\Gamma }⊢\mathsf{Tau}(t):\mathsf{ITree}(E,R)$

$\mathrm{\Gamma }⊢e:E(X)$$\mathrm{\Gamma }⊢k:X\to \mathsf{ITree}(E,R)$

$\mathrm{\Gamma }⊢\mathsf{Vis}(e,k):\mathsf{ITree}(E,R)$

Recursive calls must occur below $\mathsf{Tau}$ or inside a continuation of $\mathsf{Vis}$. Bind and interpretation are governed by the six equations (Bind-Ret)–(Bind-Vis) and (Interp-Ret)–(Interp-Vis).

For a candidate subtree relation $S$, the complete one-layer weak rules are

$a=b$

$\mathsf{EuttF}(S,\mathsf{Ret}(a),\mathsf{Ret}(b))$

$e:E(X)\text{ is identical on both sides}$$\mathrm{\forall }x:X.S(k(x),h(x))$

$\mathsf{EuttF}(S,\mathsf{Vis}(e,k),\mathsf{Vis}(e,h))$

$S(t,u)$

$\mathsf{EuttF}(S,\mathsf{Tau}(t),\mathsf{Tau}(u))$

$\mathsf{EuttF}(S,t,u)$

$\mathsf{EuttF}(S,\mathsf{Tau}(t),u)$

$\mathsf{EuttF}(S,t,u)$

$\mathsf{EuttF}(S,t,\mathsf{Tau}(u))$

$\mathsf{eutt}$ is the greatest fixed point of this monotone operator. The two asymmetric rules remain inside the inductive layer and therefore remove only finitely many unmatched silent steps.

The LTS and module rules

The artifact-local type ${\mathsf{Prog}}_E(A)$ is the greatest fixed point of $\mathcal{F}(X):=A+X+\sum _{B}E(B)\times (B\to X)$, with observations $\mathsf{Return}$, $\mathsf{Tau}$, and $\mathsf{Vis}$. Its productive substitution is the mutually corecursive pair $\mathsf{subst}$ and $\mathsf{bindSubst}$ whose six observation equations are displayed in definition 87.3; in particular, $${\mathsf{subst}}_M(\mathsf{Vis}(m,k))\equiv \mathsf{Tau}({\mathsf{bindSubst}}_M(k,M(m))).$$ The sequential-consistency judgment for finite thread traces is generated by

$\mathsf{SeqCons}(a,[])$

$a(i)=\mathsf{none}$$a^{\prime }(i)=\mathsf{some}⟨A,m⟩$$\mathrm{\forall }j\ne i.a(j)=a^{\prime }(j)$$\mathsf{SeqCons}(a^{\prime },p)$

$\mathsf{SeqCons}(a,i:\mathsf{call}(m)::p)$

$a(i)=\mathsf{some}⟨A,m⟩$$a^{\prime }(i)=\mathsf{none}$$\mathrm{\forall }j\ne i.a(j)=a^{\prime }(j)$$\mathsf{SeqCons}(a^{\prime },p)$

$\mathsf{SeqCons}(a,i:\mathsf{ret}(m,v)::p)$

For $M:\mathsf{Impl}(E,F)$ and $V:{\mathsf{Spec}}_T(E)$, the four visible thread-local linking rules are

$q(i)=\mathsf{Idle}$

$qi:\mathsf{call}(m)q[i\mapsto \mathsf{Cont}(m,M(m))]$

$q(i)=\mathsf{Cont}(m,\mathsf{Return}(v))$

$qi:\mathsf{ret}(m,v)q[i\mapsto \mathsf{Idle}]$

$q(i)=\mathsf{Cont}(m,\mathsf{Vis}(u,k))$$s{\mathsf{Step}}_V(i:\mathsf{call}(u))s^{\prime }$

$(q,s){⟶}_{\mathsf{CL}}(q[i\mapsto \mathsf{UCall}(m,u,k)],s^{\prime })$

$q(i)=\mathsf{UCall}(m,u,k)$$s{\mathsf{Step}}_V(i:\mathsf{ret}(u,v))s^{\prime }$

$(q,s){⟶}_{\mathsf{CL}}(q[i\mapsto \mathsf{Cont}(m,k(v))],s^{\prime })$

The silent case changes $\mathsf{Cont}(m,\mathsf{Tau}(p))$ to $\mathsf{Cont}(m,p)$ and leaves the underlay state fixed. Interleaving chooses one thread name and applies one thread-local rule; there is no scheduler state.

Possibility commits and LHL program rules

For possibilities $\rho ,\sigma$ over $V_F$, the two target commits are

${\rho }_S{\mathsf{Step}}_{V_F}(i:\mathsf{call}(m)){\sigma }_S$${\rho }_C(i)=\mathsf{CallPoss}(m)$${\sigma }_C(i)=\mathsf{CallDone}(m)$${\rho }_R(i)={\sigma }_R(i)=\mathsf{RetIdle}$$\mathrm{\forall }j\ne i.({\rho }_C(j),{\rho }_R(j))=({\sigma }_C(j),{\sigma }_R(j))$

$\rho {\mathsf{PossStep}}_i\sigma$

${\rho }_S{\mathsf{Step}}_{V_F}(i:\mathsf{ret}(m,v)){\sigma }_S$${\rho }_C(i)={\sigma }_C(i)=\mathsf{CallDone}(m)$${\rho }_R(i)=\mathsf{RetIdle}$${\sigma }_R(i)=\mathsf{RetPoss}(m,v)$$\mathrm{\forall }j\ne i.({\rho }_C(j),{\rho }_R(j))=({\sigma }_C(j),{\sigma }_R(j))$

$\rho {\mathsf{PossStep}}_i\sigma$

Every lifted commit and return step separately requires an inhabited successor predicate and predecessor/successor reachability coverage.

For ${\mathsf{SameExcept}}_i(f,g):=\mathrm{\forall }j\ne i.g(j)=f(j)$ and possibility predicates $X,Y$, put $$\mathsf{Advance}(X,Y):=(\mathrm{\exists }\sigma .Y\sigma )\wedge \mathrm{\forall }\sigma .Y\sigma ⟹\mathrm{\exists }\rho .X\rho \wedge \mathsf{PossSteps}(\rho ,\sigma ).$$ For interaction states $s=(q,x)$ and $t=(q^{\prime },x^{\prime })$, the exact commit obligation is The silent obligation replaces $\mathsf{Some}(e)$ by $\mathsf{None}$ and requires both the underlay state and possibility predicate to remain fixed. Use the reset and consumption operations from definition 88.6, and put $$Z_Y:={\mathsf{ConsumeSet}}_{i,m,v}(Y).$$ The exact return obligation is

The program judgment is the greatest relation closed by exactly these three outer-form rules:

$\mathcal{P}\subseteq \mathcal{Q}(v)$

$\mathcal{R},\mathcal{G},i⊢\{\mathcal{P}\}\mathsf{Return}(v)\{\mathcal{Q}\}$

$\mathsf{Stable}(\mathcal{R},\mathcal{S})$${\mathsf{Silent}}_i(\mathcal{G},\mathcal{P},\mathcal{S})$$\mathcal{R},\mathcal{G},i⊢\{\mathcal{P};\mathcal{S}\}p\{\mathcal{Q}\}$

$\mathcal{R},\mathcal{G},i⊢\{\mathcal{P}\}\mathsf{Tau}(p)\{\mathcal{Q}\}$

$\mathsf{Stable}(\mathcal{R},\mathcal{I})$$\mathsf{Stable}(\mathcal{R},{\mathcal{S}}_v)(v:A)$${\mathsf{Commit}}_i(\mathcal{G},\mathcal{P},\mathsf{call}(m),\mathcal{I})$$\mathrm{\forall }v:A.{\mathsf{Commit}}_i(\mathcal{G},\mathcal{P};\mathcal{I},\mathsf{ret}(m,v),{\mathcal{S}}_v)$$\mathrm{\forall }v:A.\mathcal{R},\mathcal{G},i⊢\{\mathcal{P};\mathcal{I};{\mathcal{S}}_v\}k(v)\{\mathcal{Q}\}$

$\mathcal{R},\mathcal{G},i⊢\{\mathcal{P}\}\mathsf{Vis}(m,k)\{\mathcal{Q}\}$

The module record additionally contains the eight field families listed in definition 88.8, including $\mathcal{C}$ and $\mathsf{all}\mathsf{\_}\mathsf{return}$.