[cpp-threads] C++ memory model (N.M. Maclaren)

[N.M. Maclaren]

On Sep 17 2009, Mark Batty wrote:
>
>> My first comment is that I hope that you will put this on the Web.
>
>I don't know where people look for documents like this besides this
>list, did you have somewhere particular in mind?

No, and I am a fine one to talk, as I don't do it :-(

>> [...] the actions must be countable [...] is this solely to make the 
>> Axiom of Choice hold?
>
>Yes, at the moment but it might be important for proving a progress
>property as well.

OK.  There is a much simpler way to do it - because it is of general
importance, I am posting it.  You can assume countability, so all you
have to do is specify a semi-infinite ordering (i.e. bounded in the
past).  End of problem.  Well, almost.

The problem with specifications that are intended to apply to permanently
running processes is that it doesn't work very well, but let's skip that.
However, it raises the importance of another question, which is whether
the initial state must be one that is generatable by a valid execution of
the specification, or whether it must obey only the explicit restrictions
in that.

That may sound purely theoretical, but I have seen a couple of real-life 
problems that boiled down to that, and they both arose in a parallel 
context. I have also seen quite a lot of interpretations that depended on 
that, for both serial and parallel code. So it's extremely obscure and 
rare, but not wholly irrelevant.


Regards,
Nick Maclaren.