CISE-ANR: SHF: Small: Scenario-based Formal Proofs for Concurrent Software

现代软件越来越多地采用并发编程，以利用多核架构提供的性能优势。不幸的是，并发编程是出了名的困难，即使在最有经验的程序员编写的代码中也存在并发错误。因此，研究人员开发了数学推理技术，试图证明这些程序是正确的，但现有的技术依赖于用户提供复杂的不变量，往往不是很直观。相比之下，来自分布式计算社区的算法设计者经常通过专注于描述线程如何交错的几个关键示例场景，为其实现的正确性提供更容易理解的论据。这个项目将弥合这一差距，从直观的论据，正式严格的证明提升基于ESTA推理。该项目的新颖之处是用于验证并发软件的新基础、算法和自动化工具，这些软件展示了基于Java的推理如何成为正式的，但也可以为日常程序员所接受。该项目的影响是（1）理论，算法和自动化验证工具，可供程序员使用，而不需要正式方法的背景，（2）证明适用于现实世界的并发程序，如Web或数据库服务器，（3）出版物和公开开源发布这些验证工具，以及（4）通过新颖的课程材料和代表性不足的群体的参与对教育产生更广泛的影响。总的来说，该项目将使验证更容易获得，并通过我们在学术界和工业界的推广，导致采用并最终更安全的并发软件。从技术上讲，该项目将场景形式化为程序的执行商，它捕获了一小部分代表性的交叉执行，但通过交换性推广到所有执行的集合，即使有无限多的线程和无限的状态空间。该项目旨在证明这些商可以用一种方便的语言简洁地描述;商可靠性的证明（即，抽象涵盖了所有的执行）可以通过与交换性相互作用的新形式的归纳系统化;可以直接从源代码自动派生;程序员可以使用这些派生并查询它们，以更好地理解其实现的并发行为。该奖项反映了NSF的法定使命，并被认为值得通过使用基金会的知识价值和更广泛的影响审查标准。

Modern software increasingly employs concurrent programming in order to exploit the performance benefits offered by multicore architectures. Unfortunately, concurrent programming is notoriously difficult and concurrency bugs exist even in code written by the most seasoned programmers. Consequently, researchers have developed mathematical reasoning techniques in attempt to prove these programs correct but existing techniques rely on the user to provide complex invariants that are often not very intuitive. By contrast, algorithm designers from the distributed computing community frequently provide more understandable arguments for the correctness of their implementations, by focusing on describing a few key example scenarios of how threads may be interleaved. This project will bridge this gap by elevating scenario-based reasoning from intuitive arguments to formally rigorous proofs. The project’s novelties are new foundations, algorithms and automated tools for verifying concurrent software that demonstrate how scenario-based reasoning can be formal, yet also approachable to everyday programmers. The project’s impacts are (1) theories, algorithms and automated verification tools for concurrent software that can be used by programmers, without the need for a background in formal methods, (2) demonstrated applicability to real-world concurrent programs such as web or databases servers, (3) publications and public open-source release of these verification tools, and (4) broader impacts on education through novel course materials and participation of under-represented groups. Overall, the project will make verification more accessible and, through our advocation in academia and in industry, lead to adoption and ultimately safer concurrent software.Technically the project formalizes scenarios as a program's execution quotient, which captures a small set of representative interleaved executions that nonetheless generalize---via commutativity---to the set of all executions, even with unboundedly many threads and infinite state spaces. The project aims to demonstrate that these quotients can be described succinctly in a convenient language; that the proof of quotient soundness (i.e., that the abstraction covers all executions) can be systematized through new forms of induction that interact with commutativity; that it is possible to automatically derive quotients directly from source code; and that programmers can use these derivations and query them to better understand the concurrent behavior of their implementations.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.