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

文章正文
发布时间:2024-07-24 19:26

李勇坚,博士,研究生导师,人工智能开放创新平台*联合学者,主要研究方向:计算机科学理论和软件理论。

*注:人工智能开放创新平台:是由贵阳市政府与中国人工智能产业创新联盟、英特尔三方共同打造的开放平台。平台结合端到端的全面技术,打造软硬件开放创新平台,加速产业应用创新,通过打造人工智能开放平台、创立人工智能创新加速器等,建立完善的技术生态、在人工智能垂直领域应用、产业对接和市场推广等发挥各方优势和资源特色,加速中国人工智能的发展和应用创新。

  0引言

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

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

  CMP存在的缺点启发我们去更深入地思考:是否能够通过主动地探索满足上述条件的可达集边缘,以使可达集收敛,并满足安全性质?如果能够主动的限定可达集能到达的范围,则可以更主动地搜索辅助不变式,从而更精确地加强抽象系统。

  因此,在这篇论文中,我们提出了L-CMP,一种自动的学习框架,通过较小实例可达集学习/挖掘辅助不变式,并且自动的用这些辅助不变式对抽象协议进行限制,最终,抽象协议的可达集可以被收敛在合理范围,安全性质也就能够保证。

  1关联规则学习

  在本文中,我们巧妙地将关联规则学习(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个项目的项目集。可以将支持计算为在同一事务中出现多个项目的概率。支持价值的最低阈值被称为最小支持度。

  2框架

  L-CMP可以分为以下两个阶段,如图1。

1547024037297371.jpg

  2.1学习不变式

  这个阶段旨在通过学习算法寻找出辅助不变量。在这个阶段,我们首先收集协议的一个小实例m(通常是m=2)的可达状态集合(步骤1)。然后,我们直接从协议描述中提取原子谓词,并将它们看作项目集以指导数据集的转换(步骤2)。这一步对于第二阶段是必要的,第四节解释了背后的原因。接下来,通过关联规则学习,可以学习一组关联规则(步骤3)。值得注意的是,我们使用的数据集由一个小型的协议实例进行转换,因此由于实例的大小有限,无法表示整个参数化协议的行为。此外,我们已经应用了对称减少技术来使一些大协议中的可达状态最小化,导致数据集的不完整性。因此,需要额外的步骤(步骤4)。我们将这些关联规则视为候选不变量并将它们输入模型检查器Murphi。如果他们持有协议的一些小实例(大于m),则它们被视为辅助不变量。如果某些失败,失败的将从候选不变集中消除。最后,左边的候选不变量作为辅助不变量。

1547024037769344.jpg

  2.2参数抽象和卫式加强

  这个阶段是抽象协议,并使用辅助不变量加强抽象规则的卫式部分。首先,辅助不变量以及协议中的转换规则将通过分配具体索引来实例化(步骤5)。这一步为加强步骤提供了便利。接下来,通过以关联规则的形式添加辅助不变量的结果,递归地加强规则守护(步骤6)。然后,通过删除关于不可观察节点的局部变量来抽象加强的规则(步骤7)。值得注意的是,我们提出了一个映射操作,它建立了守卫与行动之间的关系,以便最大限度地加强规则。之后,加强和抽象的规则将附加到原始协议并送入模型检查器(步骤8)。请注意,用于加强守则规则的辅助不变量也需要验证将它们翻译成Murphi代码后。自动翻译的过程较为简单,所以我们在本文中就不赘述。如果抽象协议实例通过大小为$m+1$的模型检测器,则结束框架(步骤10),否则就需要调整学习算法中的参数,并且框架开始下一轮学习(步骤9)。

  3实验结果

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

  4结论

  在本文中,我们提出了一个自动框架L-CMP,它可以在一个统一的框架中自动学习辅助不变量,并进行抽象参数和卫式加强。我们工作的创新性集中体现在于以下两个方面:1.我们不是通过分析计数器例子来手动制定不同的变体,而是通过关联规则学习从协议的可达状态集合中导出不变量;2.在反例生成之后,我们不再强化协议,而是根据自动学习的不变量直接进行卫式加强。在未来的工作中,我们希望扩展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.Mining association rules between sets of items in large databases. In: Acm sigmod record. Volume 22.,ACM (1993):207–216

本文来源于中国科技期刊《电子产品世界》2019年第1期第82页,欢迎您写论文时引用,并注明出处