本站消息

站长简介/公众号

  出租广告位,需要合作请联系站长


+关注
已关注

分类  

暂无分类

标签  

暂无标签

日期归档  

暂无数据

特殊 POPL 问题的数据竞争示例 Java 内存模型混淆

发布于2024-11-02 21:05     阅读(528)     评论(0)     点赞(9)     收藏(2)


我对 SPECIAL POPL ISSUE《Java 内存模型》论文中的图 3 感到困惑。

示例(第 5 页,图 3):

Initially, x == y == 0    

Thread 1 -> r1 = x; y = r1;

Thread 2 -> r2 = y; r3 = r2 | 1; x = r2;

r1 == r2 == r3 == 1 is legal behavior.

解释 1(第 5 页,1.2 因果循环):图 3 中可以看到另一个因果循环示例(这次是描述可接受行为的示例)。为了查看结果r1 == r2 == r3 == 1,其中一个线程必须在执行读取之前执行写入。但每个写入似乎都依赖于其上方的读取。虽然这个值似乎也是凭空而来的,但它并非如此,并且可以由标准编译器转换产生,如第 2.2.2 节所述。

解释 2(第 10 页,2.2.2 依赖性突破分析和转换):图 3 显示了类似但更令人惊讶的行为。在这种情况下,编译器必须执行更深入的分析,以确定 x 和 y 的值是否保证为 0 或 1。一种可能的分析是确定在程序中表示整数值所需的位宽的分析 [Stephenson 等人,2000 年]。

在这个例子中,r1 和 r2 只能是== 1if x or y == 1只能x or y could be == 1if r1 and r2 == 1。但是的赋值1我只能在中找到,所以r3 = r2 | 1;在我看来,没有办法1得到r1r2xy

那么,这个例子是错误的还是我错了?


解决方案


你说得对。示例错误。应该是:

Initially, x == y == 0
Thread 1 -> r1 = x; y = r1;
Thread 2 -> r2 = y; r3 = r2 | 1; x = r3;

您可以在Jeremy Manson 的博士论文图 1.3 中看到正确示例



所属网站分类: 技术文章 > 问答

作者:黑洞官方问答小能手

链接:http://www.javaheidong.com/blog/article/691853/7abe6388a84e2848425d/

来源:java黑洞网

任何形式的转载都请注明出处,如有侵权 一经发现 必将追究其法律责任

9 0
收藏该文
已收藏

评论内容:(最多支持255个字符)