Re: JavaMemoryModel: "synchronizes with"

From: Bart Jacobs (bart.jacobs@cs.kuleuven.ac.be)
Date: Thu Mar 25 2004 - 12:26:58 EST


Bill Pugh wrote:
> On Mar 25, 2004, at 10:17 AM, Bart Jacobs wrote:
>
>> Doug Lea wrote:
>>
>>> Bart nicely expanded on my suggestion to use "synchronizes with"
>>> instead here. I think we can adopt an equally rigorous usage that
>>> will still also allow use of "happens before" in main spec, by
>>> identifying "synchronizes-with" with the second clause of the HB
>>> definition. As in:
>>> I happens-before J if:
>>> 1) I is before J in program order
>>> 2) I synchronizes-with J
>>> 3) I happens-before K happens-before J for some K
>>> I synchronizes-with J if:
>>> I is an unlock or volatile write, and J is a matching unlock or
>>> volatile read that comes after I in the total order of
>>> synchronization actions. [Or whatever exact wording JSR133
>>> decides to go with here.]
>>
>>
>> I find this surprising.
>>
>> - (Is "allowing the use of happens-before" a valid motivation for
>> anything?)
>>
>> - With your definition, "synchronizes-with" is much less useful.
>> Importantly, it cannot be used in documentation for class libraries. A
>> client of a class library is interested in the actions of starting a
>> method invocation and returning from a method invocation, and the
>> edges between those actions; however, there are no synchronizes-with
>> edges between such actions since these are not synchronization actions
>> (unlocks, volatile writes, locks, volatile reads). Therefore, you need
>> program order and you need transitivity.
>
>
>
> The synchronizes-with interactions are the ones that need to be documented.
> The others can be inferred, and don't need to be documented.

I think what you're saying comes down to this: the documentation is at a
level of informality where there is no difference between saying "A
happens-before B" and saying "A synchronizes-with B". In that case, it
is misleading to define synchronizes-with formally as something
different from happens-before, as above.

Consider the example of Thread.interrupt:

Documentation A:
An invocation of Thread.interrupt synchronizes with a subsequent
invocation of Thread.isInterrupted.

Formally speaking, documentation A is false, since (the start/return of)
an invocation is not a synchronization action. Documentation A is true
only if you are at a level of informality where happens-before and
synchronizes-with are the same thing.

Documentation B:
An invocation of Thread.interrupt performs an action A and a subsequent
invocation of Thread.isInterrupted performs an action B such that A
synchronizes-with B.

Documentation B is true on the condition that by "an invocation I
performs an action A" you mean that the start of I happens-before A and
A happens-before the return of I. If you insist that A must be between
the start and the return of I in program order, then you are restricting
the implementation of these methods in a way that is not observable by
clients.

Another gripe I have with this definition is that it forces the use of
synchronization, even when program order might be sufficient. For example:

interface RealFunction {
     double evaluate(double x);
}

double computeIntegral(RealFunction f)

The documentation for this method might guarantee that the start of any
callback on evaluate performed during an invocation I of computeIntegral
happens-after the start of I. One implementation of this method could
perform callbacks in another thread and use synchronization, but another
implementation could choose to perform all callbacks in the thread of I.
If the documentation said: "the start of I synchronizes-with the start
of a callback", then an implementation would be forced to perform
synchronization, even if all callbacks occur in the thread of I.

>
> My only concern about the use of "synchronizes-with" is that is sounds
> symmetrical, and it is not.

I agree. It would probably be a bad idea to define "synchronizes-with"
as a non-symmetrical relation. I would suggest defining and using
something like "A synchronizes with B and A goes before B" for the
directed graph, and "A synchronizes with B" as a symmetrical relation.

-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel



This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:01:01 EDT