SHF: Small: Verified High Performance Data Structure Implementations

21世纪的计算基础设施需要数据处理引擎来接收、存储、分析和提供大量数据，以及快速连续到达的大量请求。为了获得必要的响应性，这些系统同时处理许多请求，并使用复杂的技术来确保并发请求不会相互干扰。这些技术非常容易出错，系统设计或实现中的错误可能导致对查询的错误响应和错误信息的存储。这个项目的目标是开发证明现有系统被正确实现的技术，以及通过构造构建正确的新系统的技术。该项目的新颖之处是用于显示复杂并发程序产生正确结果的原则，以及这些原则在实际高性能存储系统中的应用。该项目的影响是为存储系统提供更可靠的软件，包括云服务、web服务器和数据仓库，使人们和企业能够依赖在线存储数据的系统。该项目建立在并发分离逻辑和机器检查程序验证方面的最新进展之上，这使研究人员能够证明用C等语言编写的并发程序正确地实现了高级规范。特别是，该项目检查了松弛内存操作的影响，它以使程序员的内存行为模型复杂化为代价，提供了更高的性能。这些操作用于编程模式，如乐观并发控制，这是几个最先进的数据库实现的特性。该项目涉及扩展松弛内存推理，以实际规模应用于C程序，并展示单个操作级别的松弛内存推理如何与快照隔离等高级数据库正确性属性相关。这种推理的结果是为针对多核体系结构优化的存储系统提供应用程序级正确性的强大数学保证，并在此过程中开发可用于验证其他高性能并发软件系统的技术。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Computational infrastructures of the 21st-century require data processing engines that receive, store, analyze, and provide massive amounts of data, with large numbers of requests arriving in rapid succession. To achieve the necessary responsiveness, these systems process many requests simultaneously and use sophisticated techniques to ensure that concurrent requests do not interfere with each other. These techniques are highly error-prone, and mistakes in the design or implementation of a system can lead to incorrect responses to queries and the storing of incorrect information. The goal of this project is to develop techniques for proving that existing systems are correctly implemented, and for building new systems that are correct by construction. The project's novelties are the principles used to show that sophisticated concurrent programs produce the correct results, and the application of these principles to real-world high-performance storage systems. The project's impacts are more reliable software for storage systems, including cloud services, web servers, and data warehouses, allowing people and businesses to rely on the systems that store their data online.The project builds on recent advances in concurrent separation logic and machine-checked program verification, which allow researchers to prove that concurrent programs as written in languages like C correctly implement high-level specifications. In particular, the project examines the effects of relaxed-memory operations, which give higher performance at the cost of complicating the programmer's model of memory behavior. These operations are used in programming patterns such as optimistic concurrency control, which feature in several state-of-the-art database implementations. The project involves scaling up relaxed-memory reasoning to apply to C programs at a realistic scale, and showing how relaxed-memory reasoning at the level of individual operations relates to high-level database correctness properties like snapshot isolation. The upshot of such reasoning is to produce strong mathematical guarantees of application-level correctness for storage systems optimized for multicore architectures, and in the process to develop techniques that can be used to verify other high-performance concurrent software systems.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.