Wright, Daniel, Dalvandi, Sadegh, Batty, Mark, Dongol, Brijesh (2023) Mechanised Operational Reasoning for C11 Programs with Relaxed Dependencies. Formal Aspects of Computing, 35 (2). pp. 1-27. ISSN 1433-299X. (doi:10.1145/3580285) (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided) (KAR id:99629)
The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided. (Contact us about this Publication) | |
Official URL: https://doi.org/10.1145/3580285 |
Abstract
Verification techniques for C11 programs have advanced significantly in recent years with the development of operational semantics and associated logics for increasingly large fragments of C11. However, these semantics and logics have been developed in a restricted setting to avoid the thin-air-read problem. In this paper, we propose an operational semantics that leverages an intra-thread partial order (called semantic dependencies ) induced by a recently developed denotational event-structure-based semantics. We prove that our operational semantics is sound and complete with respect to the denotational semantics. We present an associated logic that generalises a recent Owicki-Gries framework for RC11 RAR (repaired C11) with relaxed and release-acquire accesses. We describe the mechanisation of the logic in the Isabelle/HOL theorem prover, which we use to prove correctness of a number of examples.
Item Type: | Article |
---|---|
DOI/Identification number: | 10.1145/3580285 |
Additional information: | For the purpose of open access, the author has applied a CC BY public copyright licence to any Author Accepted Manuscript version arising from this submission. |
Uncontrolled keywords: | Theoretical Computer Science, Software |
Subjects: |
Q Science > QA Mathematics (inc Computing science) Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, |
Divisions: | Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing |
Funders: |
Engineering and Physical Sciences Research Council (https://ror.org/0439y7842)
Royal Academy of Engineering (https://ror.org/0526snb40) Association for Real Change (https://ror.org/04b8c7j14) |
SWORD Depositor: | JISC Publications Router |
Depositing User: | JISC Publications Router |
Date Deposited: | 03 Feb 2023 14:33 UTC |
Last Modified: | 05 Nov 2024 13:05 UTC |
Resource URI: | https://kar.kent.ac.uk/id/eprint/99629 (The current URI for this page, for reference purposes) |
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):