----- Original Message -----
From: "Sarita Adve" <sadve@cs.uiuc.edu>
> 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.
I think it is worth noting that there are programs that might be deemed "not
correctly synchronized" by your definition, but are still "correct" in the
intent of the program (i.e. not broken or wrong). An example is the
double-check lock idiom where the code within the double-check is
idempotent. Another example is for caching algorithms that avoid
synchronization in ways that would cause rare race conditions, but the
result of such a race condition is not bad, provided that the common case is
for the race to win the way you want it to.
-- David Smiley
-------------------------------
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