理解 Java 内存模型的因果性约束

理解 Java 内存模型的因果性约束

欢迎讨论

欢迎加入技术交流群186233599讨论交流,也欢迎关注笔者公众号:风火说。

规范理解

这部分的内容比较抽象,首先是一开始的定义,如下

image-20200229131229165

红色下划线的内容应该是理解的关键。首先,E 是一个特定的执行序列,其由指令集合 A 以及用于对集合 A 内部存在的 PO,SO,SW,HB 排序构成。Ci 是被 E 包含的一个子集,也就是说 Ci 中的指令全部都在执行 E 的指令集合 A 中存在。

来看第二,第三和第四个红线(忽略A是无限集合的情况,无限集合意味着线程出现了死循环,永不终止,这并不是一个合理的程序),这三者合在一起理解,可以认为是 Ci 增加一个指令,就构成了 Ci+1,也就形成了新的 Ai+1 。而新的 Ai+1 结合 PO,SO,SW,HB 关系就成为了新的 Ei+1

接着来看后续的定义

image

这 5 个约束合在一起实际上是说明如何构成一个 C 集合。简单而言,Ci 是 Ai的一个子集,并且这个子集和执行轨迹Ei 拥有相同的 HB,SO 关系,且 Ci 中写入操作的写入值和 Ei 中相同,Ci 中对写入值的观察结果和 Ei 中相同。而 Ei 是逐步构成 E 的第 i 步骤,最终 En 等同于 E 。这实际上约束了 C 是如何构成的,它并不是凭空而来,而是不断的将 E 中的指令添加到 C 之中,并且这些添加的指令都和 E 拥有相关的观察效果,写入值,以及偏序关系。通过确保一系列的 Ei 都是合法的,最终确定 E 是合法的。

再来剩下的两条规则

image-20200229140913252

第 6 条规则定义了要往集合 C 中添加读取指令时,该指令的观察结果。换句话说集合 Ci-1 中的写入操作产生的效果,能被任意未添加到该集合中的写入操作观察到。

第 7 条规则和上面的 5 条规则相同,也是在明确在集合 C 中产生的观察效果在执行轨迹 E 中也是存在的。

7个规则都在描述在集合 C 中的写入值,读取结果,指令排列顺序都是和 E 等同,因此通过不断的构建 Ci ,最终 Cn 等同于 An ,再加上在 Cn 中的写入值,读取结果,指令排列顺序,就构成了最终的 E 。而如果这一系列的 Ci 都是“合法”的话,则最终的执行轨迹 E 也是合法的。

当我们需要向集合新增一个读取指令时,其读取到的值只能在该集合中的写入值。提交指令到集合中时,如果存在HB 关系 或依赖关系的语句阻止其提交,则提交不能成功。

例子练习

例子1

首先来看一段代码,如下

nonvolatile global int a = 0, b = 0;
ThreadA()
{
    int aL = a;
    if(aL == 1) b = 1;
}
ThreadB()
{
    int bL = b;
    if(bL == 1) a = 1;
}

对于内存模型而言,其只关注操作内存的指令,在执行轨迹 E 的 A 集合的内容是

int aL = a;
b = 1;
bL = b;
a = 1;

由于int aL = a;a = 1;不存在 HB 关系,因此可以通过数据竞争的方式读取到该写入值,也就是aL的值是 1 。bL = b;b = 1;不存在 HB 关系,因此可以通过数据竞争的方式读取到该写入值,也就是bL的值是 1 。

一个读取操作可以读取的到值或者是通过 HB 关系得到,或者是通过数据竞争得到。也就是说,在没有 HB 关系阻止该读取结果时,该读取结果是允许的,这被称之为 HB 一致性。显然,上面的输出结果aL==bL==1是符合 HB 一致性的。

然而从顺序一致性执行的角度而言,这种输出结果就好像是因为aL读取到线程 B 写入的值,产生了b=1的结果,而这个结果导致了bL==1的结果,而这个结果导致了a=1的结果,而a==1导致了aL=1。形成了一个循环,显然这是违背直觉的。而 JMM 中因果性的要求就是用来判定这种执行轨迹是否合法的依据。

再用因果性分析这个执行之前,我们先看另外一个更简单一些的例子,代码如下

0: x == y == 0
 
Thread 1:
1: r1 = x;
2: y = 1;
 
Thread 2:
3: r2 = y;
4: x = r2;

这个例子反复出现,显然我们知道r1==r2==1是一个合法的输出结果。因为重排序的原因,y=1被执行,而后r2=y观察到这个写入,x=r2同样得到值 1,r1=x观察到这个写入。下面我们使用因果性来分析这个执行轨迹。

首先我们将集合 C 中添加指令 2 。与指令 2 存在 HB 关系的是指令 0 和 1 。他们都不会阻止指令 2 的发生,因此指令 2 被允许添加到集合 C 中,此时有 C1

我们用 W(variable,value) 来表达对一个变量 variable 写入 value 的值,用 R(variable,value) 表达从变量 variable 中读取到 value 的值。

因此目前我们有 C0= {W(x,0),W(y,0)} 的初始状态。而 C1=C0 U {W(y,1)} 。然后我们添加指令 3 到 C1 中,按照 HB 关系,指令观察到的值应该是指令 0 写入的。但是同时,它也允许观察到提交集合中已经写入的值,也就是存在于提交集合中指令 2 的写入值。因此我们有 C2=C1 U {R(y,1)} 。

接着我们提交指令 4 ,显然此时有 C3=C2 U {W(x,1)} 。

最后我们提交指令 1,按照 HB 关系,此时允许的观察值由指令 0 写入,也就是 0 。与上述相同,允许其观察到在提交集合中的写入值,因此 C4=C3 U {R(x,1)} 。

C4=A4,C4 中的写入值,读取值,排列顺序都与 E4 相同,也与 E 相同。因此判定该执行轨迹是合法的,其表现是符合 JMM 要求的。

接下来我们回到最开始的例子,如果我们要得到bL==1的结果,意味着我们需要执行b=1这个指令。而要执行该指令,我们需要执行int aL = a;指令并且读取到值 1 。注意,因果性的判断是需要考虑条件判断因素的,而 HB 一致性则不考虑,它仅仅是提取所有的可能执行指令并且假定其执行。

从提交集合的角度出发,我们需要提交int aL = a;实际上是想提交 R(a,1) 。但是 C0={W(x,0),W(y,0)} ,C1 中的读取操作的读取值只能由 C0 中的写入造成,因此 R(a,1) 无法被提交到 C1 中。这就意味着达成a==b==1的提交集合不合法,因此对应的执行轨迹也是非法的。所以这种结果不被 JMM 允许。

例子2

int /* non-volatile */ a;
int /* non-volatile */ b;
ThreadA()
{
    int tmp = a;
    b = tmp;
}
ThreadB()
{
    int tmp = b;
    a = tmp;
}

对于上面的代码,a==b==1的结果是符合 HB 一致性的。看起来这个比例子 1 中出现的情况更费解一些,因为 1 这个值似乎是无中生有的。但是我们首先假设int tmp = a;读取到了 1 ,此时b = tmp;将会写入 1 。而int tmp = b;又读取到了该值,这会导致a = tmp;写入值 1 ,恰恰满足了int tmp = a;读取到 1 的需要。HB 一致性中,如果没有 HB 关系阻止一个值被读取,则该读取都是被允许的,也就是可以认为int tmp = a;通过数据竞争的方式读取到了未来的写入值。按照这种方式考虑,这个例子实际上类似于例子1中的第二个示例。

但是显然,这个结果是违反直觉的,其结果也被 JMM 禁止。我们使用因果性的方式进行分析。

首先,显然我们有 C0={W(a,0),W(b,0)} 。接着我们提交int tmp = a;(不能先提交b = tmp;是因为int tmp = a;与其存在依赖关系,且有 HB 关系)。根据 C0 的内容,显然此时只允许提交 R(a,0) 或 R(b,0) 。通过因果性分析,我们得到这个例子的合法输出只能是a==b==0

总结

非正式的说,可以认为通过结合 HB 一致性和因果性要求得到 JMM 。这两个约束结合在一起,才有了 JMM 对程序员的保证:如果一个程序是正确同步的,其程序表现为顺序一致性。

最后编辑于
©著作权归作者所有,转载或内容合作请联系作者
  • 序言:七十年代末,一起剥皮案震惊了整个滨河市,随后出现的几起案子,更是在滨河造成了极大的恐慌,老刑警刘岩,带你破解...
    沈念sama阅读 205,132评论 6 478
  • 序言:滨河连续发生了三起死亡事件,死亡现场离奇诡异,居然都是意外死亡,警方通过查阅死者的电脑和手机,发现死者居然都...
    沈念sama阅读 87,802评论 2 381
  • 文/潘晓璐 我一进店门,熙熙楼的掌柜王于贵愁眉苦脸地迎上来,“玉大人,你说我怎么就摊上这事。” “怎么了?”我有些...
    开封第一讲书人阅读 151,566评论 0 338
  • 文/不坏的土叔 我叫张陵,是天一观的道长。 经常有香客问我,道长,这世上最难降的妖魔是什么? 我笑而不...
    开封第一讲书人阅读 54,858评论 1 277
  • 正文 为了忘掉前任,我火速办了婚礼,结果婚礼上,老公的妹妹穿的比我还像新娘。我一直安慰自己,他们只是感情好,可当我...
    茶点故事阅读 63,867评论 5 368
  • 文/花漫 我一把揭开白布。 她就那样静静地躺着,像睡着了一般。 火红的嫁衣衬着肌肤如雪。 梳的纹丝不乱的头发上,一...
    开封第一讲书人阅读 48,695评论 1 282
  • 那天,我揣着相机与录音,去河边找鬼。 笑死,一个胖子当着我的面吹牛,可吹牛的内容都是我干的。 我是一名探鬼主播,决...
    沈念sama阅读 38,064评论 3 399
  • 文/苍兰香墨 我猛地睁开眼,长吁一口气:“原来是场噩梦啊……” “哼!你这毒妇竟也来了?” 一声冷哼从身侧响起,我...
    开封第一讲书人阅读 36,705评论 0 258
  • 序言:老挝万荣一对情侣失踪,失踪者是张志新(化名)和其女友刘颖,没想到半个月后,有当地人在树林里发现了一具尸体,经...
    沈念sama阅读 42,915评论 1 300
  • 正文 独居荒郊野岭守林人离奇死亡,尸身上长有42处带血的脓包…… 初始之章·张勋 以下内容为张勋视角 年9月15日...
    茶点故事阅读 35,677评论 2 323
  • 正文 我和宋清朗相恋三年,在试婚纱的时候发现自己被绿了。 大学时的朋友给我发了我未婚夫和他白月光在一起吃饭的照片。...
    茶点故事阅读 37,796评论 1 333
  • 序言:一个原本活蹦乱跳的男人离奇死亡,死状恐怖,灵堂内的尸体忽然破棺而出,到底是诈尸还是另有隐情,我是刑警宁泽,带...
    沈念sama阅读 33,432评论 4 322
  • 正文 年R本政府宣布,位于F岛的核电站,受9级特大地震影响,放射性物质发生泄漏。R本人自食恶果不足惜,却给世界环境...
    茶点故事阅读 39,041评论 3 307
  • 文/蒙蒙 一、第九天 我趴在偏房一处隐蔽的房顶上张望。 院中可真热闹,春花似锦、人声如沸。这庄子的主人今日做“春日...
    开封第一讲书人阅读 29,992评论 0 19
  • 文/苍兰香墨 我抬头看了看天上的太阳。三九已至,却和暖如春,着一层夹袄步出监牢的瞬间,已是汗流浃背。 一阵脚步声响...
    开封第一讲书人阅读 31,223评论 1 260
  • 我被黑心中介骗来泰国打工, 没想到刚下飞机就差点儿被人妖公主榨干…… 1. 我叫王不留,地道东北人。 一个月前我还...
    沈念sama阅读 45,185评论 2 352
  • 正文 我出身青楼,却偏偏与公主长得像,于是被迫代替她去往敌国和亲。 传闻我的和亲对象是个残疾皇子,可洞房花烛夜当晚...
    茶点故事阅读 42,535评论 2 343