Rooting for Eﬃciency
Mechanised Reasoning about Array-Based Trees in Separation Logic
Qiyuan Zhao

George Pîrlea

Zhendong Ang

National University of Singapore
Singaporeqiyuanz@comp.nus.edu.sg

National University of Singapore
Singapore
gpirlea@comp.nus.edu.sg

National University of Singapore
Singaporezhendong.ang@u.nus.edu

Umang Mathur

Ilya Sergey

National University of Singapore
Singaporeumathur@comp.nus.edu.sg

National University of Singapore
Singapore
ilya@nus.edu.sg

Abstract

Used to represent virtually any kind of data with hierarchicalordering, trees admit a simple encoding in both functional
programming languages, as algebraic data types (ADT), andin imperative ones, as pointer-based linked structures without internal sharing. Most tree-manipulating programs canbe expressed as recursive traversals, whose control ﬂow mimics the shape of the underlying data structure. Thanks to thisfact, reasoning about tree manipulations can be conducted
via simple induction principles, which made such computations popular topics in studies on program derivation [13, 29],transformation [4, 35], and veriﬁcation [2, 10].
In this work, we focus on a less well-studied way to represent trees in heap-manipulating programs written in imperative languages such as C: as arrays. Developers choose
an array-based encoding of trees for eﬃciency reasons—it
allows constant-time random access to node data, requires
less memory to store, and enjoys better cache locality thanpointer-based representations. From the perspective of formal reasoning about tree-manipulating programs, the array
representation comes with a number of new challenges. Firstof all, tree traversals implemented by means of addressing
elements in an array via integer indices do not immediately
yield familiar induction principles. Furthermore, programs
working with array-based tree representations often exploit
the fact that children of a node are arranged into a contiguousarray segment: this enables eﬃcient non-recursive traversals, but complicates veriﬁcation due to the need to devise
complex loop invariants. Finally, while arrays are conceptually similar to pointers, they require slightly more delicate
reasoning in common formalisms, such as Separation Logic(SL) [28, 31], as proof obligations involving their element
indices require one to keep track of the indices’ numeric
properties to avoid, in particular, out-of-bounds errors.
The motivation for this work came out of our eﬀort ofverifying in Coq a C implementation of Tree Clocks [22]—anintricate imperative data structure that implements a stateof-the-art version of logical clocks via an array-based tree
and extensively takes advantage of the array encoding for thesake of eﬃciency. SL-based reasoning about complex linked

Array-based encodings of tree structures are often preferable to linked or abstract data type-based representations
for eﬃciency reasons. Compared to the more traditional
encodings, array-based trees do not immediately oﬀer convenient induction principles, and the programs that manipulatethem often implement traversals non-recursively, requiring
complex loop invariants for their correctness proofs.
In this work, we provide a set of deﬁnitions, lemmas,
and reasoning principles that streamline proofs about arraybased trees and programs that work with them. We showcase
our proof techniques via a series of small but characteristic
examples, culminating with a large case study: veriﬁcationof a C implementation of a recently published tree clock data
structure in a Separation Logic embedded into Coq.
CCS Concepts: • Software and its engineering → Software veriﬁcation.
Keywords: array-based trees, logical clocks, separation logic
ACM Reference Format:
Qiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur, and Ilya
Sergey. 2024. Rooting for Eﬃciency: Mechanised Reasoning about
Array-Based Trees in Separation Logic. In Proceedings of the 13th
ACM SIGPLAN International Conference on Certiﬁed Programs andProofs (CPP ’24), January 15–16, 2024, London, UK. ACM, New York,NY, USA, 15 pages. https://doi.org/10.1145/3636501.3636944

1 Introduction
There are hardly any other basic data structures in Computer Science as ubiquitous, versatile, and beloved as trees.
Permission to make digital or hard copies of part or all of this work forpersonal or classroom use is granted without fee provided that copies are
not made or distributed for proﬁt or commercial advantage and that copies
bear
this noticeand thefullacitation
the ﬁrst page.
Copyrights for thirdThis work
is licensed
under
Creativeon
Commons
Attribution-ShareAlike
4.0
International
License.
party
componentsof this work must be honored. For all other uses, contact
the owner/author(s).
CPP ’24, January 15–16, 2024, London, UK© 2024 Copyright held by the owner/author(s).
ACM ISBN 979-8-4007-0488-8/24/01
https://doi.org/10.1145/3636501.3636944

45

CPP ’24, January 15–16, 2024, London, UK

Qiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur, and Ilya Sergey

structures with “deep” internal sharing and unstructured
aliasing has been addressed, to some extent, in the past [24,36]. However, we found those developments inapplicable forour goal due to their focus on a more general setup targetinggraph-like structures and, therefore, imposing extra proof
overhead when tackling tree-speciﬁc proof obligations.
To document the lessons we learned from our veriﬁcation experience, in this paper, we articulate a number ofchallenges we faced during while verifying several characteristic procedures that manipulate array-based trees. We
then describe reasoning principles and auxiliary deﬁnitions
encoded in Coq that came in handy when constructing suchproofs. In particular, we argue that there are two kinds of representation predicates in Separation Logic for array-based
trees (i.e., the array view ones and the tree view ones), eachhaving its specialised utility in the proof; we also present
lemmas for smoothly “switching” between the dual views.
Another emphasis of our demonstration is the formulationof an extensible loop invariant for non-recursive tree traversals through a small collection of neat functions deﬁned
on the mathematical model of array-based trees. Finally, we
sketch the key points of our mechanised correctness proofof the tree clock data structure that has been implemented
in C and veriﬁed using the Veriﬁed Software Toolchain (VST)
framework [1], which embeds Separation Logic into Coq.
In summary, this work makes the following contributions:struct node { int val, par, sib, fch; };struct node tree[N];(a) RLT encoding in C.

par
id:i
val

sib

children nodes

fchchildren(b) Correspondence between a tree node and the struct ﬁelds.

Fig. 1. RLT: encoding in C (top) and its depiction (bottom).
sib, and fch that store the identiﬁers of the node’s parent,
right sibling, and ﬁrst (left-most) child, respectively. Fig. 1b
gives a visual depiction of such a tree. As indicated in Fig. 1b,
this structure allows the representation of RLTs of any arity.
In the rest of this section, we provide a series of illustrative examples of programs that manipulate RLTs encoded asshown in Fig. 1a, articulating the challenges of structuringformal veriﬁcation of such programs.

• A collection of small case studies illustrating the key challenges of reasoning about imperative C programs thatmanipulate array-based trees (Sec. 2);• Arboreta: a library of predicates and accompanying higherorder lemmas, as well as a set of principles that streamline
the common reasoning patterns for such program (Sec. 3);• A mechanically veriﬁed implementation of Mathur et al.’sarray-based tree clock data structure in C [22] (Sec. 4).

Formalising RLTs. Fig. 2 shows a natural encoding ofan RLT in Coq as an inductive algebraic data type: an RLT
is constructed with the Node constructor, which carries thenode identiﬁer id, the node information val and the list chn
of children. Even though the deﬁnition of the tree data typeoﬀers no constructor for an empty tree, leafs (i.e., nodes
without children) can be modelled as instances of the Nodeconstructor with empty chn. To ensure that the nodes in a tree
tr all have distinct identiﬁers, we use an extrinsic predicate
NoDupId(tr), whose presentation is postponed till Sec. 3.1.
While this fairly standard inductive deﬁnition is suﬃcientfor modelling the tree structure and stating and proving
mathematical properties of purely-functional RLTs, it is not
immediately suitable for specifying and verifying imperative programs that manipulate array-based RLTs: the logicaltree structure is not directly related to the physical one inmemory. To bridge this gap, we employ a standard technique of deﬁning a representation predicate in Separation
Logic [6, 7, 34] that relates the algebraic deﬁnition of RLTs
in Coq to the memory layout of the RLT in C.
To deﬁne a representation predicate tree_reparr for arraybased RLTs, we can use the conventional predicate arr(𝑝, ℓ)

The code repository for this paper is publicly available athttps://github.com/verse-lab/arboreta

2 Overview and Key Ideas
In this work, we reason primarily about rooted labelledtrees (RLTs), and speciﬁcally those implemented using arrays.
An RLT is a tree in which each node, besides the data it holds,
is given a unique identiﬁer (label), usually a natural number. These identiﬁers allow for node indexing and thereby
enable random-access data retrieval from the “carrier” arrayof the tree. In an imperative programming language like C,
a common approach to implementing RLTs is to use an array of structs, where each struct contains the information
associated with a node, and use array indices as node identiﬁers. Fig. 1a shows one its possible encoding in C: the tree isrepresented by the array tree, in which tree[i] stores thenode with identiﬁer 𝑖 (hereafter referred to as node 𝑖). Eachnode also stores some data in its val ﬁeld, and its relations
to other nodes in the RLT are represented by the ﬁelds par,46

Rooting for Eﬀiciency: Mechanised Reasoning about Array-Based Trees in Separation Logic
Inductive tree: Type := Node (id val: nat) (chn: list tree).
Definition NoDupId (tr: tree): Prop := (* elided *)Definition isSome [A : Type] (x : option A) :=match x with Some _ => true | None => false end.
Fixpoint find_val (x : nat) (tr : tree) : option nat :=let 'Node id v chn := tr inif (x =? id)%nat then Some velse match find isSome (map (find_val x) chn) with| Some res => res| None => Noneend.

Fig. 2. An algebraic encoding of RLT in Coq.
for arrays (available in many existing Coq embeddings ofSL [1, 8]), which states that an address 𝑝 in memory is a basepointer of an array whose elements are the elements of the(mathematical) list ℓ. Concretely, we make ℓ into a list of
payloads, where each payload is the functional model of asingle instance of the node structure shown in Fig. 1a.
Unlike the C deﬁnition in Fig. 1a, in the Coq encoding, thechild subtrees of a node are represented as a ﬁnite list. The
challenge in relating the C encoding, which connects a node
to its parents/children/sibling by virtue of the indices represented by integer ﬁelds, with the Coq encoding from Fig. 2
lies in recovering the list of nodes from the inductive tree
deﬁnition, and speciﬁcally in constructing the par, sib, andfch ﬁelds to express the tree structure. To this end, we deﬁne
a recursive projection predicate treelist_proj that relates alist of trees to a list of payloads:

Fig. 3. Coq deﬁnitions for retrieving an value from RLT.
Example 1: Random Access. Consider the following function that returns a value of an RLT node given its index x:
int get_val (int x) { return tree[x].val; }Ascribing a good formal speciﬁcation to this one-liner requires one to provide a couple of auxiliary deﬁnitions thatamount to several lines of Coq and are shown in Fig. 3. Using
the Coq function find_val as a helper, we can now ascribe
the following Hoare triple to get_val:{tree_reparr (𝑝 tree, 𝑡𝑟 ) ∗ ⌈find_val(𝑥, tr) = Some(𝑣)⌉}
get_val (𝑥){𝜆ret. tree_reparr (𝑝 tree, tr) ∗ ⌈ret = 𝑣⌉}

treelist_proj(nil, par, ℓ) ≜ ⊤treelist_proj(Node(id, val, chn) :: trs, par, ℓ) ≜ℓ [𝑖𝑑] = payload(val, par, hid(trs), hid(chn)) ∧treelist_proj(chn, id, ℓ) ∧ treelist_proj(trs, par, ℓ)(2)

The speciﬁcation above states that, assuming the node with
the identiﬁer 𝑥 holds the value 𝑣 in the algebraic representation of the RLT tr and the array-based representationof tr is available to get_val, the result ret of the call will
be exactly 𝑣. To establish this speciﬁcation, we ﬁrst needto prove an important property of find_val, namely, that
if find_val(𝑥, tr) = Some(𝑣), then for any ℓ that satisﬁes
tree_proj(tr, ℓ), ℓ [𝑥] contains 𝑣. This fact can be proven by
induction on the algebraic tree tr via the following induction
principle stating that a property holds on an RLT if it holds
on all children and on the root node itself:1

As per the deﬁnition above, the projection predicate takes
as input a list of trees, rather than a single tree, in order tomatch the structure of the Coq deﬁnition wrt. children. For
Node(id, val, chn) in the list, the predicate asserts that its
payload is the id th element of ℓ (denoted ℓ [id]), with the appropriate parent. The right sibling and ﬁrst child are obtainedby retrieving the identiﬁer of the heading node (hid) in the trs
and chn lists, respectively. The remainder of the payload list ℓ
is constrained by two recursive applications of the predicate,
treelist_proj(chn, id, ℓ) and treelist_proj(trs, par, ℓ). The indices of the nodes in the payload list ℓ are the same as theiridentiﬁers in the deﬁnition from Fig. 2, but treelist_proj could
assign identiﬁers arbitrarily, as long as they are distinct.
With the above predicate, we can now deﬁne a projection
on trees (rather than list of trees) and the representation
predicate for array-based RLTs in terms of Separation Logic:
tree_proj(tr, ℓ) ≜ treelist_proj(tr :: nil, −1, ℓ)
tree_reparr (𝑝 tree, tr) ≜ ∃ℓ, ⌈tree_proj(tr, ℓ)⌉ ∗ arr(𝑝 tree, ℓ)

CPP ’24, January 15–16, 2024, London, UK

Lemma tree_ind' (P: tree -> Prop)(Hindstep : forall (id v: nat) (chn: list tree),(forall ch, In ch chn -> P ch) -> P (Node id v chn)):forall (tr: tree), P tr.

The speciﬁcation (2) can be then proven using standard
Separation Logic rules. First, tree_reparr (𝑝 tree, tr) gives us
the logical list ℓ, which we pass to the find_val property, obtaining the fact that ℓ [𝑥] contains 𝑣. Next, from arr(𝑝 tree, ℓ)
we know that tree[x] stores the equivalent of the payloadℓ [𝑥]. Finally, from the above, we conclude that tree[x].val
returns ℓ [x].val. The key enabler of this proof is the representation predicate that links the algebraic tree with the arraybased one. Random access operations similar to get_val areparamount in implementations that manipulate array-based
RLTs, and we make use of such speciﬁcations in our chiefcase study with tree clocks outlined in Sec. 4.

(1)where tree_reparr (𝑝 tree, tr) represents the array-based RLT
tr whose base pointer is 𝑝 tree (e.g., the tree pointer in Fig. 1a).
As customary in SL, the ∗ connective stands for the separating
conjunction [31], and ⌈. . .⌉ denotes pure assertions.
2.1 Specifying Computations with Array-Based RLTs
Let us now illustrate the representation predicate by specifying and verifying a couple of RLT-manipulating programs.

1 Coq automatically derives a weaker induction principle for the tree from

Fig. 2, hence we deﬁne tree_ind' and prove it as a standalone theorem.

47

CPP ’24, January 15–16, 2024, London, UK
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

Qiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur, and Ilya Sergey

struct node tree1[N], tree2[N]; // trees
int stack[N];// assisting stack
void copyval_and_move (int root1, int root2) {// root1: the root of tree1// root2: the root of tree2
int top = -1;
stack[++top] = root2;
while (top >= 0){
int x = stack[top--];tree1[x].val = tree2[x].val;
if (tree1[x].fch != -1)
move_first_child(root1, x); // defined in Fig. 5
int tmp = tree2[x].fch;
while (tmp != -1){
stack[++top] = tmp;
tmp = tree2[tmp].sib;
}
}
}

1
2
3
4
5
6
7
8
9

Fig. 5. Example program that changes the tree’s structure.
2.2

tree2

tree1 (after)

1
val: 63val: 71
val: 22val: 54val: 05val: 43
val: 81val: 26val: 34
val: 02
val: 55val: 1

Structure-Changing Tree Operations

Before we look into copyval_and_move, let us ﬁrst verify its
subprocedure move_first_child, shown in Fig. 5.
This procedure makes the ﬁrst child of node src become
the ﬁrst child of node dst, while keeping the rest of thetree’s structure unchanged. To give its speciﬁcation, we can(a) write one or more recursive functions in Coq exhibiting
the same behaviour as the imperative program (e.g., one forpopping a child of node 𝑖 and another for prepending a child),
and then (b) state that the logical tree obtained after applying
these functions corresponds to the tree in the postcondition:(a) Structure-changing non-recursive tree traversal.
tree1

void move_first_child (int dst, int src) {/* precondition: tree1[src].fch != -1 andnode dst is not in tree1[src].fch */int tmp = tree1[src].fch;
tree1[src].fch = tree1[tmp].sib;
tree1[tmp].sib = tree1[dst].fch;
tree1[dst].fch = tmp;
tree1[tmp].par = dst;}

3
val: 7

5val: 4{tree_reparr (𝑝 tree, tr) ∗ ⌈· · · ⌉}move_first_child (dst, src)
{𝜆_.tree_reparr (𝑝 tree, tr ′ )}6val: 3(3)

where tr ′ in the postcondition may be similar in form toprepend_child(pop_child(tr, src), dst). We give one possible
deﬁnition of prepend_child later in Sec. 3.2.4.
To prove the speciﬁcation (3), ﬁrst observe that this program only involves reads and writes on the ﬁelds of thearray tree. We can unfold the tree_reparr in the precondition to obtain the initial payload list ℓ by existential elimination. Similarly, in the postcondition, the resulting tree isrepresented by another payload list ℓ ′ such that arr(𝑝 tree, ℓ ′ )holds, and we know that ℓ ′ is obtained from ℓ by applying
a sequence of transformations. It then suﬃces to show thattree_proj(tr ′, ℓ ′ ) holds. Unfortunately, this proof obligation
can be very cumbersome, since we need to show that the
payloads not touched by move_first_child have remained
unchanged in the process. We can prove this by induction,
but it is tedious, and the proof would need to be repeatedanew for every diﬀerent structure-changing operation.

(b) Example of executing copyval_and_move.

Fig. 4. A structure-changing traversal and its depiction.
Example 2: Structure-Changing Tree Traversals. Realistic programs that manipulate RLTs can be quite complex,
and may perform (imperative, non-recursive) traversals interspersed with structure-changing operations.2 Fig. 4a shows
an example of such a program, which (i) traverses the tree
stored in tree2, (ii) copies the val of each traversed node x
to the node with the same identiﬁer (the “updated node”)
in the tree stored in tree1, and (iii) moves the ﬁrst childof the updated node to be the ﬁrst child of the node root1.
Fig. 4b shows an example execution of copyval_and_move.
In the resulting tree, the value of node 3 has been updated
to 7, and node 3’s ﬁrst child in tree1, i.e., node 4, has been
moved to become a child node of node 1, which is the root oftree1. Similarly, node 5’s value has been updated to 4, andnode 5’s ﬁrst child, i.e., node 6, has been attached to node 1.
Finally, the value of node 1 is updated to 2. This example
is a simpliﬁed version of the manipulations that take placein tree clocks, and we dedicate the next two subsections tozooming in on its two challenging aspects: changing the tree
structure and performing its non-recursive traversal.

Key Idea: Dual Views. What we would really want aresome localised reasoning principles that would allow us toprove tree_proj(tr ′, ℓ ′ ) by only requiring reasoning about
the modiﬁed part of the payloads and the tree. However, thisis hard to achieve with the current representation predicate.
Prior work on Separation Logic-based veriﬁcation has
shown that one can get exactly this workﬂow by deﬁning analternative representation predicate that reﬂects tree structure via suitable placed usages of the separating conjunctionin its deﬁnition [6, 7]. We will refer to such a predicate that

2 For ease of presentation, all non-recursive traversals in this paper visit

child nodes from last to ﬁrst. Regular traversals can be handled analogously.

48

Rooting for Eﬀiciency: Mechanised Reasoning about Array-Based Trees in Separation Logic

allows one to reason about the memory manipulations inductively and employ proper localised reasoning rules (e.g.,
Frame), as a tree view predicate. In Sec. 3.2, we will show
how to deﬁne such a tree view predicate, which facilitates
verifying structure-changing RLT operations. At the sametime, we will keep using the previously-deﬁned array view
predicate to deal with random access operations, and will beswitching between the two views as needed to use the one
best suited for the veriﬁcation task at hand.

1
2
3
4
5
6
7
8
9
10

int max_val_rec (int rt) {int maxi = tree[rt].val;
int tmp = tree[rt].fch;
while (tmp != -1){
int res = max_val_rec(tmp);
if (maxi < res) maxi = res;tmp = tree[tmp].sib;}
return maxi;}

Fig. 6. Recursive traversal of an array-based RLT.

2.3 Non-Recursive Tree Traversals
Preorder or postorder tree traversals are easy to implement
recursively in both functional and imperative styles. Since
RLT nodes have unique identiﬁers, we can also implement
non-recursive traversals using a stack. This avoids recursion
overhead (e.g., allocation of stack frames), and is therefore
preferred in scenarios where eﬃciency is key.
The diﬃculty with certifying such traversals lies in stating the loop invariant. To illustrate this, let us temporarily turn our attention from loop-based implementation of
copyval_and_move to a simpler program in Fig. 6 that performs a recursive preorder traversal on array-based RLTs.
The program computes the maximum value val in the tree,
and we can straightforwardly deﬁne the functional model ofthis imperative program in Coq:

synchronously (e.g., once a node is visited in the current
iteration, its children nodes should be pushed into the stack).
The diﬃculty lies in both characterising these two aspects
and describing how they evolve in a traversal. In some cases,
it might suﬃce to deﬁne a ghost state for the visited nodes,
but this does not generalise for arbitrary traversals.
Key Idea: Tree Splitting. To verify non-recursive traversals, we need a precise characterisation of the tree structurethat has been already visited. This can be achieved by “splitting” the set of array-hosted nodes of the tree into thosealready visited and those that yet remain to be processed.
Luckily, the spatial structure of the array-based RLTs makes
it possible to deﬁne such invariants by instantiating a common “template” that constrains the two subsets of the nodes.
We detail this technique Sec. 3.3, providing a description of
the helper lemmas that facilitate such proofs.

Fixpoint max_val (tr : tree) : nat :=let 'Node _ v chn := tr in
Nat.max v (list_max (map max_val chn)).

Since max_val_rec performs recursion nearly identically to
max_val, a feasible SL speciﬁcation for max_val_rec is:′ (𝑝{tree_reparr
tree, tr, par)}max_val_rec (id_of (tr))′ (𝑝{𝜆ret. tree_reparr
tree, tr, par) ∗ ⌈ret = max_val(tr)⌉}

CPP ’24, January 15–16, 2024, London, UK

3 Arboreta: Proofs about Array-Based Trees(4)

where id_of (tr) returns the identiﬁer of tr’s root, and′ (𝑝tree_reparr
tree, tr, par) ≜∃ℓ, ⌈treelist_proj(tr :: nil, par, ℓ)⌉ ∗ arr(𝑝 tree, ℓ).

We have to use the generalised representation predicate
above because par is not −1 in the recursive call.
We can now establish speciﬁcation (4) by (a) showing that′ (𝑝tree_reparr
tree, Node(id, val, chn), par) entails that the pred′ (𝑝icate tree_reparr
tree, ch, id) holds for all ch ∈ chn, and(b) using “the value of maxi is the maximum value amongst
tr’s root and some preﬁx of its children” as a loop invariant.
Although, as we have seen, a recursive traversal similar
to max_val_rec is straightforward to specify and prove, thesituation is quite diﬀerent for copyval_and_move. Speciﬁcally,
it is unclear how to specify the loop invariant for its outerwhile-loop. There are two aspects we need to capture in thatloop invariant: (a) the contents of the stack and (b) the visited
nodes (i.e., the nodes that have already been popped from thestack in previous iterations). The two must be consistent (e.g.,a visited node should not appear in the stack) and maintained

49

In this section, we elucidate the design of Arboreta—a Coq
library with a set of proof principles that facilitate mechanised reasoning about array-based tree manipulations in
Separation Logic. We introduce its fundamental components
in Sec. 3.1. In Sections 3.2 and 3.3, we develop and apply specialised reasoning principles to solve the challenges outlined
previously in Sections 2.2 and 2.3, respectively.
3.1

Reasoning Principles for Rooted Trees

Core to Arboreta is Arboreta-P, a small collection of usefuldeﬁnitions and lemmas for pure reasoning about rooted (unlabelled and labelled) trees. The library provides a deﬁnitionof generic rooted trees, parametrised by a type parameter A,
which is the type of node data, shown in Fig. 7a. For convenience, we keep using tree as the type name of trees.
Expansion. One of the core deﬁnitions is the expansion
function, which, when applied to an algebraic tree tr, returns
a list containing all the subtrees of tr. Fig. 7b shows its
deﬁnition, and three derived deﬁnitions, for the size of atree, the subtree relation, and the list of node data. Sincea bijection exists between nodes and subtrees, expansion
serves as a building block for other deﬁnitions, e.g., NoDupId.

CPP ’24, January 15–16, 2024, London, UK

Qiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur, and Ilya Sergey

Fixpoint locate tr pos : option tree := (* ... *)Fixpoint locate_update tr (pos : list nat) new : tree :=match pos with| nil => new| x :: pos' => let 'Node a chn := tr in(a) Rooted trees and getters.
match nth_error chn x with|
Some ch =>Fixpoint expand tr : list tree :=Node a (upd_nth x chn (locate_update ch pos' new))let 'Node a chn := tr in tr :: (flat_map expand chn).
|
None => trDefinition size tr : nat := length (expand tr).
end
Definition subtr tr1 tr2 : Prop := In tr1 (expand tr2).
Definition data_list_of tr : list A := map data_of (expand tr). end.
Parameter A : Type.
Inductive tree : Type := Node (a : A) (chn : list tree).
Definition data_of tr := let 'Node a _ := tr in a.
Definition chn_of tr := let 'Node _ chn := tr in chn.

(e) Using node coordinates to update subtrees. nth_error(ℓ, 𝑥) returns Some(ℓ [𝑥]) if 𝑥 < |ℓ | and None otherwise. upd_nth(𝑥, ℓ, 𝑎)
returns the resulting list obtained by updating ℓ [𝑥] to 𝑎.

(b) Expansion and derived deﬁnitions.
Parameters (B : Type) (id_of_data : A -> B).
Definition id_of tr : B := id_of_data (data_of tr).
Definition id_list_of tr : list B := map id_of (expand tr).
Definition NoDupId tr : Prop := NoDup (id_list_of tr).

Inductive prefix : tree -> tree -> Prop :=prefix_intro : forall a chn chn_sub prefix_chn,subseq chn_sub chn ->Forall2 prefix prefix_chn chn_sub ->prefix (Node a prefix_chn) (Node a chn).
Lemma prefix_data_is_subset tr1 tr2 (Hpref : prefix tr1 tr2):
subseq (data_list_of tr1) (data_list_of tr2).

(c) Deﬁnitions related to node identiﬁers.
Parameter (B_eqb : B -> B -> bool).
Definition has_same_id x tr := B_eqb (id_of tr) x.
Definition find_node x tr : option tree :=find (has_same_id x) (expand tr).

(f) Deﬁnition of tree preﬁx and one of its property. Forall2(𝑃, ℓ1, ℓ2 )holds iﬀ |ℓ1 | = |ℓ2 | and ∀𝑖, 𝑃 (ℓ1 [𝑖], ℓ2 [𝑖]). subseq(ℓ1, ℓ2 ) holds iﬀ ℓ1
is a subsequence of ℓ2 .

(d) Deﬁnition of node ﬁnding function. B_eqb is a binary booleanfunction for checking whether two terms of type B are equal or not.

Fig. 7. Main Coq deﬁnitions from Arboreta-P.
Node identiﬁers. As the type of node data is parameterised, we also parameterise the type of node identiﬁers
into B, as shown in Fig. 7c. id_of_data extracts the node
identiﬁer from a node’s data, and id_of extracts it from anode. NoDupId is deﬁned in terms of expansion and id_of.

3.2

Dual Views: From Array to Tree and Back Again

Recall that in Sec. 2.2, we encountered the need to reason
about trees in a structure-aware fashion, and envisioned an
inductively deﬁned tree view predicate to be used as an alternative to the array view, in order to reason with ease about
structure-changing operations. In this section, we (a) derive
the tree view predicate from the array view one, (b) exploit
the tree view to apply local reasoning principles, and ﬁnally(c) shift back to the array view. In other words, we workthrough the (general) way to apply the following rule of consequence, and showcase it on move_first_child from Fig. 5:

Finding by identiﬁer. When identiﬁers come equippedwith decidable equality (e.g., natural numbers), Arboreta-P
provides a function find_node(x, tr) for ﬁnding the subtreeof tr whose root has identiﬁer x, as shown in Fig. 7d.
Node coordinate. We can assign a unique coordinate toeach node in the tree. A coordinate or position describes
how to ﬁnd that node from the root in a top-down manner,and can be represented in Coq as a list of natural numbers
storing a child index to visit at each level. We deﬁne a locate
function to access a node by coordinate (the deﬁnition istrivial and elided), and a locate_update function to replace
the subtree at a given coordinate, as shown in Fig. 7e.

𝑃 arr ⊢ 𝑃 tree

{𝑃 tree } 𝑐 {𝑄 tree }𝑄 tree ⊢ 𝑄 arr{𝑃arr } 𝑐 {𝑄 arr }3.2.1 From Array View to Tree View. As a reminder,
the representation predicate of an array is typically deﬁned
as a collection of contiguous memory blocks, as follows:3

Tree preﬁx. We say that a rooted tree tr 1 is a preﬁx of tr 2
if tr 1 is a subgraph of tr 2 and both trees have the same root.
This deﬁnition is encoded by the inductive predicate from
Fig. 7f, along with a custom induction principle (not shown).
With such an abstract deﬁnition, we can prove properties of
preﬁxes in Arboreta-P, and then prove that the trees returnedby the (possibly complicated) functions we want to verify
are preﬁxes. For instance, we use the prefix_data_is_subset
property in the tree clock case study (cf. Sec. 4).

arr(𝑝, ℓ) ≜∗ 𝑝 + 𝑖 × sizeof(𝑇 ) ↦→ ℓ [𝑖] (ArrDef)𝑖 ∈ [0,|ℓ | )where 𝑇 is the type of the payload and sizeof(𝑇 ) denotes
how much space the payload occupies in memory. Since theseparating conjunction ∗ is commutative and associative, we
can reorganise the memory blocks in the array according
3 In practical SL frameworks, the right-hand side may come with side-

conditions, such as p != NULL. We omit them to simplify the presentation.

50

Rooting for Eﬀiciency: Mechanised Reasoning about Array-Based Trees in Separation Logic

to the tree’s structure, and inductively deﬁne the tree view
predicate tree_reptree as follows:

3.2.3 From Tree View to Array View. Thus far, we havedeﬁned the tree view predicate and shown how to obtain it
from the array view predicate. However, in practice, the array
view predicate is independently useful for reasoning about
read-only operations, especially random array accesses. Thisutility may stem from specialised support provided by veriﬁcation tools for handling array operations, for instance. To
this end, a natural question could be whether we are able toswitch between the array view and the tree view on demandso as to enjoy the best parts of both views.
The answer is aﬃrmative. From the deﬁnition ArrDef,
we can prove the following entailment, which “reconstructs”
an array from contiguous memory blocks, by induction on
𝑛. Here, 𝑛 is a natural number and the type of 𝑓 is N → 𝑇 .

treelist_reptree (nil, par, p) ≜ emp
treelist_reptree (Node(id, val, chn) :: trs, par, p) ≜p + id × sizeof(𝑇 ) ↦→ payload(val, par, hid(trs), hid(chn)) ∗treelist_reptree (chn, id, p) ∗ treelist_reptree (trs, par, p)
tree_reptree (p, tr) ≜ treelist_reptree (tr :: nil, −1, p)

where hid is deﬁned in Sec. 2 before Sec. 2.1. Noting thesimilarity to the previously deﬁned list-based tree_reparr (1),
we can prove the following entailment by induction on tr:∗𝑖 ∈ids(tr ) 𝑝 + 𝑖 × sizeof(𝑇 )∗ ⌈tree_proj(tr, ℓ)⌉⊢ tree_reptree (p, tr)(MemBlksToTree)
where ids is a shorthand of id_list_of from Fig. 7c. Therefore, given tree_reparr (𝑝, tr), we can obtain the tree representation tree_reptree (p, tr) by ﬁrst unfolding arr by ArrDef
and then apply MemBlksToTree. We then combine the two
steps together and get the following:∗𝑖 ∈ [0,𝑛) 𝑝 + 𝑖 × sizeof (𝑇 ) ↦→ 𝑓 (𝑖) ⊢∃ℓ, ⌈(∀𝑖 ∈ [0, 𝑛), ℓ [𝑖] = 𝑓 (𝑖)) ∧ |ℓ | = 𝑛⌉ ∗ arr(𝑝, ℓ)(ArrIntro)

And since the tree view predicate can be also regarded as abunch of memory blocks, we can prove by induction on trthat it can be “shattered” into memory blocks whose content
is speciﬁed by a function from identiﬁers to payload:

tree_reparr (𝑝, tr) ⊢𝑖 ∈rem(tr,|ℓ | ) 𝑝 + 𝑖 × sizeof(𝑇 ) ↦→ ℓ [𝑖] ∗ tree_reptree (𝑝, tr)(ArrToTree)
where rem(tr, |ℓ |) ≜ [0, |ℓ |) \ ids(tr) contains the “remaining” memory blocks, i.e., the allocated array indices not usedby the tree. If the size of tr is |ℓ |, i.e., rem(tr, |ℓ |) is empty, ArrToTree simpliﬁes to tree_reparr (p, tr) ⊢ tree_reptree (p, tr).

∗tree_reptree (𝑝, tr) ⊢∃𝑓 , ⌈∀ℓ, (∀𝑖 ∈ ids(tr), ℓ [𝑖] = 𝑓 (𝑖)) =⇒ tree_proj(tr, ℓ)⌉ ∗∗𝑖 ∈ids(tr ) 𝑝 + 𝑖 × sizeof(𝑇 ) ↦→ 𝑓 (𝑖)(TreeToMemBlks)
Finally, by gathering the payloads with indices in rem(tr, |ℓ |),we can reconstruct the array view from the tree view:∗

3.2.2 Local Reasoning with Tree View. Let us deﬁne′ (4):′
in a way similar to tree_reparr
the predicate tree_reptree′ (𝑝, Node(𝑖𝑑, 𝑣𝑎𝑙, 𝑐ℎ𝑛), 𝑝𝑎𝑟, 𝑠𝑖𝑏) ≜tree_reptree
𝑝 + 𝑖𝑑 × sizeof(𝑇 ) ↦→ payload(𝑣𝑎𝑙, 𝑝𝑎𝑟, 𝑠𝑖𝑏, hid(𝑐ℎ𝑛)) ∗treelist_reptree (𝑐ℎ𝑛, 𝑖𝑑, 𝑝)

CPP ’24, January 15–16, 2024, London, UK𝑖 ∈rem(tr,|ℓ | ) 𝑝 + 𝑖 × sizeof (𝑇 ) ↦→ 𝑓 (𝑖) ∗ tree_reptree (𝑝, tr)⊢ tree_reparr (𝑝, tr)(TreeToArr)
Again, once rem(tr, |ℓ |) is empty, TreeToArr simpliﬁes
to tree_reptree (p, tr) ⊢ tree_reparr (p, tr). In this case, we
can switch “seamlessly” between the two views using ArrToTree and TreeToArr.

(5)

Using the properties of the magic wand [6], we can reﬂect themodiﬁcations to the functional tree made by locate_update(Fig. 7e) onto the heap state, expressing this by the following
entailment, which can be proved by induction on pos:

3.2.4 Dual Views in Action. The ability to switch between the array and tree views allows for relatively straightforward veriﬁcation of move_first_child from Sec. 2.2 against
the speciﬁcation (3). To do so, we ﬁrst express the local modiﬁcations via locate_update. For example, prepending a child
ch to a speciﬁc node of tr can be implemented as follows,when given the coordinate pos of that node inside tr:′ (𝑝, tr, par, sib)⌈locate(tr, pos) = Some(sub)⌉ ∗ tree_reptree⊢′ (𝑝, sub, par ′ , sib′ ) ∗∃par ′, sib′, tree_reptree∀sub′, id_of(sub) = id_of(sub′ ) =⇒©  ª®
′ (𝑝, sub′ , par ′ , sib′ ) −∗­tree_reptree­®
′ (𝑝, locate_update(tr, pos, sub′ ), par, sib)
tree_reptree«¬

prepend_child(tr, ch) ≜locate_update(tr, pos, Node(𝑎, ch :: chn))(WandFrameUpdate)
The entailment in WandFrameUpdate might look a bit intimidating, but the only thing it does is instantiating theanalogue of the “modus ponens” rule for ∗/−∗, “pulling out”
′ (𝑝, sub′ , par ′ , sib′ ) assertion. Note that Wandthe tree_reptree
FrameUpdate allows “pulling out” only a single subtree ata time, which is nevertheless suﬃcient for our veriﬁcation
task about tree clock. We will discuss this limitation in Sec. 5.

where we let locate(tr, pos) be Some(Node(𝑎, chn)). We canimplement popping the ﬁrst child analogously. After thoseinstantiations, we can then switch from the array view inthe precondition to the tree view via ArrToTree, apply
WandFrameUpdate to reason about the aﬀected local part,and ﬁnally recover the original array view via TreeToArr.

51

CPP ’24, January 15–16, 2024, London, UK

Qiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur, and Ilya Sergey

Current stack top: 3

2

Visited part

1

split throughthe pathfrom 1 to 3

3

4

5

adding 3
to thevisited part1
2

new Visited part

3

3

4

5

6

1

6

4

5

6

Fig. 8. Splitting a tree vertically wrt. the node 3.
Fixpoint vsplit (full: bool) tr (pos: list nat) : tree :=let 'Node a chn := tr inmatch pos with| nil => Node a (if full then chn else nil)
| x :: pos' =>match nth_error chn x with| Some ch =>let chn' := vsplit full ch pos' :: drop (S x) chn in
Node a chn'
| None => Node a nil
end
end.

3.3 Loop Invariants for Non-Recursive Traversals
As the last component of Arboreta we present an approachfor stating loop invariants to verify non-recursive tree traversals similar to that of copyval_and_move from Fig. 4a. Recall
that the solution hinted at the end of Sec. 2.3 was to explicitly characterise the “visited part” of the tree in the loop
invariant, relating it to the contents of the explicit stack.
In such traversals, at the beginning of each iteration of
the outer while-loop, the visited part is likened to the “righthalf” of the tree obtained by “splitting” the original tree
along the path from the root down to the node that will beprocessed in the current iteration (i.e., the node at the topof the stack; represented by x in Fig. 4a, for example), which
we refer to as the stack top node hereafter. After completing
the iteration, the stack top node will belong to the visitedpart in the loop invariant. This process is depicted in Fig. 8
with regard to the “working” node 3. As we will soon see,a visited part must be a preﬁx of the original tree (in thesense of the deﬁnition from Fig. 7f), so we will refer to it as
the visited preﬁx. In addition, we name the visited preﬁx atthe beginning/end of the iteration as the pre/post-iteration
visited preﬁx, respectively.
In the remainder of this subsection, we will walk throughthe intuition of formalising the idea of splitting the tree along
the path, showing how it leads to an extensible invariant definition for non-recursive traversals, and demonstrating theutility of that deﬁnition to verify the program from Fig. 4a.

Lemma vsplit_is_prefix : forall full tr pos,prefix (vsplit full tr pos) tr.

(a) Deﬁnition and lemma of vertical tree splitting.
Definition post_iter_visited_prefix tr pos : tree :=vsplit false tr pos.
Definition rsibpos (pos : list nat) : list nat :=match rev pos with nil=> nil| x :: pos' => rev ((S x) :: pos') end.
Lemma vsplit_norsib : forall tr pos, locate tr pos = None ->vsplit false tr pos = vsplit false tr (removelast pos).
Definition pre_iter_visited_prefix tr pos : tree :=vsplit (isSome (locate tr (rsibpos pos))) tr (rsibpos pos).

(b) Deﬁnitions of pre/post-iteration visited preﬁxes. When computing the pre-iteration visited preﬁx, the value of full depends onthe existence of the right sibling of the node at pos. Note that if theright sibling does not exist, then by vsplit_norsib, the computed
result will be equal to the post-iteration visited preﬁx applied to thecoordinate of the parent node, namely (removelast pos).

3.3.1 Vertical Tree Splitting. Fig. 9a provides the deﬁnition of a function for splitting the tree vertically wrt. agiven node, which is represented by its position. The function vsplit(full, tr, pos) returns the part “on the right”
after splitting tr wrt. the node at pos, whose children will be
included in the result iﬀ full is true (see the ﬁrst branch ofmatch pos with in the deﬁnition of vsplit).
We can now use vsplit to deﬁne post-iteration visited
preﬁx for a traversal loop. As an example, let us take tr tobe the tree in the leftmost part of Fig. 8. Then the coordinateof the node 3 in tr is pos3 = [1], and we can check that

Fig. 9. Coq deﬁnitions related with vertical tree splitting.

the result of vsplit(false, tr, pos3 ) is the post-iteration
visited preﬁx shown in the rightmost part of Fig. 8.
Even though the function vsplit is deﬁned to produce thepost-iteration visited preﬁx, it can also be used to obtain the
pre-iteration visited preﬁx: the pre-iteration visited preﬁx
is exactly the post-iteration visited preﬁx after “subtracting”

52

Rooting for Eﬀiciency: Mechanised Reasoning about Array-Based Trees in Separation Logic2

pos =[2]full =false

pos =[2,1]full =false

pos =[2,0]full =true

1

1

1

3

5

2

2

4

6

3

2

4

5

6

3

pos= [1]full =true

pos =[1,0]full =true

finish

1

1

1

3

5

2

4

6

3

5

2

4

6

3

Fixpoint worklist tr pos : (list (list nat)) * (list tree) :=let 'Node a chn := tr inmatch pos with| nil => (nil, nil)
| x :: pos' =>match nth_error chn x with| Some ch =>let (res1, res2) := worklist ch pos' in(map (fun i => i :: nil) (seq 0 x) ++map (fun l0 => x :: l0) res1, take x chn ++ res2)| None =>(map (fun i => i :: nil) (seq 0 (length chn)), chn)
end
end.

4

5

6

Fig. 11. Retrieving a worklist given a tree tr and a node
position pos in it. The auxiliary function seq(n, m) returns
a list of natural numbers [n; n+1; ...; m-1].

4

5

CPP ’24, January 15–16, 2024, London, UK

6

is deﬁned as an inductive Coq predicate in Fig. 12 and isparameterised by the tree tr being traversed. It relates assisting stack (captured in its ﬁrst index of type list B) and thepre-iteration visited preﬁx (i.e., its second index of type tree).
In order to use the cornerstone invariant, one has to assume
that the root has been visited before the loop begins and thatits children nodes are in the assisting stack at the start of theloop. In practice, this is almost always the case, and it is thecase for all the operations of tree clocks (cf. Sec. 4).
During a loop iteration where the assisting stack is not
empty, according to the TInv_intermediate case in Fig. 12,
the stack top node (i.e., the root of sub) will be popped, andits children nodes will be pushed into the stack before theiteration ends.4 The lemma in Fig. 12 serves to re-establish
the invariant at the end of the iteration.
A notable feature of this pure loop invariant is its extensibility: it characterises only the core components of nonrecursive traversal, thereby granting users the ﬂexibility touse it in conjunction with other invariants. In particular, one
can use this loop invariant as the cornerstone of a “larger”
loop invariant speciﬁc to a concrete non-recursive traversal. At a high-level, any such larger loop invariant can beconstructed using the following invariant template:Fig. 10. Tree traversal and vertical splitting.
the stack top node. It turns out that this deﬁnition of the
pre-iteration visited preﬁx coincides with the result obtainedby vsplit using the coordinate of the right sibling (or theparent, if the right sibling does not exist) of the stack top
node. Moreover, the coordinate of the right sibling of a node
can be calculated from the node’s own coordinate via thefunction rsibpos in Fig. 9b.
We summarise the formal deﬁnitions of pre/post-iteration
visited preﬁxes in Fig. 9b, from which we know that they areindeed tree preﬁxes by the lemma vsplit_is_prefix. Fig. 10
depicts a sequence of steps showing how the non-recursive
traversal progresses. Each subﬁgure snapshots the state at
the start of the corresponding loop iteration. The portion
encircled by red dashed line indicates the pre-iteration visited
preﬁx, and a node surrounded by blue dashed line denotes
the stack top node with pos being its coordinate. Readers areinvited to validate the deﬁnitions from Fig. 9b by using thepos and full in each subﬁgure.
3.3.2 Retrieving Stack Contents. Perhaps surprisingly,
by understanding the nature of the traversal, it becomes
possible to fully retrieve the contents of the assisting stackfrom the algebraic tree description of the stack top node. The
deﬁnition of a function worklist doing exactly that is given
in Fig. 11. The function returns a list of subtrees (the second
component of its return value) in addition to the coordinatesof their roots (the ﬁrst component of its return value). By
applying worklist on the coordinate of the stack top node,
the contents of the assisting stack can be then recoveredfrom the root identiﬁers of the returned list of subtrees. The
list of coordinates will be used later in Sec. 3.3.3.

loopinv(tr, 𝑝) ≜ ∃ stk, pf ,⌈traversal_invariant(tr, stk, pf ) ∧ · · · ⌉ ∗tree_reparr (𝑝, tr),where tr is the tree being traversed. We phrase the templateusing the array view predicate, since the structure of theoriginal tree tr is usually not changed during traversal, andthe contents of tr are retrieved via random accesses.
3.3.4 Traversal Invariant in Action. We conclude ourpresentation of Arboreta by revisiting the veriﬁcation challenge posed by the copyval_and_move function from Fig. 4a.

3.3.3 The Cornerstone Loop Invariant. At last, we cometo present a recipe for stating loop invariants to verify nonrecursive traversals using the cornerstone invariant, which

4 To align with the array-based stack implementation, in this invariant thelist-based stack has its entry/exit point at the tail position.

53

CPP ’24, January 15–16, 2024, London, UK

Qiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur, and Ilya Sergey

Inductive traversal_invariant tr : list B -> tree -> Prop :=| TInv_terminate : traversal_invariant tr nil tr| TInv_intermediate : forall stk pos sub,locate tr pos = Some sub ->stk = (map id_of (snd (worklist tr pos) ++ (sub :: nil))) ->pf = pre_iter_visited_prefix tr pos ->traversal_invariant tr stk pf.
Lemma traversal_invariant_trans tr pos sub :locate tr pos = Some sub ->traversal_invariant tr(map id_of (snd (worklist tr pos) ++ chn_of sub))(post_iter_visited_prefix tr pos).

Fig. 12. An extensible loop invariant for non-recursive traversals. In the TInv_terminate case, the assisting stack isempty and the traversal terminates. The TInv_intermediatecase snapshots the stack content and the pre-iteration visited
preﬁx given the coordinate pos of the stack top node.

𝑇1 ⊔ 𝑇2= 𝜆𝑡 . max {𝑇1 (𝑡),𝑇2 (𝑡)}(LogicalJoin)

Likewise, the copy operation 𝐶 1 ·copy(𝐶 2 ) should update 𝐶 1
so that 𝐶 1 ·val = 𝑇2 after the operation is performed.
The vector clock [11, 23] is the traditional logical clock
data structure; it represents timestamp using an array, indexed by identiﬁers of threads. Join and copy operations forthe vector clock data structure take Θ(𝑘) time, where 𝑘 is
the number of threads in the execution. In the context ofdata race detection, for executions with many events, thiscan result in prohibitively signiﬁcant slowdowns. On theother hand, the tree clock internally organises timestamp hierarchically as a tree, where nodes in the tree correspond to
threads. Join and copy operations on trees are implemented
through tree traversals, and tree’s hierarchical structure allows for pruning of the traversal, which is the key to its
optimal time complexity.
Formally deﬁned, a tree clock is a tuple TC = (tr, ThrMap),
where tr is a tree such that every node 𝑛 in the tree is a tuple𝑛 = (𝑡, c, ac, p, ch, rs), where thread identiﬁer 𝑡, clock c, andattached clock ac are scalar ﬁelds, while parent p, head child
ch, and right sibling rs are pointer ﬁelds to other nodes in
tr. Every node except tr’s root has an attached clock; for tr’s
root, its attached clock is undeﬁned and thus marked as ⊥.
Intuitively, the thread at the root of tr “owns” the tree clock
instance. Node 𝑛 1 is a child of 𝑛 2 if the root thread was “madeaware of” the thread 𝑛 2 ·𝑡 (using a message/synchronisation
operation 𝑚) via 𝑛 1 ·𝑡, and the attached clock 𝑛 2 ·ac is theclock of 𝑛 2 ·𝑡 when this message 𝑚 arrived at 𝑛 1 ·𝑡. Therefore,
for each node 𝑛, the attached clocks of its children should
be no more than 𝑛·c. Moreover, its children are arranged indecreasing order of their attached clocks, which facilitatespruning during traversal. ThrMap(𝑡) identiﬁes the uniquenode 𝑛 in tr with identiﬁer 𝑡 and serves as the timestamp.
We provide the visual representation of two exemplary treeclock instances TC 1 and TC 2 in Fig. 15.
In this paper, we focus on formalising and verifying thejoin operation of array-based tree clocks. For eﬃciency in
an intensive application like data race detection, the tree

The proof of its SL speciﬁcation with regard to a functionalreference implementation 𝑓 can be completed by instantiating the invariant template as follows:∃stk, pf ,⌈traversal_invariant(tr 2, stk, pf ) ∧ tr 1′ = 𝑓 (tr 1, pf ) ∧ · · · ⌉ ∗tree_reparr (𝑝 tree, tr 1′ ) ∗ tree_reparr (𝑝 tree2, tr 2 )4 Verifying the Tree Clock Data StructureThis section showcases the deﬁnitions and techniques ofArboreta working in tandem for verifying a large case study:
an executable C implementation the tree clock structure [22].
4.1

variant, achieves optimal asymptotic complexity in performing clock operations by novelly exploiting the hierarchicalstructure of tree.
A logical clock can be regarded as an abstract data typewhich exposes its maintained timestamp and usually supports two clock operations: join and copy. When implemented
in an imperative language, the timestamp is typically mutable, and the two operations work by modifying the timestamp stored in one of the two operands (i.e., they are in-place
operations). For an instance 𝐶 of a logical clock, we use 𝐶·val
to denote the timestamp that 𝐶 points to. Let 𝐶 1 and 𝐶 2 be
two instances of a logical clock initially pointing to timestamps 𝑇1 and 𝑇2 respectively. The in-place join operation
𝐶 1 ·join(𝐶 2 ) should update 𝐶 1 so that 𝐶 1 ·val = 𝑇1 ⊔ 𝑇2 ,where ⊔ denotes the logical join over timestamps:

Tree Clocks: A Primer

Dynamic analysis is a de facto preferred method for detecting concurrency bugs such as data races in multi-threaded
programs. Dynamic data race detectors such as ThreadSanitizer [33] and FastTrack [12] observe events of an
execution during runtime, infer the happens-before (HB) partial order [18] between them and report conﬂicting events
unordered by HB to be in a data race. These detectors play avital role in revealing data races which may lead to critical
failures in large software systems and have been extensively
applied in industrial settings.
Instead of explicitly constructing the HB partial order asa graph of events, such tools leverage time-stamping to implicitly infer the HB partial order. Analyses such as data race
detectors maintain logical clock data structures to computethe timestamp of each event accurately, potentially performing clock operations at every event. A timestamp is a mapping from the identiﬁers of threads to their respective (local)
clocks (represented by natural numbers), and the HB relation between events can be recovered by comparing theirtimestamps. Tree clock [22], a recently proposed logical clock54

Rooting for Eﬀiciency: Mechanised Reasoning about Array-Based Trees in Separation Logic
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25

Parameter thread : Type.
Record tc_nodedata : Type :=mkTCdata { tid : thread; clk : nat; aclk : nat }.
Definition treeclock : Type := tree tc_nodedata.

struct Clock { int clock_clk, clock_aclk; };struct TreeClock{int dim, root_tid, top, *S; // S: assisting stack
struct Clock* clocks;
struct Node* tree;};
void join(struct TreeClock* TC2, struct TreeClock* TC1){// ...
while (TC2->top >= 0){
int v_tid = TC2->S[TC2->top--];struct Clock* uprime_clocks = &(TC1->clocks[v_tid]);
struct Node* u_node = &(TC2->tree[v_tid]);
struct Clock* u_clocks = &(TC2->clocks[v_tid]);
int u_clock = u_clocks->clock_clk;
if (!node_is_null(u_node)){detach_from_neighbors(TC2, v_tid, u_node);}
u_clocks->clock_clk = uprime_clocks->clock_clk;
u_clocks->clock_aclk = uprime_clocks->clock_aclk;
struct Node* uprime_node = &(TC1->tree[v_tid]);
int y = uprime_node->node_par;push_child(TC2, y, v_tid, u_node);
get_upd_nodes_join_chn(TC2, TC1, v_tid, u_clock);}}(a) Functional model of the tree part of tree clock.
Definition getClock t tc :=match find_node t tc with| Some res => (data_of res).(clk) | _ => 0 end.

(b) Functional model of the timestamp maintained by tree clock.
Fixpoint getUpdatedNodesJoin tc tc' : treeclock :=let fix aux tc clk chn : list treeclock :=match chn with| nil => nil| tc' :: chn' =>
let: Node (mkTCdata v' clk_v' aclk_v') chn_v' := tc' in
if clk_v' <=? (getClock v' tc)
then (if aclk_v' <=? clk
then nil else (aux tc clk chn'))else (getUpdatedNodesJoin tc tc') :: (aux tc clk chn')
end inlet: Node data_u' chn_u' := tc' inNode data_u' (aux tc (getClock data_u'.(tid) tc) chn_u').
Fixpoint detachNodes pf tc : treeclock * list treeclock :=let: Node data chn := tc in
let: (chn', res) :=List.split (map (detachNodes pf) chn) in
let: (res', chn'') := List.partition(fun tc' => isSome (find_node (id_of tc') pf)) chn' in(Node data chn'', (List.concat res) ++ res').

Fig. 13. Fragment of join code and related struct deﬁnitions.

clock data structure is implemented using arrays instead of
explicit pointers. In this case, the join of a tree clock TC 1
into TC 2 (TC 2 ·join(TC 1 )) is performed by traversing TC 1
and updating the corresponding nodes in TC 2 , in which thetraversal is loop-based with the assistance of a stack. We
show a snippet (in C) of the join operation on array-based
tree clocks in Fig. 13.
4.2

CPP ’24, January 15–16, 2024, London, UK

Fixpoint attachNodes forest tc' : treeclock :=let: Node data_u' chn' := tc' inlet: u_pre := find (has_same_id data_u'.(tid)) forest in
let: chn_u := (match u_pre with Some u => chn_of u| None => nil end) in
Node data_u' ((map (attachNodes forest) chn') ++ chn_u).

Tree Clocks in Coq, Functionally

Definition corejoin (tc pf : treeclock) : treeclock :=let: (Node data_z chn_z, forest) := detachNodes pf tc in
let: Node (mkTCdata w clk_w _) chn_w :=attachNodes forest pf in
Node data_z((Node (mkTCdata w clk_w data_z.(clk)) chn_w) :: chn_z).

We start our tree clock mechanisation by developing its
reference implementation in Gallina, the pure functional
programming language of Coq. We will then use it in Hoarestyle speciﬁcations to connect the reference implementation
with the C code, following the relatively conventional twolayer paradigm for verifying imperative programs [3].

Definition join (tc tc' : treeclock) : treeclock :=let: mkTCdata z' clk_z' aclk_z' := data_of tc' in
if clk_z' <=? (getClock z' tc)
then tc else (corejoin tc (getUpdatedNodesJoin tc tc')).

4.2.1 Datatypes. In Fig. 14a, we model the tree part of
the tree clock as the generic functional RLT in Sec. 3.1 withthe type parameter A instantiated to be the following record
type and the type parameter B instantiated to be thread. The
id_of_data is thereby set to be the tid getter of the record.
Here thread is also a type parameter and will be instantiatedas natural numbers in proving the imperative join operation. Note that compared with the axiomatic deﬁnition ofa node (i.e., deﬁning a node as a tuple), the data held bya treeclock node does not contain the pointer ﬁelds: it is
implicitly captured in the functional RLT structure.
We model ThrMap via the function find_node introducedin Sec. 3.1, and the timestamp from a tree clock (i.e., the(c) Functional version of the tree clock join operation.

Fig. 14. Tree clock operations deﬁned in Coq.
mapping from the identiﬁer of a thread to its clock value)
can be further expressed as getClock funciton in Fig. 14b.
4.2.2 Operations. In the original tree clock presentation,
the join operation builds upon three auxiliary operations:
getUpdatedNodesJoin, detachNodes, and attachNodes. Allof them are modelled as recursive functions on tree clocks

55

CPP ’24, January 15–16, 2024, London, UK

T4
23,18

TC1

TC2

TC2’ = TC2.join(TC1)

T1
16, ⊥

T8
25, ⊥

T8
25, ⊥

T3
17,7

T2
20,9

T5
4,14

T6
15,8

T8
8,7

T10
2,15

Qiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur, and Ilya Sergey

T5
8,20

T9
10,4

T7
24,16

T1
4,4

T7
11,2

T9
10,4

T4
31,20

T3
10,2

T2
14,9

T6
15,8

T10
2,15

T2
20,9

T4
32,18

T1
16,25

T5
8,20

T3
17,7

T9
10,4

T7
24, 16

T6
15,8

T10
2,15

Fig. 15. Illustrative example of joining TC 1 into TC 2 . Each node is annotated with its thread identiﬁer, its clock and attachedclock (e.g., for node 𝑡 2 on TC 1 its clock is 20 and its attached clock is 9). The portion encircled by the blue dashed line is the
portion of TC 1 returned by getUpdatedNodesJoin(TC 2, TC 1 ) (denoted as pf ) such that a thread identiﬁer 𝑡 appears in pf if andonly if getClock(TC 2, 𝑡) < getClock(TC 1, 𝑡). And pf is a preﬁx of TC 1 . detachNodes(pf , TC 2 ) partitions TC 2 into a “pivot” tree
(encircled by the green dashed line) and a list of trees (denoted as forest, here containing the trees encircled by the red dashedlines), such that (1) for every tree in forest, its root thread identiﬁer appears in pf and no other thread identiﬁer appearing in
pf also appears in that tree; (2) the pivot tree is a preﬁx of TC 2 and does not contain any thread identiﬁer appearing in pf .
After that, attachNodes(forest, pf ) “attaches” all the trees in forest to pf by matching the root thread identiﬁers in forest; theresulting tree is the one surrounded by red and blue dashed lines in TC 2′ . Finally, the result of join TC 2′ is given by making theresult of attachNodes be the ﬁrst child of the root of the pivot tree.
and presented in Fig. 14c. To streamline the proof of theimperative join, we model the core part of join into corejoin,with join, the actual functional join operation, being its wrapper (cf. Fig. 14c). While the imperative join TC 2 ·join(TC 1 )modiﬁes TC 2 into another tree clock TC 2′ , the corresponding
functional join, i.e. join(TC 2, TC 1 ), just returns TC 2′ . Fig. 15
shows a concrete example of execution of join(TC 2, TC 1 ).

The proof of this fact closely depends on the property of
getUpdatedNodesJoin(TC 2, TC 1 ) and the lemma from Fig. 7f.
4.3

Verifying the C Implementation

As the second step of our veriﬁcation task, we ascribe a
Hoare-style speciﬁcation phrased in terms of functional treeclock manipulations from Sec. 4.2, to the C implementation5
from Fig. 13 and prove that the speciﬁcation holds.

4.2.3 Predicates and Properties. We deﬁne several extrinsic predicates to ensure well-formedness of functional
tree clocks. Speciﬁcally, the predicate valid(TC) is a conjunction of NoDupId(TC) and the conditions in Sec. 4.1 that atree clock should satisfy. We also deﬁne the binary predicate respect(TC 1, TC 2 ) to be the conjunction of the directmonoticity and indirect monoticity, which are required in thefollowing proofs. Due to space limit, we omit its concrete
statement and refer interested readers to its provenance [22].
To guarantee that the functional tree clock implements theinterfaces of logical clock correctly, we need to prove that
LogicalJoin holds for the functional join operation. Withthe timestamp model from Fig. 14b, this can be phased as:

4.3.1 The C Implementation. The imperative tree clock
joining (cf. Fig. 13) is implemented as a non-recursive tree traversal with its control ﬂow similar that of copyval_and_movefrom Fig. 4a. Notably, the imperative implementation is nothing like its functional reference counterpart from Sec. 4.2. In
the functional join, the join is done step-by-step: we ﬁrst obtain the preﬁx getUpdatedNodesJoin(TC 2, TC 1 ) in one step,then accomplish all the subtree detaching in another step,and ﬁnally do all the attaching. In the imperative version,
however, we will detach and attach a single subtree in an
iteration during the non-recursive traversal of that preﬁx;
the join is done only after ﬁnishing the traversal.

∀TC 1, TC 2, valid(TC 1 ) ∧ valid(TC 2 ) ∧ respect(TC 1, TC 2 ) =⇒∀𝑡, getClock(𝑡, join(TC 2, TC 1 )) =5 The C implementation of the tree clock is translated from the (unveriﬁed)
Java implementation accompanying the original paper [22].

max {getClock(𝑡, TC 1 ), getClock(𝑡, TC 2 )}56

Rooting for Eﬀiciency: Mechanised Reasoning about Array-Based Trees in Separation Logic

CPP ’24, January 15–16, 2024, London, UK

Table 2. Evaluation: array-based v. pointer-based tree clocks

Table 1. Rounded formalisation sizes in lines of Coq code.
Arboreta

Case Study

Total

1

2

3

4

5

6

Pure
VST

1,300
1,400

3,200
2,000

4,500
3,400

Trace len.

num.

Avg. len.

Ptr. TC (s)Arr. TC (s)Speedup

Total

2,700

5,200

7,900

(0M, 60M](60M, 112M](112M, 136M](136M, 215M](215M, 1B]

35
24
29
29
29

0.14M
102M
125M
169M
391M

0.22
162.27206.57222.36657.230.16
115.32147.22190.72463.32

1.25×
1.41×
1.40×
1.17×
1.42×

Total

146

31.41

48.90

36.10

1.35×

4.3.2 Speciﬁcation of the Imperative Join. The speciﬁcation of the imperative join is given by the following Hoare
triple, where 𝑝 1, 𝑝 2 is the pointer to TC 1, TC 2 respectively:

4.4

Proof Eﬀort

The quantitative data about our veriﬁcation eﬀorts is given
in Tab. 1. The implementation of Arboreta includes purefacts about array-based trees (Sec. 3.1) and separation logic
facts about dual views (Sec. 3.2) and amounts to 2.7 kLOC of
Coq. The formalisation of tree clocks includes the functionalreference speciﬁcation (Sec. 4.2) as well as specs and proofs
for C code (Sec. 4.3), totalling at 5.2 kLOC of Coq.
The size of the veriﬁed C codebase, not included into thestatistics in Tab. 1, is around 150 lines of code.

{tree_reparr (𝑝 2, TC 2 ) ∗ tree_reparr (𝑝 1, TC 1 ) ∗ ⌈· · · ⌉}join (𝑝 2, 𝑝 1 ){𝜆_.tree_reparr (𝑝 2, join(TC 2, TC 1 )) ∗ tree_reparr (𝑝 1, TC 1 )}where the pure assertion in the precondition is almost thesame one as required by TC 1 and TC 2 in Sec. 4.2.3, except
for some additional numeric conditions required by VST.
4.3.3 Loop Invariant and Proof Outline. The most interesting part of the proof is the invariant for while-loop
at lines 9–23 of Fig. 13. Following the strategy outlined inSec. 3.3.3, we instantiate the invariant template as follows:

4.5

Evaluation and Benchmarks

To demonstrate the practical relevance of our veriﬁed C
implementation of array-based tree clocks, we incorporated
it inside a HB-based dynamic data race detector.
We evaluate the performance of our array-based implementation over the naïve but easier-to-mechanise pointerbased tree clocks. For a controlled evaluation, our data race
detector performs analysis on oﬄine traces logged a priori;
this ensures that both implementations work on the same
trace (for each benchmark program). Conceptually, the race
detector maintains a ﬁxed number of tree clocks, processes
events one by one, updates them at each event, and checks
for data races at every access event. Our benchmark suite isderived from prior work [22] and includes 146 traces from
diﬀerent concurrent C/C++ as well as Java applications. For
each trace, we measured the time taken by the race detection
analysis, using both the naïve pointer-based, as well as our
veriﬁed array-based tree clock implementations. Our evaluation was conducted on a 64-bit Red Hat Enterprise Linux 8.4
machine with a single CPU core and 256GB RAM.
In Tab. 2, we summarise the results of our evaluation. The
table aggregates the trace logs into 5 groups, dividing theentire set into roughly equal sets based on their lengths(number of events). Column 1 and Column 2 represent therange of trace lengths and the number of traces in each grouprespectively. Column 4 (resp. column 5) reports the (geometric) mean of the time taken by the analysis that uses thepointer-based (resp. veriﬁed array-based) tree clock implementation. Column 6 reports the (geometric) mean of theresulting speedup in each group; the speedup for a givenbenchmark is measured as the ratio of the time taken by the∃stk, pf ,traversal_invariant(getUpdatedNodesJoin(TC 2, TC 1 ), stk, pf )∧ TC 2′′ = corejoin(TC 2, pf ) ∧ · · ·∗ tree_reparr (𝑝 2, TC 2′′ ) ∗ tree_reparr (𝑝 1, TC 1 )That is, the traversal_invariant predicate from Fig. 12 isinstantiated with getUpdatedNodesJoin(TC 2, TC 1 ) as an argument. This is because during the imperative traversal, thetree preﬁx getUpdatedNodesJoin(TC 2, TC 1 ) is not fully visited, hence the invariant needs to “compensate” for this tomatch the functional reference implementation.
With the main complexity of the invariant factored out
as per the core proof principles of Arboreta, the rest of theproof posed little conceptual challenge. For example, thesubprocedure push_child is a structure-changing operation,
which can be modelled in the same way as has been demonstrated for prepend_child in Sec. 3.2.4. The proof is similar
for another subprocedure detach_from_neighbors (called atline 16 of Fig. 14c) that removes a child.
The last thing to note is the switch between array viewand tree view. When verifying the code in Fig. 14c, we keepusing the array view when “stepping through” at the lines
10–14 and deal with the random access. We then switch to
the tree view to handle the structure-changing subprocedures. At the line 23, we go back to the array view, since
get_upd_nodes_join_chn (a function used for traversing children nodes) also performs various random accesses.

57

CPP ’24, January 15–16, 2024, London, UK

Qiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur, and Ilya Sergey

pointer-based implementation and the array-based implementation. Overall, the array-based implementation oﬀers
a 35% speedup, thanks to the eﬃciency oﬀered by random
access in arrays. More importantly, now this fast implementation comes with a formal correctness proof!

We are not aware of any veriﬁed implementations of treeclocks, but we believe it should be possible to use our implementation from Sec. 4 as a veriﬁed drop-in replacement
for vector clocks in some of those systems. The reason we
could not do so immediately is the mismatch between the
logical foundations of our proofs and the existing implementations of data race detectors and CRDTs. For example, mostof the existing mechanised CRDT implementations [14, 26]
are veriﬁed in Iris [17], whose proofs are therefore not directly composable with ours in VST. Mansky et al.’s veriﬁed
version of FastTrack algorithm [12, 21] features a C implementation partially veriﬁed in VST. Unfortunately, its proof
relies on bespoke speciﬁcations of logical clock operations,making it diﬃcult to plug in our implementation “as-is”. We
leave these exercises in proof composition to the future work.

5 Related Work
Our work contributes to a large body of research on mechanically veriﬁed heap-based data structures and algorithms.
Tree manipulations in Separation Logic. Verifying recursive traversals of heap-based trees in SL (mechanised ornot) is considered a standard exercise and is featured in a
number of papers and teaching materials [8, 9, 27, 30]. Reasoning about arrays in SL is also a well-studied area, in which
many problems can be reduce to reasoning about lists [15].
To the best of our knowledge, relatively few works areconcerned with array-based tree representations. Barriére
speciﬁes B+ trees in VST by providing a representation predicate that facilitates proofs about traversals via heap induction, but is less convenient to reason about random accesses,
as is allowed by the array view in our approach [5].
As described in Sec. 3.2.2, our tree view enables the useof localised reasoning rules such as WandFrameUpdate,
which, however, is restricted to scenarios involving the manipulation of only one subtree at a time. Advanced techniques have been proposed to address the more complex
cases involving multiple subtrees [7] and we plan to integrate them into Arboreta in the future.
Reasoning about graphs in Separation Logic frequently
requires deﬁning a representation predicates similar to ourtree_rep [24, 34, 36]. Even though such predicates facilitate
certain kinds of inductive reasoning [16], they impose additional proof obligations related to non-interference between
recursive calls that can be caused by deep intrinsic sharing—such obligations would not be necessary for trees.
Our approach of formulating loop invariants for nonrecursive traversals is reminiscent of Charguéraud’s specialised rules for inductive reasoning about loops [8, §6], but
is tailored for array-based trees and the respective representation predicates. We do not exclude a possibility that suchloop invariants can be automatically derived from induction
hypotheses of equivalent recursive traversals, and we areplanning to investigate this research question in the future.

6 Conclusion and Future WorkIn this work, we have presented a principled methodology
for structuring proofs about manipulations with array-based
trees in Separation Logic (SL). We implemented the main
components of our approach in a Coq library called Arboreta
and showcased them on a large case study, verifying an arraybased tree structure used in real-world data race detectors.
While our current implementation is tied to the VST framework as a Coq embedding of Separation Logic, we believe,
the key ideas of our work can be transferred to other SL embeddings, such as CFML [8], HTT [25], and Iris [17] in a relatively straightforward way. Furthermore, our pure reasoning principles concerning RLTs, such as those delineated inArboreta-P (Sec. 3.1) and those associated with non-recursive
tree traversals (Sec. 3.3), should be adaptable to other theorem provers based on higher-order logic. In the future, weare planning to extend our case studies to other array-based
tree structures, such as AVL and B+ trees. We are also planning to integrate our veriﬁed implementation of tree clocks
into the veriﬁed data race detector by Mansky et al. [21].

Data Availability
The software artefact with a snapshot of the Coq and C developments accompanying this paper is available online [38].
It contains the source code of Arboreta, the tree clock casestudy, and the harness to reproduce the experimental resultswith the data race detector described in Sec. 4.5.

Acknowledgments

Reasoning about logical clocks. Tree clocks are a particular instance of logical clocks [18]: a family of data structuresthat are frequently used as a mechanism for reasoning aboutcausality of events in concurrent and distributed systems.
Mechanised implementations of a simpler version of logical clocks—vector clocks [11, 23]—are featured in several
existing eﬀorts on veriﬁed algorithms for dynamic data race
detection [21, 32, 37]. Veriﬁed vector clocks are also an important component of certiﬁed implementations of Conﬂict-free
Replicated Data Types (CRDTs) [14, 19, 20, 26].

We thank the anonymous CPP’24 reviewers for their constructive and insightful comments. We also thank Brigitte
Pientka and Sandrine Blazy for their eﬀorts as CPP’24 Programme Co-Chairs. This work was partially supported by a
Singapore Ministry of Education (MoE) Tier 3 grant “Automated Program Repair” MOE-MOET32021-0001, MoE Tier 1
grant T1 251RES2108 “Automated Proof Evolution for Veriﬁed Software Systems”, and MoE Tier 1 grant “Tree Data
Structures for Causal Orderings in Data Race Detection”.

58Rooting for Eﬀiciency: Mechanised Reasoning about Array-Based Trees in Separation Logic

References

CPP ’24, January 15–16, 2024, London, UK[21] William Mansky, Yuanfeng Peng, Steve Zdancewic, and Joseph Devietti.
2017. Verifying dynamic race detection. In CPP. ACM, 151–163. https://doi.org/10.1145/3018610.3018611[22] Umang Mathur, Andreas Pavlogiannis, Hünkar Can Tunç, and Mahesh
Viswanathan. 2022. A Tree Clock Data Structure for Causal Orderingsin Concurrent Executions. In ASPLOS. ACM, 710–725. https://doi.org/
10.1145/3503222.3507734[23] Friedemann Mattern. 1989. Virtual Time and Global States ofDistributed Systems. In Parallel and Distributed Algorithms. NorthHolland, 215–226.
[24] Anshuman Mohan, Wei Xiang Leow, and Aquinas Hobor. 2021. Functional Correctness of C Implementations of Dijkstra’s, Kruskal’s, andPrim’s Algorithms. In CAV (LNCS, Vol. 12760). Springer, 801–826.
https://doi.org/10.1007/978-3-030-81688-9_37[25] Aleksandar Nanevski, Viktor Vafeiadis, and Josh Berdine. 2010. Structuring the veriﬁcation of heap-manipulating programs. In POPL. ACM,
261–274. https://doi.org/10.1145/1706299.1706331[26] Abel Nieto, Léon Gondelman, Alban Reynaud, Amin Timany, and Lars
Birkedal. 2022. Modular veriﬁcation of op-based CRDTs in separation
logic. Proc. ACM Program. Lang. 6, OOPSLA2 (2022), 1788–1816. https://doi.org/10.1145/3563351[27] Peter W. O’Hearn. 2012. A Primer on Separation Logic (and Automatic
Program Veriﬁcation and Analysis). In Software Safety and Security Tools for Analysis and Veriﬁcation. NATO Science for Peace and Security
Series, Vol. 33. IOS Press, 286–318. https://doi.org/10.3233/978-161499-028-4-286[28] Peter W. O’Hearn, John C. Reynolds, and Hongseok Yang. 2001. Local
Reasoning about Programs that Alter Data Structures. In CSL (LNCS,
Vol. 2142). Springer, 1–19. https://doi.org/10.1007/3-540-44802-0_1[29] José Nuno Oliveira. 2023. Program Design by Calculation.
[30] Ruzica Piskac, Thomas Wies, and Damien Zuﬀerey. 2014. Automating Separation Logic with Trees and Data. In CAV (LNCS, Vol. 8559).
Springer, 711–728. https://doi.org/10.1007/978-3-319-08867-9_47[31] John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable
Data Structures. In LICS. IEEE Computer Society, 55–74. https://doi.
org/10.1109/LICS.2002.1029817[32] Caitlin Sadowski, Jaeheon Yi, Kenneth Knowles, and Cormac Flanagan.
2008. Proving correctness of a dynamic atomicity analysis in Coq. In
Workshop on Mechanizing Metatheory, Vol. 8.
[33] Konstantin Serebryany and Timur Iskhodzhanov. 2009. ThreadSanitizer – data race detection in practice.. In Proceedings of the Workshop
on Binary Instrumentation and Applications. http://doi.acm.org/10.
1145/1791194.1791203[34] Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. 2015. Mechanized veriﬁcation of ﬁne-grained concurrent programs. In PLDI. ACM,
77–87. https://doi.org/10.1145/2737924.2737964[35] Philip Wadler. 1990. Deforestation: Transforming Programs to Eliminate Trees. Theor. Comput. Sci. 73, 2 (1990), 231–248.
https://doi.org/10.1016/0304-3975(90)90147-A[36] Shengyi Wang, Qinxiang Cao, Anshuman Mohan, and Aquinas Hobor.
2019. Certifying graph-manipulating C programs via localizations
within data structures. Proc. ACM Program. Lang. 3, OOPSLA (2019),
171:1–171:30. https://doi.org/10.1145/3360597[37] James R. Wilcox, Cormac Flanagan, and Stephen N. Freund. 2018.
VeriﬁedFT: a veriﬁed, high-performance precise dynamic race detector.
In PPoPP. ACM, 354–367. https://doi.org/10.1145/3178487.3178514[38] Qiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur, and Ilya
Sergey. 2023. Artefact for Article “Rooting for Eﬃciency: Mechanised
Reasoning about Array-Based Trees in Separation Logic”. https://doi.
org/10.5281/zenodo.10366484[1] Andrew W. Appel. 2011. Veriﬁed Software Toolchain - (Invited Talk).
In ESOP (LNCS, Vol. 6602). Springer, 1–17. https://doi.org/10.1007/9783-642-19718-5_1[2] Andrew W. Appel. 2016. Veriﬁed Functional Algorithms. Software
Foundations. Volume 3 (2016). Available at https://softwarefoundations.
cis.upenn.edu/vfa-current/.
[3] Andrew W. Appel. 2022. Coq’s vibrant ecosystem for veriﬁcationengineering (invited talk). In CPP. ACM, 2–11. https://doi.org/10.1145/
3497775.3503951[4] Patrick Bahr and Emil Axelsson. 2017. Generalising tree traversals
and tree transformations to DAGs: Exploiting sharing without thepain. Sci. Comput. Program. 137 (2017), 63–97. https://doi.org/10.1016/
j.scico.2016.03.006[5] Aurèle Barrière. 2018. VST Veriﬁcation of B+ Trees with Cursors. Technical Report. Ecole Normale Supérieure de Rennes.
[6] Qinxiang Cao, Shengyi Wang, Aquinas Hobor, and Andrew W. Appel.
2019. Proof Pearl: Magic Wand as Frame. https://doi.org/10.48550/
arXiv.1909.08789[7] Arthur Charguéraud. 2016. Higher-order representation predicates inseparation logic. In CPP. ACM, 3–14. https://doi.org/10.1145/2854065.
2854068[8] Arthur Charguéraud. 2020. Separation Logic for Sequential Programs(Functional Pearl). Proc. ACM Program. Lang. 4, ICFP (2020), 116:1–
116:34. https://doi.org/10.1145/3408998[9] Arthur Charguéraud. 2021. Separation Logic Foundations. Software
Foundations. Volume 6 (2021). Available at https://softwarefoundations.
cis.upenn.edu/slf-current/.
[10] Olivier Danvy. 2022. Fold-unfold lemmas for reasoning about recursive
programs using the Coq proof assistant. J. Funct. Program. 32 (2022),
e13. https://doi.org/10.1017/S0956796822000107[11] Colin J Fidge. 1988. Timestamps in message-passing systems that
preserve the partial ordering. In Proceedings of the 11th AustralianComputer Science Conference. 55–66.
[12] Cormac Flanagan and Stephen N. Freund. 2009. FastTrack: eﬃcientand precise dynamic race detection. In PLDI. ACM, 121–133. https://doi.org/10.1145/1542476.1542490[13] Jeremy Gibbons. 1991. Algebras for Tree Algorithms. Ph. D. Dissertation.
University of Oxford.
[14] Léon Gondelman, Simon Oddershede Gregersen, Abel Nieto, Amin
Timany, and Lars Birkedal. 2021. Distributed causal memory: modular
speciﬁcation and veriﬁcation in higher-order distributed separation
logic. Proc. ACM Program. Lang. 5, POPL (2021), 1–29. https://doi.org/
10.1145/3434323[15] Kiran Gopinathan, Mayank Keoliya, and Ilya Sergey. 2023. Mostly
Automated Proof Repair for Veriﬁed Libraries. Proc. ACM Program.
Lang. 7, PLDI (2023), 25–49. https://doi.org/10.1145/3591221[16] Aquinas Hobor and Jules Villard. 2013. The ramiﬁcations of sharing
in data structures. In POPL. ACM, 523–536. https://doi.org/10.1145/
2429069.2429131[17] The Iris Project. 2023. Iris: a Higher-Order Concurrent Separation
Logic Framework, implemented and veriﬁed in the Coq proof assistant.
https://iris-project.org/ Online.
[18] Leslie Lamport. 1978. Time, Clocks, and the Ordering of Events in
a Distributed System. Commun. ACM 21, 7 (1978), 558–565. https://doi.org/10.1145/359545.359563[19] Mohsen Lesani, Christian J. Bell, and Adam Chlipala. 2016. Chapar:
certiﬁed causally consistent distributed key-value stores. In POPL.
ACM, 357–370. https://doi.org/10.1145/2837614.2837622[20] Yiyun Liu, James Parker, Patrick Redmond, Lindsey Kuper, Michael
Hicks, and Niki Vazou. 2020. Verifying replicated data types with
typeclass reﬁnements in Liquid Haskell. Proc. ACM Program. Lang. 4,
OOPSLA (2020), 216:1–216:30. https://doi.org/10.1145/3428284

Received 2023-09-19; accepted 2023-11-25

59