分布式算法的理论计算机科学电子笔记及验证方法

理论计算机科学电子笔记162（2006）167-171www.elsevier.com/locate/entcs无事生非？Rachele Fuzzati瑞士洛桑联邦理工学院计算机与通信学院乌韦·内斯特曼德国柏林工业大学摘要在我们对分布式算法的形式化的探索中，特别是解决分布式共识的算法，我们首先发现使用代数过程演算来描述算法是很自然的。然而，为了仅仅描述的目的以及为了证明其正确性（即，其满足所需的属性），过程演算技术还没有（尚未？）是一种理想的工具在这短短在这篇文章中，我们试图找出原因。在这样做的时候，我们试图暗示我们觉得缺少在目前现有的代数过程演算，并建议什么可以或应该添加，以使他们有用的工具，分布式算法的证明。保留字：过程演算，分布式算法，验证1分布式算法术语“分布式系统”通常描述一组进程，每个进程执行一些计算并与其他进程交换消息。系统可以是同步的或异步的，并且它可以经历或不经历其（某些）进程的失败。系统中的进程可能面临一些分布式协调问题，例如，提供一些联合通信服务，并且可以尝试彼此合作以解决它们。由于过程可用性的不确定性，异步、易故障系统中协调问题的解决方案进程协作的期望结果通常表示为需要在每次系统运行中填充的属性集。术语显然，每一个这样的正确性要求w.r.t.非平凡的规范需要令人信服的证明。通常，在DA域中，由每个进程执行的活动的描述要么由一些伪编程语言代码给出，要么由一些伪编程语言代码给出1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.12.082168R. 富扎蒂Nestmann/Electronic Notes in Theoretical Computer Science 162（2006）167使用表示类似自动机的交互机器的数学结构来建模。在后一种情况下，计算步骤是直接从机器模型导出的，而在前一种情况下，它们是通过非正式的伪代码来描述的。规范通常用自然语言表达，或者使用某种形式的逻辑语言表达，但这种同样，许多证明是在一个相当非正式的水平。2使用过程演算！在DA和进程演算（PC）两个领域中，研究人员都在研究相互作用的进程及其性质。在PC中，算法被描述为微型语言的语法术语，这比DA伪代码更精确事实上，PC机配备了正式的操作语义表明，证明他们之上可能是更正式的伪代码为基础的计数器部分。最后，语法PC描述的代数基础通常支持组合推理技术，有助于将巨大的复杂系统分解为可管理的部分。总而言之，我们认为有足够的理由接近DA社区，他们的模型，以及他们的算法与PC技术的力量。所以，让我们试试。为了对第一节中提到的系统进行建模，我们可以简单地使用一个基于异步消息传递的标准PC。为了模拟进程完全互连的事实（它们可以直接在它们之间交换消息），我们可以使用一组依赖于应用程序的通信通道。对流程可能失败的事实进行建模已经变得更加复杂。事实上，PC通常不会考虑进程崩溃或通信失败的可能性，这源于这样一个事实，即在一开始，PC是为了模拟并发而创建然而，在90年代出现了一些建议，其中PC配备了明确的位置信息，通常称为站点。我们可以建立在这些建议和模型DA过程作为网站，我们可以以某种方式使崩溃的需求。3使用过程演算？有什么东西不见了吗实际上，很多事情。为了解释它们，我们将使用一个我们之前工作过的例子[3]，但是我们遇到了问题，特别是当我们意识到我们的PC工具与目标域不该示例涉及[1]中提出的一种算法（我们称之为CT），用于解决异步系统中的分布式共识，其中进程可能会因崩溃而失败该系统由固定数量的进程组成目标是使过程最终就某个值达成一致。分布式共识由协议、有效性和终止的属性来具体化。前两个是安全属性（一起告诉我们，在每次运行中，进程R. 富扎蒂Nestmann/Electronic Notes in Theoretical Computer Science 162（2006）167169运行，不崩溃的进程最终决定）。描述问题简而言之，CT算法由本地运行两个并发线程的进程定义每个进程运行一系列回合（在这些回合中，它可能扮演不同的角色），在这些回合中，它与其他站点上的伙伴交换消息，直到它的并发决策线程（由某些外部事件触发）将本地退出条件设置为true。CT算法以描述系统中单个进程行为的伪代码形式当试图使用PC的货架，以描述这样的算法，我们确定两个问题。第一个问题来自于这样一个事实，即该算法在局部状态信息中相当丰富。而多个状态参数（例如，当前轮数）对于主线程来说是完全本地的，存在（i）一个与决策线程共享的状态变量，以及存在（i i）包含消息缓冲器（在伪代码中是隐式的）的状态变量，所述消息缓冲器与从通信介质接收消息的其它循环线程共享在PC中，状态变量通常被建模为过程常数的参数然而，当状态变量在独立线程间共享时，这在这种情况下，唯一的方法似乎是一个线程（或：一条消息）持有状态，而另一个线程通过通信方式访问它，从而读取和写入该状态成为显式动作。虽然这是可能的，但并不方便，因为它会导致通信步骤的混乱甚至可能是忙等待循环，这会使随后的形式推理变得混乱。第二个问题源于这样一个事实，即与大多数（如果不是全部的话）更有趣的DA一样，CT算法不仅仅建立在简单的低级消息传递上，而是插入到多个组件的分层架构中，每个组件提供（并需要）特定的通信服务。更准确地说，CT算法需要三个底层服务的存在和正确运行：准可靠点对点通信（QP2P），2. 故障检测（FD），以及3. 可靠广播（RBC）这些服务所保证的属性是全局性的，并且要求对称性（在系统的所有站点上存在本地对等组件）。例如，FD服务需要满足全局属性：“在某个时间t之后，有一个进程不再被任何其他进程怀疑。” Forconvenience, the services underlying the CT algorithm are represented as so-called“abstractions”, which are globally defined and not as- sociatedto single sites, andwhich are simply invoked through primitive operations of the API supplied by the到目前为止，PC机或台式机不支持任何分层结构。相反，它们通常提供一个硬编码的底层服务（通常是同步或异步握手消息传递），该服务被认为足够强大，可以模拟（本地或全局）任何可能需要的服务。然而，如果我们不想只是一个模拟，我们必须扩展PC与额外的硬编码通信机制，从而使理论复杂化。170R. 富扎蒂Nestmann/Electronic Notes in Theoretical Computer Science 162（2006）167在CT算法的情况下，我们可以使用内置的（硬编码的）异步消息传递来合理地接近QP2P建模。对于FD和RBC，没有任何现有的支持。我们务实地决定采用混合方法：我们设计了FD的硬编码表示（参见[2]），同时我们通过Consensus术语中的消息传递实现（参见[1]）模拟RBC服务。我们认为这种解决办法是不合理的临时性的.理想情况下，我们应该能够通过从某个“存储库”中选择所需的硬编码通信服务来方便地组装PC核查问题在我们进入更多细节之前，让我们（有点谨慎地）陈述以下观察结果。Consensus属性是基于运行的;我们不能使用进程等价。Consensus属性是全局的，唯一的组合性是跨底层服务的接口，而不是术语本身;我们无法使用组合推理，至少在对称术语组件中无法使用。CT算法是基于圆形的。系统是异步的，每个进程在进行时独立地递增其轮计数器。这意味着在一次运行中，许多轮可以同时被CT算法的主要正确性参数大量利用推理（例如，通过归纳），指的是整数。然而，在异步系统中运行和轮数之间的关系是微妙的。例如，让我们看一下关于整数的归纳法。通常，这样的归纳从某个属性X成立的最小轮开始。在一个给定的运行中，为了找到这个起始点，可以从初始状态开始搜索X在某轮中保持的第一个状态。然而，这个过程是不正确的：由于系统的异步特性，可能在运行的稍后状态X代表一个小一点的圆！ 因此，当感应进行到较高的温度时，在一轮中，它可能会沿着给定的运行时间倒退。因此，时间的概念以及运行中的迭代的概念与异步轮的概念并不完全兼容。[1]中隐含的解决方案是将运行视为一个整体，忽略事件何时发生，只注意它们发生了。换句话说，我们应该选择一个给定运行的高度高级状态（例如，有限运行中的最后一个），然后找到一种适当的抽象方法来推理它的过去，它的历史。为此，我们不能简单地使用包含在过程项的语法中的信息，因为过去的事件不会留下任何痕迹，但同时我们也不想跟踪运行的所有单个事件，并在每次简单地寻找关于过去特定回合可能发生的事情的信息时搜索所有先前的步骤。因此，我们需要为操作语义配备一些全局簿记数据结构，以记录所有通信事件。为了在证明中有用，这种数据结构应该以某种方便的结构化方式进行簿记。目前我们只知道这取决于应用程序。. .R. 富扎蒂Nestmann/Electronic Notes in Theoretical Computer Science 162（2006）1671714总结PC还不够好。. .对于DA，我们需要（1）能够更好地处理站点内共享状态信息的PC;（2）用于DA中使用的典型全球提供的通信服务的工具箱;（3）这些服务的安全组合(4)从通信历史中提取证据相关结构的方法由于我们没有这些项目，我们目前不使用PC，但应用程序特定的重写系统，这是一个遗憾。Isn’t引用[1] Tushar Deepak Chandra和Sam Toueg 可靠分布式系统的不可靠故障检测器。Journal of the ACM，43（2）：225[2] 乌维·内斯特曼和蕾切尔·富扎蒂基于操作语义的不可靠故障检测器。在Vijay A. Saraswat，编辑，Proceedingsof ASIAN 2003，Volume 2896 ofLNCS，pages 54-71. Springer，2003年12月。[3] 乌维·内斯特曼，雷切尔·富扎蒂，马西莫·梅罗。在流程演算中建立共识模型。载于Roberto Amadio和DenisLugiez，编辑，2003年CONCUR会议记录，LNCS第2761卷，第399-414页。Springer，2003年8月。