SHF: Small: Separation Principles for Concurrent Programs: Semantics, Logics, and Methodology

SHF：小：并发程序的分离原则：语义、逻辑和方法论

• 批准号: 1017011
• 负责人: Stephen Brookes
• 金额: $ 41.87万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2010
• 资助国家: 美国
• 起止时间: 2010-08-01 至 2016-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1017011&HistoricalAwards=false
• 关键词: SHF; Small; Separation; Principles; Concurrent

Concurrent programs are widely used, in real-world applications with safety-critical requirements, so it is vital to ensure their correctness. Such programs are difficult to get right and hard to analyze, because of the huge number of ways in which concurrent threads may interact dynamically. We need to guarantee that program behavior is free of race conditions, such as concurrent attempts to update the same piece of state, since racy programs may behave erratically. Further, programs that operate on mutable data structures are prone to safety faults, such as attempts to access a previously deallocated pointer, and this is a leading cause of crashes in operating system code.This project addresses these concerns by building a theory of concurrency based on resource separation principles. This theory will offer resource-sensitive logics for program correctness, with solid semantic foundations.The project will significantly expand the scope of the author's work on concurrent separation logic, to encompass a wider range of program properties and concurrency paradigms, and combine concurrency with procedures. The project will introduce semantic models and logics for networks of communicating processes, based on aprinciple of channel separation. The intellectual merits of this proposal include the development of a unifying framework of semantic models and methodologies, with rigorous mathematical and logical underpinnings, embodying practically useful principles. In the broader setting this project aims to improve the state-of-the-art in programming methodology, facilitate the writing of reliable concurrent code, and enable formal reasoning about a wider range of problems. The project will contribute to general understanding, by informing the design of new logics, and the discovery of proof techniques, that cross paradigm barriers. The project will foster the development of improved semantically-based analysis tools for concurrent programs, to be made available for widespread use and experimentation, and to be used for real-world safety-critical applications in which concurrency is both a feature and a problem.

并发程序被广泛应用于具有安全关键需求的实际应用中，因此确保其正确性至关重要。这类程序很难得到正确的结果，也很难分析，因为并发线程可以动态交互的方式有很多。我们需要保证程序行为不受争用条件的影响，例如并发尝试更新相同的状态，因为竞争程序可能行为不规律。此外，在可变数据结构上运行的程序容易出现安全故障，例如试图访问先前释放的指针，这是操作系统代码崩溃的主要原因。该项目通过建立基于资源分离原则的并发理论来解决这些问题。该理论将为程序正确性提供资源敏感的逻辑，具有坚实的语义基础。该项目将极大地扩展作者在并发分离逻辑方面的工作范围，涵盖更广泛的程序性质和并发范例，并将并发与过程相结合。该项目将根据通道分离的原则，为通信过程网络引入语义模型和逻辑。这一提议的学术价值包括建立一个统一的语义模型和方法框架，具有严格的数学和逻辑基础，体现了实际有用的原则。在更广泛的背景下，该项目旨在改进编程方法的最新水平，促进可靠的并发代码的编写，并使更广泛的问题能够进行形式推理。该项目将通过告知新逻辑的设计和跨越范式障碍的证明技术的发现来促进一般理解。该项目将促进用于并发程序的改进的基于语义的分析工具的开发，以供广泛使用和实验，并用于并发既是一个特征又是一个问题的现实世界中的安全关键应用程序。