Re: JavaMemoryModel: Why CnC

From: Bill Pugh (pugh@cs.umd.edu)
Date: Tue Jul 29 2003 - 09:59:31 EDT


At 5:45 AM -0500 7/29/03, Sarita Adve wrote:
>Bill and Jeremy,
>
>Can you give us all a *full* intuitive description of consistency+causality
>please? We don't have one yet that includes the effect of prohibited reads.
>Or are you going to argue that you don't need to have prohibited reads in
>your intuitive description? I hope that is not the case.
>

OK, here is yet another attempt at a complete but informal semantics.

An execution is legal if and only if:

* The execution respects intra-thread semantics.

* Each read sees a write that it is allowed to see by the happens-before
   ordering.

* There does not exist an action X such that in reasoning why X occurred,
   you have to assume that X occurred. You show this by showing that X is
   guaranteed to be allowed to happen, without assuming X has happened.

   Prohibited executions/reads allow you to say that certain executions cannot
   happen, perhaps due to compiler transformations such as redundant load
   elimination. If some executions are prohibited, and X is guaranteed
   to be allowed to happen in all non-prohibited executions, then X may be
   considered to be guaranteed to be allowed to occur.

   The only prohibited reads/executions that can be considered are ones that
   restrict the writes that could be seen by a read (e.g., this read always
   sees the previous write to this variable within this thread, or this read
   always sees the same write as was seen by another read of this variable in
   this thread).

   Optional clarification:

   We say "X is guaranteed to be allowed to happen", rather than saying
   "X is guaranteed to happen", because if X is a data race read, you can't
   guarantee which write X will see. So when we say a data race R that sees W
   is guaranteed to be _allowed_ to happen, we mean that it is guaranteed that:
   - the write W is guaranteed to happen
   - the read R is guaranteed to happen (although we can't guarantee which
     write it will see)
   - it is guaranteed that R could see W (they both access the same variable
     and the happens-before ordering does not prohibit R from seeing W).

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:47 EDT