TY - GEN
T1 - Compositional Verification of Concurrent C Programs with Search Structure Templates
AU - Nguyen, Duc Than
AU - Beringer, Lennart
AU - Mansky, William
AU - Wang, Shengyi
N1 - Publisher Copyright:
© 2024 ACM.
PY - 2024/1/9
Y1 - 2024/1/9
N2 - 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.
AB - 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.
KW - concurrent separation logic
KW - fine-grained locking
KW - interactive theorem proving
KW - Iris
KW - logical atomicity
KW - Verified Software Toolchain
UR - http://www.scopus.com/inward/record.url?scp=85182948063&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85182948063&partnerID=8YFLogxK
U2 - 10.1145/3636501.3636940
DO - 10.1145/3636501.3636940
M3 - Conference contribution
AN - SCOPUS:85182948063
T3 - CPP 2024 - Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with: POPL 2024
SP - 60
EP - 74
BT - CPP 2024 - Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with
A2 - Timany, Amin
A2 - Traytel, Dmitriy
A2 - Pientka, Brigitte
A2 - Blazy, Sandrine
PB - Association for Computing Machinery, Inc
T2 - 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, in affiliation with the annual Symposium on Principles of Programming, Languages, ,POPL 2024
Y2 - 15 January 2024 through 16 January 2024
ER -