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

jingguo yao yaojingguo at gmail.com
Wed Sep 28 21:55:43 EDT 2016


Alex:


I like your explanation. Thanks.

2016-09-29 3:23 GMT+08:00 Alex Otenko <oleksandr.otenko at gmail.com>:

> 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
>
> _______________________________________________
> Concurrency-interest mailing list
> Concurrency-interest at cs.oswego.edu
> http://cs.oswego.edu/mailman/listinfo/concurrency-interest
>



-- 
Jingguo
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://cs.oswego.edu/pipermail/concurrency-interest/attachments/20160929/ff873bab/attachment-0001.html>


More information about the Concurrency-interest mailing list