[cpp-threads] Implementation of seq_cst load on x86

[Jeffrey Yasskin]

Practically, I'm looking for something to put in a comment in the
implementation of load(seq_cst), which needs to convince future
maintainers that it's correct. I was hoping for an argument at
approximately the formality of N2392. The Threads Basics argument was
a little too informal because it seems to assume a global clock and
doesn't explain why synchronization loads wind up sequentially
consistent.

Based on your mention of Peter Sewell, I found
http://www.cl.cam.ac.uk/~pes20/weakmemory/x86tso-paper.pdf, which may
be enough to link to. (If anything, that's _too_ formal.) I can
roughly see how to get from that model to sequential consistency on
xchg'es and loads, and maybe how to demonstrate the proper behavior
for mfence.

Thanks,
Jeffrey

On Sat, May 29, 2010 at 9:06 PM, Boehm, Hans <hans.boehm at hp.com> wrote:
> Peter Sewell's group (Cambridge) almost certainly has the best public formal description of the X86 memory model.  (They discuss some remaining issues with the Intel/AMD documents, though we believe they are not critical for the C++ memory model.)  They (particularly Mark Batty) have apparently also been working on formalizing the C++ memory model.  Thus I suspect they would be in the best position to give a definitive answer.  I unfortunately don't know of an existing paper that proves exactly that, but I suspect they're working on it.
>
> If you want an informal argument, I could probably construct that.  But it doesn't sound like that's what you're looking for?
>
> Hans
>
>> -----Original Message-----
>> From: cpp-threads-bounces at decadentplace.org.uk
>> [mailto:cpp-threads-bounces at decadentplace.org.uk] On Behalf
>> Of Jeffrey Yasskin
>> Sent: Wednesday, May 19, 2010 1:54 PM
>> To: cpp-threads at decadentplace.org.uk
>> Subject: [cpp-threads] Implementation of seq_cst load on x86
>>
>> Hello all,
>>
>> 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?
>>
>> Sorry if this was the wrong list to ask this question on.
>>
>> Thanks,
>> Jeffrey Yasskin
>>
>> [1]
>> http://www.justsoftwaresolutions.co.uk/threading/intel-memory-
>> ordering-and-c++-memory-model.html
>> and http://www.hpl.hp.com/personal/Hans_Boehm/c++mm/threadsintro.html