Quantcast

What can an incorrectly synchronized read see?

classic Classic list List threaded Threaded
12 messages Options
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

What can an incorrectly synchronized read see?

jingguo yao
Java code:

class Counter {
  private int val = 0;
  public synchronized int synchronizedGet() {
    return val;
  }
  public int unsynchronizedGet() {
    return val;
  }
  public synchronized void increment() {
    val++;
  }
}
class Writer extends Thread {
  private Counter c;
  public Writer(Counter c) {
    this.c = c;
  }
  @Override
  public void run() {
    c.increment();
  }
}
class Reader extends Thread {
  private Counter c;
  public Reader(Counter c) {
    this.c = c;
  }
  @Override
  public void run() {
    int unsynchronizedCount = c.unsynchronizedGet();
    int synchronizedCount = c.synchronizedGet();
    if (unsynchronizedCount > synchronizedCount)
      throw new RuntimeException("unsynchronized count is larger than synchronized count");
  }
}
public class UnsynchronizedRead {
  public static void main(String[] args) {
    Counter c = new Counter();
    Writer w = new Writer(c);
    Reader r = new Reader(c);
    w.start();
    r.start();
  }
}


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. Here is my reasoning.

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?


_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: What can an incorrectly synchronized read see?

Aleksey Shipilev-3
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
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest

signature.asc (836 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: What can an incorrectly synchronized read see?

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

David

> -----Original Message-----
> From: Concurrency-interest [mailto:concurrency-interest-
> [hidden email]] On Behalf Of Aleksey Shipilev
> Sent: Wednesday, September 28, 2016 6:23 PM
> To: [hidden email]
> 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


_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: What can an incorrectly synchronized read see?

Aleksey Shipilev-3
On 09/28/2016 10:52 AM, David Holmes wrote:
> Is there a typo there Aleksey, the only OK outcome you listed was (0,0). ???

Note that in my note, there are two classes of executions, depending on
the sequence of locks/unlocks in (R)eader and (W)riter.

(unsync, sync):
 (0, 0): justified by executions with R->W sequencing
 (0, 1): justified by executions with W->R sequencing
 (1, 0): is not justified by any executions
 (1, 1); justified by executions with W->R sequencing

>> -----Original Message-----
>> From: Concurrency-interest [mailto:concurrency-interest-
>> [hidden email]] On Behalf Of Aleksey Shipilev
>> Note that unsynchronized read can read either "0" or "1", regardless of
>> if synchronized sees "1" after it.

This is for W->R sequencing.

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

This is for R->W sequencing.

Thanks,
-Aleksey


_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest

signature.asc (836 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: What can an incorrectly synchronized read see?

Bobrowski, Maciej
Right, so the only invalid execution in any possible sequencing is the (1, 0) which was the main question of this post, correct?

-----Original Message-----
From: Concurrency-interest [mailto:[hidden email]] On Behalf Of Aleksey Shipilev
Sent: 28 September 2016 10:01
To: [hidden email]; [hidden email]
Subject: Re: [concurrency-interest] What can an incorrectly synchronized read see?

On 09/28/2016 10:52 AM, David Holmes wrote:
> Is there a typo there Aleksey, the only OK outcome you listed was (0,0). ???

Note that in my note, there are two classes of executions, depending on the sequence of locks/unlocks in (R)eader and (W)riter.

(unsync, sync):
 (0, 0): justified by executions with R->W sequencing  (0, 1): justified by executions with W->R sequencing  (1, 0): is not justified by any executions  (1, 1); justified by executions with W->R sequencing

>> -----Original Message-----
>> From: Concurrency-interest [mailto:concurrency-interest-
>> [hidden email]] On Behalf Of Aleksey Shipilev Note that
>> unsynchronized read can read either "0" or "1", regardless of if
>> synchronized sees "1" after it.

This is for W->R sequencing.

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

This is for R->W sequencing.

Thanks,
-Aleksey



--------------------------------------------------------------------------------

NOTICE: Morgan Stanley is not acting as a municipal advisor and the opinions or views contained herein are not intended to be, and do not constitute, advice within the meaning of Section 975 of the Dodd-Frank Wall Street Reform and Consumer Protection Act. If you have received this communication in error, please destroy all electronic and paper copies and notify the sender immediately. Mistransmission is not intended to waive confidentiality or privilege. Morgan Stanley reserves the right, to the extent permitted under applicable law, to monitor electronic communications. This message is subject to terms available at the following link: http://www.morganstanley.com/disclaimers  If you cannot access these links, please notify us by reply message and we will send the contents to you. By communicating with Morgan Stanley you consent to the foregoing and to the voice recording of conversations with personnel of Morgan Stanley.
_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: What can an incorrectly synchronized read see?

Aleksey Shipilev-3
On 09/28/2016 12:47 PM, Bobrowski, Maciej wrote:
> Right, so the only invalid execution in any possible sequencing is
> the (1, 0) which was the main question of this post, correct?

Correct. I wanted to show how to apply spec to arrive to this result,
and you get the collateral results for free too :)

NB: Mental trap: believing that arriving to the same result as
specification validates the alternative reasoning. (It might, though,
but you have to show that alternative reasoning gives correct answers
for all other cases too and/or has the clear boundaries where it applies)

Thanks,
-Aleksey


_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest

signature.asc (836 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: What can an incorrectly synchronized read see?

Alex Otenko
In reply to this post by Aleksey Shipilev-3
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 <[hidden email]> 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
> [hidden email]
> http://cs.oswego.edu/mailman/listinfo/concurrency-interest

_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: What can an incorrectly synchronized read see?

jingguo yao
Alex:


I like your explanation. Thanks.

2016-09-29 3:23 GMT+08:00 Alex Otenko <[hidden email]>:
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 <[hidden email]> 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
> [hidden email]
> http://cs.oswego.edu/mailman/listinfo/concurrency-interest

_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest



--
Jingguo


_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: What can an incorrectly synchronized read see?

jingguo yao
In reply to this post by Aleksey Shipilev-3
Aleksey:

Your reasoning is much more formal. Thanks.

2016-09-28 18:55 GMT+08:00 Aleksey Shipilev <[hidden email]>:
On 09/28/2016 12:47 PM, Bobrowski, Maciej wrote:
> Right, so the only invalid execution in any possible sequencing is
> the (1, 0) which was the main question of this post, correct?

Correct. I wanted to show how to apply spec to arrive to this result,
and you get the collateral results for free too :)

NB: Mental trap: believing that arriving to the same result as
specification validates the alternative reasoning. (It might, though,
but you have to show that alternative reasoning gives correct answers
for all other cases too and/or has the clear boundaries where it applies)

Thanks,
-Aleksey


_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest




--
Jingguo


_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: What can an incorrectly synchronized read see?

Alex Otenko
You need to be careful about using a “proof by example” as a proof. It is ok to use it to demonstrate what happens to two reads of two writes, but it is not a proof about all reads and all writes.

It is not as formal as it looks. How do you conclude it is sufficient to consider just two diagrams? How do you conclude it is sufficient to consider just four outcomes?

Is (500100, 100500) an allowed outcome? No? Why not?

You need to start reasoning how to arrive at the conclusion about that outcome from one of the four outcomes considered. You may discover then that you are using mechanisms that do not care about the four outcomes at all.


Alex

On 29 Sep 2016, at 03:05, jingguo yao <[hidden email]> wrote:

Aleksey:

Your reasoning is much more formal. Thanks.

2016-09-28 18:55 GMT+08:00 Aleksey Shipilev <[hidden email]>:
On 09/28/2016 12:47 PM, Bobrowski, Maciej wrote:
> Right, so the only invalid execution in any possible sequencing is
> the (1, 0) which was the main question of this post, correct?

Correct. I wanted to show how to apply spec to arrive to this result,
and you get the collateral results for free too :)

NB: Mental trap: believing that arriving to the same result as
specification validates the alternative reasoning. (It might, though,
but you have to show that alternative reasoning gives correct answers
for all other cases too and/or has the clear boundaries where it applies)

Thanks,
-Aleksey


_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest




--
Jingguo

_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest


_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: What can an incorrectly synchronized read see?

Aleksey Shipilev-3
On 09/29/2016 09:13 AM, Alex Otenko wrote:
> You need to be careful about using a “proof by example” as a proof. It
> is ok to use it to demonstrate what happens to two reads of two writes,
> but it is not a proof about *all* reads and *all* writes.
>
> It is not as formal as it looks. How do you conclude it is sufficient to
> consider just two diagrams? How do you conclude it is sufficient to
> consider just four outcomes?

If you look closely, my proof basically shows the same properties you
picked: actions that happened-before lock acquisition in one thread
cannot see the updates happening in after lock acquisition in another
thread. For the same reason your interpretation uses -- the total
ordering of locks/unlocks, plus transitivity -- we are free to only look
for two cases of relative sequencing of Reader and Writer, either R->W,
or W->R, and everything else is the extension of these two basic patterns.

But I would be very, very careful with interpretations that talk about
statements, and not the program actions with the actual values observed.
Because this is subtly broken: "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"

Statements do not form a program order. Program order is total, and
statements are not forming total order (easy example: control flow split
at conditionals). As stated, in this example:

Thread 1:
  if (false) // more complicated predicate in real-life case, of course
    y = 1
  sync(this) {
    w = 1
  }

Thread 2:
  sync(this) {
    r1 = w;
    r2 = y;
  }


...your interpretation says the "statement" y=1 happens-before r2=y,
which mandates seeing (r1, r2) = (1, 1), which is obviously incorrect.
This is an easy mistake that everyone makes when talking about JMM [1],
and it does not help that we keep perpetuating it with inaccurate claims
on public lists.

Thanks,
-Aleksey

[1]
https://shipilev.net/blog/2016/close-encounters-of-jmm-kind/#wishful-all-my-hb


_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest

signature.asc (836 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: What can an incorrectly synchronized read see?

Alex Otenko
Sure. I do mean “statements that got executed”.

The “enumerate all possible outcomes” approach can work for other cases - CAS succeeded or not; lock acquired or not; pointer set or not (even then you’d need a method to model ABA). But integer counters are more complex than that, and need a sound method of extending the enumeration of a few outcomes to all integers.


> On 29 Sep 2016, at 09:05, Aleksey Shipilev <[hidden email]> wrote:
>
> On 09/29/2016 09:13 AM, Alex Otenko wrote:
>> You need to be careful about using a “proof by example” as a proof. It
>> is ok to use it to demonstrate what happens to two reads of two writes,
>> but it is not a proof about *all* reads and *all* writes.
>>
>> It is not as formal as it looks. How do you conclude it is sufficient to
>> consider just two diagrams? How do you conclude it is sufficient to
>> consider just four outcomes?
>
> If you look closely, my proof basically shows the same properties you
> picked: actions that happened-before lock acquisition in one thread
> cannot see the updates happening in after lock acquisition in another
> thread. For the same reason your interpretation uses -- the total
> ordering of locks/unlocks, plus transitivity -- we are free to only look
> for two cases of relative sequencing of Reader and Writer, either R->W,
> or W->R, and everything else is the extension of these two basic patterns.

Sure, in the end it will have to rely on the same postulates to extend the conclusion to all integers - that’s all the postulates we can use, no magic there. I am just pointing out that the method does not tell us how we can jump from “this works for 0 and 1” to “this works for all integers”.

“pattern” is not part of JMM, so something else is needed.

Say, is (3,1) allowed? Now you need to look at R->W->W->W, W->R->W->W, W->W->R->W, W->W->W->R, provide a method of determining these are the only cases we need to consider (say, why W->W->W->R->W is irrelevant), and provide a method of reducing them to the previously considered cases before we can conclude that “everything else is the extension”.


I am not trying to say there is no way to do that (although I wouldn’t approach the problem that way), or that “enumerate all possible outcomes” is not practical - after all, that’s the only automated validation we have - I am merely pointing out that it is not a rigorous proof for the general question posed, and sweeps important details under the carpet.


Alex


> But I would be very, very careful with interpretations that talk about
> statements, and not the program actions with the actual values observed.
> Because this is subtly broken: "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"
>
> Statements do not form a program order. Program order is total, and
> statements are not forming total order (easy example: control flow split
> at conditionals). As stated, in this example:
>
> Thread 1:
>  if (false) // more complicated predicate in real-life case, of course
>    y = 1
>  sync(this) {
>    w = 1
>  }
>
> Thread 2:
>  sync(this) {
>    r1 = w;
>    r2 = y;
>  }
>
>
> ...your interpretation says the "statement" y=1 happens-before r2=y,
> which mandates seeing (r1, r2) = (1, 1), which is obviously incorrect.
> This is an easy mistake that everyone makes when talking about JMM [1],
> and it does not help that we keep perpetuating it with inaccurate claims
> on public lists.
>
> Thanks,
> -Aleksey
>
> [1]
> https://shipilev.net/blog/2016/close-encounters-of-jmm-kind/#wishful-all-my-hb
>

_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest
Loading...