![](https://csdnimg.cn/release/download_crawler_static/88754080/bg4.jpg)
S. Tasiran
,
S.Qadeer/Electronic Notes in Theoretical Computer Science 113
(
2005
)
163
如果其对应的迹是格式良好的。在本文中,我们将我们的分析限制在状
态转移系统的良构运行上。与线程
t
相关联并且位于公共方法的调用和
返回操作之间的操作序列称为该方法的
执行
如果在应用程序线程
t
对公共方法
名称
的每个调用操作(
t
,
Call
,
name
,
args
)之后,除了
thread
之外没有其他线程,则格式良好的
run
是
原子的
t
执行一个操作,直到相应的返回操作(
t
,
Return
,
name
,
rets
)发生。
因此,每个原子运行都是运行
片段
的串联,使得只有一个应用程序线程
在任何特定片段中执行操作。每个片段以应用程序线程
t
的调用动作开
始,以线程
t
的相应返回动作结束。一个状态转换系统是
原子的,
如果它
的所有运行都是原子的。
片段开头的调用动作和片段结尾的返回动作构成了片段的
签名
。一
个原子状态转移系统是
确定性的
,如果任何两个运行的两个片段具有相
同的第一个状态和相同的签名,它们也具有相同的最后一个状态。因
此,一个原子的和确定性的状态转移系统的每一个轨迹都是由一个唯一
的运行产生的。
2.2
状态转移系统之间的精化
设并发数据结构的实现由状态
转换
系统
I
=
(
VI
,
SI
,
SI
0
,
δ
I
)
给出,
其具体化由状态转换
系统
S
=
(
VS
,
SS
,
SS
0
,
δ
S
)给出. 对于
迹线
τ
和
线
t
,
令
τ
|
t
表示
τ
在与线程
t
相关联的动作上
的投影
。的
转移系统
I
精化
S
,如果对于
I
的每条迹τ
,
都有
S
的迹τ
J
使得τ
|
t
= τ
J
|对于所有的t
∈
Tid
应用程序
。
请注意,细化的定义取决于状态转换系统中被选择为可见的动作
集。在我们所谓的
I/O
细化概念中,调用和返回操作是唯一可见的操
作。直观地说,这种细化的定义表达了这样的要求,即方法调用的返回
值必须与规范的某些(原子)执行中的返回值一致。当然,我们可以使
实现的更多操作可见,并要求它们与规范中的相应操作相匹配。一个更
大的可见操作集将导致比
I/O
细化所允许的更广泛的运行时检查。第
5
节
描述了我们发现在实践中有用的可见动作的一种选择。