Dyck, Florian
(2024)
Interval Reasoning for C11 RAR.
Masters, Carl von Ossietzky Universität Oldenburg.
Abstract
Owicki-Gries reasoning extends Hoare logic to concurrent programs under the assumption of sequential consistency. In this thesis, we develop a proof calculus using interval reasoning for C11 RAR, a fragment of C11 with relaxed and release-acquire memory operations. Our proof calculus allows all Owicki-Gries proof rules not specific to memory operations to remain unchanged. We use an existing model for the C11 RAR semantics and adapt the assertion language Piccolo to reason on its states. For each thread we overapproximate in which order its thread views might occur in sets of lists, on which we define interval assertions. This way we need only a small number of model-specific assertions, which can be combined to create more complex assertions. We formally prove the soundness of our proof rules and show their utility by verifying a number of C11 litmus tests, and a C11 version of Peterson’s algorithm.
Actions (login required)
 |
View Item |
