Repository logo
  • Log In
    Log in via Symplectic to deposit your publication(s).
Repository logo
  • Communities & Collections
  • Research Outputs
  • Statistics
  • Log In
    Log in via Symplectic to deposit your publication(s).
  1. Home
  2. Faculty of Engineering
  3. Computing
  4. Computing
  5. TaDA Live: compositional reasoning for termination of fine-grained concurrent programs
 
  • Details
TaDA Live: compositional reasoning for termination of fine-grained concurrent programs
File(s)
3477082.pdf (5.7 MB)
Published version
Author(s)
D'Osualdo, Emanuele
Sutherland, Julian
Farzan, Azadeh
Gardner, Philippa
Type
Journal Article
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.
Date Issued
2021-12-01
Date Acceptance
2021-06-01
Citation
ACM Transactions on Programming Languages and Systems, 2021, 43
URI
http://hdl.handle.net/10044/1/91380
DOI
https://www.dx.doi.org/10.1145/3477082
ISSN
0164-0925
Publisher
Association for Computing Machinery (ACM)
Journal / Book Title
ACM Transactions on Programming Languages and Systems
Volume
43
Copyright Statement
© 2021 Copyright held by the owner/author(s). This work is licensed under a Creative Commons Attribution International 4.0 License (https://creativecommons.org/licenses/by/4.0/)
License URL
https://creativecommons.org/licenses/by/4.0/
Sponsor
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Commission of the European Communities
Engineering & Physical Science Research Council (E
Grant Number
EP/K008528/1 - RG65358
EP/K008528/1
795218
EP/R034567/1
Subjects
Software Engineering
0803 Computer Software
0806 Information Systems
Publication Status
Published
Article Number
ARTN 16
Date Publish Online
2021-11-10
About
Spiral Depositing with Spiral Publishing with Spiral Symplectic
Contact us
Open access team Report an issue
Other Services
Scholarly Communications Library Services
logo

Imperial College London

South Kensington Campus

London SW7 2AZ, UK

tel: +44 (0)20 7589 5111

Accessibility Modern slavery statement Cookie Policy

Built with DSpace-CRIS software - Extension maintained and optimized by 4Science

  • Cookie settings
  • Privacy policy
  • End User Agreement
  • Send Feedback