A Program Logic for C11 Memory Fences

Marko Doko, Viktor Vafeiadis

Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)peer-review

35 Citations (Scopus)

Abstract

We describe a simple, but powerful, program logic for reasoning about C11 relaxed accesses used in conjunction with release and acquire memory fences. Our logic, called fenced separation logic (FSL), extends relaxed separation logic with special modalities for describing state that has to be protected by memory fences. Like its precursor, FSL allows ownership transfer over synchronizations and can be used to verify the message-passing idiom and other similar programs. The soundness of FSL has been established in Coq.
Original languageEnglish
Title of host publicationVerification, Model Checking, and Abstract Interpretation. VMCAI 2016
EditorsBarbara Jobstmann, K. Rustan M. Leino
PublisherSpringer
Pages413-430
Number of pages18
ISBN (Electronic)9783662491225
ISBN (Print)9783662491218
DOIs
Publication statusPublished - 2016

Publication series

NameLecture Notes in Computer Science
Volume9583
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Dive into the research topics of 'A Program Logic for C11 Memory Fences'. Together they form a unique fingerprint.

Cite this