ch:linearizability-hoare-logic: ch:linearizability-hoare-logic

For return $2$, the target transition is $[2,1]\mathsf{deq}/2[1]$. The state $[1,2]$ has only a return-$1$ dequeue transition, so it is rejected. The inhabited successor predicate is therefore the singleton state $[1]$.

For the empty predicate $Q$, the assertion “every $\sigma$ satisfying $Q$ has a predecessor” is true because there is no such $\sigma$. The assertion $\mathrm{\exists }\sigma .Q(\sigma )$ is false. Deleting that existential would let an impossible concrete return update every precondition to $Q$ and then discharge every later universal obligation by vacuity. The nonemptiness clause blocks exactly this derivation.

Let ${\mathcal{P}}_i(s,P)$ mean that the lock owner in $s$ is none or $i$. Suppose an ${\mathcal{R}}_i$ step leaves owner $i$ unchanged and may change none only to none. From owner none, the result is none and ${\mathcal{P}}_i$ holds; from owner $i$, the result is $i$ and ${\mathcal{P}}_i$ holds. These two cases prove stability. If the rely restriction is deleted, another thread $j$ may change owner $i$ to owner $j$. The initial state satisfies ${\mathcal{P}}_i$ and the final state does not, so that step is a counterexample.

Choose ${\sigma }_0$ with $Y({\sigma }_0)$. For each $\sigma$ satisfying $Y$, define ${\tau }_{\sigma }$ by The hypotheses on $\sigma$ give the two pre-consumption clauses of the consumption relation in definition 88.6; the definitions give its other five clauses. Hence $${\mathsf{ConsumeSet}}_{i,m,v}(Y)({\tau }_{{\sigma }_0}),$$ which proves inhabitation. For any consumed $\tau$, its witness $\sigma$ and the seven conjuncts of ${\mathsf{Consume}}_{i,m,v}$ give idle entries at $i$, equality ${\tau }_S={\sigma }_S$, and ${\tau }_C(j)={\sigma }_C(j)$ and ${\tau }_R(j)={\sigma }_R(j)$ for every $j\ne i$. These are exactly the reset-map facts requested; no relational postcondition or guarantee has been postulated.

In state $\mathsf{UCall}(m,u,k)$, every retained possibility has the overlay call for $m$ recorded and the call-commit postcondition for $u$. When the underlay returns $v$, the return-commit premise of LHL-Vis advances to an inhabited predicate in which thread $i$ records the target return and every $j\ne i$ retains its call and return components. The concrete thread state becomes $\mathsf{Cont}(m,k(v))$. Relational composition of the call and return postconditions supplies the precondition of the continuation judgment for $k(v)$. Hence the resulting state satisfies the continuation case of the soundness invariant.

Clauses one and two of $\mathcal{I}$ permit a predicate containing only the reachable possibility $[2,1]$ after the two enqueues: it has the correct concrete prefix and was reached by compatible updates. Without clause three, the equally compatible state $[1,2]$ need not be retained. When the concrete dequeue returns $1$, $[2,1]$ has no matching target successor, so update nonemptiness fails. Clause three requires every compatible target continuation to have a represented prefix and therefore forces $[1,2]$ to remain until the return is observed. The weakened invariant fails; the completeness theorem, which uses all three clauses, is unaffected.