@inbook{7c053a7f7e5b4cf5be601125fc755c12,
title = "Tackling Real-Life Relaxed Concurrency with FSL++",
abstract = "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.",
author = "Marko Doko and Viktor Vafeiadis",
year = "2017",
month = mar,
day = "19",
doi = "10.1007/978-3-662-54434-1_17",
language = "English",
isbn = "9783662544334",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "448--475",
editor = "Hongseok Yang",
booktitle = "Programming Languages and Systems. ESOP 2017",
address = "United States",
}