SHF: Small:Verifying Complex Concurrent Data Structures with Flow Interfaces

当今网络基础设施中最关键的组成部分是协调子计算之间工作的并发数据结构。众所周知，这些软件组件很难正确实现。虽然正式的验证工具可以保证软件的可靠性，但在实际系统中发现的高度复杂的并发数据结构与适用于当今工具的相对简单的数据结构之间仍然存在差距。该项目旨在缩小这一差距。该项目维护一个软件工具和基准的存储库，这些存储库在开放源码许可下是公开可用的。教育目标包括本科生的参与和为这个项目创建的课程材料的传播。这些活动的补充是调查员继续参与高中学生的外展计划。并发分离逻辑有助于简化并发数据结构的形式正确性证明。然而，这种证明中一个反复出现的问题是，在顺序软件中工作得很好的数据结构抽象在并发设置中很难进行推理。该项目采用了一种完全不同的数据结构抽象方法，产生了一种新的分离逻辑语义模型，可以描述实践中发现的复杂并发数据结构。所获得的抽象允许在各种数据结构上推广的证明规则。这就产生了新的证明模块化技术，在这种技术中，抽象的算法模板被一劳永逸地证明是正确的，然后可以细化为具体的数据结构实现，与目前的技术水平相比，大大减少了证明的工作量。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Among the most critical components of today's cyber-infrastructure are concurrent data structures that coordinate work between sub-computations. These software components are notoriously difficult to implement correctly. While formal verification tools can guarantee the reliability of software, there remains a gap between the highly complex concurrent data structures found in real systems and the relatively simple ones amenable to today's tools. This project aims to close this gap. The project maintains a repository of software tools and benchmarks that is publicly available under open source licenses. The educational objectives include involvement of undergraduate students and the dissemination of course materials created for this project. These activities are supplemented by the investigator's continued involvement in outreach programs for high-school students. Concurrent separation logic has helped to simplify formal correctness proofs for concurrent data structures. However, a recurring problem in such proofs is that data structure abstractions that work well for sequential software are much harder to reason about in a concurrent setting. The project takes a radically different approach to data structure abstraction that leads to a new semantic model of separation logic and can describe the complex concurrent data structures found in practice. The obtained abstractions admit proof rules that generalize over a wide variety of data structures. This gives rise to novel proof modularization techniques where abstract algorithm templates are proved correct once and for all and can then be refined to concrete data structure implementations, significantly reducing the proof effort compared to the state of the art.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.