把并发历史对应到合法顺序

多个活动访问同一对象时,操作的执行区间可以重叠。线性化要求这些可观察结果能够对应到一个符合对象顺序规范的历史,就像每个操作在自己的调用与响应之间某个位置一次生效。

约束还包括真实先后:若甲操作已经返回,乙才开始,线性解释不能任意把乙放到甲之前。只有相互重叠的操作,才可能在不违反其他对象语义的前提下采用不同先后解释。

参考:[1]

结果必须符合对象本身的语义

对先入先出队列,如果x已经入队完成,随后y才开始入队,那么在没有其他取出操作时,不能先返回y而跳过x。若两个入队区间重叠,则队列历史可能允许不同的顺序,最终解释还要与所有取出结果一致。

因此线性化不只是给日志排一个时间顺序。它同时需要对象的合法行为约定;队列、栈和集合的操作意义不同,同一组返回结果在一种对象上可能成立,在另一种对象上却不成立。

参考:[1]

组合性质与实现进展要区分

Herlihy与Wing证明线性化具有局部组合性质,可以分别验证各个对象再组合推理。但一个业务操作若由多次独立调用构成,仍可能与他人交错;单个读和写都线性化,不会自动把两者合成一次原子更新。

该条件也不强制采用无锁实现。原论文明确区分行为性质与具体实现带来的阻塞甚至死锁;满足线性化不保证某条请求会在固定时间内结束。正确结果、无锁进展和延迟上限,需要不同的论证。

参考:[1]