> -----Original Message-----
> From: owner-javamemorymodel@cs.umd.edu
> [mailto:owner-javamemorymodel@cs.umd.edu]On Behalf Of Bill Pugh
> Sent: Tuesday, July 10, 2001 11:14 AM
> To: javamemorymodel@cs.umd.edu
> Subject: Re: JavaMemoryModel: Specification
>
>
> A more appropriate term, although much more clumsy, would be "In the
> simple model". In other words, we can describe a set of properties
> that, if true, means that your program is "in the simple model", and
> can be understood using sequentially consistent semantics.
>
> These properties should not be part of the formal specification, but
> rather something derived from the formal specification (and it would
> be a goal of the formal spec to allow these properties to be
> derived). If you tried to put these properties directly into the
> formal specification, I would worry that there would be
> discontinuities at the boundary between "correct" and "incorrect"
> programs.
I don't understand this last bit. On the contrary, I think that the simplest
spec will do exactly what you seem to imply it shouldn't do. This is jumping
ahead, but 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.
(1) should be stated as simply as possible, as most people will likely deal
only with (1). Of course, it should capture all important, common
programming idioms, in a way that allows all common hardware/software
optimizations.
(2) should specify only the minimal behavior for adequate security, etc.,
again with minimal system restrictions. (2) could be a function of (1). We
could also mandate that the behavior specified by (2) is seen for all (i.e.,
including correctly synchronized) programs, but that may be redundant since
the SC requirement in (1) will likely be stronger.
You seem to be saying that dividing the spec in two components is
sub-optimal due to discontinuities, which I don't understand (especially if
(2) also specifies (partial) behavior for correctly synch programs). I think
merging the two could be sub-optimal because then 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 understand this is jumping ahead, but I would like to understand your
concern about a split specification better. Also, I am not averse to a
merged specification, if I am convinced that it isn't over-specified for
correctly synchronized programs.
Also, while we are discussing specifications, I noticed a message in the
archives from 11/16/00 that you sent, and I've included below. I believe the
example you gave is handled by specifying that if A happens before B, then A
should execute before B (all these terms can be precisely defined, but the
happens-before relation depends on the spec for correctly synchronized
programs). I would be very interested in seeing other properties you may
have identified for incorrectly synchronized programs.
Sarita
From: Bill Pugh (pugh@cs.umd.edu)
Date: Thu Nov 16 2000 - 20:20:00 EST
I was thinking back on some of the questions Sarita asked. As an
example, why can't we just say "type-safety" and "not-out-of-thin-air
safety" for incorrectly synchronized programs, and leave it at that?
Put aside issues like final fields, longs and doubles, virtual method
invocation and array length for the moment. Consider just reads and
writes of fields. What guarantees do we need other than:
* type safety
* not-out-of-thin-air safety
Consider the following program:
Thread 0:
lock Foo.a
Point tmp = new Point();
tmp.x = 1;
Foo.p = tmp
unlock Foo.a
Thread 1:
lock Foo.a
Point tmp = Foo.p
print "T1: " + tmp.x;
tmp.x = 2;
unlock Foo.a
Thread 2:
Point tmp = Foo.p
tmp.x = 3;
Thread 3:
lock Foo.a
Point tmp = Foo.p;
print "T3: " + tmp.x;
unlock Foo.a
Say further than we know thread 1 acquires Foo.a after it is released
by thread 0, and that thread 3 acquires Foo.a after it is released by
thread 1.
In this case, I think we need the following restrictions:
* When thread 1 prints tmp.x, it must not print 0, the initial value of
tmp.x
(i.e., it can print 1 or 3).
* When thread 3 prints tmp.x, it must not print either 0 or 1
(i.e., it can print 2 or 3).
Basically, the requirement is:
* Among a set of threads that are properly synchronized, certain writes
will not be visible to certain reads (of the same variable)
because they have
been overwritten.
Adding additional (perhaps incorrectly synchronized) reads or writes to
the
program must not make visible any of the writes previously considered to
be
overwritten.
This is enforced by my proposal, and I'm pretty sure it is enforced
by the CRF proposal. I can't imagine any transformation that would
destroy this, but it points out some of the subtle issues we need to
enforce if we try to build a JMM from the bottom-up (e.g., what do we
need more than sequential sequential consistency for correctly
synchronized programs).
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