Commit 28bb7f11 authored by Teresa Carbajo-Garcia's avatar Teresa Carbajo-Garcia
Browse files

Update publications.bib

parent 5111132e
......@@ -1853,6 +1853,28 @@ certificate of correctness. We provide a prototype implementation and we report
on some textbook examples.},
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 = {Petar Maksimovic and
Sacha{-}{\'{E}}lie Ayoun and
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