RE: JavaMemoryModel: Relaxing formalization of "causal loop" safety

From: David Holmes (dholmes@dltech.com.au)
Date: Mon Jul 15 2002 - 11:57:39 EDT


Bill Pugh wrote:
> "Out-of-thin-air" safety requires that every read of a variable v see
> the value written by some write to v. Now, because there is no simple
> global clock, we can't require that a read see the value written by a
> _previous_ write.

I don't understand this. Is this a DSM issue? Surely uniprocessors and SMP's
do have a global clock.

> d) Relax the formalization of the causal loop aspect of "not out
> of thin air"
> safety. The specification will still say that all causal loops are
> prohibited, but only some causal loops will be prohibited by
> the formal
> rules of the specification, due to the difficulty in formally defining
> causal loops.
>
> As you can probably guess, I am now going to recommend d.

Providing a "safety net" by defining an informal property that can't be
expressed in the formal model doesn't seem unreasonable to me. There are a
number of such properties in the existing memory model - for example, the
rule that a variable can only be modified by the actions of a thread
executing the instructions of a Java program, prohibits word-tearing. The
important thing, from a specification perspective, is that such informal
properties are clearly part of the requirements of the spec.

David Holmes

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



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