Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Generating Rely-Guarantee Conditions with the Conditional-Writes Domain

James Tobler, Graeme Smith

TL;DR

This work introduces a structure called the conditional-writes domain, designed for programs where it suffices to establish only the conditions under which particular variables are written to by each thread, and formalises two versions of this approach and evaluates their implementations on a simple programming language.

Abstract

Abstract interpretation has been shown to be a promising technique for the thread-modular verification of concurrent programs. Central to this is the generation of interferences, in the form of rely-guarantee conditions, conforming to a user-chosen structure. In this work, we introduce one such structure called the conditional-writes domain, designed for programs where it suffices to establish only the conditions under which particular variables are written to by each thread. We formalise our analysis within a novel abstract interpretation framework that is highly modular and can be easily extended to capture other structures for rely-guarantee conditions. We formalise two versions of our approach and evaluate their implementations on a simple programming language.

Generating Rely-Guarantee Conditions with the Conditional-Writes Domain

TL;DR

This work introduces a structure called the conditional-writes domain, designed for programs where it suffices to establish only the conditions under which particular variables are written to by each thread, and formalises two versions of this approach and evaluates their implementations on a simple programming language.

Abstract

Abstract interpretation has been shown to be a promising technique for the thread-modular verification of concurrent programs. Central to this is the generation of interferences, in the form of rely-guarantee conditions, conforming to a user-chosen structure. In this work, we introduce one such structure called the conditional-writes domain, designed for programs where it suffices to establish only the conditions under which particular variables are written to by each thread. We formalise our analysis within a novel abstract interpretation framework that is highly modular and can be easily extended to capture other structures for rely-guarantee conditions. We formalise two versions of our approach and evaluate their implementations on a simple programming language.
Paper Structure (24 sections, 3 theorems, 97 equations, 1 figure, 1 table)

This paper contains 24 sections, 3 theorems, 97 equations, 1 figure, 1 table.

Table of Contents

  1. Introduction
  2. Programming Language
  3. Abstract State Domain
  4. Conditional-Writes Domain
  5. Small Example
  6. The stabilise Function
  7. The transitions Function
  8. The close Function
  9. Rely-Guarantee Generation
  10. Evaluation
  11. Related Work
  12. Conclusion
  13. Acknowledgments.
  14. Disclosure of Interests.
  15. Proofs
  16. ...and 9 more sections

Key Result

lemma thmcounterlemma

For any $i\in\mathcal{I}$ and $d\in\mathcal{D}$ we have:

Figures (1)

  • Figure 1: Collective semantics for generating guarantee conditions.

Theorems & Definitions (6)

  • lemma thmcounterlemma
  • proof
  • lemma thmcounterlemma
  • proof
  • lemma thmcounterlemma
  • proof