Re: [Reply] coherence litmus test and data race.

Hi Shuyang,

Thanks for your excellent reply. I'll study the links you send.

I read the article of Russ Cox as well and it is the reason I'm asking this
question.

Regards,

Peter


On Tue, Jul 13, 2021, 19:36 Shuyang Liu <[email protected]> wrote:

> Hello,
>
> According to the current definitions in JAM [1] for Java 9, the execution
> in the litmus test is forbidden. In particular, there is a CORR rule saying
> that if there are two consecutive reads to the same location reading from
> two writes, then there is a coherence order between the two writes in the
> same order. So the two writes have to be executed in the same order as
> observed and all threads in the program have to agree on the same coherence
> order.
>
> In addition, the same execution is forbidden by RC11 [2], too (with
> non-atomics). In particular, there is a reflexive hb;eco order from (r3=a)
> -hb-> (r4=a) -eco-> (r3=a), which is forbidden by the coherence rule in
> RC11. RC11 assumes a single total coherence order on writes to the same
> location, like hardware memory models.
>
> Interestingly, this blog post [3] by Russ Cox says otherwise because the
> compiler can reorder the reads. If this is true in the compilers, then the
> formal model is too strong for the language.
>
> I'm not sure if this is the correct format to reply to a post in the
> mailing list. Apologize if not.
>
> Best Regards,
> Shuyang Liu
>
> [1] John Bender and Jens Palsberg. 2019. A formalization of Java’s
> concurrent access modes. Proc. ACM Program. Lang. 3, OOPSLA, Article 142
> (October 2019), 28 pages. DOI:https://doi.org/10.1145/3360568
>
> [2] Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, and Derek
> Dreyer. 2017. Repairing Sequential Consistency in C/C++11. In Proceedings
> of the 38th ACM SIGPLAN Conference on Programming Language Design and
> Implementation (PLDI 2017). ACM, New York, NY, USA, 618–632
>
> [3] Programming Language Memory Models  https://research.swtch.com/plmm
>

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