Add Y in a separate line to the two-core model, initially X=Y=0 with no cached copies. Use the following abstract release/acquire publication contract for ordinary coherent memory in one shared domain: operations before a release are ordered before operations after an acquire that reads from that release (returns the value that release stored). There are no other writes.
Core | Ordered operations |
|---|---|
C0 publisher | W(X)=1, then release W(Y)=1. |
C1 consumer | acquire R(Y) into r1, then R(X) into r2. |
Named contract and initial X=Y=0 | Observation | Conclusion |
|---|---|---|
Specified release/acquire publication, no other writes | r1=1, r2=0 | Forbidden: the acquire read the only release of 1 and orders the payload read after X=1. |
Same contract | r1=1, r2=1 | Compatible with publication. |
Same contract | r1=0 | No publication edge from C0's release is established by that read; do not promise r2=1. |
Each annotation orders in one direction only. An acquire stops later accesses of its core from being performed before it. A release waits until every earlier access of its core is performed: in protocol terms, every earlier store holds its line in M and has been written into it. Accesses may still move into the protected region: an earlier access may be performed after an acquire, and a later one before a release.
Under TSO every load already acts as an acquire and every store as a release, since loads are performed in order and stores drain in FIFO order. That is why MP is forbidden under TSO with plain operations. RCsc acquires and releases (Arm LDAR and STLR, RISC-V .aq and .rl) are also ordered with each other, so a release followed by an acquire does not reorder. RCpc acquires (Arm LDAPR) may be performed before an earlier release to a different address.
The proof uses the identity of the write observed by the acquire. Initializing Y to 1 instead, or allowing other writers to publish the same 1, changes the argument. A trace must identify which release, not merely compare numeric flag values. In a real instruction test, exact acquire/release forms, scope and memory attributes must match the architecture's model.
Coherence is still required for each flag and payload line. It cannot manufacture the cross-location publication edge if software used ordinary unordered operations or the acquire did not read the intended release. Equally, release/acquire ordering does not authorize a dirty-responsible cache to lose the payload value during transfer.
No. That read did not observe C0's release. The publication edge used by the proof is absent, so the claimed guarantee does not follow from this contract.