> 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.
> 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. 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.
- 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
