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

Alex Otenko oleksandr.otenko at gmail.com
Wed Sep 28 15:23:24 EDT 2016


This reasoning is actually quite complicated, and the original reasoning is ok, it just needs statements justifying the claims about happens-before between unsynchronizedGet and increments.

1. All lock acquires and lock releases are in total order and establish happens-before edges between lock releases and subsequent lock acquires (definition of synchronization order)

2. All statements in program order before a lock release happen-before any statements that are in program order after the lock acquires following that lock release (definition of transitive closure)

This is justification enough for the existence of happens-before between unsynchronizedGet and some increments - ie there are writes unsynchronizedGet cannot observe.


3. unsynchronizedGet cannot observe the writes that are after subsequent synchronizedGet in total synchronization order (slightly simplified statement, since synchronization order will only contain lock acquires/releases, not the whole operations).

4. Therefore, unsynchronizedGet observes one of the writes that precede the synchronizedGet in total synchronization order.

5. unsynchronizedGet either observes the same write that the synchronizedGet observes, or some preceding write. Trivially, the values seen by unsynchronizedGet are less or equal the values seen by synchronizedGet.


Alex

> On 28 Sep 2016, at 09:22, Aleksey Shipilev <shade at redhat.com> wrote:
> 
> 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
> 
> _______________________________________________
> Concurrency-interest mailing list
> Concurrency-interest at cs.oswego.edu
> http://cs.oswego.edu/mailman/listinfo/concurrency-interest



More information about the Concurrency-interest mailing list