可线性化验证

2016-07-03

如何证明一个系统是可线性的？这个很难。有个相对简单的做法叫model check，意思是定义一个模型，假设系统是可线性化的，那么它的行为一定满足这个模型（但满足这个模型不一定是可线性化的，是必要非充分条件）。

看一个简单的例子。假设有一个变量A，两个client访问，将访问历史表示成这样子：

[{Process: 2, Type: Invoke, F: Write, Value: 9}
{Process: 1, Type: OK, F: Write, Value: 4}
{Process: 1, Type: Invoke, F: Read, Value: 9}
{Process: 1, Type: OK, F: Read, Value: 4}]

Process是执行操作的client，Type类型可以是Invoke和OK，分别表示发起请求和请求完成。F表示调用的操作，Value是操作的参数。

接下来是模型的定义。Model中保存了自己的状态，在Step函数中，当它接受一个操作后，将转化为另一个状态，返回布尔值表示这一步是否可线性化：

type Model interface {
    Step(op OP) bool
}

我们来实现一个Register模型。它有一个当前值，如果操作是读，仅当操作读到的值等于Register模型中保存的当前值时，它是合法的；如果操作是写，则用写入的值覆盖当前值。这很好理解，我们类比一下多个线程修改一个寄存器，假设线程间交错的执行次序产生的结果，等价于它们接某个依次串行执行的次序，那这个模型肯定不会发生上一步写了一个3，下一步读出一个4这种事情。

type Register int
func (r *Register) Step(op OP) bool {
    if op.Type == OK && op.F = Read && op.Value != *r {
        return false
    }
    if op.Type == Invoke && op.F = Write {
        *r = op.Value
    }
    return true
}

然后就可以用我们定义的模型来跑一遍历史，检查这个历史是否满足模型。如果不满足，那系统一定不是可线性化的。

剩下的问题就转化成了验证一串访问历史是否满足可线性化。

但是我们忽略了一个问题，(Invoke，OK)是一个pair，假设history中有两个Invoke操作：

[a b]

实际可能发生的情况是

[]
[a]
[b]
[a b]
[b a]

也就是说：可能a和b都没执行[]；只有a执行了[a]；只有b执行了[b]；a和b都执行了，顺序是先a后b[a b]；a和b都执行了，先b后a[b a]。

只要检查到某一个序列去跑我们的model能够通过，我们就算这个历史通过了：用最简单的暴力搜索，可以把所有的排列都计算出来，一个个再验证。但是当处于Invoke中的操作数稍大以后，整个可能的状态数就爆炸了。算一下20的阶乘，就发现这个数字大得不敢想象。

怎么办？有个online的算法，不是一口气把所有组合都算出来了再进行验证，而是一边计算可能的状态，一边做剪枝。[a b c]的全排列：

[]
[a] [b] [c]
[a b] [b a] [a c] [c a] [b c] [c b]
[a b c] [a c b] [b a c] [b c a] [c a b] [c b a]

基于这样一个观察，如果[b a]已经是不可能的，那么我们根本不用测试[b a c]，所有以[b a]开头的都可以剪枝！

遇到Invoke，在当前状态上生成新的可能状态。遇到OK，则进行剪枝。检测所有当前状态，去掉不满足的。这样就要以让算法more reasonable了。剩下是一些工程上的东西，只要计算一个满足条件的解，可以用深度优先。需要搜索的解空间很大，可以挖掘一下多线程。

很久之前研究了一下的东西，当时因为优先级不在这个事情上。后面热情退一点没把代码写完，就不show链接了。想想还是值得说一下原理，便写了这篇博客。