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

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

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.