按月存档: 2012/10

[翻译]Happens before偏序

分类:java, 并发, 翻译评论:0条作者:ticmy日期:2012-10-11

原文: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 (即…