> The corresponding formal part of the semantics are below. Note that I
> have clarified something: in order for a "happens before"
> relationship to be established, the release action must precede the
> acquire action.
>
> > * volatile writes and monitor exits are treated as
> synchronization releases.
> >
> > * volatile reads and monitor enters are treated as
> synchronization acquires.
> >
> >A synchronization release action and _a matching and following_
> >synchronization acquire action establish a "happens before"
> >relationship between the two threads. Program order within a thread
> >also establishes a happens before relationship, and "happens before"
> >is transitive.
> >
> >If two threads access the same normal field or array element, and one
> >of those accesses is a write, the accesses conflict. For any two
> >conflicting accesses, there should be a "happens before" relationship
> >between the two accesses. If all sequentially consistent executions
> >of a program are correctly synchronized (i.e., all conflicting
> >accesses are ordered), then the program is correctly synchronized and
> >follows sequentially consistent semantics.
Here is an alternative and equivalent way of defining a correctly
synchronized program. It's premature to be working on the formal spec yet,
but I thought I'd put it up so people can think about it before we move on.
A program is correctly synchronized if for every sequentially consistent
execution of the program, all accesses in a race are either volatile or
monitor accesses. In a sequentially consistent execution, two accesses are
said to race if they access the same location, one of them is a write, and
there is no intervening access between them.
Notes:
- The above does not distinguish between acquires and releases, but it can
be proved that it is equivalent to the happens-before based definition;
i.e., maintains the one-way barrier (acq/release) nature of volatiles and
monitors. In the context of the optimistic read idiom discussion, the
definition should also be applied to any aborted/retried accesses. So that
idiom (in original form) does not satisfy the definition since it could
generate non-volatile/monitor races.
- The phrase "no intervening access" is well-defined since all SC executions
impose a global order. It could be further formalized if needed.
- An advantage of the above definition is that it is shorter than the
happens-before definition; it may be more or less intuitive based on your
point of view.
Sarita
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:33 EDT