Publikation: TaDA Live : Compositional Reasoning for Termination of Fine-grained Concurrent Programs
Dateien
Datum
Autor:innen
Herausgeber:innen
ISSN der Zeitschrift
Electronic ISSN
ISBN
Bibliografische Daten
Verlag
Schriftenreihe
Auflagebezeichnung
URI (zitierfähiger Link)
DOI (zitierfähiger Link)
Internationale Patentnummer
Link zur Lizenz
Angaben zur Forschungsförderung
European Union (EU): 683289
Projekt
Open Access-Veröffentlichung
Core Facility der Universität Konstanz
Titel in einer weiteren Sprache
Publikationstyp
Publikationsstatus
Erschienen in
Zusammenfassung
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 that 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.
Zusammenfassung in einer weiteren Sprache
Fachgebiet (DDC)
Schlagwörter
Konferenz
Rezension
Zitieren
ISO 690
D'OSUALDO, Emanuele, Julian SUTHERLAND, Azadeh FARZAN, Philippa GARDNER, 2021. TaDA Live : Compositional Reasoning for Termination of Fine-grained Concurrent Programs. In: ACM Transactions on Programming Languages and Systems. ACM. 2021, 43(4), 16. ISSN 0164-0925. eISSN 1558-4593. Verfügbar unter: doi: 10.1145/3477082BibTex
@article{DOsualdo2021-12-31Compo-71008, year={2021}, doi={10.1145/3477082}, title={TaDA Live : Compositional Reasoning for Termination of Fine-grained Concurrent Programs}, number={4}, volume={43}, issn={0164-0925}, journal={ACM Transactions on Programming Languages and Systems}, author={D'Osualdo, Emanuele and Sutherland, Julian and Farzan, Azadeh and Gardner, Philippa}, note={Article Number: 16} }
RDF
<rdf:RDF xmlns:dcterms="http://purl.org/dc/terms/" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#" xmlns:bibo="http://purl.org/ontology/bibo/" xmlns:dspace="http://digital-repositories.org/ontologies/dspace/0.1.0#" xmlns:foaf="http://xmlns.com/foaf/0.1/" xmlns:void="http://rdfs.org/ns/void#" xmlns:xsd="http://www.w3.org/2001/XMLSchema#" > <rdf:Description rdf:about="https://kops.uni-konstanz.de/server/rdf/resource/123456789/71008"> <dc:contributor>D'Osualdo, Emanuele</dc:contributor> <dcterms:title>TaDA Live : Compositional Reasoning for Termination of Fine-grained Concurrent Programs</dcterms:title> <dc:creator>Farzan, Azadeh</dc:creator> <dc:creator>Gardner, Philippa</dc:creator> <dcterms:issued>2021-12-31</dcterms:issued> <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2024-10-18T07:59:44Z</dcterms:available> <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/71008/4/DOsualdo_2-1v5p5ybhvjv1i3.pdf"/> <dc:rights>terms-of-use</dc:rights> <dc:language>eng</dc:language> <dc:contributor>Gardner, Philippa</dc:contributor> <dc:creator>Sutherland, Julian</dc:creator> <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/> <dc:contributor>Farzan, Azadeh</dc:contributor> <foaf:homepage rdf:resource="http://localhost:8080/"/> <dc:contributor>Sutherland, Julian</dc:contributor> <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2024-10-18T07:59:44Z</dc:date> <dc:creator>D'Osualdo, Emanuele</dc:creator> <dcterms: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 that 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.</dcterms:abstract> <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/> <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/71008/4/DOsualdo_2-1v5p5ybhvjv1i3.pdf"/> <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/71008"/> </rdf:Description> </rdf:RDF>