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

并行多线程程序比顺序多线程程序更难编写，因为在编写并行程序时，除了程序的算法正确性外，程序员还必须考虑由于线程交错而可能产生的所有行为。人们普遍认为，让大量程序员能够使用多线程编程的唯一方法是提出编程范例和相关工具，这些范例和工具明确地将关于功能正确性的推理与关于由并行性引起的额外行为的推理分开。本项目研究将程序的并行正确性与其功能正确性分离的策略。首先，对于大多数并行程序，希望并行程序中线程调度器引入的不确定性不会改变程序的预期输出。该项目将开发一个断言框架，用于指定并行程序的区域在非确定性线程交错的情况下仍具有确定性行为。第二种策略是基于这样的观察：开发并行程序的一个自然步骤是，当线程交织引入额外的非确定性时，首先用可控数量的非确定性扩展顺序算法，然后进行实际的并行化。本项目将研究非确定性顺序程序作为规范机制的使用，这样对于并行程序的每次执行都存在相应的非确定性顺序程序的等效执行。这种非确定性顺序程序将并行正确性从函数正确性中分离出来。

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.