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

Background: Shuyang and colleagues are working on a formal model ("JAM") 
that accounts for jdk9+ VarHandle modes 
(http://gee.cs.oswego.edu/dl/html/j9mm.html), C++ interoperability 
(modulo intrinsic differences), updated processor mappings, and JSR133 
JMM bugfixes, that could become a basis for revised JLS spec.

On 7/13/21 12:36 PM, Shuyang Liu via Concurrency-interest 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
_______________________________________________
Concurrency-interest mailing list
[email protected]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest