Commutativity describes circumstances in which two programs executed in sequence yield the same result regardless of their execution order. Fundamentally, commutativity o!ers a kind of independence that enables parallelization or simplifies program analysis by collapsing equivalent cases. As such, this property has long been of interest in many areas including databases [35], parallelizing compilers [32], scalable [8] and distributed systems [33], and smart contracts [12,29]. Commutativity is also used in verification, including e!orts to simplify proofs of parameterized programs [20], and concurrent program properties [19] such as termination [26], dynamic race detection [21], and information flow [13].
E!orts in commutativity analysis seek to infer or verify commutativity conditions-the initial conditions (if any) under which code fragments commute. For example, Rinard and Kim [23] verify commutativity conditions by relating a data structure to its pre/post-conditions, then showing commutativity of that abstraction. Later, methods were developed to automatically synthesize commutativity conditions for specifications and for imperative program fragments [2,3,7,6], which can be used to automatically parallelize programs [32,30,6].
Objectives. Considering its many applications, it would be appealing to extend commutativity analysis to the heap memory model. However, few works thus far have targeted heap-modifying programs. Pîrlea et al. [29] describe a commutativity analysis with some heap treatment, but with the limited scope of heap disjointness/ownership. Eilers et al. [14] employ, but do not verify, commutativity to reason about information flow security in concurrent separation logic. This paper thus aims to analyze commutativity of heap programs.
Challenges & Contributions. Commutativity reasoning can be challenging for heap-manipulating programs, but is more straightforward for functions over simple mathematical objects. With that in mind, this paper presents an abstract domain which is amenable to existing commutativity condition verification and synthesis techniques [2,3,7], and allows conditions found in said abstract space to immediately yield concrete separation-logic-style conditions for heap programs. For instance, given a simple mathematical list representation of a stack data structure, we can easily find that the functions push and pop operating on these lists commute when the first (i.e. top) list element equals the value being pushed. We may then thread down and apply this condition to concrete push and pop methods. For this threading to be sound, we design the domain to handle various complications of heap programs, including observational equivalence of heap data structures, nondeterminism of address allocation, and improperly allocated heaps and resultant program failure.
In summary, the contributions of this paper include: (Sec. 4) We introduce a simple abstract domain that is amenable to abstract commutativity reasoning, which can soundly entail concrete commutativity. The domain is designed to lift heap-allocated structures to mathematical objects (e.g. value lists to encode a stack) via separation-logic-style predicates, while cleanly handling ambiguous or improperly allocated heaps. We then describe the semantics of abstract programs, and establish a soundness relationship between abstract and concrete programs in the style of abstract interpretation [10], which enables the reduction of concrete to abstract commutativity.
(Sec. 5) We define concrete and abstract commutativity, and present our main soundness theorem: that a valid commutativity condition for two concrete programs may be derived immediately from commutativity reasoning performed (much more easily) on their corresponding abstract programs. These derived concrete conditions are also framed, i.e. if the programs commute under a given initial heap layout, they also commute in any larger layout.
(Sec. 6) We define a way to compose abstractions, which mirrors the separating conjunction on concrete heaps, and present compositional commutativity properties. Composition aids in settings with multiple allocated data structures, and working with arguments/return values.
(Sec. 7) We share four complete examples: a non-negative counter, two-place unordered set, linked-list stack, and the composition of a counter and stack.
(Supplement) Our work is implemented in Coq, on top of Separation Logic Foundations [5]. All theorems, lemmas and properties have been proved in Coq (except for the example programs written in the concrete semantics of §3.3).
Limitations. In this paper we establish the theory necessary for deriving heap commutativity from abstract commutativity reasoning. We leave implementation of this theory, including automation and synthesis, future work.
We summarize our work through the example of a stack, implemented as a heap-allocated linked list, with typical push and pop methods (pop fails if the stack is empty). For simplicity, method arguments or return values are stored in method-specific pre-allocated heap cells (e.g. a).
Inconvenience of concrete heap commutativity. We would like to know if push and pop always commute or, otherwise, whether there is a pre-condition P under which they commute. Verifying whether assume(P );push;pop is equivalent to assume(P );pop;push is not amenable to typical relational reasoning techniques [36], because the swapped orders of push and pop (or, in general, f and g) do not yield meaningful alignment points [27,1]. So, the problem amounts to performing four forward symbolic executions per method pair, meaning quadratically many executions as the number of methods grows. There are, however, efficient CEGAR/CEGIS methods for verifying and even synthesizing a condition P of logical method pre/postconditions [2,3,7]. We now discuss a simple abstraction of the Stack methods as mathematical functions, how our theory relates the concrete heap to this abstraction, and how this enables concrete commutativity conditions to be immediately derived from the results of simpler (automatable) abstract commutativity reasoning.
Abstract commutativity. Let us, for the moment, set aside the concrete heap implementation, and consider a simple mathematical representation of a stack as a list of values, along with functions over the stack with an input/output "cell":
Here, push appends the input value to the stack, and pop removes and returns the topmost value, but fails (yields →) on an empty stack. Reasoning about commutativity of these mathematical objects is convenient, and synthesizing commutativity conditions can now be automated [2,3,7]. For this example, given an initial stack s, push(u) and push(v) commute when u = v; push(u) and pop() when s = u :: _; and pop() and pop() when s = x :: x :: _ for some x.
The question we ask in this paper, is how we might abstract the concrete programs so that, from these abstract commutativity conditions, we can immediately obtain concrete conditions. We show that this is indeed possible; for example, in the case of push a ω and push b ω we obtain the (separation logic) precondition: ↑u. stk + (_) ↓ a ↔ ↗ u ↓ b ↔ ↗ u, where stk + (_) asserts that the heap contains a properly allocated stack. We now summarize how to achieve this using the Stack example.
Step 1: Projecting heaps to abstract Stacks. To soundly lift concrete heap structures into an abstract domain, we must accommodate various complications of the heap, such as improperly allocated heaps, observationally equivalent layouts, and allocation nondeterminism. We achieve this by choosing a set of abstract values X (such as value lists to represent stacks), and a projection function ω which maps concrete heaps into X. Whether a heap is "well-structured" depends on the choice of ω. For the Stack, ω encodes that the only valid heaps for the abstraction are those containing a correctly allocated linked stack. We say that such heaps are within the purview of the abstraction at hand, meaning they will be amenable to abstract commutativity reasoning.
Of course, ω must also account for heaps which are not properly allocated to be representable by a value in X. To this end, every abstract domain includes a special element ✁ ("cross"), to which ω maps all inappropriately structured, or "out-of-purview", heaps. Commutativity w.r.t. such heaps cannot be reasoned about meaningfully in the abstract space.
For our Stack example, the abstract values X are lists of non-null concrete values, and the projection function ω maps a heap to such a list by checking (via separation logic heap predicates [28]) whether it contains a valid linked list, and extracting the contents of said list. Precisely:
By existentially quantifying the intermediate addresses of the linked stack and omitting them from the extracted abstract value, we render stacks observationally equivalent if and only if their contained values match.
Step 2: Abstract domain for commutativity. The next question is how this projection should induce an abstract domain, while soundly respecting concrete programs, and enabling commutativity reasoning. The key is to "wrap" the abstract values X into a domain that also includes elements which track if abstract commutativity still entails concrete commutativity. Namely, we add the abstract value ✁ for out-of-purview heaps, ✂ ("check") for an ambiguous collection of in-purview heaps, → as a failure state, and ⇐ for a collection of heaps both in-and out-of-purview. Instrumenting ω appropriately induces a Galois connection [11] between this abstract domain and the concrete heap domain.
For abstract commutativity to soundly entail concrete commutativity, we establish a soundness relation between concrete and abstract programs, in the style of abstraction interpretation [10]. It demands that push a ω overapproximate push, and that push a ω fail when push fails on an in-purview heap.
In the remainder of this paper we formalize the above discussion, share properties of commutativity, and define composition on abstract domains. Then in §7 we elaborate on the Stack example (adding a peek operation) along with other examples. All definitions, lemmas, theorems, and examples have been mechanized in Coq (available in the supplement), except for those concerning the example concrete semantics in §3.3.
Here we outline conventions and notations for heaps and heap predicates, as well as our choice of concrete heap semantics.
A heap is a finite partial map from addresses (L) to concrete values (V). Denote the set of all heaps with H, the set of non-null values as V ↑ = V \ {null}, and the finite address domain of heap h with dom(h).
Concrete values may be any typical datatypes (integers, booleans, pairs, etc.) which are generally fixed in size (e.g. an unbounded list would not typically be stored as one concrete value). Addresses themselves can be treated as concrete values. Assume unlimited addresses are available, namely ⇒h. dom(h) ⊋ L.
Heaps h 1 and h 2 are disjoint (h 1 → h 2 ) i! dom(h 1 ) → dom(h 2 ). The union of disjoint heaps (h 1 + h 2 ) yields the combined partial map of h 1 and h 2 . Dually, a heap may be partitioned into smaller disjoint heaps.
Heap equality is defined extensionally.
A heap predicate characterizes the addresses and values of heaps. Given heap predicate ! on H, !(h) denotes that h satisfies !, and H(!) denotes the set of all !-satisfying heaps. Sometimes we parameterize a heap predicate on some domain V . In this case, !(v, h) denotes that h satisfies ! with v ↘ V .
Aside from heap predicates containing pure logical expressions and quantifiers, we will describe heap contents directly with two standard predicates from separation logic [31,28]. The points-to predicate p ↔ ↗ v, for p ↘ L and v ↘ V, holds for h i! dom(h) = {p} and h(p) = v. The separating conjunction operator ! ↓ ", for predicates ! and ", holds for h i! h = h 1 + h 2 for some h 1 and h 2 s.t. h 1 → h 2 and !(h 1 ) and "(h 2 ). ↓ is commutative and associative.
We will also want to characterize when a portion of a heap satisfies a particular predicate. For this, we define heap predicate extension:
We choose to represent concrete programs as total functions over heaps, so that our semantics are highly general, and thus broadly applicable; we admit semantics which are nondeterministic, but must be constructive and must terminate. Nondeterminism mainly arises during address allocation, though this work is agnostic to the source of nondeterminism.
to the following properties:
1. On any initial heap h, f terminates or fails in finite time. 2. If f successfully terminates on h, then f (h) yields the set of all possible final heaps in which f may terminate. If f fails on h, then f (h) = ⫅̸. 3. f reads any input arguments from, and writes any outputs to, fixed locations on the heap. We explore this in §7. 4. f acts locally.
Local action enforces that f does not modify data outside its footprint, as a weak form of the typical frame rule of separation logic [31]. For any particular semantics that satisfies framing by construction, the local action constraint should immediately hold for all concrete programs. When working with compound abstractions, we will define a stronger framing property (Def. 14).
For two programs to commute, they must terminate without failure in the first place. To that end, we classify the initial heaps upon which f can execute.
Su"cient heaps contain the necessary addresses, which map to appropriate values, for f to run. In contrast, heaps in the footprint of f contain appropriate addresses, but may not contain appropriate values; thus a heap in f 's footprint on which f fails cannot be "corrected" with further allocations. Precisely:
Our concrete domain, as the counterpart to our eventual abstract domain, will be C ↭ ω(H). Concrete transformers over this domain map from sets of heaps to sets of heaps. We derive these transformers directly from programs:
f yields the set of all possible output heaps given a set of inputs, but fails entirely if f fails on any individual input. Relatedly, we define the composition/sequence of two programs so that the second program fails entirely if it fails on any one output of the first program; namely, f ; g ↭ ḡ ↖ f .
We share here a simple language called Himp, which featuring allocation (ref), deallocation, writing (↙), reading (!), and branching. We will use Himp in our example programs throughout the paper, as an instance of the general semantics above. (N.B. Himp has not been formalized in Coq. However, all of our results regarding the general semantics have been proved in Coq.)
Himp has a nondeterministic allocation procedure: for any initial heap h, ref yields an address from a set fresh(h) where fresh(h) ∝ L and fresh(h) → dom(h).
All other terms are deterministic. We elide the remaining details of Himp's semantics, which are typical for an imperative heap language. When working with
Himp programs throughout the paper, we implicitly lift them to the concrete programs described by Def. 2.
In this section we formalize our abstract domain and abstract programs operating within this domain, and establish a soundness relationship between concrete and abstract programs. This will let us perform commutativity reasoning easily with abstract objects, and obtain concrete commutativity results for free.
We design our abstract domain to lift heap-allocated structures to mathematical objects. Each instance of an abstraction consists of a set of abstract values (e.g. integers, sets, sequences) and a mapping from heaps into said values. A heap with an appropriately allocated structure to be mapped to an abstract value is said to be "within the purview" of a given abstraction. On the other hand, poorly structured heaps are "outside the purview" of the abstraction, and get mapped to a special abstract value, ✁ ("cross").
When constructing an abstraction, we impose a locality constraint which demands that information extracted from heaps be finite in scope, so that any heap containing a valid structure is in-purview. Some results of this work actually do not depend on this constraint. However, it is a valuable property to strive for, and indeed it should hold for any typical data structure abstraction.
The abstract domain is defined formally as follows:
Definition 4. Build an abstraction A = ′X, ω∞ from a set of abstract values X = {x 1 , x 2 , . . . }, and a projection function ω : H ↗ X+✁ subject to the locality constraint that for any disjoint h and h
Denote all in-purview heaps of A with Prv(A) ↭ {h | ω(h) ↘ X}, and denote its abstract values and projection function with X A and ω A .
A A is a complete lattice, and is thus equipped with a typical join (▽) operation. Recalling from §3.2 that our concrete domain is C = ω(H), we connect the concrete and abstract domains as follows:
Definition 5. Define abstraction and concretization functions ϖ A : C ↗ A A and ϱ A :
ϖ A and ϱ A are each monotone, and together they form a Galois connection [11] which induces meanings for values in A A : → is the failure state, x i ↘ X abstracts sets of in-purview heaps which all map to x i , ✂ abstracts any set of in-purview heaps, ✁ out-of-purview heaps, and ⇐ any heaps. We now share three basic examples of abstract domains. In subsequent sections we will reason about concrete and abstract programs which operate on the defined structures. In §7 we explore each example in full.
A "hello world" data structure in commutativity is the non-negative counter (NNC)-an integer which may be incremented, decremented (but not below 0), and read. We abstract an NNC located at address p as Ctr p := ′N, ω∞, where ω(h) := n if (p ↔ ↗ n) + (h) for n ↘ N, else ✁. The extension (Def. 1) on the predicate (p ↔ ↗ n) ensures that Ctr p satisfies locality, allowing the domain to capture any heap containing a counter.
Consider an unordered set containing at most two elements of type T ⇑ V ↑ . These elements are stored at fixed addresses p and q, with null otherwise stored as a placeholder. One might construct X and ω for this structure in a few equivalent ways, the key property being that concrete two-sets containing the same elements should map to the same abstract value, regardless of their order. In the following approach, the abstract values are simply mathematical sets of size at most two. We define Set T p,q := ′{S ↘ ω(T) | |S| ∋ 2} , ω∞ with:
Note how we use set + p,q throughout ω to satisfy locality. One technicality is ensuring that ω is well-defined, namely that ω(h) yields one unambiguous abstract value for each h. In Coq we prove this ω is indeed well-defined.
Reiterating our overview example ( §2), consider a stack implemented on the heap as a linked list and accessed at fixed address ε. Constructing new cells when pushing to the stack involves nondeterministic address allocation; two stacks containing the same values but di!erent intermediate addresses should be considered observationally equivalent. To achieve this, our recursive construction of ω will existentially quantify intermediate addresses, and not lift them explicitly into the abstract domain. We define Stk ω := ′list(V ↑ ), ω∞ with
Again, we must show that each h satisfies stk + (h, s) for at most one s ↘ list(V ↑ ).
A notion of isomorphism between abstract domains will also prove useful:
if such a bijection exists.
This definition is in fact stronger than necessary for some of our results; future work may warrant distinguishing isomorphism from a weaker notion of equivalence which relaxes the bijectivity requirement of ς. See Appx. A for an example in which we construct a two-set abstraction which is isomorphic to that of Ex. 2.
We design our abstract semantics so that concrete heap behavior (valid or invalid) can be threaded up to the abstract domain with enough precision that, later, abstract commutativity will soundly entail concrete commutativity ( §5). An abstract program in the context of abstraction A = ′X, ω∞ is any function from X to A , from which we derive an abstract transformer over A (recall from Def. 4 that A = X + → + ⇐ + ✁ + ✂). While these transformers could be constructed in various ways, for our purposes the following will su"ce: Definition 7. m denotes the abstract transformer derived from m : X ↗ A , where m(x) = → for x = →, m(x) for x ↘ X, and ⇐ otherwise.
To relate the behavior of an abstract program m defined in A to a concrete program f , we establish a notion of soundness (recall ϖ from Def. 5):
The first condition is typical for abstract interpretation, demanding that m overapproximate f . This lets us be imprecise with the definition of abstract programs if desirable (e.g. to avoid complex behaviors), the trade-o! being that concrete commutativity conditions eventually derived may yield false negatives (i.e. not be the weakest precondition). The second soundness condition demands that m fail (yield →) whenever f fails on an in-purview input. Because the failure sink state is at the bottom of the abstract lattice (Def. 4), without this condition there could be scenarios where two abstract programs successfully commute, but their corresponding concrete programs fail to execute.
Throughout our examples in §7 we will implicitly use the fact that program soundness is preserved by isomorphism. Namely, if m ↫ A f and
We now return to the example of the non-negative counter and its abstraction Ctr p (see Ex. 1), to define the corresponding concrete and abstract programs for increment and decrement. We cannot define read in Ctr p , because read must write its output to an additional location on the heap. We similarly must wait to revisit our two-set and linked stack examples, whose methods all have inputs and/or outputs. We develop the machinery needed for inputs and outputs in §6, and reason fully about all three examples in §7.
Consider an NNC allocated at address p. We begin with concrete implementations of increment and decrement, written in the Himp language ( §3.3), and implicitly lift them to concrete programs.
Next, defining abstract increment and decrement functions in Ctr p is intuitive:
We can show that incr p ↫ Ctrp incr p and decr p ↫ Ctrp decr p with typical symbolic execution techniques. Had we defined decr to fail when the counter is 0, rather than skip, we would have to define decr p (0) = → to maintain soundness.
With our concrete and abstract semantics established, we now define commutativity in the concrete and abstract spaces. We then relate the two with a soundness theorem that reduces concrete commutativity reasoning to simpler reasoning about abstract programs.
We say concrete programs f and g commute, under a notion of observational equivalence on a subset of all heaps, when f ; g and g; f both terminate successfully and yield observationally equivalent outcomes. We denote an obs. eq. relation with [!, ∀], for a predicate ! on H and an eq. relation ∀ on H(! + ).
Then concrete commutativity is defined precisely as:
Definition 9. For commutativity condition P on H, f and g commute under
The eq. relation we use for concrete commutativity is often very similar to the relation implicitly induced by an abstraction. We can make this explicit by deriving a concrete relation in terms of an abstraction, a technique we will use extensively in the remainder of the paper.
Define the shorthand f φ↼ P A g for f φ↼ P [Prv(A),↗ A ] g. Naturally, a user is responsible for choosing an observational equivalence relation (or in light of Def. 10, an abstraction) which is su"ciently descriptive for their purposes. Properties of concrete commutativity include:
Next we define abstract commutativity, in a manner so that we can achieve a useful soundness guarantee in relation to concrete commutativity.
Note how we only accept outcomes within the purview of A. We reject →, as non-failure is a prerequisite for commutativity. We also reject ✁, ✂, and ⇐, as such outcomes are not precise enough to guarantee meaningful commutativity.
To relate abstract and concrete commutativity, we must first relate the relevant abstraction and observational equivalence relation:
This definition of capture is preserved by abstraction isomorphism. Additionally, A always captures [Prv(A), ∀ A ], a fact we will frequently use implicitly.
We now present the central result of our work, the sound commutativity theorem, which o#oads the verification (via symbolic execution) of concrete commutativity conditions to much simpler reasoning about abstract programs:
Sound commutativity takes a valid abstract commutativity condition, and transforms it automatically into a concrete condition. For instance, suppose ω A takes the fairly common form ω A (h) = x if "(x, h) for x ↘ X A , else ✁, for some heap predicate ". In this case, the concrete condition we derive from abstract condition Q is ↑x ↘ X. " + (x, h) ↓ Q(x). Indeed, any condition we derive with Thm. 1 is extended (Def. 1). This provides framing for free-it guarantees if f and g commute in some heap context, then they also commute in any larger context. With sound commutativity established, we can summarize the overall pattern of reasoning: (i) construct an abstract domain, (ii) define abstract programs for each concrete program and prove soundness between them using symbolic execution, (iii) verify or synthesize commutativity conditions for abstract program pairs, and (iv) immediately derive concrete conditions.
Returning to the NNC programs defined in Ex. 4, we can perform abstract commutativity reasoning easily. For instance, to verify that incr p φ↼ Q Ctrp decr p for Q(n) ⇓ n > 0, we simply evaluate:
With proofs of soundness (Def. 8) of incr and decr w.r.t. incr and decr, we can immediately derive via Thm. 1 that f φ↼ P + Ctrp g where P ⇓ ↑n ↘ N + . p ↔ ↗ n. Note how we use the equivalence imposed by Ctr p as our concrete observational equivalence relation (Def. 10).
We might synthesize an abstract condition interactively (we leave automation to future work), by trying to prove that incr and decr commute under ⇐, and seeing where the proof gets stuck. In this case, we will get stuck showing that 1 = 0 under an initial abstract value of 0. By constraining that n > 0, the proof can be completed; thus n > 0 is a valid precondition.
In this section, we expand upon our established tools for abstracting data structures and performing commutativity analysis, by defining composition of abstract domains. This enables compositional reasoning in settings with multiple data structures, and provides the machinery we need to reason about concrete programs with inputs and outputs allocated on the heap.
Various compositional operators on abstract domains have been used in abstract interpretation, such as Cartesian product, reduced product, and reduced cardinal power [9], but these operators do not suit our needs. The composition of two abstractions ought to yield a new abstraction; however, these existing operators would not produce a valid abstraction, not even up to isomorphism.
A composition of abstractions should respect the disjointness of the concrete structures which are individually abstracted. We achieve this with the abstract conjunction operator, denoted A ↓ B, which is defined to mirror the concrete separating conjunction. The purview of A ↓ B will contain heaps which can be partitioned into joint halves that are respectively in the purviews of A and B.
A technicality of Def. 13 is ensuring that ω(h) maps to a unique (a, b) pair (or to ✁) for every h. We show in Coq that this uniqueness does hold, due to the locality constraint of Def. 4. Additionally, when A and B satisfy locality, so too does A ↓ B. Abstract conjunction is compatible with, and is commutative and associative up to, abstraction isomorphism; we use these facts implicitly throughout §7. Much like the heap separating conjunction, A ↓ B may be unsatisfiable, i.e. ω A↑B maps all heaps to ✁. Commutativity reasoning w.r.t. an unsatisfiable domain is still valid, albeit meaningless, as there are no in-purview heaps. Applying the concrete observational equivalence construction of Def. 10 to composition, we get
.2 Concrete Program Capture E!ective compositional reasoning will often require that behavior of the concrete programs of interest are "captured" by the abstract domains in use. For instance, incr has well-defined behavior w.r.t. Ctr p , but not Stk ω . If we prove properties about incr w.r.t. Ctr p , we should be able to derive how incr behaves w.r.t. Ctr p ↓ Stk ω (namely it leaves the stack untouched). However, if we reason about incr w.r.t. Stk ω , we will learn nothing about how incr behaves w.r.t. Stk ω ↓ Ctr p .
To this end, we say that an abstraction A captures program f if (1) heaps in the purview of A are in the footprint of f , (2) f maps in-purview heaps to inpurview heaps, and (3) f maintains its specific in-purview mappings when any disjoint heaps are tacked onto the initial heap (thus strengthening local action in an abstraction-specific manner). Precisely:
Proving capture can be less burdensome than it appears-if we have shown that m ↫ A f for m s.t. image(m) ⇑ X A + →, then conditions (1) and ( 2) immediately hold for f . We also expect that (3) should hold automatically for all abstractions and all Himp programs (and other typical heap languages). Capture is preserved by abstraction isomorphism, and if A captures f then A ↓ B captures f .
Capture yields a common form of concrete commutativity: commutativity from noninterference. If two programs operate on disjoint structures, then they automatically commute whenever they individually terminate without failure:
Theorem 2. If A and B capture f and g respectively, then
Finally, we will often discuss program capture and soundness in the same breath, so we provide a convenient shorthand:
A f denotes that m ↫ A f and A captures f .
In service of sound commutativity reasoning in compound abstract domains, we define a way to compose abstract programs:
Definition 16. Given m and n defined in A and B respectively, their conjunc-
The compound program soundness theorem then states that the conjunction of two abstract programs soundly abstracts the sequence of two concrete programs (in either order), so long as these concrete programs operate on disjoint structures (via capture). We also derive an abstract frame rule of sorts.
A f and n ↫ CAP B g, then m↓n ↫ CAP A↑B f ; g and m↓n ↫ CAP A↑B g; f .
With composition of abstract domains and their programs established, we can demonstrate new compositional commutativity soundness properties, beginning with compound abstract commutativity:
From this, along with sound commutativity (Thm. 1) and compound program soundness (Thm. 3), we yield compound sound commutativity, which allows us to compose individual commutativity results about pairs of programs operating on disjoint structures:
Note how this result still holds even if A ↓ B is unsatisfiable, because the concrete commutativity condition requires that the initial heap maps to a valid abstract value. From this theorem we derive framed sound commutativity:
Let's contrast this result with our prior sound commutativity result (Thm. 1), which also includes a form of framing. Thm. 1 says that, within the parameters of a chosen abstraction and concrete observational eq. relation, the derived concrete commutativity condition is framed. On the other hand, Cor. 2 guarantees-under the stronger premise of capture-that the programs commute under a framed concrete condition within A, as well as within the purview and observational equivalence imposed by any compound abstraction containing A.
In this section we reiterate and expand on our working examples: a non-negative counter, a two-set, a linked-list stack, and the composition of a stack and counter.
For each example, we (i) define concrete programs; (ii) construct an abstract domain and abstract programs; (iii) perform abstract commutativity reasoning; (iv) prove soundness between the concrete and abstract programs; and (v) derive concrete commutativity conditions. As (v) follows directly from (iii) and (iv), we sometimes omit it for brevity.
Throughout these examples, we will need to abstract the arguments and return values of methods. To that end we define the "address domain" Addr, which simply captures the value stored at a given heap address. For address p and values V ⇑ V considered valid, construct Addr V p := ′V, ω∞, where ω(h
We will also use some shorthands. We may omit abstract program compositions rendered trivial by (Cor. 1), e.g. if m is defined in A and we are reasoning in A ↓ B, we may write m rather than m ↓ id . Furthermore, we will leverage the associativity and commutativity of abstract composition up to isomorphism to reason about abstract programs which have been defined in a similar but "outof-order" compound abstraction. We use the addresses on which an abstract program is parameterized as unique identifiers for how the input and output tuples of said program should be implicitly permuted.
Consider a non-negative counter structure allocated at p, featuring the following concrete operations written in Himp: We verify commutativity conditions for incr and decr w.r.t. an initial value n ↘ X Ctrp . By evaluating the abstract programs (as in Ex. 5) we find that incr p and incr p commute under ⇐, incr p and decr p under n > 0, and decr p and decr p under ⇐. We cannot compare incr or decr with read directly, as they are defined in di!erent domains. So we consider incr p ↓id and decr p ↓id in Ctr p ↓Addr N r , while preserving soundness w.r.t. the concrete programs via Cor. 1. We can verify that, for an initial value (n, _) ↘ X Ctrp↑Addr N r , incr p ↓ id and read r p never commute, and decr p ↓ id and read r p commute under n = 0. Lastly, we pair read with itself, recognizing that the two read executions should write their outputs to di!erent locations (this idea returns in the subsequent examples). So with addresses r and s, we consider read r p ↓ id and read s p ↓ id defined in Ctr p ↓ Addr N r ↓ Addr N s , and find that they commute under ⇐.
To derive concrete commutativity from these abstract results, we first find with symbolic execution the soundness and capture facts (recall shorthand 15) that incr p ↫ CAP Ctrp incr p , decr p ↫ CAP Ctrp decr p , and read r p ↫ CAP Ctrp↑Addr N r read r p . Now we may immediately derive framed concrete commutativity conditions via Thm. 1. For each program pair, we characterize f φ↼ P + A g (recall shorthand 10): f g A P incr p incr p Ctr p ↑n ↘ N. p ↔ ↗ n incr p decr p Ctr p ↑n ↘ N + . p ↔ ↗ n decr p decr p Ctr p ↑n ↘ N. p ↔ ↗ n incr p read r p Ctr p ↓ Addr N r → decr p read r p Ctr p ↓ Addr N r ↑x ↘ N. p ↔ ↗ 0 ↓ r ↔ ↗ x read r p read s p Ctr p ↓ Addr N r ↓ Addr N s ↑n, x, y ↘ N. p ↔ ↗ n ↓ r ↔ ↗ x ↓ s ↔ ↗ y 7.2 Two-Set
Consider an unordered set containing at most two elements of type T ⇑ V ↑ . We define concrete add, remove, and member-test methods, each parameterized on the set locations p and q (we omit p and q subscripts for brevity), as well as input address a and/or output address r.
Define abstraction Set T p,q := ′{S ↘ ω(T) | |S| ∋ 2} , ω∞ with:
Next we construct abstract programs add and rem in B = Set T p,q ↓ Addr T a , and mem in C = Set T p,q ↓ Addr T a ↓ Addr B r :
We analyze commutativity w.r.t. A = Set T p,q ↓ Addr T a ↓ Addr T r ↓ Addr T b ↓ Addr T s (though only the mem/mem pair utilizes all four Addr domains).
Programs Condition on (S, u,
After proving that add a ↫ CAP B add a , rem a ↫ CAP B rem a , and mem r a ↫ CAP C mem r a , we again can derive concrete commutativity conditions for add, rem, and mem. In particular, we use the observational equivalence induced by Aas our concrete eq. relation, which ensures that concrete two-sets with the same values in di!erent orders are considered equivalent. We omit for brevity the concrete conditions, which each amount to "the program pair commutes w.r.t. [Prv(A), ∀ A ] on h if ω(h) satisfies the abstract condition."
We now expand upon the example from the overview ( §2) of a stack of non-null values, implemented as a linked list accessible at address ε. We consider its push, pop, and peek methods, where pop fails on an empty stack. To account for the lack of an is_empty operation, peek outputs null on an empty stack.
Once again, we abstraction define Stk ω := ′list(V ↑ ), ω∞ where
null) Next we verify commutativity conditions for each abstract program pair w.r.t.
We then find through symbolic execution that push a ω ↫ CAP B push a ω , pop a ω ↫ CAP B pop a ω , and peek a ω ↫ CAP C peek a ω . Finally, we freely derive commutativity conditions for each concrete pair w.r.t. [Prv(A), ∀ A ], which we again omit for brevity.
Suppose we augment our stack data structure with a counter to track the stack's size. The concrete operations for this structure would be
cpush a ω,p := push a ω ; incrp cpeek a ω := peek a ω cpop a ω,p := pop a ω ; decrp csize r p := read r p We can similarly define abstract programs with composition. Namely, the following are defined in Stk ω ↓ Ctr p , with Addr domains joined on as appropriate: cpush a ω,p := push a ω ↓ incr p cpeek a ω := peek a ω ↓ id cpop a ω,p := pop a ω ↓ decr p csize r p := id ↓ read r p
We analyze commutativity of these abstract programs in A = Stk ω ↓ Ctr p ↓ Addr U a ↓ Addr V b . For each pair, we leverage Lem. 1 to derive a condition for free from our prior analyses (ε and p subscripts are omitted):
For our requisite soundness and capture facts, we use compound soundness (Thm. 3) to derive for free that cpush a ω,p ↫ CAP A cpush a ω,p , cpop a ω,p ↫ CAP A cpop a ω,p , cpeek a ω ↫ CAP A cpeek a ω , and csize a p ↫ CAP A csize a p . With this and our abstract commutativity conditions, we may freely derive concrete conditions for cpush, cpop, cpeek, and csize. One interesting case is the cpop/csize condition, which demands a nonempty stack with size 0. This cannot occur with a correctly initialized stack and counter, meaning in practice cpop and csize never commute.
To the best of our knowledge there are no existing works on commutativity reasoning specifically geared toward heap-based programsfoot_0 . We covered some other works in §1, and here discuss some of those and others in more detail.
Commutativity without the heap. Some prior works focused on verifying and even inferring commutativity properties, though not with a heap memory model. These include aforementioned work such as Kim and Rinard [23] who verified commutativity properties in two steps: verifying an implementation satisfies its ADT specs, and then verifying commutativity of the ADT spec. Further in that direction, Bansal et al. [2,3] showed that commutativity conditions of ADT specs could be synthesized, and introduced the tool Servois, which was later improved as Servois2 [7]. Chen et al. [6] adapted these approaches to perform commutativity analysis on (non-heap) imperative programs. Finally, Koskinen and Bansal [24] also verified commutativity, but not of heap-based programs.
Commutativity with the heap. Pîrlea et al. [29] describe the CoSplit tool, which performs a commutativity analysis on a smart contract language. Their analysis determines commutativity of heap operations, but only when commutativity can be determined based on heap ownership. Thus, their approach could not handle the examples in this paper including the Counter, which involves commutative updates to the same heap cell. Eilers et al. [15] leverage commutativity modulo user-specified abstractions to prove information flow security in the space of relational concurrent separation logic.
Exploiting commutativity for verification. Commutativity is a widely used abstraction in many verification tools, which use commutativity specifications as user-provided inputs. In the context of concurrent programs, QED [16] and later CIVL [25] both use commutativity (more specifically, left/right movers) to build atomic sections. The Anchor [22] verifier also uses commutativity for a more automated approach of verifying concurrent programs. Commutativity is also used for proofs of parameterized programs [20], operational-style proofs of concurrent objects [17] and termination of concurrent programs [26]. Abstract commutativity relations have also been used in reductions for verification [19]. A summary of the use of commutativity in verification was given by [18].
Abstract domains for the heap. Other works have focused on the intersection of abstract interpretation and heap logics, although they do not specifically target commutativity, and generally seek to abstract the semantics of separation logic rather than reasoning about particular allocated structures. Sims [34] constructs a detailed abstract domain for representing separation logic heap predicates. Calcagno et al. [4] introduce separation algebras, which generalize the semantics of separation logic.
We have demonstrated how commutativity analysis on concrete heap programs can be reduced to much simpler reasoning about mathematical objects in an abstract space. We have designed our abstract domain to account for allocation nondeterminism, concrete observational equivalence, and improperly allocated heap structures. We formalized this domain, laid out the abstract semantics and program soundness relation, established a sound commutativity theorem, and introduced composition of abstractions for multi-structure program settings. We then worked through several examples illustrating the convenience of analyzing abstract program commutativity and deriving concrete results. Our work has been implemented in Coq and is available in the supplement.
In future work we plan to pursue automation by implementing an abstract interpreter, and exploring how it can be combined with existing commutativity synthesis techniques in the abstract domain [2,7]. Furthermore, we will explore how our model of data structure abstraction could be applicable to various kinds of heap-style reasoning other than commutativity. We are also interested in augmenting our abstract domain to feature an abstract value subset lattice, which would permit nondeterministic abstract programs and reasoning about bounded divergence commutativity.
Some early elements of our work appeared in a current author's Master's thesis (anonymized for review). However, that work was not published, only applied to deterministic programs, and lacked the abstract domain that we present here.