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