Compositional verification of concurrent C programs with search structure templates

DT Nguyen, L Beringer, W Mansky… - Proceedings of the 13th …, 2024 - dl.acm.org
Proceedings of the 13th ACM SIGPLAN International Conference on Certified …, 2024dl.acm.org
Concurrent search structure templates are a technique for separating the verification of a
concurrent data structure into concurrency-control and data-structure components, which
can then be modularly combined with no additional proof effort. In this paper, we implement
the template approach in the Verified Software Toolchain (VST), and use it to prove
correctness of C implementations of fine-grained concurrent data structures. This involves
translating code, specifications, and proofs to the idiom of C and VST, and gives us another …
Concurrent search structure templates are a technique for separating the verification of a concurrent data structure into concurrency-control and data-structure components, which can then be modularly combined with no additional proof effort. In this paper, we implement the template approach in the Verified Software Toolchain (VST), and use it to prove correctness of C implementations of fine-grained concurrent data structures. This involves translating code, specifications, and proofs to the idiom of C and VST, and gives us another look at the requirements and limitations of the template approach. We encounter several questions about the boundaries between template and data structure, as well as some common data structure operations that cannot naturally be decomposed into templates. Nonetheless, the approach appears promising for modular verification of real-world concurrent data structures.
ACM Digital Library
以上显示的是最相近的搜索结果。 查看全部搜索结果