线性一致性

线性一致性（Linearizability），或称原子一致性或严格一致性指的是程序在执行的历史中在存在可线性化点P的执行模型，这意味着一个操作将在程序的调用和返回之间的某个点P起作用。这里“起作用”的意思是被系统中并发运行的所有其他线程所感知。

历史

线性一致性是Maurice P. Herlihy 与 Jeannette M. Wing共同提出的关于并行对象行为正确性的一个条件模型。在此之前，Lamport已经提出了顺序一致性的概念。

严格的定义

I/O自动机

Herlihy 的论文中采用了 Nancy A. Lynch 和 Mark R. Tuttle 所发明的 I/O自动机（I/O automata） 模型来定义线性一致性的概念。在 I/O automata 中程序的执行用 历史(History/schedule)来描述。所谓历史就是指一个有限的方法调用和响应事件构成的集合。严格地：我们先定义执行片段(Execution fragment)为序列：${\displaystyle {s_{0},e_{1},s_{1},....e_{n},s_{n}}}$，其中${\displaystyle s_{i}}$为此I/O自动机的状态集，定义执行序列(Execution sequence)为${\displaystyle s_{0}}$是初始状态的执行片段。那么历史就是执行序列中的事件子序列。在我们即将研究的并发系统中，历史中的输出事件(Output event)和输入事件(Input event)分别对应线程P对对象X的调用(Invoke)和响应(Response)。下面将响应事件记做${\displaystyle R(P,res,X)}$，将调用事件记做${\displaystyle I(P,op,X)}$其中P为线程名称，op为操作名称，X为对象名称，res为返回值。

基本概念

• 定义响应事件${\displaystyle R(P,res,X)}$与调用事件${\displaystyle I(P',op,X')}$相匹配(match)，如果P=P',X=X'。
• 顺序历史(Sequential history)：历史H是顺序的，如果满足以下两个条件：
  • H中的第一个成员为调用事件；
  • 除了H中的最后一个调用事件之外，H 由相邻的、两两相匹配的调用事件和响应事件组成。
• 并发历史(Concurrent history)：不是顺序历史的历史称为并发历史。
• 在线程P上的子历史(Process subhistory)${\displaystyle H|P}$定义为H在线程P上的射影，即H中所有线程名为P的事件构成的子集。
• 如果对于H中任意的P，H|P 是顺序历史，则称H是良形式的(well-formed)。
• 等价的两个历史H与H'：${\displaystyle H\iff H'}$ 定义为 ${\displaystyle \forall P,H|P=H'|P}$。
• 操作(Operation) e 定义为相匹配的一对调用事件和响应事件。
• 完备化函数Complete(H)：Complete(H)的结果是包含在H中的、最大的、仅含有互相匹配的调用事件和响应事件的时间序列。
• 历史集S是前缀闭(prefix-closed)的，如果${\displaystyle \forall H\in S,\forall e,H^{e}\in S}$，其中${\displaystyle H^{e}}$代表H中以操作e结尾的一个前缀。
• 对象X顺序性说明(Sequential specification)定义为对象X的前缀闭的顺序历史集。顺序性说明描述了一个对象所有可能的顺序行为。
• 合法的(Legal)顺序历史指的是${\displaystyle \forall x,H|x}$（指H中对象为x的那些事件）属于x的顺序性说明。

线性一致性的形式化定义

• 对于给定的一个历史H，其中必然蕴含着一个非自反的偏序关系${\displaystyle <_{H}}$（可称之为“之前” - precede），其定义如下：${\displaystyle e_{0}<_{H}e_{1}}$， 若 ${\displaystyle res(e_{0})}$在${\displaystyle inv(e_{1})}$之前。

• 如果满足以下条件，则定义历史 H是线性一致的(或可线性化的-linearizable)：

1. 首先我们将H 扩展为 ${\displaystyle \mathbf {H'} }$；
2. ${\displaystyle Complete(\mathbf {H'} )}$等价于一个合法的顺序历史S；
3. ${\displaystyle <_{H}\subseteq <_{S}}$

例子

线性一致性的性质

• 线性一致性最重要的性质就是其“局部性”（Local property, 或可组合性 - Compositional），即数个线性一致单对象历史的组合也是线性一致的。
• 线性一致性的非阻塞性(Non-blocking property)：线程P对完全操作(total function)的调用永远不会阻塞。

严格一致性

相关的话题

• 任务并行
• 内存一致性模型
• 顺序一致性

参考资料

1. Linearizability: A Correctness Condition for Concurrent Objects, MAURICE P. HERLIHY and JEANNETTE M. WING Carnegie Mellon University