Compositional Reasoning for Pointer Structures

2006 ◽  
pp. 115-139 ◽  
Author(s):  
Yifeng Chen ◽  
J. W. Sanders
Keyword(s):  
Compositional Reasoning

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

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.

Engineering MDA into Compositional Reasoning for Analyzing Middleware-Based Applications

2005 ◽  
pp. 130-145 ◽  
Author(s):  
Mauro Caporuscio ◽  
Davide Di Ruscio ◽  
Paola Inverardi ◽  
Patrizio Pelliccione ◽  
Alfonso Pierantonio
Keyword(s):  
Compositional Reasoning
Sign in / Sign up

Export Citation Format

Share Document