Sciweavers

Share
VMCAI
2016
Springer

A Program Logic for C11 Memory Fences

3 years 7 days ago
A Program Logic for C11 Memory Fences
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.
Marko Doko, Viktor Vafeiadis
Added 11 Apr 2016
Updated 11 Apr 2016
Type Journal
Year 2016
Where VMCAI
Authors Marko Doko, Viktor Vafeiadis
Comments (0)
books