SHF: Small: Specifying and Verifying Essential Deterministic Behavior of Concurrent Programs

SHF：小：指定和验证并发程序的基本确定性行为

• 批准号: 1018730
• 负责人: Koushik Sen
• 金额: $ 47.54万
• 依托单位: University of California-Berkeley
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2010
• 资助国家: 美国
• 起止时间: 2010-08-01 至 2015-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1018730&HistoricalAwards=false
• 关键词: SHF; Small; Specifying; Verifying; Essential

Parallel multi-threaded programs are more difficult to write than their sequential counterparts because while writing parallel programs programmers must consider all possible behaviors due to thread interleavings, in addition to the algorithmic correctness of the program. A widespread belief is that the only way to make multi-threaded programming accessible to a large number of programmers is to come up with programming paradigms and associated tools that explicitly separate reasoning about functional correctness from reasoning about additional behaviors arising due to parallelism.This project investigates strategies for separating the parallelization correctness aspect of a program from its functional correctness. First, for most parallel programs it is desired that the non-determinism introduced by the thread scheduler in a parallel program does not change the intended output of the program. This project will develop an assertion framework for specifying that regions of a parallel program behave deterministically despite non-deterministic thread interleaving.The second strategy is based on the observation that a natural step in the development of a parallel program is to first extend the sequential algorithm with a controlled amount of non-determinism, followed by the actual parallelization, when additional non-determinism is introduced by thread interleavings. This project will investigate the use of non-deterministic sequential programs as a specification mechanism, such that for each execution of a parallel program there exists an equivalent execution of the corresponding non-deterministic sequential program. Such non-deterministic sequential programs decouple parallelization correctness from functional correctness.

并行多线程程序比其顺序对应程序更难编写，因为在编写并行程序时，程序员还必须考虑由于线程的算法正确性，因此由于线程交织而导致的所有可能行为。 一种普遍的信念是，使许多程序员可以访问多线程编程的唯一方法是提出编程范式和相关工具，这些工具和相关工具明确地将有关功能正确性的推理与对并行性产生的其他行为进行推理的推理分开。该项目调查了该项目的策略，以使其合理的函数性方面的正确性分开其功能性的效果。首先，对于大多数并行程序，希望线程调度程序在并行程序中引入的非确定性不会改变程序的预期输出。 该项目将开发一个断言框架，以指定尽管非确定性线程相互交织，但平行程序的区域仍在决定性地行为。第二个策略是基于观察到的，即并行计划的开发自然步骤是首先扩展顺序算法，而不是进行实际的并行性，而不是进行实际的，而不是进行实际的介绍。该项目将调查非确定性顺序程序作为规范机制的使用，以便对于平行程序的每个执行，都存在相应的非确定顺序程序的等效执行。这样的非确定顺序程序将并联的正确性从功能正确性中解脱出来。