可线性化验证

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链接了。想想还是值得说一下原理,便写了这篇博客。

SQL