ch:concurrent-separation: ch:concurrent-separation

Problem and result. Build a finite scheduler for the control states of the CAS loop without collapsing physical reduction into abstract commitment. The accepted program prints eight named results followed by the exact summary in subsubappendix E.3.20.

Representation. Use Phase with constructors Ready, Loaded Nat, and Returned Nat. A World stores the physical counter, abstract commit count, and the two phases. Keeping both counters is load-bearing: one may then assert that load and failed CAS preserve the abstract count. A single current-counter field would be unable to detect accidental commitment on a failure branch.

First complete version. Implement one load and one CAS function for each thread. Load changes Ready to Loaded counter. CAS compares that saved value with the current counter. Equality increments the physical counter and commit count together and returns the saved value. Inequality changes the phase back to Ready and preserves both counts. Check the uncontended case before adding interleavings.

The racing calculations. Load both threads at counter $5$. In one test, run the left CAS first and then the right CAS; in the symmetric test, reverse them. The loser must be ready with counter $6$ and one commit. For the retry test, load the loser again and execute its CAS; the final counter is $7$, the commit count is $2$, and the return values are $5$ and $6$.

Logical boundary checks. Implement authority validity as the finite inequality fragment <= authority. Accept equal values and reject a fragment one larger than the authority. Model namespace access by a Boolean recording whether it is open; an open namespace cannot be opened again. Finally, model one exchanger step as a function of a pair that returns the swapped pair. This last function represents one paired transition, not two independent unary calls.

A failing version. In the failure branch of the right CAS, increment both counters while returning the thread to ready. The source still typechecks and audits cleanly, but the left-wins and retry oracles fail. Restore preservation of both counters to repair the implementation.

Acceptance test. Run the four commands from subsubappendix E.3.20. Require the eight exact case names, the final summary, and audit output []. Compare the run byte for byte with accepted-output.txt.

Mathematical boundary. The checker replays the physical schedule of section 45.1, the authority inequality of definition 45.4, and the paired transition of section 45.7. It does not interpret Iris propositions, masks, fancy updates, invariants, weakest preconditions, or atomic-update continuations. Consequently it supplies no proof of theorem 45.9, theorem 45.10, corollary 45.11.