Tackling Real-Life Relaxed Concurrency with FSL++

Marko Doko, Viktor Vafeiadis

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

32 Citations (Scopus)

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.
Original languageEnglish
Title of host publicationProgramming Languages and Systems. ESOP 2017
EditorsHongseok Yang
PublisherSpringer
Pages448-475
Number of pages28
ISBN (Electronic)9783662544341
ISBN (Print)9783662544334
DOIs
Publication statusPublished - 19 Mar 2017

Publication series

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

Fingerprint

Dive into the research topics of 'Tackling Real-Life Relaxed Concurrency with FSL++'. Together they form a unique fingerprint.

Cite this