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

Alex Otenko oleksandr.otenko at gmail.com
Thu Sep 29 03:13:03 EDT 2016


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 <yaojingguo at gmail.com> wrote:
> 
> Aleksey:
> 
> Your reasoning is much more formal. Thanks.
> 
> 2016-09-28 18:55 GMT+08:00 Aleksey Shipilev <shade at redhat.com <mailto:shade at redhat.com>>:
> 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
> Concurrency-interest at cs.oswego.edu <mailto:Concurrency-interest at cs.oswego.edu>
> http://cs.oswego.edu/mailman/listinfo/concurrency-interest <http://cs.oswego.edu/mailman/listinfo/concurrency-interest>
> 
> 
> 
> 
> -- 
> Jingguo
> 
> _______________________________________________
> Concurrency-interest mailing list
> Concurrency-interest at cs.oswego.edu
> http://cs.oswego.edu/mailman/listinfo/concurrency-interest

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


More information about the Concurrency-interest mailing list