RE: JavaMemoryModel: Specification

From: Bill Pugh (pugh@cs.umd.edu)
Date: Tue Jul 10 2001 - 20:19:20 EDT


At 4:31 PM -0500 7/10/01, Sarita Adve wrote:
>I would ideally like to evolve to the point where we can have the
>spec itself as being in two parts:
>
>(1) A specification of programs for which the system will appear
>sequentially consistent. Call these correctly synchronized programs.
>
>(2) A specification that states behavior for incorrectly synchronized
>programs.

No, this would be a big mistake.

In addition to the reasons I alluded to previously (and Keith spelled
out in more detail), there is a much more important reason to avoid
this approach.

The biggest problem with this approach is that if your program is
absolutely 100% datarace free, then you use volume 1 of the
specification.

However, if there exists even a single line of code anywhere in your
application or any of the libraries that has a data race, then you
have to put volume 1 back on the shelf and take down volume 2: "The
semantics of incorrectly synchronized programs".

My experience has been that lots of people make synchronization
errors, and I doubt we could get to a point where all of the Java
libraries were 100% synchronization error free.

Secondly, in Java, we want to allow applications to run untrusted
code. But if running untrusted code that contained a single
synchronization error moved your entire application from volume 1
semantics to volume 2 semantics, no one would be willing to run
untrusted code.

What we need is the ability to contain synchronization errors, so
that a synchronization error in one part of the program doesn't
destroy the correctness of synchronization elsewhere in the program.

And I think the only way to do that is to have one semantics that
describes the behavior of all programs, correctly and incorrectly
synchronized, and then to be able to derive properties of those
semantics for correctly synchronized programs.

At 4:31 PM -0500 7/10/01, Sarita Adve wrote:
>you will have to give what
>I call a "system-centric" spec for correctly synchronized programs, and it
>is highly likely that it will be over-specified for both synchronized and
>unsynchronized programs. Further, all the corner cases to guarantee SC for
>synchronized programs will have to be explicitly handled, and it could get
>pretty complicated.

I love a challenge. :-)

More seriously, I think we can make this approach work. If not, back
to the drawing board.

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