[concurrent] notes from Leslie Lamport

Leslie Lamport’s "How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs" defines sequential consistency:

The customary approach to designing and proving the correctness of

multiprocess algorithms for such a computer assumes that the following

condition is satisfied: the result of any execution is the same as if

the operations of all the processors were executed in some sequential

order, and the operations of each individual processor appear in this

sequence in the order specified by its program. A multiprocessor

satisfying this condition will be called sequentially consistent.

Even on ARM/POWER: threads in the system must agree about a total order for the writes to a single memory location.

“weakly ordered” defined as follows:

Let a synchronization model be a set of constraints on memory accesses

that specify how and when synchronization needs to be done.

Hardware is weakly ordered with respect to a synchronization model

iff it appears sequentially consistent to all software that

obey the synchronization model.