SHF: Small: Contracts for Message-Passing Parallel Programs

软件在科学和工程中扮演着越来越重要的角色。飞机、摩天大楼和汽车的设计；气候模拟和天气预报；新药物的开发，只是使用计算机程序模拟自然现象的众多努力中的一小部分。然而，研究表明，这些程序中的许多都带有可能导致不正确结果的缺陷（“bug”）。在其他软件领域也是如此，但是科学软件的问题特别严重，原因有几个。最重要的是，许多科学软件都是“传递消息”的并行软件——设计用于在“超级计算机”上执行，而“超级计算机”是由数千个处理器组成的网络。虽然有许多方法可以帮助开发可验证的正确顺序程序，但其中很少有方法可以扩展到并行程序。“契约式设计”方法——通过将程序分解成可以独立指定和验证的部分来工作——就是这样一种方法，并且已经成功地应用于各种领域的顺序程序。西格尔教授的项目是将这种方法扩展到消息传递并行程序，从而开发出更加可靠的科学和工程应用程序。该方法以各种方式概括和扩展了现有的契约规范和验证机制。与顺序的情况一样，使用了过程分解，但是每个过程可以由多个进程执行，这些进程不一定是同步运行的。合同的前置条件和后置条件被解释为“集体断言”。这些表达式可以引用多个进程的状态，并且具有特殊的语义：为了计算这样的表达式，在每个进程经过断言位置时获取其本地状态的快照；从每个进程获得快照后，将它们组合成一个全局状态，在该状态中对表达式进行评估。契约还必须引用消息缓冲区的状态，例如，表示从一个进程到另一个进程没有未接收的消息。符号执行和模型检查技术用于验证过程是否满足其契约。这些想法正在作为精确科学软件工具包（TASS）的扩展来实现，并应用于使用广泛使用的消息传递接口的C语言编写的程序。

Software plays an increasingly important role in science and engineering. The design of aircraft, sky scrapers, and automobiles; climate modeling and weather prediction; and the development of new pharmaceuticals, are just a few of the many endeavors that use computer programs to simulate natural phenomena. Yet studies have shown that many of these programs are ridden with defects ("bugs") that may lead to incorrect results. The same is true in other software domains, but the problems with scientific software are particularly acute for several reasons. Most significantly, much scientific software is "message-passing" parallel software---designed to execute on "supercomputers" which are networks of many thousands of processors. While there are many methods to help develop verifiably correct sequential programs, few of these have been extended to parallel programs. The "Design by Contract" methodology --- which works by decomposing a program into parts that can be specified and verified independently --- is one such approach, and has been successfully applied to sequential programs in a variety of domains. Professor Siegel's project is extending that methodology to apply to message-passing parallel programs, enabling the development of much more reliable scientific and engineering applications.The approach generalizes and extends existing contract specification and verification mechanisms in various ways. As in the sequential case, a procedural decomposition is used, but each procedure can be executed by multiple processes that are not necessarily running in lockstep. The contract pre-conditions and post-conditions are interpreted as "collective assertions". These are expressions that can refer to the state of multiple processes and have a special semantics: to evaluate such an expression a snapshot of the local state of each process is taken as it passes through the assertion location; once a snapshot has been obtained from each process they are composed to form a global state in which the expression is evaluated. Contracts must also refer to the state of the message buffers, for example, to express that there are no unreceived messages from one process to another. Symbolic execution and model checking techniques are used to verify a procedure satisfies its contract. These ideas are being realized as an extension to the Toolkit for Accurate Scientific Software (TASS), and applied to programs written in C with the widely-used Message Passing Interface.