This document adds to the prose description of the operational model. Here we note the major changes made to the model, and some ways of recovering older deprecated behaviour within our PPCMEM tool.

Changelog (inclusive of PPCMEM bug fixes)

Roughly in reverse-chronological order, since PLDI'11:

• Harmonise the preconditions of Partial Coherence Commitment rule, the Write Reaching Coherence Point rule, and the Accept Successful Write-Conditional Request rule, so that attention is paid to writes separated by a barrier, both from any thread whatsoever. This makes a difference on, among others, Z6.1+sync+lwsync+addr, found by Luc Maranget and independently Alan Stern.

• Restart reads to the same address when a program-order earlier read is satisfied (in PLDI'12 when they were committed). This makes a difference on MP+sync+ctrl-detr, found by Luc Maranget.

• Fix the internal instruction semantics to do address computations before data, so that (e.g.) writes that are only data-dependent on previous reads can start forwarding their value when that read is satisfied. There is no analogous useful purpose to doing data computation first, since an address-unknown write cannot forward. This makes a difference on LB+datas+WW, found by Peter Sewell and Luc Maranget.

• Strengthen requirements in thread subsystem rules to use "fully determined addresses" where appropriate, not just currently determined addresses, where the model speaks about program-order accesses that "might be to the same address". This makes a difference, among others, on MP+lwsync+addr-isync, found by Alan Stern.

--- the following two were described in our PLDI'12 paper ---

• Introduce write-conditional and (therefore) coherence points, which adds 3 new storage subsystem rules, Accept Successful and Failing Write-Conditional Requests and Write Reaching Coherence Point, together with modifications to check coherence point conditions in Accept Write Request and Partial Coherence Commitment rules, and corresponding modifications in the thread subsystem rules. Believed to be observationally indistinguishable, but the implemented version was buggy and could be distinguished for, e.g. Z6.1+sync+lwsync+addr.

• Forbid reads that are program-order after an uncommitted lwsync barrier to be satisfied (in PLDI'11 they could be, but would be forced to restart at the lwsync commit time). Believed to be observationally indistinguishable.

Model Options

With the (old) model option barrier_coherence_weak, Precondition 5 of Accept a Successful Write-Conditional Request was absent, and Precondition 3 of Write Reaching its Coherence only asked for a barrier from the writing thread. This version describes the (default) barrier_coherence_strong model option.

Action 1 of Satisfy Memory Read from Storage Subsystem is not done for the (old, buggy) model option restart_on_read_commit. Correspondingly, the Commit Instruction has an additional action: for a read, restart all in-flight memory reads and read-reserves that have read from a different write to the same address (unless that read read-from an in-flight write). This version describes the (default) model option restart_on_read_satisfy.