MPI程序中的错误和解决方法：形式方法和模型检查技术的有效性评估

理论计算机科学电子笔记193（2007）19-27www.elsevier.com/locate/entcsMPI程序Ganesh Gopalakrishnan和Robert M.Kirby科比1，2犹他大学计算机学院美国犹他州盐湖城84112摘要高端计算被普遍认为是科学和技术领导力的战略工具。高端计算的很大一部分是在运行消息传递接口（MPI）库的集群上进行的。MPI已经成为高性能计算（HPC）的事实标准。我们的研究解决了避免MPI程序中的错误的需要，通过从使用正式规范到使用原位模型检查技术的技术组合。 本文详细介绍了这些技术的有效性评估，以及作为我们未来的工作计划。关键词：MPI，分布式程序，消息传递，形式方法，模型检查，形式规范1介绍高端计算（有时称为高性能计算或HPC）的重要性在现代环境中几乎不需要动机。HPC被公认为是科学和技术领导力的战略工具。高端计算的很大一部分是在运行消息传递接口（MPI [1]）库的集群上进行的。在这些应用中，系统模型发生在广泛的现实世界的应用-从化学锅炉到天气模型的任何地方-通过仿真研究。MPI已经成为HPC中事实上的标准。正如一位专家所观察到的[2]，MPI1电子邮件：ganesh@cs.utah.edu2电子邮件：kirby@cs.utah.edu1571-0661 © 2007由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2007.10.00520G. Gopalakrishnan，R.M.Kirby/Electronic Notes in Theoretical Computer Science 193（2007）19• 可移植性：对可移植性的需求很高，因为代码往往比硬件更长寿。• 将原语平滑映射到硬件架构的能力。• 各种各样的调用，允许每个用户找到与他们的需求相匹配的子集。• 它的正交性是指允许的特征组合。就像一般的并行程序一样，MPI程序也可能包含bug。具体而言，MPI程序错误的来源已被确定为包括以下内容。 首先，MPI库中的大量函数可能会让开发人员不堪重负。第二，MPI最常在非正式层面教授或学习。因此，编写高级MPI应用程序的程序员可能会忽略一些极端情况。最后，MPI程序不是静态的;当移植到新的硬件平台时，有时需要手动重新调整。本文是关于我们正在进行的研究，强调使用正规的方法，使创建无错误的MPI程序更容易。我们的方法包括：（i）开发MPI库的形式化模型，（ii）开发现场（运行时）模型检查工具，以及（iii）开发静态分析支持，以提高模型检查的效率。本文简要介绍了我们在这些领域正在进行的工作，以及我们未来的计划。作者希望感谢Gary Lindstrom教授在犹他大学进行的并行计算研究中的影响，并感谢他对本文报告的研究的反馈和鼓励。本文的其余部分组织如下。在第2节中，我们概述了我们正在开发MPI正式规范的工作。在第3节中，我们描述了我们的工作，开发一个原位模型检查MPI。VeriSoft [13]在直接模型检查C/C++程序的上下文中引入了原位模型检查。我们的程序被认为是MPI程序中这个想法的第一个实现。在第4节中，我们对迄今为止的工作进行了评估，并为未来得出结论相关工作：到目前为止，只有另外一个小组--Siegel和Avrunin的小组--积极研究了使用MPI进行高性能计算的形式化方法。他们过去的一些出版物包括[7，8，9]。 这些工程与我们的主要区别如下：(i)在Siegel和AvruninG. Gopalakrishnan，R.M.Kirby/Electronic Notes in Theoretical Computer Science 193（2007）1921- 而不是我们所遵循的原地方法。这两个引擎之间的相似之处在于，这两个引擎都旨在影响并发编程的一个非常重要的领域。2MPI的形式规范即使是有经验的程序员也会误解复杂的库，如MPI，这是有据可查的不幸的是，目前他们必须澄清他们的理解的资源都不令人满意：（i）标准文档中使用的自然语言和半形式化符号的混合可能会被误解，（ii）他们通过在实际平台上进行的“实验”观察到的行为(iii)正式的规范，因为它们是书面的和可获得的，对从业者没有什么直接帮助。随着向多核和其他新颖平台的转移，强调“什么”而不是“如何”的API规范可能会导致更有效的实现。API实现的程序分析、验证和平台测试都可以从正式规范中受益。在我们之前的工作中[16]，我们在TLA+中捕获了大约10%的MPI-1.0原语（主要用于点对点通信）[18]。TLA+在（至少）微软和英特尔的实践工程师中得到了广泛的使用。我们在Microsoft Visual Studio（VS）并行调试器环境中构建了一个C前端，用户可以通过它提交简短（但棘手）的MPI程序，并嵌入断言。嵌入的C语句以及MPI调用被转换为TLA+，通过TLC模型检查器运行[18]。当断言失败时，错误跟踪将变成VS调试器步进命令。这种方法为从业者提供了一种工具，用于基于正式的语义描述来理解MPI，该语义描述可以作为一次性活动由专家进行验证。我们的正式规范保留了与MPI参考文件的交叉引用标签，引用了相关参考文件的行号和页码。 另一个具有类似动机的项目（但不是C前端）是[17]，它形式化了Win32 API的内核线程过程虽然我们之前的工作证明了我们的方法的前景，但我们遗漏了许多细节，包括与数据传输有关的细节我们目前的项目处理MPI-2.0（它有300多个API函数，而MPI-1.0只有128此外，我们的新工作：（i）完善我们先前的工作;(ii)考虑了更多的功能;（iii）提供了丰富的测试集合，有助于验证我们的规范;（iv）模块化规范，允许重用。当前TLA+规范中主要部件的近似尺寸（不包括注释和空白行）如表1所示。 我们忽略弃用的函数。 此外，那些需要22G. Gopalakrishnan，R.M.Kirby/Electronic Notes in Theoretical Computer Science 193（2007）19我们对底层操作系统的形式化描述被省略了。框架和我们的TLA+模型可以从[15]下载。在第4节中，我们描述了我们未来关于MPI形式化工作的计划主模块#primitives（#lines）点对点通信三十五（八百）用户定义的数据库二十七（四百五十）集团和企业管理三十四（六百）集群内集体通信十六（四百五十）拓扑十八（二百五十）MPI 1.1十（一百）过程管理十（二百）单向沟通15（600）（est. ））集体沟通十四（三百）I/O即将到来MPI 2.0中的接口和环境三十五（七百）表1. 规格尺寸3MPI程序的原位模型检测MPI程序中的错误是由许多原因引起的，例如：（i）在将阻塞发送/接收转换为非阻塞发送/接收的手动优化期间，（ii）在使用通配符通信（以及由此产生的非确定性）的上下文中，以及（iii）在使用单边通信的程序中[3]。程序员非常清楚在所有的交错中测试并行程序的必要性。他们也知道这是不可能的，因此证实了对被猜测为足够的交织的测试-模型检查[5]通过对所有可能的交织进行详尽的搜索来帮助调试许多并发系统-尽管是在适当抽象的系统模型上。例如，最近获得ACM著名软件奖的SPIN [6]系统已被用于验证许多真实世界的协议。为了使模型检验在实践中取得成功：（i）设计者必须拥有适度昂贵的技术来创建要验证的协议的模型。(ii)他们必须能够检查并发系统中的一小部分交织，并且能够使用适当的偏序约简算法来声称剩余的交织是等价的，因此不需要检查。我们已经开发了一个名为ISP（原位偏序）的工具，它渴望成长为一个实用的MPI模型检查器。在唯一的其他积极的研究领域，开发一个模型检查器的MPI程序[9]，采取以下方法：（i）他们建模MPI原语直接在Promela（SPING. Gopalakrishnan，R.M.Kirby/Electronic Notes in Theoretical Computer Science 193（2007）1923拉伸SPIN的特性以模拟高级特性，例如非阻塞通信命令。当这些运动依靠SPIN的成功时(i) 它们引起了大量的工作来精确地用Promela或C建模MPI原语;（ii）MPI程序可能由于错误的库函数而有缺陷;（iii）精确地建模嵌入MPI原语的C++（通常）代码是乏味且容易出错的;以及（iv）许多MPI程序是用用户级库的层编写的;理解和精确地建模它们是乏味的前期工作。在ISP中，我们采用基于动态偏序约简（DPOR）的动态（运行时）模型检查方法[13，14]。关于ISP的第一篇[4]通过几个小例子展示了如何让DPOR为MPI工作。它展示了我们如何获得偏序约简的优势，以及如何在建模MPI原语、嵌入C++代码或用户级库时完全避免用户排序-与[ 7，8，9 ]相比，所有优势都是如此本文提供了[4]中缺少的重要测量。它描述了我们的新实现，这是一个总重写我们的旧实现，方便实验。我们的新实现采用MPI的形式语义（在[12]中描述）更忠实地制定偏序约简算法。它实现了更多的MPI原语，包括通配符和许多集合。它提供了可能的改进，因为搜索优化类似于中国邮递员之旅[11]。最后，提出了将静态分析和基于ISP的模型检测相结合的方法3.1为什么动态依赖？部分降阶试图消除由交换动作产生的冗余迹。考虑在两个线程中并发启用的两个C语句a[j++]和a[k--] 如果j！K- 在运行时最清楚的事实（静态分析通常不能准确地确定这样的信息）。DPOR在运行时利用这种依赖信息，从而帮助消除不必要的交织。MPI原语的交换行为（如通配符通信）如何？事实证明，正如我们在[12]中所示，治疗它们需要DPOR方法。这是因为与通配符匹配的潜在通配符也只有在运行时才能最准确地知道。如果该信息没有被准确地确定，比如说通过特设静态分析，则需要保守的方法（24G. Gopalakrishnan，R.M.Kirby/Electronic Notes in Theoretical Computer Science 193（2007）193.2ISP如何工作目前ISP检查死锁和本地断言冲突。对于每个MPI函数（例如MPI发送），ISP提供了一个替换函数（适度的一次性替换）。当被调用时，这些替换函数首先通过TCP 套接字咨询中央调度器（第N+1个进程）。如果调度程序给予许可，则替换函数调用PMPI send（每个MPI实现都提供了PMPI send，并且具有与MPI send相同的功能）。这允许调度程序根据一个任意的交织来推进给定MPI程序的进程，直到所有进程都达到MPI finalize。ISP检查操作的结果跟踪，并在其每个选择点处进行记录，其中可以选择不同的过程基于动态依赖性，这种替代选择被认为是必要的在当前跟踪中的操作之间（详细信息请参见[14]如果在选择点i，J一个不同的进程p被认为是必须运行的，ISP（这是不可能的），使用J它来到选择点i，选择p运行。 我们在[4]中的研究表明，ISP中的DPOR算法可以大大减少交织次数。3.3结果和评估我们运行了三个简单的例子：（i）并行梯形规则计算（Trap），（ii）Pi的蒙特卡罗评估（MC），以及（iii）使用单侧MPI通信的字节范围锁定协议（BR）。这些程序仍然是“小”的，远不及真实世界的MPI程序的大小;然而，为了能够处理真实世界的程序，必须对ISP进行类似于这里所确定的改进。字节范围协议实际上是一个现实的协议[3]。这些代码以及其他详细信息（包括ISP• 对于Trap，立即发现了故意引入的死锁。在校正之后，在总共33次交错上彻底搜索程序，花费8.94秒。其中，重启MPI系统花费了8.44秒！• 对于MC，自动检测到三个死锁（在不经意的检查中并不明显）（详见我们的网站）。在纠正代码后，ISP运行了3，427次交织，耗时15.52分钟，其中15.077分钟用于重启MPI系统。•对于BR，在探索62个交织之后发现了一个死锁。修正后，代码运行超过11，000次交织，运行被杀死3http://www.cs。乌塔湖Ed u/f or mal_v er i fi c a t o n/p p 08-是p/。G. Gopalakrishnan，R.M.Kirby/Electronic Notes in Theoretical Computer Science 193（2007）1925（在我们耗尽BR的执行空间之前，等待对ISP的进一步改进）。3.4对ISP的3.4.1消除重启开销MPI系统的重启时间显然是主要开销。这个代价是要付出的，因为与现有的维护状态哈希表的模型检查器相反，我们不能轻松地维护包括MPI程序状态以及MPI运行时系统的访问状态的哈希表！在诉诸重新执行时，我们实际上是在依赖确定性重放。我们考虑使用现有的MPI检查点系统，但目前已经分配了一个低优先级的路径，而不是以下方向。中文邮递员之旅：在MPI Finalize之前，重新初始化用户级别的状态变量，然后在每个进程中“go to”，然后立即将其初始化为MPI Init的标签，怎么样？由此产生的执行将类似于中国邮递员之旅。初步实验表明，MC的执行时间从15.52分钟减少到63秒，发现相同的死锁。对于陷阱，时间从8.94秒减少到0.347秒。由于MPI程序是“数据独立的”（通常有变量，不在控制流），我们将研究是否（以及如何）静态分析可能有助于避免重新初始化一些用户级变量。此外，我们不重新初始化MPI运行时状态。这实际上可以帮助检测资源泄漏;例如，许多用户草率地编写代码，依赖于MPI finnalize来释放动态创建的通信器。保守状态记录：即使使用DPOR，也可能（由于无状态搜索）在探索的不同轨迹中重复常见的“尾序列”。我们将研究估计（和记录）访问状态的保守方法;与模型检查器不同，在类似于ISP的工具中，完整的状态记录和重新访问检查是昂贵的3.4.2悬停精度屏障插入：用户是否可以插入一对MPI屏障指令，请求ISP仅在其范围内执行交织？这些障碍可以在以后移动到MPI程序的其他部分这可以帮助用户本地化模型检查，遵循他们自己对程序的见解循环剥离：由于大多数MPI程序都有调用MPI操作的循环，因此（通过静态分析）剥离一些迭代并让它们单独被ISP捕获和交织似乎很有吸引力/必要。MPI程序循环的其他迭代仍然必须执行26G. Gopalakrishnan，R.M.Kirby/Electronic Notes in Theoretical Computer Science 193（2007）19这些通信我们对这个想法的初步实现很快告诉我们，这必须相当小心地完成。特别地，在每一步，ISP我们的经验表明，使ISP因此，如果我们要在ISP中实现循环剥离，应该以与ISP当前调度程序兼容的方式完成3.4.3强度折由于MPI程序通常是数据独立的，因此适当的静态分析方法可以消除相当数量的嵌入式C++代码。3.4.4分布式搜索ISP本身遵循高度并行化的算法。替代的brackets- ings可以很好地由一个大集群的其他节点来探索。我们为PThreads [10]（一种没有共同代码的不同线程）实现了ISP算法，这表明通过适当设计的启发式算法，在大型集群上实现线性加速是可能的。关于综合系统项目的进一步计划见第4节。4评估和结论4.1的评估鉴于MPI的重要性，我们认为，它是必要的开发工具，支持形式化的方法在MPI程序的设计和调试。我们的工作解决了为MPI提供正式语义的问题，并建立了一个模型检查器，不需要繁琐和容易出错的建模步骤。关于MPI的形式语义，我们关于形式规范的未来计划是彻底调试它，并完全集成到我们的Microsoft Visual Studio环境中。关于原位模型检测，我们提出了实用的模型检测方法，可以通过智能编排MPI进程之间的交织来检测大型MPI程序中的潜在死锁。这项工作依赖于[14]的动态偏序约简工作的适应，以有效地用于MPI。细节在第3节和[4]中概述G. Gopalakrishnan，R.M.Kirby/Electronic Notes in Theoretical Computer Science 193（2007）19274.2今后工作我们今后的工作将包括两个不同的阶段。首先，我们计划更严格地分析我们的MPI正式规范，并找到可靠反馈的方法我们的ISP计划是开发新的静态和动态分析的组合，获得MPI程序，是从一个类已知的是难以调试，并衡量我们的工具的效率引用[1] 的消息通过接口论坛MPI：一消息传递接口标准。http://www.mpi-forum.org/网站。[2] W. D.格洛普“Learning from the Success of MPI,” In[3] S. Pervez等人，“Formal Verification of Programs that use MPI One-sided Communication,”[4] S. Pervez 等 人 ， “Practical Model Checking Method for Verifying Correctness of MPIPrograms,” EuroPVM/MPI, 2007[5] E.M. Clarke，O.Grumberg和D.Peled，[6] G. J. Holzmann，[7] Stephen F. Siegel和George Avrunin，LNCS卷2989。[8] Stephen F.西格尔“Efficient verification of halting properties for MPI programs with wildcard[9] S.F. Siegel，[10] 、Y.Yang等人，“Distributed[11] http://mathworld.wolfram.com/ChinesePostmanProblem.html[12] 、 R. Palmer 等 人 ， “Semantics Driven Dynamic Partial-Order Reduction of MPI-basedParallel Programs,” PADTAD[13] 、黑果山核桃P.Godefroid，[14] C. Flanagan，P. Godefroid，[15] www.cs.utah.edu/formal验证。[16] 作者：Robert Palmer，Michael Delisi，Ganesh Gopalakrishnan and Robert M. Kirby，“消息传递 库 的 形 式 化 和 分 析 方 法 ” 。 2007 年 7 月 ， 第 12 届 工 业 关 键 系 统 形 式 化 方 法 国 际 研 讨 会（FMICS），德国柏林[17] Win32 Threads API规范http://research.microsoft.com/users/lamport/tla/threads/threads.html[18] research.microsoft.com/users/lamport/tla/tla.html[19] 约翰·雷诺兹。分离逻辑：共享可变数据结构的逻辑。第17届IEEE计算机科学逻辑研讨会（LICS），2002年。