参数化数据结构的抽象和演绎方法的应用：以分布式共享内存一致性协议为例

《理论计算机科学电子笔记》50第4期（2001年）VEPAS 2001URL：http://www.elsevier.nl/locate/entcs/volume50.html15页具有参数化状态空间的K. Baukus K. 斯塔尔计算机科学和应用数学研究所CAU Kiel，PreusserSTR.1{9}，D-24105基尔，德国。kba@informatik.uni-kiel.dekst@informatik.uni-kiel.deS.BensalemY. LakhnechVerimag，中心方程，2 Av. 来自维格纳特，38610德国，法国。bensalem@imag.frlakhnech@imag.fr摘要一般来说，参数化网络的真阳离子是不可判定的。近年来，已经进行了大量的研究来识别参数化系统的子类，其中某些性质是可判定的。一些结果是基于参数化系统的抽象，以便使用模型检查技术来建立这些属性。在以前的一篇论文中，我们提出了一种方法，允许计算在可判定逻辑WS1S中建模的参数化系统的抽象。这些WS1S系统提供了一种直观的方法来描述非状态过程的参数化系统。然而，在实践中，由于不受限制的数据结构，网络中的进程本身处于休眠状态。边界性的一个来源可以是参数化数据结构的使用。另一个典型的来源可能是在参与过程的子集上存在排列结构。例如，这是组成员资格或分布式共享内存一致性协议的情况。在本文中，我们使用演绎方法来处理这样的网络，其中数据结构由进程数和附加参数化。我们展示了如何推导出一个抽象的WS1S系统，该系统可能会受到算法验证。为了说明该方法，我们使用PVS作为演绎veri阳离子部分，使用pax和SMV工具作为算法部分来验证分布式共享内存一致性协议的正确性。c2001年由爱思唯尔科学B. 根据C C BY-NC-ND许可证开放获取。2VEPAS 2001 {K.鲍库斯，K.斯塔尔，S.Bensalem和Y.拉赫内克1引言具有未知数量节点的网络实际上无处不在，例如，在计算机上运行的进程、令牌环中的机器、LAN甚至万维网本身。因此，为这样的参数化网络开发了一系列算法，如互利、领导者选举、组成员资格或分布式内存算法，并且期望它们对任何特定数量的参与者都有效地工作。Hence，虽然已知该问题是不可判定的（Apt和Kozen，[2]），但人们对这样的协议的真实性非常感兴趣。此外，已经开发了用于参数化网络的受限类的真实性的自动化和半自动化方法。[18，25，5，23，14，19]中提出的演绎方法基于过程数量的归纳。这些方法需要一个网络不变量，该网络不变量抽象任意数量的进程，并尊重保留要验证的属性的预排序。[13，10，11]中提出的算法方法表明，对于任意大小的环网络和客户端-服务器系统的类，存在这样的k，即参数化网络的真阳离子可以简化为大小为k的网络的真阳离子。[17]中提出的一种半自动化方法使用了用正则语言表示参数化网络状态集的思想，其中另外使用nite状态换能器来计算前置传感器。在[1，16]中，加速技术被应用于考虑在微小的时间内进行跃迁的概念。在[3]中，我们展示了如何在可判定逻辑WS1S中表示参数化系统，即，系统的当前状态被建模为WS1S中描述了自然数的nite子集和网络中进程的转换在WS1S中提供布尔抽象关系该方法用于验证多个参数化协议。通过附加标记算法和公平性条件的提升（[4]），我们能够很好地建立这些协议的生存性属性。该方法在一个名为pax1的工具中实现，该工具使用Mona的决策过程来检查WS1S公式的充分性。在本文中，我们展示了如何将此方法与演绎验证相结合，以验证不能满足上述要求的协议，即网络中的每个进程都有无限的状态空间。在这里，我们提出了不受限制的不同原因。首先，我们处理有两个参数的问题;一个给我们进程的数量，另一个对每个进程本身进行参数化。第二，通常情况下，渲染进程使用数据结构来保存有关其他进程的信息，1 http://www.inf或rm at ik. 一个i-k，即l。de/~kb a/pax3VEPAS 2001 {K.鲍库斯，K.斯塔尔，S.Bensalem和Y.拉赫内克即，它们的数据结构跨越所涉及的进程的子集，因此是不受限制的。我们使用一个典型的例子来说明我们的方法：分布式共享内存协议。该协议有两个参数：进程数和内存页数。为了确保独占写入和多次读取，进程必须知道其他进程的实际访问权限。我们在PVS框架中给出了这类协议的一般抽象，并展示了如何使用pax和SMV分析抽象的WS1S系统，以证明协议的安全性和生存性特性2方案描述为了说明我们的方法，我们验证了Li和Hudak在[20]中提出的分布式共享内存一致性协议。分布式共享内存（DSM）的概念是允许分布式环境中的处理器使用彼此的本地内存。DSM系统为处理器网络提供虚拟地址空间。它们在网络上复制或迁移数据，以处理来自在处理器上运行的线程的请求。Li和Hudak的协议是一个多读取器、单写入器协议;允许多个进程读取同一数据，而写入访问是独占的。作为读/写请求主题的数据被组织到页面中。每个处理器上的页表维护每个页的处理器的当前访问无论处理器拥有哪个页面，状态都可以被读取或写入并保留信息。所有者是对页面具有写入权限的最后一个处理器。此外，如果处理器没有页面的本地副本，或者如果页面已被其他处理器修改，则状态可能为nil。当处理器想要升级其权限（从零到读取或从读取到写入）时，它通过广播发送相应的请求。所有者处理请求;对于读取请求，它将请求处理器添加到副本集（具有读取访问权限的处理器列表）。 副本中的处理器-当处理器想要写入访问时，必须被通知。这些处理器中的每一个都必须知道它已将其页表更改为空。然后，所有权更改为请求处理器。 图1中的伪代码描述了各种操作。[12]作为一种通信机制，我们假设有一个中央请求队列，所有请求都发送到该队列。确认将直接发送给请求处理器。方案描述立即为我们提供了四个真正的阳离子目标：独家所有权：每个页面总是有一个最多的所有者。独占写入：每当有一个处理器具有对p的写入访问权限时，就没有具有读取访问权限的处理器4VEPAS 2001 {K.鲍库斯，K.斯塔尔，S.Bensalem和Y.拉赫内克请求RD（P）PTable[p].lock：=true;对p的广播读取请求;获取rd ack（p）PTable[p].access：=读取;PTable[p].lock：=假;请求WR（P）PTable[p].lock：=true;对p的广播写入请求;获取wr ack（p，copy-set）PTable[p].access：=inv;请求无效（p，复制集）;无效请求（p，copyset）For k in Copyset DO发送P到K的投资请求;读取nilack（i）PTable[p].复制集：=PT表[P].copysetnfig;发送rd ack（p，i）PTable[p].lock：=true;如果PTable[p].owner然后PT表[p].copyset：=PT表[p].copyset[fig;PTable[p].访问：=读取;发送确认和P到I; FIPTable[p].lock：=false;发送wr ack（p，i）PTable[p].lock：=true;如果PTable[p].Owner，则将p和副本集发送到i;PTable[p].access：=nil;PTable[p].Owner：=false; FIPTable[p].lock：=false;发送发票确认（p）如果PTable[p].access=读取然后PTable[p].access：=无;发送确认消息; FI获取所有者如果PTable[p].copyset=;和PTable[p].access=inv THENPTable[p].access：=写入; PTable[p].copyset：=;;PTable[p].Owner：=真; PTable[p].lock：=假; FI图1. 根据DSM协议的具有读取访问页面p的权限的处理器始终在p的所有者的副本集中，但所5有者本身除外。活动性：每当处理器请求访问权限时，它最终会获得这些权限。6AA AA A AAAA AVEPAS 2001 {K.鲍库斯，K.斯塔尔，S.Bensalem和Y.拉赫内克3通过抽象首先，让我们回顾一下一些nition和通过抽象证明系统时间性质的概念。 给定无死锁2转换系统S =（V;; T）和完全抽象关系A，我们说SA =（VA;A; TA）是S w.r.t.的抽象。如果满足以下条件，则以SvS A表示：（1）1（）和（2）11 对于CorresPOnding2T，2T A。如果A是nite，则调用nite抽象关系。让它成为一个LTL为mulae和让它[]（分别。 [[A]]）不包括"的集合或"的集合"。'）。然后，从S到S，1（[']）[[']]，和S j='we可以得出Sj='。 这句话被称为前v个结果，它是抽象的最佳真阳离子：因为如果S A是nite，它可以自动成为SAj='A。事实上，在没有存在量子阳离子的情况下，任何时间逻辑都可以得到类似的preser-v-ation结果，例如 8CTL？[2]或[3][4]。如 果 我 们 已 经 证 明 了 一 些 状态 性 质' 在 S 中 是 不 变 的 ， 即Sj=2'，we可以在条件（2）to（20）下（\f（s; s）jsj=';sj=' g）110 1 0 1A这允许搜索一些较小的抽象系统，以便为具体系统建立属性。我们用S v S A来表示这种类型的抽象。在情况S是一个公平的过渡系统，F是公平性公式，如果F A是公式ofS的公平性，那么by需要1（[：F]）[[：F]]，weh ave与上面的结果相同。我们用S v F S A来表示这种类型的抽象。3.1使用PVS的我们的目标是使用抽象技术验证Li和Hudak的DSM协议。在[3]中，我们介绍了如何在WS1S可判定逻辑中为具有nite进程的网络自动计算抽象。未调整的是，Li和Hudak的协议处理参数化的页数（在参数化的处理器数量之外），并且每个页表条目包含一组（复制集）处理器索引。为了减少处理器的状态空间，我们引入了全局复制（PVS声明见图2）。此变量对所有处理器都是全局的。每当拥有页面所有权的处理器更新其本地副本集时，我们都会向其添加分配。如果我们能证明某个处理器的本地副本集在需要时与全局副本一致，我们就可以删除所有本地副本集。2 在本文中，我们只考虑可以通过添加空闲过渡来实现的无死锁定过渡系统。7VEPAS 2001 {K.鲍库斯，K.斯塔尔，S.Bensalem和Y.拉赫内克访问：类型 =f写入，nil，读取，inv验证g请求：类型 =f读取请求，g写入请求直接：类型 =f写入ck，读取ck，nilreqgN，P：posnat处理器：类型=以下（N）页面：类型=以下（P）复制集类型：type=setof[处理器]请求c通道：类型 =list[[Pr ocessor，Requests，Page]]直接c通道：类型 [已停止!列表[[直接，P年龄]无确认：类型=[页面! 列表[处理器]PageEntry：类型=[#访问：[处理器!访问]，还是主人？L OCKED？[已停止![bolol]，复制集：[处理器! 复制设置类型]、发送copy、全局copy：Copy设置type#]状态：类型=[#PageTable：[页面!PageEntry]，请求：请求c通道，DirectCom：Directc频道，Nils： Nil Acks#]图2. PVS理论为了处理第二个参数（页面参数），我们标识了一类参数化网络，我们可以通过将第二个参数实例化为1来验证其某些属性。这些中间步骤为我们提供了一个可在WS1S中呈现的简化系统，但仍然允许证明原始协议的属性。我们使用PVS [22]来建立还原。由于PVS允许对规范阳离子使用高阶逻辑，因此直接为图1中的伪代码提供PVS模型。图3显示了表示为前状态和后状态之间关系的示例转换。使用PVS，它可以直接证明在需要时，全球复制集与本地复制集匹配。该属性（见图4）在所有转换上都是归纳的，并且最初是完全线性的，因此是不变的。此步骤如前所述，网络协议经常处理跨网络中的处理器集的数据结构作为示例，我们列出了第2节中描述的共享内存协议或组成员协议。为了说明通过引入所有处理器使用的全局结构来减小每个进程的状态空间的想法8如何可以应用于其他协议，让我们考虑组成员资格协议。布里和每个人9VEPAS 2001 {K.鲍库斯，K.斯塔尔，S.Bensalem和Y.拉赫内克s，s1：变量状态i：var处理器p：var页面reqrd（s，s1，i，p）：bool=访问（PageTable（s）（p））（i） =零^锁定？（PageTable（s）（p））（i）^s1=s，其中[（ PageTable）（p）：= PageTable（s）（p）与[（锁定？（i）：=真，要求：=cons（（i，读取请求，p），请求）图3.请求读取访问全局Local（s，i，p）：bool=（所有者？（PageTable（s）（p））（i）复制集（PageTable（s））（i） =全局复制（PageTable（s））图4.所有者的全局副本和副本集的平等性处理器跟踪哪些处理器仍处于活动状态并是网络工作的重要检测到持续的通信错误，并将处理器从功能良好的处理器的成员发运列表中删除。这些协议有两个感兴趣的属性：一致性，意味着运行良好的处理器同意它们的成员列表;有效性，意味着最终将检测到错误，然后成员列表与运行良好的处理器集相关联。我们通过演绎地证明rst协议来分析同步组成员协议。然后，我们可以通过使用由处理器自己维护的全局成员列表来简化系统。现在，回到我们的DSM协议。即使我们删除了所有本地副本集，我们也有一个处理器系统，其中每个处理器都维护一个参数化页数的页表。但是，我们观察到（并可以用PVS证明），所有转换只更改一个页面的页面条目，并且只消耗或产生与该页面相关的消息。我们在下一个Nition中x这些设S（N; P）是具有N个处理器和第二个参数P的参数化系统。 让处理器在一些消息队列上通信q1; ：;q k，其中ea ch消息的形式为（i;ms g;p），其中i

下载后可阅读完整内容，剩余1页未读，立即下载