> There is a general rule in compilers that no program should be able
> to detect the reordering done by a compiler. A similar rule holds for
> the multithreaded case. For example,
This seems like a circular argument: It assumes a base semantics for the
program, but it is exactly those semantics that we are trying to define. By
"no program should be able to detect," I assume the meaning is that it
should not be able to detect a violation of these base semantics. For a
multithreaded case, while we are still trying to find the base semantics,
what does "no program should be able to detect the reordering" mean?
More concretely, for the first two examples below, would we want to allow
the reorderings if the variables were not volatile? Why or why not?
Along the same lines, Bill said:
> add something like weak fairness to the formal semantics: that if a
> thread has a infinite number of opportunities to make progress, it
> will make progress.
Lazy release consistent software DSMs don't obey the above in general. (The
second example below - called Example 1 - breaks if the variables are not
volatile.) Statements like the above therefore need to be made in the
context of the rest of the memory model.
I can elaborate on more specifics regarding the connection between liveness
and the memory model. But that may be premature since I think Bill would
like to see us drive towards a consensus on the rest of the model first.
Sarita
>
> At 4:07 PM -0500 6/29/01, Sarita Adve wrote:
> >Example 2:
> >----------
> >Thread 1:
> >while (some condition that is always true) {;}
> >Volatile1 = 1
> >
> >Thread 2:
> >if (Volatile1 == 1)
> > print "Error"
> >
> >If statements of Thread 1 are reordered, Thread 2 prints Error,
> which is not
> >SC.
>
> If the actions in thread 1 are reordered, then the program could
> detect a reordering that is not possible an execution of the original
> program. Of course, since we have multithreaded programs, we have to
> consider some of the strangeness that arises due to incorrectly
> synchronized programs.
>
>
> At 4:07 PM -0500 6/29/01, Sarita Adve wrote:
> >Example 1:
> >----------
> >Initially all variables are 0
> >Thread 1
> >Volatile1 = 1
> >while (A == 0) {;}
> >
> >Thread 2
> >while (Volatile1 != 1) {;}
> >print "Success"
>
> This example is a little different. An execution in which Thread 2
> never printed "Success" could be explained by an execution in which
> Thread 1 never got any time slices. To fix this, I think we need to
> add something like weak fairness to the formal semantics: that if a
> thread has a infinite number of opportunities to make progress, it
> will make progress.
>
> For example, that means in the following code:
>
> Example 3:
> Thread 1
> while (true)
> synchronized(A) {
> print "Thread 1"
> }
>
> Thread 2
> while (true)
> synchronized(A) {
> print "Thread 2"
> }
>
> it would be illegal to hoist the synchronization out of the loop
> (which would result in only one thread printing messages).
>
> I believe this also handles cases such as code spin waiting on a
> volatile variable.
>
> Note, however, that finite loops could be transformed. For example,
> in example 3, if the while loops were instead for loops that counted
> to one million, it would be legal to hoist the synchronization out of
> the loop. We discussed this a while back; while there are some
> quality of service issues, I think it would be far too nasty to have
> specific trip counts embedded in the formal semantics (e.g., "if a
> thread is able to make progress 100,000 times, it will make progress
> by no later than the 100,000th time it is able to make progress").
>
>
>
> Bill
>
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:32 EDT