Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

An Abstract Domain for Heap Commutativity (Extended Version)

Jared Pincus, Eric Koskinen

TL;DR

An abstract domain in which commutativity synthesis or verification techniques can safely be performed on abstract mathematical models is introduced and, from those results, one can directly obtain commutativity conditions for concrete heap programs.

Abstract

Commutativity of program code (i.e. the equivalence of two code fragments composed in alternate orders) is of ongoing interest in many settings such as program verification, scalable concurrency, and security analysis. While some have explored static analysis for code commutativity, few have specifically catered to heap-manipulating programs. We introduce an abstract domain in which commutativity synthesis or verification techniques can safely be performed on abstract mathematical models and, from those results, one can directly obtain commutativity conditions for concrete heap programs. This approach offloads challenges of concrete heap reasoning into the simpler abstract space. We show this reasoning supports framing and composition, and conclude with commutativity analysis of programs operating on example heap data structures. Our work has been mechanized in Coq and is available in the supplement.

An Abstract Domain for Heap Commutativity (Extended Version)

TL;DR

An abstract domain in which commutativity synthesis or verification techniques can safely be performed on abstract mathematical models is introduced and, from those results, one can directly obtain commutativity conditions for concrete heap programs.

Abstract

Commutativity of program code (i.e. the equivalence of two code fragments composed in alternate orders) is of ongoing interest in many settings such as program verification, scalable concurrency, and security analysis. While some have explored static analysis for code commutativity, few have specifically catered to heap-manipulating programs. We introduce an abstract domain in which commutativity synthesis or verification techniques can safely be performed on abstract mathematical models and, from those results, one can directly obtain commutativity conditions for concrete heap programs. This approach offloads challenges of concrete heap reasoning into the simpler abstract space. We show this reasoning supports framing and composition, and conclude with commutativity analysis of programs operating on example heap data structures. Our work has been mechanized in Coq and is available in the supplement.

Paper Structure

This paper contains 25 sections, 7 theorems, 29 equations.

Table of Contents

  1. Introduction
  2. Overview
  3. Preliminaries
  4. Heaps and Heap Predicates
  5. Concrete Semantics
  6. An Example Concrete Language
  7. Abstract Domain
  8. Constructing the Domain
  9. Isomorphism of Abstract Domains
  10. Abstract Semantics and Soundness
  11. Sound Commutativity
  12. Defining Commutativity
  13. Sound Commutativity Theorem
  14. Abstract Domain Composition
  15. Concrete Program Capture
  16. ...and 10 more sections

Key Result

theorem 1

If $m \rightsquigarrow_{\sf A} f$, $n \rightsquigarrow_{\sf A} g$, $m \mathrel{\hat{\bowtie}}^{Q}_{\sf A} \space n$, and $\mathsf{A}$ captures $[\mathrm{\Psi},\sim]$, then $f \bowtie^{P^+}_{[\mathrm{\Psi},\sim]} \space g$, where $P(h) \equiv \pi_\mathsf{A}(h) \in X_\mathsf{A} \wedge Q(\pi_\mathsf{A}

Theorems & Definitions (22)

  • definition 1
  • definition 2
  • definition 3
  • definition 4
  • definition 5
  • definition 6
  • definition 7
  • definition 8
  • definition 9
  • definition 10
  • ...and 12 more