Possibility Reasoning and Linearizability Hoare Logic

Definition 88.1 — Thread and interaction states¶

For underlay signature $E$ and overlay signature $F$, a thread state is $$\mathsf{Idle}\mid \mathsf{Cont}(m,p)\mid \mathsf{UCall}(m,u,k),$$ where $m:F(A)$, $p:{\mathsf{Prog}}_E(A)$, and the last form records a suspended underlay call $u:E(B)$ with continuation $k:B\to {\mathsf{Prog}}_E(A)$. A thread map assigns one such state to every $i:\mathsf{Name}(T)$. For $V_E:{\mathsf{Spec}}_T(E)$, an interaction state is a pair $(q,s)$ of a thread map and a state of $V_E$.

Definition 88.2 — Possibilities and possibility sets¶

For a target specification $V_F:{\mathsf{Spec}}_T(F)$, a possibility is a triple $$\rho =⟨{\rho }_S,{\rho }_C,{\rho }_R⟩.$$ The component ${\rho }_S$ is a state of $V_F$. The components ${\rho }_C$ and ${\rho }_R$ are partial maps indexed by thread. For each thread, ${\rho }_C$ has one of the three forms $$\mathsf{CallIdle},\mathsf{CallPoss}(m),\mathsf{CallDone}(m).$$ For each thread, ${\rho }_R$ is $\mathsf{RetIdle}$ or $\mathsf{RetPoss}(m,v)$. A possibility set is represented by its predicate $$\mathsf{PossSet}(V_F):=\mathsf{Poss}(V_F)\to \mathsf{Prop}.$$ Thus the representation admits the empty predicate. Nonemptiness is a proof obligation of commit and return updates, not an invariant of the data type.

Definition 88.3 — Lifted possibility update¶

Let $P,Q:\mathsf{PossSet}(V_F)$. Define $\mathsf{Advance}(P,Q)$ to mean

1. $Q$ is inhabited;

2. every $\sigma$ satisfying $Q$ is reachable by $\mathsf{PossSteps}$ from some $\rho$ satisfying $P$.

The first clause prevents the empty predicate from satisfying an update merely by vacuity. The second is the artifact’s direction of lifted coverage: successors must have represented predecessors. A rule may prune an incompatible predecessor, as the next calculation requires; no converse coverage is built into $\mathsf{Advance}$.

Definition 88.5 — Assertions, relations, and stability¶

A precondition is a predicate $\mathcal{P}(s,P)$. A relational assertion is a predicate $\mathcal{R}(s,P,t,Q)$. Relational composition is $$(\mathcal{R};\mathcal{G})(s,P,u,W):=\mathrm{\exists }t,Q.\mathcal{R}(s,P,t,Q)\wedge \mathcal{G}(t,Q,u,W).$$ For a precondition $\mathcal{P}$, the mixed composition used below is $$(\mathcal{P};\mathcal{R})(t,Q):=\mathrm{\exists }s,P.\mathcal{P}(s,P)\wedge \mathcal{R}(s,P,t,Q).$$ The relation $\mathcal{Q}$ is stable under $\mathcal{R}$ when $$(\mathcal{Q};\mathcal{R})(s,P,t,Q)⟹\mathcal{Q}(s,P,t,Q).$$ A precondition is stable when taking one $\mathcal{R}$ step from a state that satisfies it yields another state that satisfies it. A postcondition is stable pointwise in its returned value. We abbreviate this relation-stability condition by $\mathsf{Stable}(\mathcal{R},\mathcal{Q})$.

Definition 88.6 — Commit, silent, and return obligations¶

For maps $f,g$ with domain $\mathsf{Name}(T)$, put $${\mathsf{SameExcept}}_i(f,g):=\mathrm{\forall }j:\mathsf{Name}(T).j\ne i⟹g(j)=f(j).$$ The relation $\mathsf{UnderStep}(u,\omega ,u^{\prime })$ is exactly the local relation given by CL-Underlay-call, CL-Underlay-ret, and the silent clause following those rules; $\omega$ is respectively a call, a return, or $\mathsf{None}$. Let $s=(q,x)$ and $t=(q^{\prime },x^{\prime })$ range over interaction states, and let $X,Y:\mathsf{PossSet}(V_F)$.

The judgment $${\mathsf{Commit}}_i(\mathcal{G},\mathcal{P},e,\mathcal{Q})$$ for $e:\mathsf{Event}(E)$ is the following quantified formula:

The judgment ${\mathsf{Silent}}_i(\mathcal{G},\mathcal{P},\mathcal{Q})$ is exact when Thus a silent step changes one thread state but keeps both the underlay state and the possibility predicate fixed.

Define ${\mathsf{Reset}}_i(q,x):=(q[i\mapsto \mathsf{Idle}],x)$. For $m:F(A)$ and $v:A$, the consumption relation is and $${\mathsf{ConsumeSet}}_{i,m,v}(Y)(\tau ):=\mathrm{\exists }\sigma .Y(\sigma )\wedge {\mathsf{Consume}}_{i,m,v}(\sigma ,\tau ).$$ The judgment $${\mathsf{ReturnStep}}_i(\mathcal{G},\mathcal{P},m,v,\mathcal{C})$$ is the formula This display includes every premise of the artifact definition: the thread-return observation, successor inhabitation and coverage inside $\mathsf{Advance}$, the two pending-status facts, the reset, and preservation of all unselected possibility components.

Definition 88.8 — Verified implementation families¶

A witness $$\mathsf{VerifyImpl}(V_E,V_F,\mathcal{R},\mathcal{G},\mathcal{P},M,\mathcal{Q},\mathcal{C})$$ consists of families indexed by thread, operation, and return type satisfying:

1. every ${\mathcal{R}}_i$ is reflexive and transitive;

2. $i\ne j$ implies ${\mathcal{G}}_i\subseteq {\mathcal{R}}_j$;

3. overlay invocations and returns by $i$ lie in ${\mathcal{R}}_j$ for $i\ne j$;

4. the initial interaction state and singleton initial possibility satisfy every ${\mathcal{P}}_i(m)$;

5. every ${\mathcal{P}}_i(m)$ is stable under ${\mathcal{R}}_i$;

6. after completing one operation, the continuation condition ${\mathcal{C}}_i(m,v)$ implies the precondition of the next operation;

7. every implementation body $M(m)$ satisfies the program judgment from ${\mathcal{P}}_i(m)$ through invocation and rely closure to ${\mathcal{Q}}_i(m)$;

8. the field $\mathsf{all}\mathsf{\_}\mathsf{return}$ proves $${\mathsf{ReturnStep}}_i({\mathcal{G}}_i,{\mathcal{P}}_i(m);{\mathcal{Q}}_i(m,v),m,v,{\mathcal{C}}_i(m,v))$$ for every $i,m,v$.

The family $\mathcal{C}$ and the final field are part of the frozen signature. Omitting either one proves a weaker record than the artifact’s $\mathsf{VerifyImpl}$.