[concurrency-interest] What can an incorrectly synchronized read see?

David Holmes davidcholmes at aapt.net.au
Wed Sep 28 04:52:33 EDT 2016


Is there a typo there Aleksey, the only OK outcome you listed was (0,0). ???

David

> -----Original Message-----
> From: Concurrency-interest [mailto:concurrency-interest-
> bounces at cs.oswego.edu] On Behalf Of Aleksey Shipilev
> Sent: Wednesday, September 28, 2016 6:23 PM
> To: concurrency-interest at cs.oswego.edu
> Subject: Re: [concurrency-interest] What can an incorrectly synchronized
> read see?
> 
> Hi,
> 
> On 09/28/2016 09:23 AM, jingguo yao wrote:
> > I think that unsynchronizedCount <= synchronizedCount is always true
> > for the above code provided that JVM implementations of read and write
> > operations for int type are atomic.
> 
> They are atomic, mandated by JLS.
> 
> 
> > When increment happens-before synchronizedGet, synchronizedGet sees
> 1.
> > And there is no happens-before order to prevent unsynchronizedGet from
> > seeing initial_write or increment. So unsynchronizedGet sees1 0 or 1.
> >
> > Happens-before digram for this case:
> >
> >   initial_write ---> increment ---> synchronizedGet
> >                                       ^
> >               unsynchronizedGet------/
> >
> > When synchronizedGet happens-before increment, synchronizedGet sees
> 0. Since
> > unsynchronizedGet happens-before increment, it can't see 1 written
> > by increment. It can only see 0 written by initial_write.
> >
> > Happens-before digram for this case:
> >
> >   initial_write ---> synchronizedGet ---> increment
> >                         ^
> >   unsynchronizedGet----/
> >
> > Is my reasoning correct?
> 
> Not quite, because I think it confuses the notion of program statements
> and actions in JMM. The analysis should use JMM rules as stated, like below.
> 
> Happens-before consistency says that in valid executions, the read has
> two relations with writes: a) with the writes that are tied in
> happens-before with the read in question, the read can see only the
> *latest* write in HB -- not the one before it, not the one after the
> read in HB; b) with the writes that are not tied in happens-before with
> the read in question, the read can see whatever such write.
> 
> So, these both are valid executions under JMM:
> 
>                                r(val):0 --po-\
>                                              |
>  w(val, 1) --po/hb--> unlck(m) --sw/hb--> lck(m) --po/hb--> r(val):1
> 
> 
>                                r(val):1 --po-\
>                                              |
>  w(val, 1) --po/hb--> unlck(m) --sw/hb--> lck(m) --po/hb--> r(val):1
> 
>  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
>                                ^^^^^^^^^^^   ^^^^^^^^^^^^^^^^^^^^^^^^^
>                                  unsynch                 synch
>      parts done by Writer              parts done by Reader
> 
> 
> Where:
>   w(F,V) is the write of value "V" to field "F"
>   r(F):V is the read of value "V" from field "F"
>   lck/unlck(M) are the lock and unlock of the monitor M
>   --po/hb--> is the happens-before edge induced by program order
>   --sw/hb--> is the happens-before edge induced by synchronizes-with
>   --po--> is "just" the program order
> 
> Note that unsynchronized read can read either "0" or "1", regardless of
> if synchronized sees "1" after it.
> 
> Can the unsynchronized see "1", but the synchronized see "0"? Now, this
> is where it gets interesting. We cannot use the execution from above to
> justify reading synchronized "0", because synchronizes-with mandates
> seeing "1". Therefore, we need to reverse the order of Writer and Reader:
> 
> 
>                   parts done by Reader
>     unsync                                  synch
>  vvvvvvvvvvvvvv       vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv
> 
> vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv
> v
> 
>  r(val):V1 --po/hb--> lck(m) --po/hb--> r(val):V2 --po/hb--> unlck(m)
>                                                               /
>       /-----------------------sw/hb--------------------------/
>       v
>     lck(m) --po/hb--> w(val, 1)
> 
>  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
>     parts done by Writer
> 
> Now, let's see what (V1, V2) combinations do not violate JMM:
>  (0, 0) -- ok, both see some (default?) "0" write from before
>  (1, 0) -- NOT OK, r(val):V1 cannot see the w(val,1) that's after in HB!
>  (0, 1) and
>  (1, 1) -- NOT OK for this particular execution, because r(val):V2 sees
> the "future" write w(val,1). Notice, however, that both these results
> are justified by the execution at the very beginning, when Writer and
> Reader are sequenced in another order.
> 
> Hope this helps.
> 
> Thanks,
> -Aleksey




More information about the Concurrency-interest mailing list