[cpp-threads] Implementation of seq_cst load on x86

[Peter Sewell]

Jeffrey Yasskin writes: 
> I've seen assertions [1] that load(memory_order_seq_cst) can 
> be implemented as a simple mov on x86 as long as
> store(memory_order_seq_cst) is implemented as xchg. Does 
> anyone know of a paper that proves this claim from the 
> guarantees in Intel's and AMD's architecture documents?

We discuss those guarantees in the CACM and TPHOLs2009 papers at
http://www.cl.cam.ac.uk/~pes20/weakmemory/.  In terms of the
abstract-machine version of the x86-TSO model there, xchg flushes the
local store buffer, so programs which consist only of
memory_order_seq_cst operations would behave sequentially
consistently.  As Hans surmises, we are thinking about stronger
results along these lines, but there's nothing complete yet.

best wishes,
Peter