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排序,因此形成了争用。 

时间: 2024-10-29 21:23:25