References & Citations
Computer Science > Programming Languages
Title: A Concurrent Program Logic with a Future and History
(Submitted on 5 Jul 2022 (v1), last revised 11 Nov 2022 (this version, v2))
Abstract: Verifying fine-grained optimistic concurrent programs remains an open problem. Modern program logics provide abstraction mechanisms and compositional reasoning principles to deal with the inherent complexity. However, their use is mostly confined to pencil-and-paper or mechanized proofs. We devise a new separation logic geared towards the lacking automation. While local reasoning is known to be crucial for automation, we are the first to show how to retain this locality for (i) reasoning about inductive properties without the need for ghost code, and (ii) reasoning about computation histories in hindsight. We implemented our new logic in a tool and used it to automatically verify challenging concurrent search structures that require inductive properties and hindsight reasoning, such as the Harris set.
Submission history
From: Sebastian Wolff [view email][v1] Tue, 5 Jul 2022 23:17:35 GMT (144kb)
[v2] Fri, 11 Nov 2022 16:56:24 GMT (149kb,D)
Link back to: arXiv, form interface, contact.