Commit 5111132e authored by Teresa Carbajo-Garcia's avatar Teresa Carbajo-Garcia
Browse files

Update publications.bib

parent 41340450
......@@ -1825,26 +1825,6 @@ correctness of several essential properties of the module, and discovering two s
previously unknown bugs.},
author = {Emanuele D'Osualdo and
Azadeh Farzan and
Philippa Gardner and
Julian Sutherland},
title = {TaDA Live: Compositional Reasoning for Termination of Fine-grained
Concurrent Programs},
journal = {ACM Transactions on Programming Languages and Systems (TOPLAS), submitted Jan 2020; accepted 2021.},
year = {2021},
abstract = {We present TaDA Live, a concurrent separation logic for reasoning compositionally about the termination of
blocking fine-grained concurrent programs. The crucial challenge is how to deal with abstract atomic blocking:
that is, abstract atomic operations that have blocking behaviour arising from busy-waiting patterns as found in,
for example, fine-grained spin locks. Our fundamental innovation is with the design of abstract specifications
that capture this blocking behaviour as liveness assumptions on the environment. We design a logic that
can reason about the termination of clients which use such operations without breaking their abstraction
boundaries, and the correctness of the implementations of the operations with respect to their abstract
specifications. We introduce a novel semantic model using layered subjective obligations to express liveness
invariants, and a proof system that is sound with respect to the model. The subtlety of our specifications and
reasoning is illustrated using several case studies.},
author = {Emanuele D'Osualdo and
Felix Stutz},
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment