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.