P2P算法验证：环形结构化覆盖网络的案例研究

理论计算机科学电子笔记181（2007）35-47www.elsevier.com/locate/entcsP2P算法的验证：一个案例研究Rana Bakhshi皇家理工瑞典KistaDilian Gurov2皇家理工瑞典斯德哥尔摩摘要结构化对等（P2P）覆盖网络中存在并发加入和节点故障的维护问题是深入研究的主题。众所周知，P2P系统底层的各种算法很难设计和分析。因此，在验证P2P算法时，真正的挑战是找到足够的抽象级别来建模算法并执行验证。本文提出了一个环形结构化P2P网络的抽象模型。我们的模型是基于进程代数的，它以其成熟的理论，为许多基本的P2P算法的验证提供了正确的抽象层次。作为一个案例研究，我们验证的Chord，最有名的P2P覆盖网络的稳定算法的正确性。为了证明算法的正确性，我们给出了Chord系统在进程代数中的具体化和实现，并建立了两者之间的互模拟等价性。保留字：对等系统、验证、进程代数。1介绍近年来，分布式应用和P2P网络受到了极大的重视。这样的系统是分散的和高度动态的，允许任意数量的节点加入和离开网络。在大多数P2P系统中，最基本的操作是数据项的有效定位，而网络中节点是否可达是一个关键问题。P2P网络结构1电子邮件：ranab@kth.se2电子邮件地址：dilian@nada.kth.se1571-0661 © 2007 Elsevier B.V. 在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.01.05236R. Bakhshi，D.Gurov/Electronic Notes in Theoretical Computer Science 181（2007）35并根据应用需求维护具有特定拓扑的覆盖网络。鲁棒P2P系统从假设的初始状态开始产生期望的拓扑。对于大型系统，需要仔细设计以确保稳定算法的正确性。这样的系统的一个例子是Chord [14]，一个简单的健壮的结构化P2P系统，实现了分布式哈希表（DHT）抽象[3]。分布式哈希表将关键字（数据标识符）映射到覆盖网络的节点，并提供用于定位负责给定节点的当前对等节点的设施。Chord通过执行稳定化算法来保持节点加入和离开系统时的分布式状态。在描述这种算法的文献中，例如Stoica等人的原始Chord论文。[15]，正确性证明是在高抽象级别上概述的，并且倾向于不提供操作语义。另一方面，模型检查技术并不直接适用于P2P系统的验证，因为这些系统本质上是动态的，并且具有无限状态行为。因此，一个真正的挑战是找到一个正确的抽象级别，在这个级别上对算法进行建模并执行验证。本文总结了Chord稳定化算法的形式验证结果。它专注于Chord协议[14]的纯加入模型，其中任意数量的节点可以加入网络，每个节点都运行稳定化算法。利用进程代数分析了稳定化算法的正确性。所选择的进程代数是π-演算[8，13]，这是一种用于建模并发和分布式程序的自然语言，特别适合于指定具有动态变化通信拓扑的移动系统。本文的主要结果是：• 一个抽象的制定动态网络与环拓扑（节。4）.• 根据π演算对动态Chord系统的规范和实现进行建模（第4节）。• 使用弱互模拟关系对规范和实现的等价性进行了形式化证明，从而确立了Chord稳定化算法的正确性5）。相关工作。以前所有用进程代数对基于环的网络进行建模的研究都假设网络中的节点数量是固定的。基于DHT的DKS系统的查找算法已被验证用于使用值传递CCS的网络的静态模型[4]。Palamidessi [10]用混合选择的π-演算证明了对称环上的领导者选举问题。本文假设存在一个特殊的自由输出通道，用于与“外部世界”进行通信。它还假设存在一个特殊的子集，从一对一的映射与自然数配备的名称集合，以识别网络中的各个进程。Phillips等人。 [11]采用类似的方法来解决Mobile Ambients演算中的相同问题。R. Bakhshi，D.Gurov/Electronic Notes in Theoretical Computer Science 181（2007）3537其他形式化方法，例如断言证明方法，已经被用于P2P网络中环形拓扑的并发维护问题[7]。Krishnamurthy等人。 [6]使用基于主方程的方法对Chord进行了分析研究。请注意，我们工作中提出的模型符合实际算法的正式证明超出了本文的目标。但是，该算法的相对简单性，用Erlang编程语言的语法编写，允许通过简单的检查将两者与高水平的置信度联系起来。Noll和Roy [9]的研究解决了将Erlang映射到π演算中的问题。2Chord协议在本节中，我们简要介绍Chord协议，重点是其稳定算法。与这项工作无关的细节，例如key对节点的分配，被排除在论文之外，可以在Stoica等人中找到。 [14 ]第10段。Chord是一种自组织分布式P2P查找协议，它支持一种操作：给定一个密钥，它将密钥映射到一个节点上（图1）。通过将键与每个数据项关联，并将键/数据项对存储在键映射到的节点上，可以在Chord之上轻松实现数据定位。Chord可以有效地适应节点加入和离开系统，即使系统不断变化，也可以回答查询。图1：弦环恒等式空间在和弦， 每个节点都有一个n位标识符(ID)，其被假定为唯一的并且属于称为ID空间的集合。节点{k1，k2，...，k n}<$N，N是一组自然数。发送和接收的值是在有限个索引集I <$Nn上的项。我们设λ和λ是N上模n的加法和减法，结果总是严格小于模。当一个新节点加入网络时，它应该被放置在环中具有正确ID的两个节点一个节点的两个基本邻居是它的前任和继任者，根据I上的偏序选择。一 个节点被称为一个在集合论中具有H Dx的集合的子集，如果在集合论中的第一个节点被定义为x，则定义为：Succ（x，m）={y∈m}|（y<$x）=m in{（z<$x）|z∈mI}。函数succ：I×P（I）→ I是定义良好的，因为z<$x=y<$xi <$z<$y=0;P（I）这是一个权力的自我。根据定义的系统信息，预先确定或更新以下信息：pred（x，m<$）={y∈m<$|（y<$x）=max{（z<$x）|z∈m} m usemx todenteunionm{x}.⊆I}∪{x∈/mˆ| ⊥}. 我们38R. Bakhshi，D.Gurov/Electronic Notes in Theoretical Computer Science 181（2007）350%新的节点加入子一个Chord环， noden2n'！{“find_successor“，n}3接收4{“find_successor“，n5c：=n6端8%，平行于10回路11接收12{“find_successor“，n13ifn14n'！{“find_successor“，搜索结果}15n16快！{“find_successor“， n17端18端20%稳定化算法21stab（）->22succ！{”req_predecessor”，n}23接收24{“resp_receessor“，n25ifn26intn=n27succ！{”notify“， n}28端30%的平行于32回路33接收34{“req_receessor“，n35n '！{”resp_precedent”，pred}36{“notify“，n' } ->37ifpred=nil <$n38pred：=n39端40端稳定算法。为了在参与节点的集合发生变化时断言查找正确执行，Chord必须确保每个节点的后继指针是最新的它这样做使用稳定算法，图。二、定义2.1一个Chord环是稳定的，如果对于所有节点u，precedor（successor（u））=u，并且没有节点v使得u v successor（u）。Chord协议的Pure Join模型假设节点没有为了简化网络表示，该模型不包括在协议的一般模型中考虑的后继列表和手指表。稳定方案保证节点加入环的方式，保持现有节点的可达性，即使在面对并发加入。图二. Join算法虽然Chord的稳定算法在原始论文[ 14 ]中以“RPC风格”提出这反映在我们的版本的稳定算法，在图。二、该算法以Erlang编程语言的语法给出[1]。对于Erlang的形式语义，参见例如。[12 ]第10段。在Erlang中，通信是-R. Bakhshi，D.Gurov/Electronic Notes in Theoretical Computer Science 181（2007）3539进程间进程通过进程消息队列（“邮箱”）是异步的我的意思是，我的意思是，定义将事件发送到进程I;赋值表示为：=; receiveX end检查进程传入的邮箱并传递第一个X模式匹配元素;loopXend在loop中执行X。{“M“，I}表示由ID为I的进程发送的M类型的消息。当节点n第一次启动时，它运行join（2，其中nJ是任何已知的Chord节点。join（）函数要求nJ找到n的直接后继者，但不会让网络的其余部分知道n。所有节点执行图2中第8-16行给出的代码系统中的每个节点定期执行stab（）。当节点n运行stab（）时（见图2），它向后继节点询问后继节点如果节点p加入系统，这将是一种情况。此外，stab（）通知节点n的后继节点n只有当后继者不知道比n更近的前趋者时，它才会这样做。这种稳定算法[14]保证了Chord环收敛到一个稳定的配置，即环拓扑，尽管并发连接，如果系统开始在稳定的配置（定义。2.1）。图3.第三章。连接时的稳定性图示图3示出了联接操作的示例。节点26在节点21和32之间加入系统。弧线表示后继关系。（a）最初，节点21指向节点32;（b）节点26通过执行join（），要求任何已知节点查找其后继节点（即，32)并指向它;（c）stab（）将节点21的后继更新为节点26。3π演算由于Chord系统是动态的，即节点可以自由加入网络，我们选择的建模形式是π-演算[8，13]。它基于进程和名称的概念进程之间的通信通过名称（通道）进行。在通道p上输出值v的进程Q（即，p=v.Q）可以与尝试从通道p读取的并行进程QJ（即，p（z）.QJ）同步。作为值发送的名称可以在以后用作通信通道此功能允许进程在计算期间动态建立连接。40R. Bakhshi，D.Gurov/Electronic Notes in Theoretical Computer Science 181（2007）35本节简要回顾π演算的语法和操作语义。有关更多详细信息，请参阅Milner [8]和Sangiorgi和Walker [13]。本节介绍了Borgstréometal的原始工作原理。 [4]在结构化P2P系统的静态情况下。u，v：：=o，p，x名字|in，id渠道|⊥未确定值|ki，kj整数，ID|succ（x，m）继任者|pred（x，m）前任e，eJ，eJJ：：=u表达式φ，φ：：=e=eJ布尔测试|e∈（eJ，eJJ]间隔检查m，mJ，mJJπ：：=τ|p<$−→v|p（−→v）集合，子集普雷菲克斯||（−→v）.P−→u−→v.P抽象具体化Q、R：：=过程|M求和||（Q|右）（ν−→p）Q并联组成限制|ifn thenQ elseRif语句||！QQ−→v复制过程常数M，MJ：：=0不作为|π.Q过程动作|M+MJ选择见图4。语法我们的模型和Chord协议的稳定方案的验证3）。R. Bakhshi，D.Gurov/Electronic Notes in Theoretical Computer Science 181（2007）3541操作语义学π演算的操作语义由承诺规则定义[8，13]：−（R-RCT-L）JJτ（一）J（p（z）.Q + M）|（p<$v<$.Q + M）→{v/z}Q|Q（R-TAU）−τ。Q+M→τQ（二）42R. Bakhshi，D.Gurov/Electronic Notes in Theoretical Computer Science 181（2007）35πQ→π QJ（R-PAR-L）πJ（三）Q|R→Q |R（R-RES）Q→QJπ（四）J（νp）Q→（νp）Q省略了（1）、（3）的对称形式。表达式的求值是一个函数[·]]：Eπ→N，其中Eπ是一组π-演算表达式（图1）。（3）：[[e]] ={ki， ife =ki;，otherwise}谓词eb（·）执行布尔检查：eb（e1=e2）为真i [[e1]]=[[e2]]（5）eb（e1∈[e2，e3]）为真i <$[ei]]=ki∈I，其中i= 1， 3且0≤k1<$k2≤k3<$k2（六）为了计算if语句的表达式，π演算被扩展为约简关系>，满足以下规则：ifn thenQ elseQJ>Q，ifeb（n）（7）如果，则Q，否则QJ> QJ，如果，则b（k）（8）和对应的承诺规则：Q >QJQJ→πQJJ（R-RED）Q→πQ（九）JJ互模拟在π演算中，过程的标准等价关系是双模拟[8，13]。直觉上，如果两个系统可以逐步匹配彼此的动作，那么它们是双相似的。强版本和弱版本之间的区别在于对沉默行为的看法，τ。设Pπ是一组π-演算过程表达式（图3）。定义3. 1对于一个简单的函数π，图中的given。3，therelationsndπ如下所示被定义为(i) P→ Q意味着有一个零个或多个反应的序列P →. → Q。定义形式上，= →，→的传递自反闭包。π p1pn(ii) 设π = p1. p n. P → Q表示P → P1. → P n对于所有y，→πdefp1pn= →... →定义3.2集合Pπ上的二元关系S是强模拟，如果，无论何时πJ JπJ JPSQ，如果P→P，则P →Q。Q→Q和PSQ。R. Bakhshi，D.Gurov/Electronic Notes in Theoretical Computer Science 181（2007）3543如果S及其逆都是强模拟，则S是强互模拟并由m表示。定义3.3集合Pπ上的二元关系S是弱模拟，如果，无论何时PSQ，如果P<$PJ，则<$QJ。Q≠QJ和PJSQJ;pujJpujJ J如果P = P，则Q。Q = P_Q和P_S_Q;pJ JpJ J J如果P是P，那么P是Q。QQ和PSQ。如果S和它的逆都是弱模拟，则S是弱互模拟，记为S。4建模我们现在描述一个用于Chord协议的规范和实现的正式模型。系统的动态模型应该清楚地定义拓扑，并表示节点到系统的连接。请注意，所有通道都是单向和单一用途的（即每种类型的通道用于一种类型的消息，如图所示）7），因为它是建议的基础π演算。规格。我们将Chord协议指定为网络中节点的集合，形成环形拓扑并不断增长。一般来说，节点可以以任意顺序加入网络。由于系统的内部结构对观察者是隐藏的，一个主要问题是如何指定环的行为。我们提出的方法是添加一个令牌环协议，即一个抽象的令牌顺时针通过沿环，在和弦协议的顶部。进程环表示节点的环。节点之间的通信没有指定;因此，内部链接是受限制和不可观察的。 唯一可见图5：工艺环动作是每个节点特定端口的输出，代表其ID（图1）。5）。环（ki，m）τ.idki.环succ（ki，m），mΣ+τ.环k，mk（10）I jkj∈I\m这里m表示系统中已经存在的节点的标识符集合; id ki 是仅由节点ki执行的输出端口，因此，以抽象的方式表示节点; succ（ki，m）是节点ki从集合m中的后继;I是索引的有限集合。Ring行为由以下非确定性选择表示：44R. Bakhshi，D.Gurov/Electronic Notes in Theoretical Computer Science 181（2007）350% %nn ewnodejoinng aChordringcontainingg noden2n'！{“find_successor“，n}3接收4{“find_successor“，n5c：=n6端8%，平行于10回路11接收12{“find_successor“，n13ifn14n'！{“find_successor“，搜索结果}15n16快！{“find_successor“，n17端18端20%%稳定算法21stab（）->22succ！{”req_predecessor”，n}23接收24{“resp_receessor“，n25ifn26intn=n27succ！ {”notify“，n}28if（nn））->29succ！ {”notify“，n}30端32%在平行于34回路35接收36{“req_receessor“，n37n '！{”resp_precedent”，pred}38{“notify“，n' } ->39ifpred=nil <$n40pred：=n41if（pred = n）（succ = n）->42intn=n43succ！{”notify“，n}44端45端见图6。改进稳定算法• 新节点可以加入环，允许网络通过将其ID添加到集合m来增长。获取相邻链路的过程由τ执行。在这里，我们不重新定义这个或这个数据，因为这个节点在这个工作中是连接的，即。e. kj∈I\m.• 节点在其信道（idki）上执行输出，前面是τ，并将令牌传递给最近的邻居，即其后继者。这就形成了一个连续输出的循环，其中每个后继输出都在等待它的前一个输出被启用。实施.Chord被实现为并发移动进程的产品-每个节点一个进程，其中所有请求/响应都根据图中给出的算法处理二、与我们的规范一样，我们通过添加令牌环端口来扩展Chord协议的实现。该扩展不会影响稳定算法，因为该端口上的反应在x中，在x中，在x中，在x中。12 3 4R. Bakhshi，D.Gurov/Electronic Notes in Theoretical Computer Science 181（2007）354541π演算使用同步通信，这意味着在某些情况下可能会发生死锁或错误行为这包括节点尝试联系自身的情况因此，我们对原始算法进行了两次修改，如图2所示，以处理网络中有一个和两个节点的情况。稳定化算法的修改版本见图1。六、进程P是不在网络中但可以加入网络的节点−−→−−→ .−−→−→−−→−−→−→ΣP（inkj，inki）（ν inkj）inkiinkj.inkj（inz）.Aidkj，inkj，inkz，（十一）4 4 4他是一个节点的ID，它连接到网络，还不是环的一 部 分 ; 在 ki 中 ， 是 Chord 环 中 任 意 节 点 的 “findsuccessor”端口。图7所示的过程A用编码的稳定算法定义了一个网络节点（图6）。它存储关于自身、其后继者和其前身的信息：A（ido，−in→o，−in→s，−in→p）ins−in→o.Aido，−in→o，−in→s，−in→p图7：工艺Ao−→zz−→po−→o−→z −→p+ 在1（in）.在2（in）.o−→zz−→oo−→o−→z −→p+ 在2（在）。（如果z∈（o，s），则在3中，在n中。o−→o−→s−→pelse（ifz =o thenA id，in，in，ins−→oo −→o −→s −→po −→zelsein3in.A id，in，in，in）+ 在3（在）。（如果p=z∈（p，o））z−→oo −→o −→z −→zthen（if（p=o）（s=o）thenin3in.A id，in，in，ino−→o−→s−→zo−→o −→s −→pelse一个id，in，in，in）else一个id，in，in，in）o−→zz−→so −→o −→s −→p+ 在4（在）。（如果z∈（o，s），则在4中，s−→zo −→o −→s −→pelsein4in.A id，in，in，in）ooo−→o −→s −→ps+ in，in，in，in|在5. 0（12）−→xx x x x x其中：in={x，in1，in2，in3，in4，in5}。O−→o这里o是节点的ID，−→s- 其专用输出端口，−→p- ID和侦听（输入）端口节点;在- 后继设备的ID和入端口，以- 前代的ID和端口节点A使用其邻居的入端口来发送消息。这些链接是通过执行以下操作获得的（见（12）和图11）。6）：46R. Bakhshi，D.Gurov/Electronic Notes in Theoretical Computer Science 181（2007）35o−→z•等待来自新节点的和入端口;检查新节点的后继者是否是后继者，如果是，R. Bakhshi，D.Gurov/Electronic Notes in Theoretical Computer Science 181（2007）354754我k k kkJ J J Jz−→s返回后继节点s−→z将新节点的信息绕圈传递给后继节点（在4圈内）。该片段由图10中的第10-18行呈现。六、o−→z• 从另一个节点接收z−→p前导信息到消息中，并将此消息发送回（在2个字节内）。有关代码的详细信息，请参见图36-37行。六、o−→z• 监听z∈（o，s）满足，通知发送方，使其通过发送其ID和入端口并更新后继者信息而成为节点的前任。如果检查失败，则仅当z=o时才确认后继者是其前导者。这对应于图24-27中的线六、o−→z• 从另一个节点获得通知（在3（在））与节点条件p=0，z∈（p，o）-如果为真，则更新前任信息;此外，如果p = o = s，则更新继任者有关代码的详细信息，请参阅图38-43行。六、• 通过发送“请求前导”消息从后继者请求信息s−→osage（in1yearin year）. 这是根据图22的线完成的六、• 一个人，一个人;一个人，一个人;一个人，一个人。0）和信号5 5特殊端口（IDO）。ProcessImpl实现Chord协议，由节点A、准备加入网络的节点P和令牌的集合组成，所有这些都并行运行−−→−−→−−→Impl（ki，m）（νin kj，in ki，in kl）（（in ki. 0个）|（Σ−−→Pin kj，in kv）||kJ∈mJJ<$m−−→−→−→Aidi，ini，si，pi|kl∈mJ<$mkj∈I\mkv∈mJ−−→−→−→Aidkl，inkl，skl，pkl）（十三）J −→x−−−−−−−→−→x−−−−−−−→JJ当kj∈I\m且dki∈m;s= insucc（x，m） 和p（x，m）;m是一组其中包含连接但未在Chord环中建立的所有节点，即注意，当所有节点都放在Chord环中并且m=mJ<$mJJ时，mJJ可以为空。5验证我们现在提出的弦的稳定化算法的正式验证的结果下验证使我们确信，稳定算法最终将固定每个节点的直接后继者（因为我们考虑纯连接模型），网络最终将再次形成环形拓扑。直觉上，如果所有节点都将得到48R. Bakhshi，D.Gurov/Electronic Notes in Theoretical Computer Science 181（2007）35关于其前任的正确信息，即节点将获得右邻居和左邻居。我们通过建立它们的行为等价性来验证实现的正确性如果这两个模型是双相似的，那么算法正确地工作，即最终产生一个包含加入网络的新节点的环形拓扑。我们用来展示规范（10）和实现（13）是（弱）双相似的，是证明它们是同一个保护方程组的解，然后利用推广的π-演算的唯一解定理[8，13]定理5.1设环和Impl定义如上。然后环管安装该定理通过证明规范（10）和实现（13）解决了以下保护方程组来证明ΣX（ki，m）τ. 伊德基岛X∈su cc（ki，m），m∈+τ.Xki， mkj（14）kj∈I\m其中ki∈m，kj∈I\m.证明的更多细节出现在本文的完整版本[2]。6结论在本文中，我们介绍了一个抽象模型的结构化P2P网络与环形拓扑结构。我们选择的建模形式主义是π演算，移动进程的演算，是基于观察到的P2P系统是一个高度动态的性质，允许节点加入和离开网络在任何时候。我们通过在Chord作为环网络的规范和稳定算法的实现之间建立弱互模拟来验证Chord稳定算法的正确性目前的案例研究表明，π-演算提供了一个合适的理论验证相对简单的P2P算法。它扩展了以前的结果的正确性的另一个P2P系统的查找算法的静态情况下，没有节点加入和失败[4]。未来的工作需要包括P2P网络的其他方面，包括网络中存在故障，添加手指表和后继者列表等。此外，π演算模型可以形式化，互模拟证明可以在定理证明系统（如Isabelle/HOL）中进行R. Bakhshi，D.Gurov/Electronic Notes in Theoretical Computer Science 181（2007）3549引用[1] J. Arm s trong， R. Virdinging ， C. 是 的 ， 还 有 M 。 我会 给你的 。在Erlan g中 进 行 了 一 致 的Programmingg。Prentice Hall，第二版，1996年。[2] R. Bakhshi和D.古罗夫Peer-to-Peer算法的验证：案例研究。技术报告，信通技术，2006年5月。http://www.nada.kth.se/http：//www.example.com/papers/chord.ps.gz。[3] Hari Balakrishnan，M. Frans Kaashoek，David Karger，Robert Morris，and Ion Stoica. 在P2P系统中查找数据。ACM来文，2003年2月。[4] JohannesBorgstr ？om ， UweNestmnn ， LucOnaaAlima ， anddDilianGurov.VerrifyngaStructurdPeer-to-Peer Overlay Network：The Static Case.《全球计算》，第250[5] 乔治·福克斯。消息传递：从并行计算到网格。科学与工程计算问题。IEEE Distributed Systems Online，3（8）：70 -73，2002年9月/10月。[6] Supriya Krishnamurthy，Sameh El-Ansary，Erik Aurell，and Seif Haridi.扰动下弦的统计理论。2005年2月在美国纽约伊萨卡举行的第四届对等系统国际讲习班[7] 李晓舟、贾亚德夫·米斯拉和C.格雷格·普雷斯顿简要通知：环的并发维护。见Soma Chaudhuri和ShayKutten，编辑，PODC，第376页。ACM，2004年。[8] 罗宾·米尔纳通信和移动系统：π演算。剑桥大学出版社，纽约，纽约，美国，1999年。[9] Thomas Noll和Chanchal Kumar Roy。在π演算中对Erlang建模。ErlangPress.[10] Catuscia Palamidessi。比较同步和异步π演算的表达能力。在Symposium on Principles of ProgrammingLanguages，第256-265页[11]国际商会菲利普斯和M.G.维廖蒂环境过程环中的领导选举。在Proceedings of Express：Workshop onExpressiveness in Concurrency，London，August 2004，Volume 128 ofElectronic Notes in TheoreticalComputer Science，pages 185-199. Elsevier，2005年。[12] Lar s-soul A k e Fr e d lund.为解决ErlangCode的问题而进行的新工作。PhDthe s is，RoyalIns t tt eofTechnology，Kista，Sweden，2001年8月。[13] 大卫·桑吉奥吉和大卫·沃克。π演算：移动过程理论。剑桥大学出版社，纽约，纽约，美国，2001年。[14] 放大图片作者：John W.弗兰斯·卡舒克和哈里·巴拉克里希南 Chord：一个面向互联网应用程序的可扩展对等查找服务。2001年计算机通信应用、技术、架构和协议会议论文集，第149-160页。ACM Press，2001.[15] 放大图片作者：J. J.弗兰斯·卡舒克，弗兰克·达贝克，哈里·巴拉克里希南。Chord：一个面向互联网应用程序的可扩展对等查找服务。技术报告，MIT，2002年1月。