深入浅析一致性模型之Linearizability

Posted 2021-12-09 qfjavabd

　　在Sequential Consistency之后，Linearizability出现了，它具有更强的一致性。

　　Linearizability的官方定义是来自于《Linearizability: A Correctness Condition for Concurrent Objects》，相比于Sequential Consistency定义的简洁，它的定义可是非常详细，我们一起简要的看一下吧。

　　history

　　一个并行系统的一个执行序列叫做一个history，由一系列的invocation和response事件组成。

　　invocation事件一般写作

　　

 

　　x是操作对象，op表示操作，args*是参数列表，A是进程。

　　Invocation的response写作

　　

 

　　term表示终止条件，res*是结果的列表。

　　如果一个response和invocation的进程和操作对象一致，认为这个response match这个invocation。

　　假设H是一个history，那么complete(H)是H只包含invocation和对应的match的response的最长子序列。

　　sequential history

　　sequential history的定义很简单：

　　第一个事件是invocation

　　如果一个invocation不是在最后，那么每个invocation后面都紧跟着match的response。每个response后面都紧跟着invocation。

　　原文中的定义是

　　Each invocation, except possibly the last, is immediately followed by a matching response. Each response is immediately followed by a matching invocation.

　　我感觉有问题，因为response可以match invocation，而invocation怎么match response则没有定义。

　　这里可以看出，sequential history中，操作没有互相覆盖，每个操作都认为是原子的，瞬时生效。

　　

 

　　legal sequential history

　　对象x在history H的子历史是H中所有对象为x的子序列。写作

　　H|x

　　对象x应该定义一个sequential specification，表示它的行为属性，比如先进先出就是队列的行为属性。

　　对一个sequential history H，如果每个对象的子历史都符合这个对象的sequential specification，就说明H是legal的。

　　equivalent history

　　进程P在history H中的子历史指的是H中所有进程为P的子序列。写作

　　H|P

　　对于历史H和H’来说，如果对每个进程P，都有H|P=H’|P，那么H和H’就是equivalent

　　linearizable history

　　对于一个history H，我们定义一个偏序关系h，如果操作a的response早于操作b的invocation，那么a p= b。注意这里的“早于”比较的是真实的物理时间(real-time)。=

　　注意这是一个偏序关系而不是全序关系，因此在H中，有可能存在操作X和Y，既不存在Xh p= h= x，例如下图中a和b就不存在这种关系。= y=

　　

 

　　给定一个history H，我们可以在H结尾追加任意个数的response使之变成H’

　　当H’满足以下条件时，认为H是linearizable：

　　complete(H’)和某个legal sequential history S是equivalent的

　　h p= s=

　　我的理解是，linearizable history和一个保留了原来真实时间顺序的legal sequential history等效了。

　　下面的执行历史可以认为是linearizable。

　　

 

　　因为可以找到某个符合条件的S。

　　

 

　　注意，W(1)h p= h= r(1)，这两个关系必须要保留，但w(1)和w(3)则不存在先后关系。=

　　Linearizability和Sequential Consistency

　　Linearizability比Sequential Consistency要严格很多，实际上Sequential Consistency仅仅要求本地顺序得到保留，而Linearizability要求保留真实时间顺序。

　　下面的系统可以认为Sequential Consistency，但不是Linearizability。

　　

 

　　Linearizability和Serializability

　　Linearizability经常和Serializability混淆，实际上Serializability一般指的是数据库的隔离级别，两者描述的不是同一个领域的东西。

?