Happens before

简介:

原文:http://www.cs.umd.edu/class/fall2010/cmsc433/lectures/happens-before.txt

译者:丁一

“Happens before”是由Leslie Lamport引入的用来描述程序事件的一种偏序关系。

将多线程的执行看作是事件E的轨迹R,定义如下(轨迹只是一种次序):


Events E ::= start(T)
	  |  end(T)
	  |  read(T,x,v)
  	|  write(T,x,v)
	  |  spawn(T1,T2)
	  |  join(T1,T2)
	  |  lock(T,x)
	  |  unlock(T,x)


这里T是一个线程标识符,x是一个变量,v是一个值。read(T,x,v)事件表示线程T从变量x中读出值v。同时假定轨迹R是结构良好的,即要求在R中,线程T的第一个事件必须是start(T)。在end(T)之后不再有线程T相关的事件。

设E1 < E2为E1和E2在轨迹中出现的顺序,它是可传递的、反自反的和反对称的。定义轨迹R中的happens-before次序(<:)如下:
E1 <: E2,当且仅当E1 < E2,且下列条件之一成立:


  a) thread(E1) = thread(E2)
  b) E1为spawn(T1,T2), E2为start(T2)
  c) E2为join(T1,T2),E1为end(T2)
  d) E1为unlock(T1,x),E2为lock(T2,x)
  e) 存在这样的E3:E1 <: E3 且 E3 <: E2 (即,happens-before次序是可传递的)


可见性
假设轨迹R中有EW == write(T1,x,v1) 和 ER == read(T2,x,v2),如果:
a) ER <: EW (即,读事件与写事件间有happens-before次序)
b) 存在一个介入的事件EW2 == write(T,x,v3),有EW <: EW2 <: R (即,第一次写的值被第二次覆盖了)

则,EW对ER不可见(即v1 != v2)。否则,EW对ER可见,ER中的读操作就能看的见EW中写入的值。例如:


 (起始 x = 0)
Thread 1:      Thread 2:
x = 1;         y = x;
y = 2;


这是一些可能的轨迹:


R1 == write(T1,x,1); read(T2,x,0); write(T2,y,0); write(T1,y,2)
R2 == write(T1,x,1); read(T2,x,1); write(T2,y,1); write(T1,y,2)
R3 == read(T2,x,0); write(T1,x,1); write(T2,y,0); write(T1,y,2)
R4 == write(T1,x,1); read(T2,x,1); write(T1,y,2); write(T2,y,1)
R5 == read(T2,x,0); write(T1,x,1); write(T1,y,2); write(T2,y,0)


注意在轨迹R1中,T2读取x获得的值是0;这是合理的,因为轨迹中x=1和x=2在那个时刻都是可见的;这是由于T1写值到x中没有”happen before”读操作。轨迹R2读得1。在轨迹R3中,T2线程的读操作先发生,所以它能读到的唯一可能的值就是x的初始值:0. 轨迹R4和R5分别类同于R2和R3,只是最后两个事件的顺序颠倒了。这些轨迹展示了y的最终结果,如果运行该程序,可能为0,1或2.

再来一个例子:


 (起始 x = 0)
Thread 1:      Thread 2:
lock(y);       lock(y);
x = 1;         x = x + 1;
unlock(y);     unlock(y);


下面是两个可能的轨迹:


R1 == lock(T1,y); write(T1,x,1); unlock(T1,y);
      lock(T2,y); read(T2,x,1); write(T2,x,2); unlock(T2,y)

R2 == lock(T2,y); read(T2,x,0); write(T2,x,1); unlock(T2,y)
      lock(T1,y); write(T1,x,1); unlock(T1,y);


在第一个轨迹中,线程T2从x中读得1。这是因为write(T1,x,1)先于read(T2,x,1)发生—这两个事件因为unlock(T1,y) <:lock(T2,y)以及传递性的存在而成为有序的。这个时刻T2不可能读到0。另一个轨迹中T2首先获得锁。

数据争用
有了happens-before次序,就可以准确地定义数据争用:轨迹R中的两个事件,其中至少有一个写事件,访问同一块内存区域,根据happens-before规则它们是无序的,就会发生数据争用。接下来有几个例子,第一个例子跟上面的一样:


 (起始 x = 0)
Thread 1:      Thread 2:
x = 1;         y = x;
y = 2;


对于这两个线程任何可能的执行,线程对x、y的写操作 与 线程2读取x、写入y之间没有次序关系。这样就形成了数据争用。这里有一个可能的轨迹,E11 == write(T1,x,1), E21 == read(T2,x,0), E22 == write(T2,y,0)以及 E12 = write(T1,y,2):
轨迹R == E11; E21; E22; E12

在这个轨迹中,E11和E21形成了数据争用:它们没有被happens-before排序,然后访问了同一个变量,其中E11事件是一个写操作。其它的数据争用包括E11和E22之间,E12和E21之间以及E12和E22之间。

再来一个例子:


Thread 1:      Thread 2:
lock y;        print(x);
x = 1;
unlock y;


这里线程2的读事件(为了print)与线程1的写事件之间仍然存在数据争用。下面是一个可能的轨迹:
lock(T1,y); write(T1,x,1); unlock(T1,y); read(T2,x,0)

在这个轨迹中,write(T1,x,1)事件与read(T2,x,1)事件之间存在数据争用,因为这两个事件没有被happens-before排序。这是由于,尽管在这个轨迹中实际上是有顺序的( < 顺序),但是它们位于不同的线程中且它们之间没有同步事件。这个程序所有可能的轨迹都有这种争用。注意上面的轨迹中,读和写事件没有在同一时刻发生–在轨迹中它们只是无序的。

下面这个程序有时会表现出争用:


Thread 1:      Thread 2:
x = 1;         lock y;
lock y;        unlock y; 
unlock y;      print(x);


这个例子中,下面的轨迹不存在数据争用:
write(T1,x,1); lock(T1,y); unlock(T1,y); lock(T2,y); unlock(T2,y); read(T2,x,1)

在这种情况下,读和写事件被happens before排序了,因为根据前面的规则unlock(T1,y) <: lock(T2,y),所有其它的事件被轨迹顺序 < 排序,加上传递性,就有了write(T1,x,1) <: read(T2,x,1),所以没有争用。

下面这个轨迹确实展示了一种争用:
lock(T2,y); unlock(T2,y); write(T1,x,1); read(T2,x,0); lock(T1,y); unlock(T1,y)

这里,写事件和读事件没有被happens-before排序,因此形成了争用。 

目录
相关文章
|
7月前
|
IDE Java Shell
Java的开发环境的搭建
Java的开发环境的搭建
|
存储 安全 数据安全/隐私保护
13 Tornado - Cookie
13 Tornado - Cookie
55 2
|
缓存 分布式计算 Java
Hbase性能优化
版权声明:本文为博主原创文章,未经博主允许不得转载。 https://blog.csdn.net/tomnic_ylwang/article/details/81105619 一、性能优化 1.
1721 0
|
2天前
|
弹性计算 人工智能 安全
对话 | ECS如何构筑企业上云的第一道安全防线
随着中小企业加速上云,数据泄露、网络攻击等安全威胁日益严重。阿里云推出深度访谈栏目,汇聚产品技术专家,探讨云上安全问题及应对策略。首期节目聚焦ECS安全性,提出三道防线:数据安全、网络安全和身份认证与权限管理,确保用户在云端的数据主权和业务稳定。此外,阿里云还推出了“ECS 99套餐”,以高性价比提供全面的安全保障,帮助中小企业安全上云。
对话 | ECS如何构筑企业上云的第一道安全防线
|
10天前
|
调度 云计算 芯片
云超算技术跃进,阿里云牵头制定我国首个云超算国家标准
近日,由阿里云联合中国电子技术标准化研究院主导制定的首个云超算国家标准已完成报批,不久后将正式批准发布。标准规定了云超算服务涉及的云计算基础资源、资源管理、运行和调度等方面的技术要求,为云超算服务产品的设计、实现、应用和选型提供指导,为云超算在HPC应用和用户的大范围采用奠定了基础。
179612 21
|
19天前
|
人工智能 自然语言处理 前端开发
从0开始打造一款APP:前端+搭建本机服务,定制暖冬卫衣先到先得
通义灵码携手科技博主@玺哥超carry 打造全网第一个完整的、面向普通人的自然语言编程教程。完全使用 AI,再配合简单易懂的方法,只要你会打字,就能真正做出一个完整的应用。
9561 27
|
5天前
|
机器学习/深度学习 分布式计算 供应链
阿里云先知安全沙龙(上海站) ——大模型基础设施安全攻防
大模型基础设施的安全攻防体系涵盖恶意输入防御和基础设施安全,包括框架、三方库、插件、平台、模型和系统安全。关键漏洞如CVE-2023-6019(Ray框架命令注入)、CVE-2024-5480(PyTorch分布式RPC)及llama.cpp中的多个漏洞,强调了代码安全性的重要性。模型文件安全方面,需防范pickle反序列化等风险,建议使用Safetensors格式。相关实践包括构建供应链漏洞库、智能化漏洞分析和深度检测,确保全方位防护。
|
7天前
|
JSON 分布式计算 数据处理
加速数据处理与AI开发的利器:阿里云MaxFrame实验评测
随着数据量的爆炸式增长,传统数据分析方法逐渐显现出局限性。Python作为数据科学领域的主流语言,因其简洁易用和丰富的库支持备受青睐。阿里云推出的MaxFrame是一个专为Python开发者设计的分布式计算框架,旨在充分利用MaxCompute的强大能力,提供高效、灵活且易于使用的工具,应对大规模数据处理需求。MaxFrame不仅继承了Pandas等流行数据处理库的友好接口,还通过集成先进的分布式计算技术,显著提升了数据处理的速度和效率。
|
23天前
|
Cloud Native Apache 流计算
资料合集|Flink Forward Asia 2024 上海站
Apache Flink 年度技术盛会聚焦“回顾过去,展望未来”,涵盖流式湖仓、流批一体、Data+AI 等八大核心议题,近百家厂商参与,深入探讨前沿技术发展。小松鼠为大家整理了 FFA 2024 演讲 PPT ,可在线阅读和下载。
5169 15
资料合集|Flink Forward Asia 2024 上海站
|
3天前
|
机器学习/深度学习 人工智能 安全
通义视觉推理大模型QVQ-72B-preview重磅上线
Qwen团队推出了新成员QVQ-72B-preview,这是一个专注于提升视觉推理能力的实验性研究模型。提升了视觉表示的效率和准确性。它在多模态评测集如MMMU、MathVista和MathVision上表现出色,尤其在数学推理任务中取得了显著进步。尽管如此,该模型仍存在一些局限性,仍在学习和完善中。