基于学习的缓存一致性协议带参验证

关注文章

一、背景

带参系统存在于许多应用领域中,比如缓存一致协议等。因为它的研究价值,验证这样的系统的也就吸引来了形式化验证、模型检测和定理证明等社区的关注。要想验证带参系统的正确性,就必须验证任意实例大小的系统中的正确性,而这被证明是一个无法判定的问题。

尽管这样的难度,但是很多方法仍然被提出来试图解决这个问题。CMP方法是其中最成功的方法之一。它用模型检测的方法来验证Intel、flash等大型的协议。通过保留m个节点, 并用一个抽象的节点NOther来替代其他所有剩余节点的行为。通过这样的抽象,一个原始的协议就被抽象成了一个由m+1个节点组成的抽象写意。然后通过分析模型检测器提供的反例,循环构造一系列引理来限制抽象节点NOther的行为,使得协议可以收敛,且不会违反原有性质。如果最终原始性质和引理都能在抽象协议中被检验通过,那么就能推导出原始协议在任意大小的实例下也都能成立。但是,CMP方法是在模型检测机给出反例之后,采取的是被动补救措施。这样的被动方法由于依赖于人工理解和指导,而无法自动化。而且“寻找反例-卫式加强”这样的循环,所需要的次数未知,这也就使得可达集是否能收敛、抽象协议能否满足安全性质成为未知。

CMP存在的缺点启发我们去更深入地思考:是否能够通过主动地探索满足上述条件的可达集边缘,以使可达集收敛,并满足安全性质?如果能够主动的限定可达集能到达的范围,则可以更主动地搜索辅助不变式,从而更精确地加强抽象系统。 因此,在这篇论文中,我们提出了L-CMP,一种自动的学习框架,通过较小实例可达集学习/挖掘辅助不变式,并且自动的用这些辅助不变式对抽象协议进行限制,最终,抽象协议的可达集可以被收敛在合理范围,安全性质也就能够保证。

二、关联规则学习

在本文中,我们巧妙地将关联规则学习(Association rule learning)与卫式加强做结合,成功达到了寻找辅助不变式及自动卫式加强的目的。 关联规则学习是Agrawal等人提出的基于规则的机器学习方法。它的目的是利用一些有趣性的量度来识别数据库中发现的强规则。基于强规则的概念,Rakesh Agrawal等人引入了关联规则以发现由超市的POS系统记录的大批交易数据中产品之间的规律性。许多有效的关联规则算法,如Apriori,Eclat和FP-growth。在本文中,我们使用Apriori作为关联规则的学习算法进行学习。 给定由一组事务组成的数据集D,记为D = {t1,t2,…,tm}。 设I = {i1,i2,…,in}是一组包含许多项目的项集。 每个交易t包含一个项目子集。 一个关联规则的形式是X→Y,其中X,Y∈ I. X被称为前件,Y是规则的后件。 此外,还有一些约束条件来衡量规则的重要性。 在本文中,我们重点关注两个标准:支持度和置信度。

  支持度: 它测量在同一事务中发生的项目集的频率。 K频繁项目集是频繁集合中包含K个项目的项目集。 可以将支持计算为在同一事务中出现多个项目的概率。 支持价值的最低阈值被称为最小支持度。

三、框架

L-CMP可以分为以下两个阶段: 学习不变式:这个阶段旨在通过学习算法寻找出辅助不变量。在这个阶段,我们首先收集协议的一个小实例 m(通常是m = 2)的可达状态集合(步骤1)。然后,我们直接从协议描述中提取原子谓词,并将它们看作项目集以指导数据集的转换(步骤2)。这一步对于第二阶段是必要的,第四节解释了背后的原因。接下来,通过关联规则学习,可以学习一组关联规则(步骤3)。值得注意的是,我们使用的数据集由一个小型的协议实例进行转换,因此由于实例的大小有限,无法表示整个参数化协议的行为。此外,我们已经应用了对称减少技术来使一些大协议中的可达状态最小化,导致数据集的不完整性。因此,需要额外的步骤(步骤4)。我们将这些关联规则视为候选不变量并将它们输入模型检查器Murphi。如果他们持有协议的一些小实例(大于m),则它们被视为辅助不变量。如果某些失败,失败的将从候选不变集中消除。最后,左边的候选不变量作为辅助不变量。   参数抽象和卫式加强:这个阶段是抽象协议,并使用辅助不变量加强抽象规则的卫式部分。首先,辅助不变量以及协议中的转换规则将通过分配具体索引来实例化(步骤5)。这一步为加强步骤提供了便利。接下来,通过以关联规则的形式添加辅助不变量的结果,递归地加强规则守护(步骤6)。然后,通过删除关于不可观察节点的局部变量来抽象加强的规则(步骤7)。值得注意的是,我们提出了一个映射操作,它建立了守卫与行动之间的关系,以便最大限度地加强规则。之后,加强和抽象的规则将附加到原始协议并送入模型检查器(步骤8)。请注意,用于加强守则规则的辅助不变量也需要验证将它们翻译成Murphi代码后。自动翻译的过程较为简单,所以我们在本文中就不赘述。如果抽象协议实例通过大小为$m + 1$的模型检测器,则结束框架(步骤10),否则就需要调整学习算法中的参数,并且框架开始下一轮学习(步骤9) 。

description

三、实验结果

我们将L-CMP应用于5个经典的带参协议上进行实验,实验结果如下表:

其中,列名分别为协议名称、频繁集个数、最小支持度、关联规则个数、辅助不变式个数、所用不变式个数、总运行时长、所耗内存峰值、抽象协议能否通过验证。 可以看到,我们的L-CMP能够很好地对包括Flash协议在内的各个协议进行很好的验证。

四、总结

在本文中,我们提出了一个自动框架L-CMP,它可以在一个统一的框架中自动学习辅助不变量,并进行抽象参数和卫式加强。 我们工作的创新性集中体现在于以下两个方面:

我们不是通过分析计数器例子来手动制定不同的变体,而是通过关联规则学习从协议的可达状态集合中导出不变量; 在反例生成之后,我们不再强化协议,而是根据自动学习的不变量直接进行卫式加强。

在未来的工作中,我们希望扩展L-CMP的验证能力,使其能证明一般的安全性质和活性性质,而不仅局限于不变式。 参考文献 [1] Lv, Y., Lin, H., Pan, H.: Computing invariants for parameter abstraction.In: Proceedings of the 5th IEEE/ACM International Conference on Formal Methods and Models for Codesign, IEEE Computer Society (2007) 29–38 [2] Apt, K.R., Kozen, D.C.: Limits for automatic verification of finite-stateconcurrent systems. Information Processing Letters 22(6) (1986) 307–309 [3] Chou, C.T., Mannava, P.K., Park, S.: A simple method for parameterized verification of cache coherence protocols. In: FMCAD. Volume 4., Springer (2004) 382–398 [4] Agrawal,R.,Imielin ́ski,T.,Swami,A.:Miningassociationrulesbetweensets of items in large databases. In: Acm sigmod record. Volume 22.,ACM (1993) 207–216

{{panelTitle}}
支持Markdown和数学公式,公式格式:\\(...\\)或\\[...\\]

还没有内容

关注微信公众号