TY - CHAP
T1 - Tackling Real-Life Relaxed Concurrency with FSL++
AU - Doko, Marko
AU - Vafeiadis, Viktor
PY - 2017/3/19
Y1 - 2017/3/19
N2 - We extend fenced separation logic (FSL), a program logic for reasoning about C11 relaxed access and memory fences. Our extensions to FSL allow us to handle concurrent algorithms appearing in practice. New features added to FSL allow for reasoning about concurrent non-atomic reads, atomic updates, ownership transfer via release sequences, and ghost state. As a demonstration of power of the extended FSL, we verify correctness of the atomic reference counter (ARC), a standard library of the Rust programing language, whose implementation relies heavily on advanced features of the C11 memory model. Soundness of FSL and its extensions, as well as the correctness proof of ARC have been established in Coq.
AB - We extend fenced separation logic (FSL), a program logic for reasoning about C11 relaxed access and memory fences. Our extensions to FSL allow us to handle concurrent algorithms appearing in practice. New features added to FSL allow for reasoning about concurrent non-atomic reads, atomic updates, ownership transfer via release sequences, and ghost state. As a demonstration of power of the extended FSL, we verify correctness of the atomic reference counter (ARC), a standard library of the Rust programing language, whose implementation relies heavily on advanced features of the C11 memory model. Soundness of FSL and its extensions, as well as the correctness proof of ARC have been established in Coq.
U2 - 10.1007/978-3-662-54434-1_17
DO - 10.1007/978-3-662-54434-1_17
M3 - Chapter (peer-reviewed)
SN - 9783662544334
T3 - Lecture Notes in Computer Science
SP - 448
EP - 475
BT - Programming Languages and Systems. ESOP 2017
A2 - Yang, Hongseok
PB - Springer
ER -