SHF: Small: Verified High Performance Data Structure Implementations

点击翻译按钮获取中文摘要

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.