ch:concurrent-separation: ch:concurrent-separation

After thread 1 succeeds, the physical value is $6$ and the return multiset is $\{5\}$. Thread 2’s stale CAS fails, so neither quantity changes. It loads $6$, successfully compares and swaps $6$ for $7$, and returns $6$. The final physical value is $7$, and the return multiset is $\{5,6\}$. The successful CAS steps, and only those steps, change the physical counter and may represent the abstract transitions $5{⟶}_{\mathsf{a}}6$ and $6{⟶}_{\mathsf{a}}7$.

In the affine instance, every listed assertion is affine. The assertions $\mathsf{True}$, $◻P$, and ${\mathsf{inv}}_N(P)$ are persistent. Exclusive points-to $\ell {\mapsto }_{\mathsf{h}}v$ is not persistent: duplicating it would produce two full owners of the same physical cell and contradict (Pt-exclusive). The persistently modality makes its body duplicable by construction. A named invariant is duplicable as a controlled access capability; its body is not duplicated.

The first opening begins at $E$ with $\uparrow N\subseteq E$ and leaves the mask $E\setminus \uparrow N$. A second use would require $\uparrow N\subseteq E\setminus \uparrow N$, which is false. The first closing continuation consumes $▹(\ell {\mapsto }_{\mathsf{h}}5)$ and changes the mask from $E\setminus \uparrow N$ back to $E$. The premise $\uparrow N\subseteq E$ then holds again, so a later opening is admissible. At no point are two copies of the points-to assertion available.

A frame compatible with $\bullet m\cdot \circ n$ cannot contain a second authority; write its largest fragment index as $k$. Validity gives $k\le m$. After the simultaneous update, both $k\le m+1$ and $n+1\le m+1$, so the maximum fragment index is compatible with the new authority. Hence the update preserves every frame.

For the rejected update, take $m=n$ and the empty additional frame. Its target is $\bullet m\cdot \circ (m+1)=(m,m+1)$, which is invalid because $m+1\nleqq m$. Thus even the empty frame witnesses failure.

At the load, opening supplies $\ell {\mapsto }_{\mathsf{h}}v$; loading preserves it, so the abort continuation consumes the same assertion and restores the atomic update. At CAS, opening supplies the current $\ell {\mapsto }_{\mathsf{h}}w$. When the comparison succeeds, CAS produces $\ell {\mapsto }_{\mathsf{h}}(w+1)$, and the commit continuation produces the postcondition at return value $w$. When it fails, CAS preserves $\ell {\mapsto }_{\mathsf{h}}w$, and abort restores the atomic update for the recursive call. Committing at load would select $v$ before the successful CAS; another thread could change the cell to $w\ne v$, so the eventual returned old value would be $w$, not the prematurely committed $v$.

Absence of stuck reachable threads follows from the not-stuck clause of corollary 45.11. None of the other four claims follows. The weakest precondition is partial, so it gives no termination or fairness. Its postcondition is $\mathsf{True}$, so it records neither the final cell nor the returned values. The semantics is HeapLang’s interleaving semantics, not a weak-memory or fairness model.

Before load, the atomic update is available at the empty client mask and no points-to resource is owned by the loop proof. Opening it yields $\ell {\mapsto }_{\mathsf{h}}v$, an abort continuation returning the same assertion, and a commit continuation expecting $\ell {\mapsto }_{\mathsf{h}}(v+1)$. The load preserves the points-to assertion; abort closes the update, restores the empty mask, and no abstract transition has occurred.

Before CAS the update is opened afresh at current value $w$. Success yields $\ell {\mapsto }_{\mathsf{h}}(w+1)$; commit closes the update, restores the mask, produces the client postcondition at return $w$, and records $w{⟶}_{\mathsf{a}}w+1$. Failure yields $\ell {\mapsto }_{\mathsf{h}}w$; abort closes the update and restores the mask for the Löb hypothesis, with no abstract transition.

Opening the invariant yields an $m$ with $\ell {\mapsto }_{\mathsf{h}}m\ast {\mathsf{own}}_{\gamma }(\bullet m)$. Combining the authority with the client’s ${\mathsf{own}}_{\gamma }(\circ n)$ is valid, so (Auth-agree) gives $n\le m$. A successful CAS changes the physical assertion to $\ell {\mapsto }_{\mathsf{h}}(m+1)$; simultaneously use (Auth-inc) to obtain ${\mathsf{own}}_{\gamma }(\bullet (m+1))\ast {\mathsf{own}}_{\gamma }(\circ (n+1))$. Return the new points-to assertion and authority to the invariant. The client retains the fragment ${\mathsf{own}}_{\gamma }(\circ (n+1))$.

In the pinned increment.v, lines 22–23 state incr_phy_spec for incr_phy at the empty mask, with exclusive physical points-to $v$, post-state $v+1$, and return $v$. Lines 104–108 state incr_spec for the atomic-heap incr at the atomic-heap namespace, conditional on heap_inv, with the corresponding abstract points-to contract. Lines 175–177 state incr_client_safe: heap_inv entails the default-mask weakest precondition for incr_client, whose postcondition is $\mathsf{True}$. The client definition on lines 170–173 calls incr. Program equality or a refinement connecting that interface program to incr_phy is not among these theorem premises, so substituting the latter program is not licensed.

The independent relation $R(a,r)$ can contain every pair of values, so it permits $a$ to return any possible partner. Two independent memberships $R(a,r_1)$ and $R(b,r_2)$ do not imply $r_1=b$ and $r_2=a$; they may choose unrelated values. A useful specification must retain a shared matching relation whose one transition consumes the two pending offers and simultaneously establishes both cross-equalities. This is the paired transition in (Exchange), not two independent choices.