[cpp-threads] Examples of cross-thread ordering

[Jeremy Manson]

Shaz Qadeer wrote:
> I have one question about the synchronization order and one question
> about the synchronizes-with relation.
> 
> (1) I still don't understand how one figures out the synchronization
> order by observing a multithreaded execution.  Consider the following
> execution in which x is a volatile variable:
> // thread T1
> x = 1
> 
> // thread T2
> x = 2
> 
> What is the total synchronization order in this case?

This is a program, not an execution.

To give me an execution, you would have to give me a synchronization 
order.  The synchronization order is part of the execution.

The way the model works is that the execution is an input (including the 
synchronization order), and the model validates it.

Sometimes I am a little loose with my phraseology, so I am sorry if I 
said anything to mislead you earlier.

Your next question is probably "where does this execution ultimately 
come from"?  The somewhat flip answer is that that's the user's problem. 
  It is pretty easy to build one, though.  We have to assume an existing 
single-threaded semantics, but this assumption is built into the JMM 
(the existing semantics is called "The Rest of the Java Language 
Specification").  This single-threaded semantics, given a program, could 
generate actions -- you have to provide your own decision procedure for 
which values are returned by reads.  Any total order among the 
synchronization actions in this program would be a potential 
synchronization order; you just have to pick one and hope that the JMM 
validates it.

A trivial example of this would be anything that generates an SC 
execution.  To get the synchronization order, you simply pluck out the 
synchronization actions in the order they appear.

Ultimately, there is what you come up may or may not be validated by the 
JMM, but that's more to do with the decision procedure for which value 
can be returned by a read than the difficulty of generating a 
synchronization order.  We proved SC executions will be validated, and 
we proved that changing the program order among independent reads and 
writes has no effect on validation, so that covers a fair bit of ground.

You also might be looking for an operational semantics.  Our early 
attempts at a JMM were operational, but we stopped after we realized 
that such a semantics would be hopelessly more complicated than what we 
ultimately developed.


> (2) Suppose one does manage to come up with the synchronization order
> somehow.  Then the Java memory model says: "Each volatile write
> synchronizes-with all subsequent volatile reads of the same variable in
> the synchronization order".  What is the rationale for this definition?
> I could suggest at least two other plausible candidates:
> - Each volatile read/write synchronizes-with all subsequent volatile
> read/write to the same variable
> - Each volatile write synchronizes-with all subsequent volatile reads to
> the same variable that read the value written by the write
> Why did you choose your particular definition?

We considered both of these definitions, each of which provide different 
guarantees.  It came down to implementability vs. usefulness.  The first 
one you mention introduced more execution overhead on realistic 
platforms (specifically, extra work on x86, which would have been bad). 
  The second one provided fewer guarantees, but we could pick up the 
extra guarantees for free on realistic platforms, and they were useful 
ones (IIRC).

We had lots of arguments with fairly smart people about which platforms 
we cared about, and what would be useful / realistic on those platforms. 
  Just like what is happening on this list at this very moment, in fact!

It also mapped well to existing models, like location consistency and 
release consistency.

So, basically, your answer is that everyone agreed that it was 
lightweight enough to be implementable, and provided useful guarantees 
to programmers.  You can spelunk through the old JMM list archive 
looking for discussions on the topic if you feel so inclined.

I am very happy with the programmability of this model, because you 
basically get acquire/release semantics, which I find easy to 
understand.  That's just one person's opinion, though.

					Jeremy