Verifying C11 programs operationally | Zendy

Simon Doherty | Zendy; Brijesh Dongol | Zendy; Heike Wehrheim | Zendy; John Derrick | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Verifying C11 programs operationally

Author(s) -

Simon Doherty,

Brijesh Dongol,

Heike Wehrheim,

John Derrick

Publication year - 2019

Publication title -

surrey open research repository (university of surrey)

Language(s) - English

Resource type - Conference proceedings

DOI - 10.1145/3293883.3295702

Subject(s) - mutual exclusion , computer science , fragment (logic) , programming language , operational semantics , thread (computing) , observability , semantics (computer science) , axiom , theoretical computer science , separation logic , memory model , invariant (physics) , mathematical proof , shared memory , mathematics , parallel computing , geometry , mathematical physics

This paper develops an operational semantics for a release-acquire fragment of the C11 memory model with relaxed accesses. We show that the semantics is both sound and complete with respect to the axiomatic model of Batty et al. The semantics relies on a per-thread notion of observability, which allows one to reason about a weak memory C11 program in program order. On top of this, we develop a proof calculus for invariant-based reasoning, which we use to verify the release-acquire version of Peterson's mutual exclusion algorithm.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research