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

Aleksey Shipilev shade at redhat.com
Wed Sep 28 04:22:56 EDT 2016


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
 vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv

 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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <http://cs.oswego.edu/pipermail/concurrency-interest/attachments/20160928/6bc7714b/attachment.sig>


More information about the Concurrency-interest mailing list