Alone together: compositional reasoning and inference for weak isolation

Gowtham Kaki; Kartik Nagar; Mahsa Najafzadeh; Suresh Jagannathan

doi:10.1145/3158115

Alone together: compositional reasoning and inference for weak isolation

Proceedings of the ACM on Programming Languages ◽

10.1145/3158115 ◽

2018 ◽

Vol 2 (POPL) ◽

pp. 1-34 ◽

Cited By ~ 10

Author(s):

Gowtham Kaki ◽

Kartik Nagar ◽

Mahsa Najafzadeh ◽

Suresh Jagannathan

Keyword(s):

Compositional Reasoning

Download Full-text

Foundations for Circular Compositional Reasoning

Automata, Languages and Programming - Lecture Notes in Computer Science ◽

10.1007/3-540-48224-5_68 ◽

2001 ◽

pp. 835-847 ◽

Cited By ~ 10

Author(s):

Mahesh Viswanathan ◽

Ramesh Viswanathan

Keyword(s):

Compositional Reasoning

Download Full-text

Functional Verification of Power Gated Designs by Compositional Reasoning

Computer Aided Verification - Lecture Notes in Computer Science ◽

10.1007/978-3-540-70545-1_42 ◽

2008 ◽

pp. 433-445 ◽

Cited By ~ 2

Author(s):

Cindy Eisner ◽

Amir Nahir ◽

Karen Yorav

Keyword(s):

Functional Verification ◽

Compositional Reasoning

Download Full-text

SIMPAL: A Compositional Reasoning Framework for Imperative Programs

10.31274/etd-180810-5893 ◽

2017 ◽

Author(s):

Lucas G. Wagner

Keyword(s):

Compositional Reasoning

Download Full-text

Probabilistic contracts: a compositional reasoning methodology for the design of systems with stochastic and/or non-deterministic aspects

Formal Methods in System Design ◽

10.1007/s10703-010-0107-8 ◽

2010 ◽

Vol 38 (1) ◽

pp. 1-32 ◽

Cited By ~ 10

Author(s):

Benoît Delahaye ◽

Benoît Caillaud ◽

Axel Legay

Keyword(s):

Compositional Reasoning

Download Full-text

Trace-based compositional reasoning about fault tolerant systems

Lecture Notes in Computer Science - PARLE '93 Parallel Architectures and Languages Europe ◽

10.1007/3-540-56891-3_16 ◽

1993 ◽

pp. 197-208 ◽

Cited By ~ 9

Author(s):

Henk Schepers ◽

Jozef Hooman

Keyword(s):

Fault Tolerant ◽

Compositional Reasoning ◽

Fault Tolerant Systems

Download Full-text

Taming Message-Passing Communication in Compositional Reasoning About Confidentiality

Programming Languages and Systems - Lecture Notes in Computer Science ◽

10.1007/978-3-319-71237-6_3 ◽

2017 ◽

pp. 45-66 ◽

Cited By ~ 5

Author(s):

Ximeng Li ◽

Heiko Mantel ◽

Markus Tasch

Keyword(s):

Message Passing ◽

Compositional Reasoning

Download Full-text

TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs

ACM Transactions on Programming Languages and Systems ◽

10.1145/3477082 ◽

2021 ◽

Vol 43 (4) ◽

pp. 1-134

Author(s):

Emanuele D’Osualdo ◽

Julian Sutherland ◽

Azadeh Farzan ◽

Philippa Gardner

Keyword(s):

Case Studies ◽

Separation Logic ◽

Proof System ◽

Concurrent Programs ◽

Semantic Model ◽

Compositional Reasoning ◽

Fine Grained ◽

Fundamental Innovation ◽

Concurrent Separation Logic

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.

Download Full-text