SHF: Small: Contracts for Message-Passing Parallel Programs

SHF：小型：消息传递并行程序的合约

• 批准号: 1319571
• 负责人: Stephen Siegel
• 金额: $ 45万
• 依托单位: University of Delaware
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2013
• 资助国家: 美国
• 起止时间: 2013-09-01 至 2018-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1319571&HistoricalAwards=false
• 关键词: SHF; Small; Contracts; Message; Passing

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.

软件在科学和工程中起越来越重要的作用。飞机，天空刮刀和汽车的设计；气候建模和天气预测；而新药的开发只是使用计算机程序模拟自然现象的众多努力中的一些。然而，研究表明，其中许多程序都被缺陷（“ bug”）释放，这可能会导致结果不正确。在其他软件领域也是如此，但是科学软件的问题尤其严重，原因有几个。最重要的是，许多科学软件是“通话”并行软件 - 旨在在“超级计算机”上执行，这些软件是数千个处理器的网络。虽然有许多方法可以帮助确定正确正确的顺序程序，但其中很少有扩展到并行程序。 “通过合同设计”方法 - - 通过将程序分解为可以独立指定和验证的零件，就是一种方法，已成功应用于各种域中的顺序程序。 Siegel教授的项目正在扩展该方法，以适用于通行的并行计划，从而可以开发更可靠的科学和工程应用程序。该方法以各种方式概括并扩展了现有的合同规范和验证机制。与顺序的情况一样，使用过程分解，但是每个过程都可以通过不一定锁定的多个过程执行。合同前条件和条件后的条件被解释为“集体主张”。这些表达式可以指代多个过程的状态并具有特殊的语义：为了评估这样的表达式，每种过程的局部状态的快照是通过断言位置的；一旦从每个过程中获得快照后，它们就会形成评估表达式的全局状态。合同还必须参考消息缓冲区的状态，例如，以表达从一个过程到另一个过程的未收到的消息。符号执行和模型检查技术用于验证程序满足其合同。这些想法已被实现为用于准确的科学软件（TAS）的工具包的扩展，并应用于C中编写的和广泛使用的消息传递界面的程序。