On Tue, Sep 15, 2015 at 10:58 AM, Caldarale, Charles R < chuck.caldar...@unisys.com> wrote:
> > From: Yilong Li [mailto:yilong...@runtimeverification.com] > > Subject: Re: RV-Predict bugs > > > The following is a valid execution trace consists of 5 events: > > T1 T2 > > 1 READ null > > 2 WRITE s > > 3 READ s > > 4 READ ??? > > 5 READ s > > > where s is the result of sm.getString("sc.200"). > > > The question is what value T2 can read and then return in event 4. > > It's not clear what the READ ??? is intended to represent. > I put ??? there because I am trying to reason about what value this read can see. Sorry for the confusion. > > > The question boils down to: does the write in event 2 prevent event 4 > from > > reading the initial null value of st_200? > > It doesn't, but that's not the real problem. Well, it is the problem (at least part of it) because JLS says "Informally, a read *r* is allowed to see the result of a write *w* if there is no *happens-before* ordering to prevent that read." In this case, there is no HB ordering preventing event 3 to read the initial null value put by JVM. > Let's expand the example a bit: > > T1 T2 > 1 READ null from st_200 > 2a allocate obj > 2b WRITE obj->field > 2c WRITE obj into st_200 > 3 READ obj from st_200 > 4 READ obj->field > > Since there is no actual ordering of steps 2b (object initialization) and > 2c (object publication) in T1, T2 can observe them in the reverse order and > pick up an unitialized value for field. > OK, now I see what you are talking about. But consider the following hashcode example: public int hashCode() { if (hashCode == 0) { hashCode = computeHashCode(); // no object creation involved } return hashCode; } There is no object initialization/publication involved at all but the problem still exists: this method could return 0 even if the if-statement sees a non-zero value. Yilong > - Chuck > > > THIS COMMUNICATION MAY CONTAIN CONFIDENTIAL AND/OR OTHERWISE PROPRIETARY > MATERIAL and is thus for use only by the intended recipient. If you > received this in error, please contact the sender and delete the e-mail and > its attachments from all computers. > > > --------------------------------------------------------------------- > To unsubscribe, e-mail: dev-unsubscr...@tomcat.apache.org > For additional commands, e-mail: dev-h...@tomcat.apache.org > >
