![](https://csdnimg.cn/release/download_crawler_static/88617412/bg4.jpg)
R. Kavanagh
,
S.Brookes/Electronic Notes in Theoretical Computer Science 336
(
2018
)
223
(a)
在(
x=v
)
r
↓
T
中对
x
的所有写入中,
存在在
T
下最大的写入(
x
:
=v
J
)
w
,在
(
x=v
)
r
↓
P
中对
x
的所有写入都在(
x
:
=v
J
)
w
↓
T
中,并且
v=v
J
;
或者
(b)
在(
x=v
)
r
↓
P
中所有对
x
的
写入中,存在
P
下最大的写入(
x
:
=v
J
)
w
,并
且(
x
=
v
)
rT
(
x
:
=
v
J
)
w
和
v
=
v
J
两者
;
或者
(c)
在(
x
=
v
)
r
↓
T
或(
x
=
v
)
r
↓
P
中没有对
x
的
写入,并且
σ
(
x
)
=
v
。
(L)
LoadOp
:
对于所有读
r
∈
P
和所有动作
a
∈
P
,
r<
P
a
蕴涵
r<
T
a
。
(S)
StoreStore
:
对于所有写
w
,
w
J
∈
P
,
w<
P
w
J
蕴涵
w<
T
w
J
。
(F)分叉:如果α
1P
α
2
,α
1P
α
3
,且α
2
#
P
α
3
,则α
1T
α
2
和α
1T
α
3
。
(J)连接:如果
α
1
P
α
3
,
α
2
P
α
3
,且
α
1
#
P
α
2
,则
α
1
T
α
3
和
α
2
T
α
3
。
我们简单地说
T
与
P
是
TSO-
相容的,如果存在某个初始状态
σ
,从
该初始状态
σ
它们是
TSO-
相容
的。
公理(O)、(VA)、(VB)、(L)和(S)直接改编自[12]附录K.2中给出的
形式规范。我们引入公理(VC),以简化我们的演示文稿的例子。通过要求程序首
先写入它们读取的任何位置,它可以被省略,除了例子之外,我们将始终假设我们
的
TSO
一致的顺序不需要(V
C
)。虽然形式规范没有提供公理(F)和(J),但它
们与
[12]
的附录
J.6
所预期的行为一致。直觉上,公理(V
B
)要求每当处理器从一个
位置读取时,它必须使用其写缓冲器(如果存在)中对该位置的最近写入,并且如
果在其写缓冲器中没有这样的写入,但是我们已经观察到对该位置的全局写入,则
(VA)要求最近的这样的写入是一次读取。我们的介绍与正式的规格略有特别是,
我们不考虑指令提取或原子加载-存储操作,也不考虑缓存操作,因为它们可以通过
分叉和立即连接实现为我们语义中的派生操作为了与我们的
pomset
开发保持一致,
我们也假设顺序是严格的。
如果
T
对于P是TSO-相容的,则在P上存在一个(不一定是唯一的)全序,它与P
是
TSO-
相容的并且包含
T
。 这是一致 根据我们的物理直觉:给定一个实际执行,
我们可以想象对操作进行时间线性化。因此,我们可以把所有与
P TSO
一致的序
看
作是
与
P TSO
一致的总序的弱化。应该注意不要将线性化和
TSO
一致的总订单联系
起来。例如,考虑程序顺序
线性化
x
:
= 2<x
:
= 3<x = 3<x = 2
与程序顺序不是
TSO
一致的,因为它违反了
(V
A
)
;
顺序
x
= 2
<x
:
= 2
<x
= 3
<x
:
= 3
不是程序顺序的线性化,但与它是
TSO
一致的。
当我们在程序顺序中先写后读,但在线性顺序中交换时,就像在这个例子中一
样,我们可以想象写被卡在写缓冲器中,并在写之前观察读