Re: JavaMemoryModel: final fields, again

From: jmanson@cs.umd.edu
Date: Thu Jul 31 2003 - 17:26:46 EDT


Hi Hans,

Sorry I took so long to get back. These are very reasonable concerns to
have with the final field semantics as they are in the sample chapter.

By the way, for those who want to understand our motivation in more
detail, I suggest you look at

http://www.cs.umd.edu/~pugh/java/memoryModel/newFinal.pdf

which has the semantics, the justification and explanation for it in great
detail. Anyone interested in understanding the formal semantics of final
fields as we laid them out should probably look over the informal
description in the chapter, and look at the formal description in this
other document.

> Thanks Jeremy. I'm actually fairly happy with those answers. My real
> goal here is to come up with an alternate description which I can
> understand more easily, and which makes the implementation consequences
> a bit clearer. Here's an attempt:

A worthy goal.

> 1) We define the relation ddd as follows:
> We say b ddd1 a ("b is definitely data dependent in one step on a") if
> action a either
> - copies a value into r1, which is one of the inputs to b, or
> - loads a value into r1, which is one of the inputs to b, and this is
> the first time that value is read in the thread. (????)
> Ddd is the reflexive-transitive closure of ddd1. (More on the
> terminology later.)
>
> 2) A write action w in t0 is seen by a read action r in t1 through a final
> field x.f if there are write actions wf and wx in thread t0 writing x.f
> and x respectively and read actions rx and rf in a different thread t1
> reading x and x.f respectively, such that
>
> - wf and w happen before the constructor for x (i.e. the freeze action
> on x.f) completes, and the freeze happens before wx.
>
> - r ddd rf and rf ddd rx, i.e. t1 reads x (the published pointer), then
> x.f (the final field), and then performs r, which is definitely data
> dependent on the final field x.f.
>
> - rx reads the value written by wx.
>
> 3) If a write action w is seen by a read r thread a final field, then
> the read must see w or another write that happened no earlier. This is
> the only additional constraint imposed by final fields.
>
> Is this correct? If not, can it be tweaked to become correct?

This is a good first approximation. However, there are some corner cases
I see - not all of them are likely programming patterns, but they should
be covered.

First, ddd1 should not be the first time a value is loaded in a thread.
This is because a value could be loaded later in the thread in program
order, but moved earlier in the thread than the load of the final field.
In fact, any read of that memory location in thread t1 that is not via a
dereference chain from the final field should "taint" the location.

Next, it doesn't completely deal with writes to final fields due to
deserialization. For instance, we construct an object, deserialize into it
twice (from two different threads, with no happens-before relationship),
and publish it. Which values for the final fields it is guaranteed to
see?

Another issue that came up in our discussions is that freezes should "pass
between" threads. Take this example:

T1 T2 T3
o.f1 = 42; r1 = Global.a; s1 = Global.b;
freeze o.f1; Global.b = r2; s2 = s1.f1;
Global.a = o;

There is no reason for T3 not to get the same guarantees as T2, and see
42. I'm not sure you quite cover this; you say that the freeze has to
happen before the write of the object reference, which it doesn't here.

There are some other issues that came up that I think probably apply here;
the document I mention above is a good starting point.

                                        Jeremy

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



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