Efficient Race Detection with Futures

TL;DR

This paper introduces efficient algorithms, MultiBags and MultiBags+, for on-the-fly race detection in task parallel programs using futures, with theoretical guarantees and empirical validation.

Contribution

It presents two new algorithms that improve race detection efficiency for programs with restricted and general futures, respectively.

Findings

MultiBags runs in near-constant time for restricted futures.

MultiBags+ extends to general futures with acceptable overhead.

Empirical results confirm the practical efficiency of both algorithms.

Abstract

This paper addresses the problem of provably efficient and practically good on-the-fly determinacy race detection in task parallel programs that use futures. Prior works determinacy race detection have mostly focused on either task parallel programs that follow a series-parallel dependence structure or ones with unrestricted use of futures that generate arbitrary dependences. In this work, we consider a restricted use of futures and show that it can be race detected more efficiently than general use of futures. Specifically, we present two algorithms: MultiBags and MultiBags+. MultiBags targets programs that use futures in a restricted fashion and runs in time $O(T_1 \alpha(m,n))$, where $T_1$ is the sequential running time of the program, $\alpha$ is the inverse Ackermann's function, $m$ is the total number of memory accesses, $n$ is the dynamic count of places at which parallelism is created. Since $\alpha$ is a very slowly growing function (upper bounded by $4$ for all practical purposes), it can be treated as a close-to-constant overhead. MultiBags+ an extension of MultiBags that target programs with general use of futures. It runs in time $O((T_1+k^2)\alpha(m,n))$ where $T_1$, $\alpha$, $m$ and $n$ are defined as before, and $k$ is the number of future operations in the computation. We implemented both algorithms and empirically demonstrate their efficiency.

Full text

Specifically, we present two algorithms: MultiBags and MultiBags+. MultiBags targets programs that use futures in a restricted fashion and runs in time $O(T_{1}\alpha(m,n))$, where $T_{1}$ is the sequential running time of the program, $\alpha$ is the inverse Ackermann’s function, $m$ is the total number of memory accesses, $n$ is the dynamic count of places at which parallelism is created. Since $\alpha$ is a very slowly growing function (upper bounded by $4$ for all practical purposes), it can be treated as a close-to-constant overhead. MultiBags+ is an extension of MultiBags that target programs with general use of futures. It runs in time $O((T_{1}+k^{2})\alpha(m,n))$ where $T_{1}$, $\alpha$, $m$ and $n$ are defined as before, and $k$ is the number of future operations in the computation. We implemented both algorithms and empirically demonstrate their efficiency.

††journalyear: 2019††copyright: acmcopyright††conference: 24th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming; February 16–20, 2019; Washington, DC, USA††price: 15.00††doi: 10.1145/3293883.3295732††isbn: 978-1-4503-6225-2/19/02

1. Introduction

Races constitute a major source of errors in parallel programs. Since they lead to nondeterministic program behaviors, they are extremely challenging to detect and debug. In this work, we focus on the problem of race detection for task-parallel programs, where the programmer denotes the logical parallelism of the computation using high-level parallel control constructs provided by the platform, and lets the underlying runtime system perform the necessary scheduling and synchronization. Examples of task parallel platforms include OpenMP (OpenMP 4.0, 2013), Intel’s TBB (Reinders, 2007; Intel Corporation, 2012), IBM’s X10 (Charles et al., 2005), various Cilk dialects (Frigo et al., 1998; Danaher et al., 2008; Leiserson, 2010; Intel Corporation, 2013), and Habanero dialects (Barik et al., 2009; Cavé et al., 2011).

In the context of task parallel programs, the focus is typically on detecting determinacy races (Feng and Leiserson, 1997) (also called general races (Netzer and Miller, 1992)), which occur when two or more logically parallel instructions access the same memory location and at least one access is a write. In the absence of a determinacy race, a task parallel program for a given input behaves deterministically.

Over the years, researchers have proposed several determinacy race algorithms (Mellor-Crummey, 1991; Feng and Leiserson, 1997, 1999; Raman et al., 2010, 2012; Bender et al., 2004; Fineman, 2005; Utterback et al., 2016; Surendran and Sarkar, 2016b; Xu et al., 2018) for task parallel code. These algorithms perform race detection on the fly as the program executes, and consist of two main components: (1) an access history that keeps track of previous readers and writers for each memory location; and (2) a reachability data structure for maintaining and querying whether two instructions are logically in parallel. On each memory access, the detector checks whether the current access is logically parallel with the previous accessors (stored in the access history) to determine whether a race exists.

Most prior work focuses on a restricted set of computations, namely computations that can be represented as series-parallel dags (SP dags) (Valdes, 1978) with nice structural properties, such as ones generated using fork-join parallelism (i.e.,spawn/sync or async/finish). Prior works show that one can race detect computations that are SP dags efficiently by exploiting the nice structural properties. In particular, the reachability data structure can be maintained and queried with no asymptotic overhead for both serial (Bender et al., 2004; Fineman, 2005) and parallel executions (Utterback et al., 2016). Moreover, the access history needs to store only a constant number of accessors per memory location to correctly race detect for such computations (Feng and Leiserson, 1997, 1999; Mellor-Crummey, 1991).

The use of futures has become a popular way to extend fork-join parallelism. Since their proposal (Friedman and Wise, 1978; Baker and Hewitt, 1977) in the late 70s, futures have has been incorporated into various parallel platforms (Lu et al., 2014; Cavé et al., 2011; Fluet et al., 2010; Charles et al., 2005; Chandra et al., 1994; Kranz et al., 1989; Arvind et al., 1986; Halstead, 1985). Researchers have studied scheduling bounds (Blelloch et al., 1997; Arora et al., 1998) and cache efficiency (Spoonhower et al., 2009; Herlihy and Liu, 2014) for using futures with fork-join computations. Kogan and Herlihy (2014) study linearizability of concurrent data structures accessed using futures. Surendran and Sarkar (2016a) proposed using futures to automatically parallelize programs.

The use of futures can form arbitrary dependencies, and thus computations generated by a parallel program that uses futures are no longer series-parallel. However, not much work has been done on race detecting programs with more general dependence structures.

Two prior works exist on race detection for programs that use futures and both are sequential (no known parallel algorithms exist). An algorithm proposed by Surendran and Sarkar (2016c) has high overheads — the running time is $O(T_{1}(f+1)(k+1))$ where $T_{1}$ is the work, or sequential running time of the program without race detection, $f$ is number of future objects and $k$ is the number of future operations. That is, the running time of the race detection algorithm increases quadratically with the total number of futures used in the program. More recently, Agrawal et al. (2018) present a sequential algorithm to perform race detection on SP dags with $k$ added non-series-parallel edges in $O(T_{1}+k^{2})$ time, which is the best known running time. The algorithm is difficult to implement however, since it requires storing all the nodes in the computation graph and traversing the graph during execution to update labels. Thus, no actual implementation of the algorithm exists to date.

Contributions

While prior work on race detection has focused on either structured SP dags or unrestricted use of futures that generates arbitrary dependences, we consider a restricted use of futures. Researchers have observed in other contexts (Herlihy and Liu, 2014) that using futures in a restricted manner can reduce scheduling and cache overheads. We define a specific structured use-case of futures that allows us to perform race detection much more efficiently than general use of futures. This class of futures is quite natural and can be checked with program analysis. We provide the precise definition in Section 2; informally, it requires that the instruction that creates the future is sequentially before the instruction that uses the handle.

We present two practical algorithms for race detecting programs with futures: MultiBags and MultiBags+. The main contribution for both algorithms is a novel reachability data structure. Both algorithms run the program sequentially for a given input and report a race if and only if one exists, following the same correctness criteria as prior work. MultiBags focuses on structured use of futures and incurs very little overhead — a multiplicative overhead in the inverse Ackermann’s function, which is upper bounded by $4$ for all practical purposes (Cormen et al., 2009). MultiBags+ is an extension of MultiBags, which handles general use of futures and has overhead comparable to the state-of-the-art theoretical algorithm (Agrawal et al., 2018) (i.e., multiplicative overhead of the inverse Ackermann’s function) and can be implemented efficiently. We have implemented both algorithms and empirically evaluated them. The empirical results show that both algorithms can maintain reachability efficiently for their designated use cases.

Specifically, we make the following contributions:

• $\bullet$

MultiBags: We propose MultiBags, an algorithm to race detect programs that use structured futures (Section 4). We prove its correctness and show that it race detects in $O(T_{1}\alpha(m,n))$ time where $T_{1}$ is the work, $\alpha$ is the inverse Ackermann’s function (upper bounded by $4$), $m$ is the number of memory accesses, and $n$ is the dynamic count of places at which parallelism is created. Since $\alpha$ is a very slow-growing function, this bound is essentially $O(T_{1})$ for all intents and purposes.

• $\bullet$

MultiBags+: We propose MultiBags+, an algorithm to race detect programs that use general futures (Section 5). We prove its correctness and show that it race detects in $O(T_{1}+k^{2})\alpha(m,n)$ time where $T_{1}$, $\alpha$, $m$, and $n$ are defined as above, and $k$ is the number of future operations in the computation (Section 5). Again, since the inverse Ackermann’s function is slow growing function, the running time is $O(T_{1}+k^{2})$ for all intents and purposes. Compared to the state-of-the-art proposed by Agrawal et al. (2018), MultiBags+’s running time has a multiplicative overhead of the inverse Ackermann’s function. Unlike the state-of-the-art, however, MultiBags+’s relative simplicity allows it to be implemented efficiently in practice. We provide a more detailed comparison between our MultiBags+ algorithm and the state-of-the-art (Agrawal et al., 2018) in Section 5.

• $\bullet$

FutureRD: We have built a prototype race detector called FutureRD based on MultiBags and MultiBags+. Empirical evaluation with FutureRD shows that our algorithms allow reachability to be maintained efficiently, incurring almost no overhead (geometric means of $1.06\times$ and $1.40\times$ overhead for MultiBags and MultiBags+, respectively). The overall race detection incurs geometric means of $20.48\times$ and $25.98\times$ overhead, respectively.

2. Preliminaries and Definitions

Parallel control constructs:

Our algorithms are described assuming parallelism in programs is generated using four primitives: spawn, sync, create_fut and get_fut. The algorithms themselves are general and can be applied to platforms that use other constructs that generate similar types of dags. We assume that spawn and sync are used to generate fork/join or series/parallel structures. In particular, for the purposes of this paper, function $F$ can spawn off a child function $G$, invoking $G$ without suspending the continuation of $F$, thereby creating parallelism; similarly, $F$ can invoke sync, joining together all previously spawned children within the functional scope.111Some constructs, such as async/finish primitives have slightly different restrictions, they still generate SP dags and our algorithms can be modified to apply to these programs. We assume create_fut and get_fut primitives are used to create and join futures, respectively. Like spawn, one can precede a function call to $G$ in $F$ with create_fut, which allows $G$ to execute without suspending $F$. Unlike spawn, however, parallel function calls created with create_fut can escape the scope of a sync — a subsequent sync joins together previously spawned functions but does not wait for function calls preceded by create_fut to return. Instead, create_fut returns a future handle $h$, which the program must explicitly invoke get_fut on to join with the corresponding computation (i.e., $G$). If $G$ has not completed when get_fut is called, then get_fut blocks until $G$ finishes and a result is obtained.

Modeling parallel computations:

One can model the execution of a parallel program for a given input as a dag (directed acyclic graph) $G_{\mathit{full}}$, whose nodes are strands — sequence of instructions containing no parallel control – and edges are control dependencies among strands. The dag unfolds dynamically as the program executes. A strand $u$ is sequentially before another strand $v$ (denoted by $u\prec v$) if there is a path from $u$ to $v$ in the dag; two nodes $u$ and $v$ are logically parallel if there is no path from one to the other. The performance of a computation can be measured in two terms: the work $T_{1}$ of the computation is the execution time of the computation on a single processor; the span (also called depth or critical-path length) $T_{\infty}$ of the computation is its execution time on an infinite number of processors (or, longest sequential path through the dag).

Series-parallel dags:

Computations which use only spawn and sync can be modeled as series-parallel dags (SP-dag) (Valdes, 1978) that have a single source node with no incoming edges and a single sink node with no out-going edges. Upon the execution of a spawn, a fork node is created with two outgoing edges: one leads to the first strand in the spawned child function and one leads to the continuation of the parent. Upon the execution of a sync, a join node is created, that has two or more incoming edges, joining the previously spawned subcomputations.222Technically, a sync can join multiple children; therefore, a join node can have more than two parents. For simplicity, in this paper, we assume each join has exactly two incoming edges. One can modify all our algorithms to the more general case easily.

SP dags can be constructed recursively as follows.

• $\bullet$

Base Case: the dag consists of a single node that is both the source and the sink.

• $\bullet$

Series Composition: let $G_{1}=(V_{1},E_{1})$ and $G_{2}=(V_{2},E_{2})$ be SP-dags on distinct nodes. Then a series composition $G$ is formed by adding an edge from $\mathit{sink}(G_{1})$ to $\mathit{source}(G_{2})$ with $\mathit{source}(G)=\mathit{source}(G_{1})$ and $\mathit{sink}(G)=\mathit{sink}(G_{2})$.

• $\bullet$

Parallel Composition: let $G_{L}=(V_{L},E_{L})$ and $G_{R}=(V_{R},E_{R})$ be SP-dags on distinct nodes. Then the parallel composition $G$ is formed as follows: add a fork node $f$ with edges from $f$ to both sources, and a join node $j$ with edges from both sinks to $j$. $\mathit{source}(G)=f$ and $\mathit{sink}(G)=j$. We refer to $G_{L}$ and $G_{R}$ as the left subdag and right subdag, respectively, of both the fork $f$ and join $j$.

Adding futures:

We model computations that employ futures in addition to spawn and sync as a set of independent SP dags connected to each other via non-SP edges due to create_fut and get_fut calls. If a function $F$ spawns a function $G$, then the strands of $F$ and $G$ are part of the same SP dag. However, if function $G$ calls $H$ using a create_fut call, then the first strand, say $v$, of $H$ is the source of a different SP dag. The last strand of $H$ will be the sink node of this SP dag. Therefore, if a program calls create_fut $f$ times — that is, it creates $f$ total futures in addition to the main program — then it has $f+1$ SP dags which are connected to each other via non-SP edges.

These non-SP edges are incident on strands that end with create_fut and ones that immediately follow strands that ended with get_fut. A strand $u$ in function $G$ that ends with $h=\texttt{create{\char 95\relax}fut}(F)$ has two outgoing edges — one non-SP edge to the first strand in $F$, and one SP edge to the continuation in $G$. We say that $u$ is the creator of $F$ denoted by $\texttt{creator}(F_{j})$. The first strand of $F$ is the source of a new SP-dag which contains all strands of $F$ and the functions it calls (recursively) using spawn and the last strand of $F$ is the sink of this SP-dag. Similarly, strand $u$ in $H$ immediately follows a $\texttt{get{\char 95\relax}fut}(h)$ call where $h$ is the future handle for future $F$ has two incoming edges — one SP edge from the strand that ended with the get_fut call in the current function $H$ and one non-SP edge from the last strand of the $F$. We say $u$ is the getter of $F_{j}$ denoted as $\texttt{getter}(F)$. We say that $u\prec_{SP}v$ if there is a path from $u$ to $v$ using only SP edges.

This model is quite general and subsumes computations that can arise from futures (Lu et al., 2014; Cavé et al., 2011; Fluet et al., 2010; Charles et al., 2005; Chandra et al., 1994; Kranz et al., 1989; Arvind et al., 1986; Halstead, 1985) or other future-like (such as “put” and “get” (Budimlić et al., 2010; Taşırlar and Sarkar, 2011)) parallel constructs proposed in the literature. Therefore, our algorithm would work on all of these primitives.

Structured futures:

We place the following restrictions on structured futures: (1) Single-touch: Every future handle is called with get_fut at most once. (2) No race on future handles: There is a sequential dependence in the program from the point where a future is created (via create_fut which initializes a future handle) to the point where it is read (via get_fut).More precisely, if strand $u$ terminates with a $f\mathrel{\hskip 1.0pt=\hskip 1.0pt}\texttt{create{\char 95\relax}fut}(F)$ call and strand $v$ terminates with a $\texttt{get{\char 95\relax}fut}(f)$ call, then $u\prec v$ in the computation.

Eager execution:

Both our algorithms execute the computation sequentially and execute the program in depth-first eager order. When the execution reaches $\texttt{create{\char 95\relax}fut}(F)$ (after executing $\texttt{creator}(F)$) call or a $\texttt{spawn}(F)$ call, it always executes the function $F$. When $F$ returns, then the next node of the parent function (the one after the continuation edge) is executed. This execution order automatically has the property that all functions that must join at a sync point have already returned when the execution reaches the sync; therefore, the execution never blocks at a sync. Similarly, for structured futures, this execution has the property that the execution will never block at a get_fut. For general futures, we restrict our attention to computations where the use of futures is forward-pointing: for every future $F$, $\texttt{creator}(F)$ executes before $\texttt{getter}(F)$ in the depth-first eager execution. Without this restriction, sequential execution of the original program could deadlock, in which case our algorithm race detects up to the point where it deadlocks.

3. Managing Access History

As mentioned in Section 1, there are two important components in a race detector: access history and reachability data structure. MultiBags and MultiBags+ differ in how they maintain reachability but manage access history similarly. This section discusses how they manage access history — for each memory location $\ell$, the access history maintains enough information about the previous accesses to $\ell$ so that future accesses to $\ell$ can detect races.

When race detecting a series parallel program, it is sufficient to store a constant number of previous reader strands and a single previous writer strand in the access history(Feng and Leiserson, 1997; Mellor-Crummey, 1991). When a strand $s$ accesses a memory location $\ell$, it checks if some subset (based on whether $s$ is reading or writing) of $\ell$’s previous accessors are in parallel with $s$. Therefore, each memory access leads to at most a constant number of queries into the reachability data structure.

This property no longer holds for programs with futures, however. In particular, the access history for a memory location $\ell$ still holds only one writer strand, namely the most recent writer strand, $\texttt{last-writer}(\ell)$. However, it must now store an arbitrarily large reader-list. Race detection proceeds as follows. Whenever a strand $s$ reads from a memory location $\ell$, the detector checks the reachability data structure to determine whether $s$ is logically parallel with $\texttt{last-writer}(\ell)$; if so, a race is reported. Otherwise, $s$ is added to $\texttt{reader-list}(\ell)$. When a strand $s$ writes to a memory location $\ell$, the race detector must check $s$ against all readers in $\texttt{reader-list}(\ell)$ and with $\texttt{last-writer}(\ell)$. If $s$ is in parallel with any of them, then it declares a race. Otherwise, the $\texttt{reader-list}(\ell)$ is set to $\emptyset$ and $s$ is stored as $\texttt{last-writer}(\ell)$. We can empty the reader list without missing any races because anything that executes later that would be in parallel with these readers must also be in parallel with $s$ (the new $\texttt{last-writer}(\ell)$), and a race will be reported with $s$.

A key thing to notice here is the following: the total number of queries into the reachability data structure (i.e., checking one access against another for race) is bounded by the total number of memory accesses in the computation. Since we can empty all the readers $\texttt{reader-list}(\ell)$ whenever we encounter a $\texttt{last-writer}(\ell)$, a reader is checked against some writer at most twice: when it is inserted into the reader list, and right before it is removed. Thus, the total number of queries to the reachability data structure is bounded by $O(T_{1})$, where $T_{1}$ is the work of the computation. We shall relate this observation formally to the performance bound of MultiBags and MultiBags+ later in Sections LABEL:sec:structuredOmitted and A.

4. MultiBags for Structured Futures

We now describe MultiBags, which can race-detect programs with structured futures in time $O(T_{1}\alpha(m,n))$ where $T_{1}$ is the work of the program, $\alpha$ is the inverse Ackermann’s function, $m$ is the number of memory accesses in the program and $n$ is the number of spawn and create_fut calls. Since the inverse Ackermann’s function is a very slowly growing function, the bound is close to optimal.

Notation:

Note that programmatically, spawn and sync are subsumed by create_fut and get_fut since we can convert a spawn to create_fut and sync to a series of get_fut calls, one on each function spawned in the current function scope. In the case of general use of futures discussed in Section 5, we distinguish between SP edges (generated by spawn and sync) and non-SP edges generated by create_fut and get_fut since the bound depends on $k$, the number of get_fut calls, and converting all sync calls to get_fut calls will increase this number. For structured futures, however, the bound does not depend on $k$; therefore, for simplicity in this section, we assume that we only have create_fut and get_fut constructs to create parallelism.

The computation dag consists of three kinds of nodes — regular strands with one incoming and one outgoing edge, creator strands which end with a create_fut call with two outgoing edges, and getter strands (that come immediately after a get_fut call) with two incoming edges. It also consists of three kinds of edges: spawn edges are edges from creator nodes to the first strand of the future; join edges are edges from last strand of a future to getter nodes; all other edges (that go between strands of the same function instance) are continue edges.

4.1. Algorithm

This algorithm is similar to the SP-Bags algorithm for detecting races for series-parallel programs (Feng and Leiserson, 1997). As with that algorithm, we will use a the fast disjoint-set data structure (Tarjan, 1975). The data structure maintains a dynamic collection $D$ of disjoint sets and provides three operations:

• $\bullet$

$A=\textnormal{Make-Set}(D,x):$ Creates a new set $A=\left\{x\right\}$ and adds it to the disjoint sets data structure $S$.

• $\bullet$

$A=\textnormal{Union}(D,A,B):$ Unions the set $B$ into $A$ and destroys $B$. We will sometimes overload notation and say $\textnormal{Union}(D,x,y)$ where $x$ and $y$ are elements in the set instead of sets. This means that we union the sets containing $x$ and $y$ into the set containing $x$.

• $\bullet$

$\textnormal{Find}(D,x)$ returns the set that contains the element $x$.

In this section, we only have one disjoint set data structure; therefore, $D$ is implicit.

As mentioned in Section 2, and like SP-Bags, MultiBags depends on the depth-first eager execution of the computation. MultiBags maintains a bag (a set in the union-find data structure) for each function instance $F$ which has been created and for which get_fut has not yet been called (these bags can be stored with the future handle). This bag is labeled either an $S$-bag, represented by $S_{F}$ or a $P$-bag, represented by $P_{F}$. The algorithm maintains these bags as shown in Figure 1. The strands of a particular function $F$ are always added to $S_{F}$ before they execute.

The algorithm looks similar to SP-Bags (Feng and Leiserson, 1997). The main difference is that when the function $G$ returns, its $S$-bag $S_{G}$ is renamed as $P_{G}$ bag; in SP-bags, $S_{G}$ would be unioned with $P_{F}$, the parent function of $G$. However, this small difference is crucial for handling programs with structured futures rather than series-parallel programs. In addition, the proof for correctness of this algorithm for structured futures is significantly different than the proof of correctness of SP-bags for series-parallel programs.

Figure 2 shows the operation of this algorithm on an example program which uses structured futures. Each rectangle is a function instance and nodes are strands. The straight dashed lines going towards the left represent create_fut edges while the curved dashed lines represent get_fut edges. Consider step 12 when the first node of function $F$ is executing. All nodes except node 4 are sequentially before this strand and are correspondingly in some $S$-bag. Node 4 is in parallel with this strand and is in a $P$-bag.

4.2. Proof of Performance and Correctness

First, we state the performance bound — the proof is essentially identical to the proof of performance of SP-Bags, since the algorithm is quite similar.

Proof of Performance of MultiBags

Theorem 4.1.

The running time of MultiBags when detecting races for a program with work $T_{1}$ is $T_{1}\alpha(m,n)$ where $m$ is the number of memory accesses and $n$ is the number of create_fut calls.

Proof.

The fast disjoint-sets data structure provides the bound of amortized time $O(\alpha(m,n))$ per operation where $m$ is the number of operations and $n$ is the number of sets. For our program, $m$ is at most the number of memory accesses and $n$ is the number of create_fut calls. Note here, again, that unlike series parallel computations, each write may generate multiple queries; however, for the reason as explained in Section 3, the total number of queries is bounded by the two times the total number of memory accesses since each writer removes the entire reader-list. Therefore, the total running time is $O(T_{1}\alpha(m,n))$. ∎

Intuition for the proof

In order to argue that MultiBags is correct, we must prove the following theorem.

Theorem 4.2.

If the currently executing strand is $v$, then a previously executed strand $u$ is currently in an $S$ bag iff $u\prec v$.

In order to prove this theorem, we define two more terms. A node $u$ is a spawn predecessor of a node $v$ if there is a path from $u$ to $v$ which consists of only spawn and continue edges. A node $u$ is a join predecessor of $v$ if there is a path from $u$ to $v$ that consists of only join and continue edges. Spawn and join successors are defined in the symmetric way. We will overload notation and say that a strand $u$ is a spawn predecessor of a function $F$ if there is a path from $u$ to the first strand of $F$ that consists of only spawn and continue edges and similarly a strand $v$ is a join successor of $F$ if there is a path from the last strand of $F$ to $v$. Each node is its own spawn and join predecessor and successor.

The algorithm works due to the following observations.333We implicitly assume that when we refer to any strand (or function), it is either currently executing or has already executed (we have no knowledge of strands or functions that are still to execute). We say that a function is active if it has started executing, but has not completed (returned). While a function $F$ is active, $S_{F}$ exists and $P_{F}$ doesn’t because $P_{F}$ is only created upon $F$’s return. All strands of an active function $F$ are in $S_{F}$. After a function has returned, $S_{F}$ is destroyed; $P_{F}$ exists if get_fut has not been called on $F$’s future handle and if $P_{F}$ exists, then all strands of $F$ are in $P_{F}$. After a function has joined (get_fut has been called) then neither $S_{F}$ nor $P_{F}$ exist.

Property 1 is a property of eager executions.

Property 1.

When a strand $v$ is currently executing, all spawn predecessors of $v$ are part of some active function. The converse is also true; all strands $w$ that are part of active functions are spawn predecessors of $v$.

We need two other properties. The first one is a static property of paths in a program with structured futures as follows. If there is a path from a strand $u$ to stand $v$,444In general, there can be many paths from $u$ to $v$. then there must be a path where the first (possibly empty) part of the path consists of only join and continue edges, while the second (possibly empty) part of the path contains only spawn and continue edges. In other words, there is a path where no join edges follow spawn edges. More formally, for any two nodes $u$ and $v$, if $u\prec v$, then we can find a node $w$ where $u$ is a join-predecessor of $w$ and $w$ is a spawn predecessor of $v$. Combining with Property 1, we get:

Observation 1.

Consider a completed strand $u$ and a currently-executing strand $v$ where $u\prec v$. The furthest join successor of $u$, say $w$, must be part of an active function.

This observation allows us to concern ourselves only with paths that go through nodes of active functions. In particular, to detect races, it is sufficient to try to check if the furthest join successor $w$ of any previously executed node $u$ is part of an active function. If so, the observation implies that $u\prec w$ and we already know from Property 1 that $w\prec v$; therefore, $u\prec v$. If not, then $u\not\prec v$.

The second property is a dynamic property of MultiBags which allows to precisely check this. In particular, it states the following (which combined with the previous observation gives us the theorem):

Observation 2.

Consider an already completed node $u$. Say, at time $t$, $u$’s furthest join successor $w$ is part of a function $G$. If $G$ is active, then $u$ is in $G$’s $S$ bag, otherwise $u$ is in $G$’s $P$ bag.

An informal argument about why this property is true follows: In Line 1, MultiBags unions $P_{G}$ into $S_{F}$ when $G$ joins with an active function $F$. This suggests the following: Consider a particular strand $u$ in function $G$. Say at time $t$, $w$ is the furthest join successor strand of $u$ which has executed (or is executing). (This strand is well defined since there is no branching in a path that contains only join and continue edges.) Say $w$ is part of function $F$. Then at time $t$, $u$ is in $F$’s bag. $F$’s bag is an $S$ bag if $F$ is active. Therefore, to check if $u$’s furthest join successor $w$ is active, it suffices to check if $u$ is in an $S$ bag, which is precisely what MultiBags does.

If we combine Observations 1 and 2, we get the theorem. Say $v$ is executing at time $t$ and consider a previously executed node $u$ and say $w$ is the furthest join successor of $u$. If $u\prec v$, then by the first observation, $w$ is part of an active function and therefore, by the second observation, $u$ is in an $S$ bag. On the other hand, if $u\parallel v$, then $w$ can not be part of an active function — if it was, then by Property 1, $w\prec v$ and therefore, $u\prec v$ (a contradiction). Therefore, $u$ is in a $P$ bag.

When the computation does a memory access, it simply checks if the previous accesses are in an $S$ In order to do queries, the algorithm operates as follows:

1. (1)

Currently executing strand $s$ reads location $\ell$: check if $\texttt{last-writer}(\ell)$ is in a $P$ bag; if so, declare a race. Otherwise, append $r$ to $\texttt{reader-list}(\ell)$ 2. (2)

Currently executing strand $s$ writes to location $\ell$: check if any reader $r\in\texttt{reader-list}(\ell)$ is in a $P$ bag; if so, declare a race. Otherwise, empty the reader list and set $\texttt{last-writer}(\ell)=w$.

Proof of Correctness of MultiBags

First, we prove the static property stated in Observation 1. In order to prove it, we first define a canonical order on the futures of the program and show that we can always order the functions in this canonical order.

Lemma 4.3.

We can always find a canonical order.

Proof.

The order starts with the main function; we then progressively add futures to the computation. A future $F$ can only be added if its creator strand and getter strand have already both been added.

We will induct on adding new futures. We can always start since the main function is added first. At some point, we have already added some futures, say a set $S$. Next, we will add the future $F$ such that there is no future $G$ such that $\texttt{creator}(F)\prec\texttt{creator}(G)$ where both creator nodes are in $S$. There must be some such future (if there are more than one, we can choose arbitrarily). Since no future was created sequentially after $F$ was created, and the strand before the $\texttt{getter}(F)$ is sequentially after $\texttt{creator}(F)$, $\texttt{getter}(F)$ must also be in $S$; therefore, it is legal for us to pick $F$ as the next future in our canonical order. ∎

We now use this canonical order to induct on the futures. In particular, we can show that the static property stated in Observation 1 (stated more formally and completely in the following lemma) by inducting on the futures in the canonical order.

Lemma 4.4.

If $u\prec v$, then there exists a path from $u$ to $v$ that contains two sections: the first path (possibly empty) contains only join and continue edges and the second part (possibly empty) contains only spawn and continue edges. In other words there is never a spawn edge followed by a join edge on this path. In addition, this path is unique. Therefore, If $u\prec v$, then there is some node $w$ (possibly $u$ or $v$) which is a join successor of $u$ and a spawn predecessor of $v$.

Proof.

Induct on futures in the canonical order (which we can always find according to Lemma 4.3) and show that this is true as we add futures one by one.

Base case: We first have only the main strand, so this is true trivially.

Inductive case: Assume that after we have added a set $S$ of futures, the statement is true. We now add a new future $F^{\prime}$.

Consider any nodes $u$ and $v$ in this new dag where $u\prec v$. If neither $u$ nor $v$ are in $F^{\prime}$, then the addition of $F^{\prime}$ does not add any new paths between $u$ and $v$ (since the only new path added is between $\texttt{creator}(F)$ and $\texttt{getter}(F)$ and there was already a path between them before we added $F^{\prime}$). In addition, any new path added does have a spawn followed by a join — therefore, the uniqueness is preserved. Therefore, we only need consider pairs where either $u$ or $v$ are in $F^{\prime}$. If $u$ is in $F^{\prime}$ and $v$ is not, then the path from $u$ to $v$ must go from the last strand of $F^{\prime}$ to $\texttt{getter}(F^{\prime})$ and then to $v$. By inductive hypothesis, the path from $\texttt{getter}(F^{\prime})$ already follows the desired property and the path from $u$ to $\texttt{getter}(F^{\prime})$ only contains join and continue edges. Therefore, the property still holds. A symmetric argument applies when $v$ is in $F^{\prime}$. ∎

We then prove the dynamic property stated in Observation 2 by looking at the execution as it unfolds. For each function $F$, we define its operating function $G$ as the function containing the “furthest join descendant” of the last executed strand of $F$. An active function is its own operating function. If a function is not active (it has returned), it may be confluent or non-confluent. It is confluent if its operating function is active; otherwise it is non-confluent. By definition, the operating function of a non-confluent function is always non-confluent. A confluent function can never be its own operating function, but a non-confluent function $F$ may be its own operating function if its $\texttt{getter}(F)$ has not yet executed.

The following lemma is proved by induction on the program as it executes.

Lemma 4.5.

(a) When a function $F$ is active, all its strands are in its $S$ bag. (b) If a function $F$ is confluent, then all its strands are in its operating function $G$’s $S$ bag. (c) If a function $F$ is non-confluent, then all its strands are in its operating function $G$’s $P$ bag.

Proof.

When a function is first called, it has an $S$ bag and its strands are placed in the $S$ bag. They remain in this $S$ bag while it is active. Once the function returns, all its items move to a $P$ bag. For the other two statements, we induct on time after $F$ returns.

Base Case: When $F$ returns, $\texttt{getter}(F)$ has not yet been called. Therefore, it is its own operating function; it is non-confluent; and all its strands are in its own $P$ bag.

Inductive Case: We will do this by two cases:

Case 1: $F$ is non-confluent and $G$ is its (non-confluent) operating function; by inductive hypothesis, all strands of $F$ are in $G$’s $P$ bag. The only thing that can make changes the location of its strands is if $\texttt{getter}(G)$ executes, say by function $H$. At this point, $H$ (which is currently active) becomes the operating function for both $G$ and $F$ — therefore, $F$ is now confluent. All strands of $F$ (and incidentally $G$) move to $H$’s $S$ bag.

Case 2: $F$ is confluent and $G$ is its (active) operating function; by inductive hypothesis, all strands of $F$ are in $G$’s $S$ bag. The only thing that changes the location of $F$’s strands is if $G$ returns. At this point $G$ becomes non-confluent (since it is no longer active); therefore $F$ also becomes non-confluent. All of $F$’s strands move to $G$’s $P$ bag. ∎

The combination of static and dynamic properties leads to the proof of correctness. The intuition is that if a function $F$ is confluent, then there is some strand $w$ in its (active) operating procedure which is a join successor of all strands of $F$ and a spawn predecessor of currently executing strand.

Theorem 4.2 0.

If the currently executing strand is $v$, then a previously executed strand $u$ is currently in an $S$ bag iff $u\prec v$.

Proof.

By Lemma 4.4, we know that if $u\prec v$, then we can find a node $w$ such that $u$ is a join predecessor of $w$ and $w$ is a spawn predecessor of $v$. By Property 1, since $v$ is executing, the function containing $w$, say $G$, is still active. Therefore, by definition, the function containing $u$ is confluent. Therefore, by Lemma 4.5, $u$ is an $S$ bag.

If $u$ does not precede $v$, then there is no path from $u$ to $v$. Therefore $u$ can not have a path to any strand $w$ in any active function (otherwise by the second statement of Property 1, since $w$ has path to $v$, $u$ will also have a path to $v$). Therefore, by definition, $u$ is non confluent. By Lemma 4.5, $u$ is in a $P$ bag. ∎

5. MultiBags+ for General Futures

We now consider general use of futures for programs that use both spawn/sync constructs and also futures. In particular, we consider programs where most of the parallelism is created using spawn and sync, but there are also $k$ future get_fut operations. For these programs, we provide a race detection algorithm that runs in total time $O(T_{1}\alpha(m,n)+k^{2})$, where $T_{1}$ is the work of the program, $\alpha$ is the inverse Ackermann’s function, $m$ is the number of memory accesses in the program and $n$ is the number of spawn and create_fut calls. To put this bound in context, a series-parallel program has $k=0$ — in this case (and in fact, for any program where $k=O(\sqrt{T_{1}})$), the MultiBags+ runs in time $O(T_{1}\alpha(m,n))$. Since the inverse Ackermann’s function grows slowly (upper bounded by $4$), this bound is close to asymptotically optimal.

As mentioned in Section 2, MultiBags+ depends on eager execution of the computation and we assume that our futures are forward-pointing. Therefore, the depth-first execution never blocks on a get_fut call since the corresponding future has already finished executing.

Notation:

Unlike in Section 4, we must distinguish between spawn and create_fut (similarly, between sync and get_fut) for MultiBags+. The computation dag consists of five kinds of nodes: (1) regular strands with one incoming and one outgoing edge; (2) spawn strands which end with a spawn instruction and have with two outgoing edges; (3) creator strands which end with a create_fut instruction and have with two outgoing edges; (4) sync strands which begin immediately after a instruction and have with two incoming edges; and (5) getter strands which begin immediately after get_fut instruction and have with two incoming edges. Some strands can have two incoming and two outgoing edges (if they start immediately after a get_fut or sync instruction and end with a spawn or create_fut); these strands are correspondingly in both categories.

The computation dag also consists of five kinds of edges: spawn edges are from spawn nodes to the first strand of the corresponding spawned function; join edges are from last strand of a spawned function to the corresponding sync node; create edges from the creator strand to the first stand of the future function; and get edges from the last strand of a future function to the corresponding getter node. Each future can have multiple get edges if it is a multi-touch future.555For context, in Section 4, both spawn and create edges were called spawn edges and both join and get edges were called join edges.

Reachability data structures:

Recall that we can model computations that employ futures as a set of series-parallel dags (SP dags) plus some non-SP edges (Section 2). When we need to check if $u\prec v$, if they are already in the same SP dag (i.e., $\text{SP-Dag}(u)=\text{SP-Dag}(v)$, as defined in Section 2), the disjoint-sets data structure maintained by MultiBags can readily answer the reachability query correctly. We only run into trouble due to use of general futures when $\text{SP-Dag}(u)\neq\text{SP-Dag}(u)$ but a path exists between them via (possibly more than one) non-SP edges.

Thus, MultiBags+ maintains two data structures, and both utilize fast disjoint-sets data structure described in Section 4. The first disjoint-sets data structure, called $D_{SP}$, is virtually identical to the data structure used in Section 4: we maintain $S$ and $P$ bags for each function, and the operations performed on $D_{SP}$ are identical to those described in Section 4 in the case of create_fut, and spawn is treated in the same way as create_fut. In addition, sync is treated like get_fut. The only difference is that we do not perform any operation on this data structure on get_fut (since we allow multi-touch futures). We can use $D_{SP}$ to correctly answer reachability query between two strands if they are in the same SP dag. Intuitively, for reasons similar to the structured case, all strands that are currently stored in an $S$ bag are sequentially before the currently executing strand. Note that all strands that are stored in a $P$ bag are not necessarily in parallel with the current strand, due to non-SP edges — we will use the second data structure to answer that query.

The second data structure handles the additional complication in reachability query when two strands are connected via non-SP edges. This data structure has two components: (1) a disjoint-sets data structure called $D_{NSP}$ that maintains a collection of disjoint-sets, and each strand is added to $D_{NSP}$ when encountered; and (2) a separate dag called $\mathcal{}R$ that contains some of the sets from $D_{NSP}$. The high-level idea is that these sets are made of connected series-parallel subdags of the original dag $G_{\mathit{full}}$. For any two nodes $u$ and $v$ in different SP dags, MultiBags+ ensures that $u\prec v$ in $G_{\mathit{full}}$ iff $\textnormal{Find}(D_{NSP},u)\prec\textnormal{Find}(D_{NSP},v)$ in $\mathcal{}R$ (the sets they are in are connected in $\mathcal{}R$).

We call sets also in $\mathcal{}R$ as the attached sets, which store nodes that are subdags which start and/or end with creator or getter strands.666This is not quite accurate; for technical reasons, some attached sets start/end with regular, spawn, and join nodes as well. $\mathcal{}R$ explicitly maintains reachability relationship that arises due to non-SP edges between nodes in the attached sets. $\mathcal{}R$ is simply a dag (with each node being an attached set), but it is not series-parallel. Thus, to answer reachability queries quickly between nodes in $\mathcal{}R$, MultiBags+ maintains a full transitive closure of all sets in $\mathcal{}R$ — whenever a set is added to $\mathcal{}R$, its reachability from all sets already added to $\mathcal{}R$ is explicitly computed and stored. Therefore, one can check if $A\prec B$ in $\mathcal{}R$ in constant time.

If every set could be in $\mathcal{}R$ we would be done. We must keep $\mathcal{}R$ small, however, since every time we add a set to $\mathcal{}R$ we compute a full transitive closure, which is expensive. It turns out that it is difficult to simultaneously put all strands in attached sets and keep $\mathcal{}R$ small. In order to cope with this, some strands are in unattached sets, which are only stored in $D_{NSP}$. Intuitively, an unattached set contains nodes of a complete series-parallel subdag which have no incident non-SP edges. Each unattached set $U$ has two additional fields, attached predecessor and attached successor, which point to attached sets that act as $U$’s proxies when querying $\mathcal{}R$. $U$’s attached predecessor, denoted as $U.attPred$, is set when $U$ is created; therefore, it always points to some attached set. $U$’s attached successor, denoted as $U.attSucc$, is set at some later point; it either points to some attached set or may be null. An attached set is always its own attached predecessor and successor. We will overload notation and say that node $u$’s attached predecessor is $\textnormal{Find}(D_{NSP},u)$’s attached predecessor (and similarly for attached successor).

Answering queries:

Figure 3 shows how the reachability data structures are queried to find out if a path exists between some previously executed node $u$ and the currently executing node $v$. In the first part of the query (lines 3–3), we query $D_{SP}$ and if $u$ is in the $S$ bag, then we can conclude that $u\prec_{\mathit{full}}v$ and return. If $u$ is in the $P$ bag, then we check if attached successor of $u$ precedes the attached predecessor of $v$ in $\mathcal{}R$; if so, we say that $u\prec_{\mathit{full}}v$. Otherwise $u$ is in parallel with $v$.

Maintaining $D_{SP}$, $D_{NSP}$, and $\mathcal{}R$:

Figure 4 shows the code for maintaining reachability relationships between nodes in the computation. The first thing we do during a spawn, create_fut, return and sync is to manipulate $D_{SP}$ (lines 4, 4, 4, and 4) in a manner identical to Section 4.777Since we are assuming binary forking, we sync with one function at a time.

Now lets consider the manipulations of $D_{NSP}$ and $\mathcal{}R$. It uses an auxiliary function $\textnormal{Attachify}(u)$, which simply checks if $U_{u}=\textnormal{Find}(D_{NSP},u)$ is an unattached set, and if so, converts it into an attached set by adding it to $\mathcal{}R$ and adding an edge from $U_{u}.\mathit{attPred}$ to $U_{u}$ in $\mathcal{}R$.

The attached and unattached sets change as the execution continues. MultiBags+ unions sets in $D_{NSP}$ growing both attached and unattached sets. Two attached sets are never unioned together. Whenever we union an attached set and an unattached set, we always union the unattached set into the attached set; therefore, the resulting set is attached and remains in $\mathcal{}R$. On the other hand, an unattached set contains nodes of a complete series-parallel subdag which have no incident non-SP edges. In particular, consider a parallel composition of two series-parallel subdags $G_{1}$ and $G_{2}$. Say $G_{1}$ has no incident non-SP edges. Then all nodes of $G_{1}$ constitute an unattached set if either the join node that joins $G_{1}$ and $G_{2}$ has not executed yet, or if $G_{2}$ has an incident non-SP edge. At a high-level, this design allows us to have the property that each non-SP edge only leads to a constant number of attached sets. Since only attached sets are in $\mathcal{}R$, this idea allows us to keep $\mathcal{}R$ small, allowing us to get good performance.

Figure 5 shows a computation dag with futures and its corresponding $\mathcal{}R$ at the end of the computation. As can be seen in this example, sets $X,Y$ and $Z$ are all unattached and each have the above property. In Appendix A, Figure 9 shows the dag when it has been partially executed while nodes 23 and 31 are executing, respectively and all unattached sets in those examples also have this property.

Due to space limitations, all the proofs are omitted to Appendix A. Here we simply state the performance and correctness theorems.

Theorem 5.1.

MultiBags+ detects races in time $O(T_{1}\alpha(m,n)+k^{2})$ for programs with $T_{1}$ work, $k$ get_fut calls, $m$ memory accesses, and $n$ number of strands.

Theorem 5.2.

If the program is executed in a depth first eager execution order, $\textnormal{Query}(u,v)$ returns true iff $u\prec v$ in $G_{\mathit{full}}$.

Comparison to algorithm by Agrawal et al. (Agrawal et al., 2018):

As we have fully described the MultiBags+ algorithm, we discuss the differences between MultiBags+ and the the-of-the-art algorithm by Agrawal et al. (Agrawal et al., 2018) and provide an analytical analysis as to why the algorithm by Agrawal et al. is much more challenging to implement in practice.

The algorithm by Agrawal et al. utilizes the following data structures to answer reachability queries: 1) an order-maintenance data structure for answering series-parallel queries; 2) the full computation DAG to update and maintain “anchor-predecessors” and “proxies” used to infer “anchor-successors;” and 3) a reachability matrix $\mathcal{}R$ which contains anchor nodes to answer reachability queries involving non-SP edges. The functionalities served by these data structures are similar to that of $D_{SP}$, $D_{NSP}$, and $\mathcal{}R$ in MultiBags+; in particular, their algorithm utilize anchor-predecessors and anchor-successors to allow for correct reachability queries involving non-SP edges, sharing similar roles as the attached predecessors and attached successors in MultiBags+. The main difference is in the second data structure and how the anchor-predecessors and anchor-successors are maintained.

In the algorithm by Agrawal et al., the mechanism for maintaining anchor-predecessors and proxies (which are used to infer anchor-successors) are more complex. In particular, to maintain anchor-predecessors, the algorithm maintains the full computation dag, and each strand (a node in the dag) explicitly stores its anchor-predecessor. However, anchor-predecessors can sometimes change as the program executes. When that occurs, the algorithm must explicitly traverse subpart of the dag and update some of the predecessors explicitly. The asymptotic complexity of such updates is still ok because the paper argues that a strand’s anchor predecessor can only change a constant number of times.

Similarly, the algorithm maintains a proxy per strand, used to infer a strand’s anchor-successor. A proxy for a strand is stored instead of its anchor-successor is because, while an anchor-predecessor of a node can change a constant number of times, its anchor-successor can change many times. Thus instead, the algorithm maintains a proxy, which indirectly allows the algorithm to deduce its anchor-successor. Like the anchor-predecessor, a proxy of a node can only change a constant number of times, and when that occurs, the algorithm again explicitly traverses the relevant subdag and updates the proxies explicitly.

We argue that this algorithm is harder to implement and likely has higher overheads due to the following reasons. First, explicitly maintaining the entire program dag and also storing each strand’s anchor-predecessor and proxy would be more memory intensive than keeping these strands in union-find data structures which are tagged appropriately. Second, explicit dag traversals in order to update proxies and anchor-predecessors of nodes would be expensive (even though the asymptotic complexity is manageable). This prior work establishes the state-of-the art time bound for race detecting programs that use general futures, but no implementation exists.

6. Experimental Evaluation

This section empirically evaluates FutureRD that implements MultiBags and MultiBags+ described earlier. We first evaluate the practical efficiency of these algorithms and then the performance difference between them, focusing on the impact of the additional $k^{2}$ overhead that MultiBags+ incurs, where $k$ is the number of get_fut operations.

Implementation of FutureRD

FutureRD works by instrumenting parallel program executions: upon the execution of a parallel construct (i.e., spawn, sync, create_fut, and get_fut), it invokes the necessary operations to update the reachability data structures; likewise, upon the execution of a memory access, it invokes the necessary operations to update the access history data structure and query both data structures.

We use Intel Cilk Plus (Intel, 2013) as our language front end, which is a C/C++ based task parallel platform that readily supports fork-join parallelism. Cilk Plus does not currently support the use of futures, however, so we have implemented our own future library. Since our race detector executes the program sequentially with eager evaluation of futures, the future library never actually interacts with Cilk Plus runtime during race detection.

Both MultiBags and MultiBags+ utilize disjoint-sets data structures to maintain reachability as described in Section 4). MultiBags+ additionally needs to maintain $\mathcal{}R$ as part of its reachability data structure (defined in Section 5). Conceptually, $\mathcal{}R$ is simply a boolean reachability matrix where each cell $(i,j)$ indicates whether there is a path from attached set $i$ to attached set $j$. FutureRD maintains $\mathcal{}R$ as a vector of bit vectors, representing the reachability between any two sets using a single bit. Whenever an edge is added to $\mathcal{}R$, reachability is transitively propagated via parallel bit operations.

FutureRD maintains the access history like a two-level direct-mapped cache, and keeps track of the reader list and last writer at four-byte granularity (all our benchmarks perform four-byte or larger accesses). That is, to query or update readers/writers for an address $a$, the more significant bits of $a$ are used to index into the top-level table and the rest of the bits are used to index into the second-level table.

Experimental setup

We evaluate FutureRD using six benchmarks: longest-common subsequence (lcs), Smith-Waterman (sw), matrix multiplication without temporary matrices (mm), binary tree merge (bst) as described by Blelloch and Reid-Miller (1997), Heart Wall Tracking (heartwall), and Dedup (dedup). Heart Wall Tracking and Dedup both contain parallel patterns that cannot be easily implemented using fork-join constructs alone. The Heart Wall Tracking algorithm is adapted from the Rodinia benchmark suite (Che et al., 2009) that tracks the movement of a mouse heart over a sequence of ultrasound images. Dedup is a compression program that exhibits pipeline parallelism (Bienia and Li, 2010), taken from the Parsec benchmark suite (Bienia et al., 2008). All but dedup have two implementations: structured and general futures; dedup does not utilize the flexibility of general futures. We use the following input sizes: lcs uses $N=16k$, mm and sw use $N=2048$, heartwall uses $10$ images, dedup uses input large, and bst uses input tree sizes $8\mathrm{e}6$ and $4\mathrm{e}6$. For Figures 6 and 7, we use base case $B=\sqrt{N}$ for lcs, mm, and sw to keep the work the same for the baseline, MultiBags, and MultiBags+ (since MultiBags+ has $k^{2}$ additional overhead). We then vary the base case size for Figure 8.

We ran our experiments on an Intel Xeon E5-4620 with $32$ 2.20-GHz cores on four sockets. Each core has a 32-KByte L1 data cache, 32-KByte L1 instruction cache, a 256-KByte L2 cache. There is a total of 500 GB of memory, and each socket shares a 16-MByte L3-cache. All benchmarks are compiled with LLVM/Clang 3.4.1 with -O3 -flto running on Linux kernel version 3.10. Each data point is the average of $5$ runs with standard deviation less than $5\%$ with the exception of running dedup with full race detection, which sees a standard deviation under $9\%$.

Practical efficiency of FutureRD

First, we evaluate the overhead of FutureRD and show that the algorithms can be implemented efficiently. To get the sense of where the overhead comes from, we ran the application benchmarks with four configurations:

• $\bullet$

baseline: running time without race detection;

• $\bullet$

reachability: running time with only the reachability components, including the instrumentation overhead to capture parallel control constructs;

• $\bullet$

instrumentation: running time with memory-access instrumentation overhead on top of the reachability configuration, but does not maintain or query the access history;

• $\bullet$

full: running time with the full race detection overhead.

Figure 6 shows the list of programs that employ structured futures running with different configurations, where FutureRD maintains reachability using the MultiBags algorithm. First, observe that the reachability configuration incurs almost no overhead, except for bst, which has very little work per parallel construct. Since the operations on the disjoint-sets data structure are very efficient, as long as there is sufficient work per parallel construct, the overhead of maintaining reachability in MultiBags should be low. These program contains large number of memory accesses, however, and thus adding instrumentation for memory accesses alone incurs additional $2$–$4.5\times$ overhead.

Going from the instrumentation configuration to the full race detection incurs another $6$–$10\times$ overhead, with the exception of dedup. We expect the additional overhead incurred to be about $8$–$10\times$ because the full configuration transforms every memory access into updates to access history and queries to both access history and reachability data structures. Thus, each memory access is translated into a few function calls and several pointer chases to multiple data structures. The benchmark heartwall only incurs additional $6\times$, because it spends non-negligible amount of time performing I/O (reading in image files). Finally, dedup is an outlier because dedup calls into a dynamic library to perform compression, which we could not recompile to include instrumentation. Thus, any memory accesses performed within the library do not incur additional overhead. Since the compression takes up a substantial amount of execution time, the additional overhead is small.

Figure 7 shows the runtime of programs that employ general futures where FutureRD maintains reachability using the MultiBags+ algorithm. The additional overhead incurred going from one configuration to the next is similar to Figure 6 except the higher overhead from MultiBags+ is evident in the reachability configuration.

Over five benchmarks (excluding dedup, since we could not instrument its compression library), we see a geometric mean overhead of $1.06\times$ and $1.40\times$ to maintain reachability using MultiBags and MultiBags+, respectively. Full race detection exhibits $20.48\times$ and $25.98\times$ overhead, respectively.

Comparison between MultiBags and MultiBags+

Next, we compare the performance difference between MultiBags and MultiBags+. To evaluate the overhead difference between them, we run the same programs (i.e., with structured futures) with both algorithms. Although MultiBags+ is designed for general futures, it also works with programs that use structured futures, albeit with an additional $k^{2}$ overhead, where $k$ is the number of get_fut calls.

For lcs, sw, and mm, $k$ is dictated by how much the base case is coarsened — the smaller the base case, the more get_fut calls, and the higher $k$ is (which leads to higher overhead). Runtimes shown before used base case of $B=\sqrt{N}$ to keep the work asymptotically the same across baseline, MultiBags, and MultiBags+. Now we decrease the base case size below (i.e., increase $k$) to see how the overhead of MultiBags+ changes compared with the overhead of MultiBags.

Figure 8 shows the measurements for running programs with structured futures using MultiBags and MultiBags+ in the reachability configuration with different base cases. The overhead difference between MultiBags and MultiBags+ can readily be observed in Figures 6 and 7 — compared to MultiBags, MultiBags+ incurs $2+\times$ more overhead running dedup and $3+\times$ more running bst for maintaining reachability. Here we show additional numbers for benchmarks where varying base case sizes changes $k$.

The measurements with lcs and mm bear out the extra overhead of MultiBags+. The lcs benchmark has $\Theta(n^{2})$ work versus $\left(n/B\right)^{2}$ futures, while mm has more work ($\Theta(n^{3})$), but also requires $(n/B)^{3}$ futures. With a higher ratio of futures to total work, the overhead is more apparent. Moreover, the memory required for the reachability matrix $\mathcal{}R$ becomes substantial for small base cases, adding more overhead. The sw benchmark, however, has $\Theta(n^{3})$ work compared to $\left(n/B\right)^{2}$ futures, so the effect of smaller base cases is small.

7. Related Work

Besides works discussed in Section 1, researchers have considered race detection for other structured computations. Dimitrov et al. (2015) propose a sequential near-optimal race detection algorithm for two-dimensional dags which also exhibit nice structural properties. Subsequently, Xu et al. (2018) propose a race detector for two-dimensional dags with asymptotically optimal parallel running time. Lee and Schardl (2015) propose a sequential race detector for fork-join computations with reductions, where the computation dag is almost series-parallel except when reductions are performed.

Beyond task parallel code, there is a rich literature on race detection for programming models that generate nondeterministic computations, such as ones that employ persistent threads and locks. For such models, since the dag necessarily depends on the schedule, the best correctness guarantee that a race detector can provide is for a given program, for a given input, and for a given schedule. Early work (Savage et al., 1997; von Praun and Gross, 2001) employs lock-set algorithm, which provides wide coverage but can lead to many false positives, because it cannot precisely capture happens-before (HB) relations formed between threads.

A vector-clock (VC) based algorithm such as one proposed by Flanagan and Freund (2009) can capture HB precisely for a given schedule. Such algorithm can be used on computation with arbitrary dependences, but naively applying it to task parallel code would be impractical, since it requires storing a VC of length $n$ with each each memory location querying against it per access, incurring a multiplicative factor of $n$ overhead on top of the work, where $n$ is the number of strands, which can be on the order of millions.

In the context of race detecting nondeterministic code, researchers have investigated hybrid approaches incorporating VC and lock-set (O’Callahan and Choi, 2003; Pozniansky and Schuster, 2003; Yu et al., 2005; Serebryany and Iskhodzhanov, 2009) to trade-off precisions and coverage. More recently, researchers have proposed predictive analysis to explore alternative feasible schedules among close by instructions to increase the coverage (e.g. (Smaragdakis et al., 2012; Said et al., 2011; Liu et al., 2016; Kini et al., 2017)) while keeping the precision.

Acknowledgements

This research was supported in part by National Science Foundation grants CCF-1150036, CCF-1527692, CCF-1733873, and XPS-1439062. We thank the referees and our shepherd for their excellent comments.

Appendix A Proofs from Section 5

Proof of Performance of MultiBagsPlus

Theorem 5.1 0.

MultiBags+ detects races in time $O(T_{1}\alpha(m,n)+k^{2})$ for programs with $T_{1}$ work, $k$ get_fut calls, $m$ memory accesses, and $n$ number of strands.

Proof.

We create three new attached sets when we encounter a create_fut edge and 2 new sets when we encounter a get_fut edge. The only interesting part is when we encounter a sync (lines 4–4). When neither of the component SP-dags have a non-SP edge (lines 4–4) or if only one of them has a non-SP edge(lines 4–4), no new attached sets are created. The only case where (at most two) additional attached sets are created is if both subcomponents have non-SP edges (lines 4–4). The total number of such sync nodes is $O(k)$. Therefore, MultiBags+ creates $O(k)$ attached sets. Each time an attached set is created, it takes $O(k)$ time to insert it into $\mathcal{}R$ since MultiBags+ maintains a transitive closure. Other than this, each operation (Make-Set, Union and Find) into $D_{SP}$ and $D_{NSP}$ runs in $\alpha(m,n)$. As we argued in Section 3, each memory access generates a constant number of queries. We see from the code that each query leads to a single Find into $D_{SP}$ and a constant number of Finds into $D_{NSP}$. Therefore, the total cost of race detection is $O(T_{1}\alpha(m,n)+k^{2})$. ∎

Proof of Correctness of MultiBags+

We will use the example of Figure 5 to illustrate the proof. Figure 9 shows the same dag and the corresponding $\mathcal{}R$ with all the attached and unattached sets when it has been partially executed while nodes 23 and 31 are executing, respectively.

We will redefine the terminology a little bit differently than Section 4. A node $u$ is a spawn predecessor of a node $v$ if there is a path from $u$ to $v$ which consists of only spawn, create and continue edges. A node $u$ is a join predecessor of $v$ if there is a path from $u$ to $v$ that consists of only join and continue edges. Notice the asymmetry here — a creator node is the corresponding future’s spawn successor, but the future is not the getter node’s join predecessor. This mimics the actions of the algorithm on $D_{SP}$, since spawn and create_fut behave identically while sync and get_fut do not.

We can now define operating function and confluence in the manner identical to Section 4 and it should be clear that Property 1 and Lemma 4.5 still hold.

First consider the first part of the query, where we just check if $u$ is in the $S$-bag. As shown in lines 4 and 4, when a function $F$ calls either $\texttt{spawn}(G)$ of $\texttt{create{\char 95\relax}fut}(G)$, the algorithm exactly mimics MultiBags, simply creating an $S$-bag for $G$ containing the first node of $G$. Similarly, on function $G$’s return, $S_{G}$ becomes $P_{G}$. Finally, when a function $F$ calls sync on function $G$, it mimics get_fut in structured future and $P_{G}$ is unioned in $S_{F}$. The only difference is that nothing happens on get_fut to $D_{SP}$. Therefore:

Lemma A.1.

Consider the currently executing strand $v$ and a previously executed strand $u$. The following is true: (a) If $u$ is in an $S$ bag, then $u\prec v$; further more, there is a path from $u$ to $v$ consisting of only spawn, create, join and continue edges. (b) If there is a path from $u$ to $v$ consisting of only spawn, create, join and continue edges (no get edges), then $u$ is in an $S$ bag.

Proof.

Since moves to $S$-bags happen in a more restricted setting here than in Section 4, statement (a) follows somewhat intuitively from Section 4. More formally, from Lemma 4.5, if $u$ in an $S$ bag, then either the function containing $u$ is active, or $u$’s operating function is active. Therefore, either $u$ or some join successor of $u$ is part of an active function — therefore, $u$ is sequentially before $v$ by Property 1.

For (b), say $X=\text{SP-Dag}(u)$ and let $w$ be the last node in $X$ on the path from $u$ to $v$ (if $v$ is in $X$, then $v=w$). Since the path from $u$ to $w$ does not contain any get_fut edges, this path can not go through any create_fut edges either (since a create_fut edge will take execution out of $X$ and one would need a get_fut edge to come back). Therefore, since SP dags are a special case of structure futures, and $u$ is sequentially before $w$, $u$ must have been in some $S$ bag when $w$ executed (from Theorem 4.2). After $w$ executed, no strand of $X$ was executed, therefore $u$ can not have moved to a $P$ bag since then. ∎

We now consider the case when $D_{SP}$ returns false and use $D_{NSP}$. Here, we must prove that if $u$ is in a $P$ bag when $v$ executes (otherwise, the query returned), then $u\prec_{\mathit{full}}v$ iff there is a path in $\mathcal{}R$ from $u.\mathit{attSucc}$ to $v.\mathit{attPred}$. We have to make a few observations in order to see this.

The following two lemmas state some structural properties of attached and unattached sets and can be proven by inducting on set unions done by the algorithm.

Lemma A.2.

Each unattached set consists of the nodes belonging to a maximal series-parallel subdag $Q$ such that (1) all nodes in the subdag have been executed, (2) there are no create_fut or get_fut edges in $G_{\mathit{full}}$ incident on nodes in $Q$, (3) there are at most two arcs in $G_{\mathit{full}}$ incident on nodes in $Q$—one directed towards $Q$’s source, and one directed out from $Q$’s sink.

Proof.

Induct on the construction. When we create an unattached set, it consists of a single node. When we merge sets without marking them attached, they are always complete series parallel dags (lines 4–4) with no incident non-SP edges. ∎

Lemma A.3.

The nodes in each attached set induce a series-parallel subdag $Q$ such that if we contract all maximal series parallel dags within it, it forms a chain.(1) if there is a get_fut or a create_fut edge directed towards a node in $Q$, then it is directed towards the source, (2) if there is a get_fut or create_fut edge directed from a node in $Q$, then it originates on the sink. Unlike the unattached sets, attached sets do not necessarily match the series-parallel decomposition of $G_{\mathit{full}}$—an attached set may have many incoming or outgoing edges.

Proof.

We induct on the growth of sets. The sets always start by containing single nodes. We union sets at two places: On lines 4–4, we union an entire series-parallel subdag together. In this case, the sets containing $t_{1}$ and $t_{2}$ are unattached and have no incident non-SP edges by Lemma A.2. Therefore, only the set containing $f$ may be attached. By induction, it can only have an incident non-SP edge at its source node. Before the unions, Its sync node is $f$ and it clearly does not have an outgoing non-SP arc since it is a spawn node, not a create_fut node.

On line 4, we union the set which contains a spawn node $f$ with a set containing one of spawn’s successors $s_{a}$. By induction, the set containing $f$ only has an incident non-SP edge towards its source. Similarly, the set containing $s_{a}$ can only have a non-SP edge directed away from its sink node (again $s_{a}$ is its source node and it does not have a non-SP edge directed towards it since its previous instruction $f$ is not a get_fut or sync call).

Similarly, on line 4, we union a sync node with a set containing sync nodes successor. Again, we induct in a similar manner. ∎

We can see that the above lemmas are true for examples shown in Figures 5 and 9. From the above two lemmas, we can see that if $u$ and $v$ are in the same attached or unattached set, and $u\prec_{\mathit{full}}v$ then $u\prec_{SP}v$ since $u$ and $v$ are in the same SP-dag and there are no incoming or outgoing non-SP edges to nodes within the dag except at the source and sink. Therefore, $D_{SP}$ will answer the query between them correctly.

The following key lemma says that the relationship between nodes in two different attached sets is always correctly represented in $\mathcal{}R$.

Lemma A.4.

Consider nodes $u$ and $v$, where $A_{u}=\textnormal{Find}(D_{NSP},u)$ and $A_{v}=\textnormal{Find}(D_{NSP},v)$ are distinct attached sets. Then $u\prec_{\mathit{full}}v$ iff $\textnormal{Find}(D_{NSP},u)\prec_{\mathcal{}R}\textnormal{Find}(D_{NSP},v)$.

The proof of the lemma is complicated and depends on many structural properties of the sets; however, there are two main intuitions. First, if we only consider only attached sets containing nodes of a single series parallel dag $D$ (ignoring all create_fut and get_fut edges) then the attached sets form the same series parallel relationship as $D$. This can be seen from in Figure 5 where $A,B,C,E,I,J,K,L,M$ and $N$ form a series parallel dag and induce the same dependencies as the original dag. Therefore, if the path from $u$ to $v$ doesn’t contain any create_fut or get_fut edges, then we get the correct relationship.

Second, say there is a path $p$ from $u$ to $v$ which contains create_fut and get_fut edges. Walk along the path from $u$ until we encounter the first such edge. Let $w$ the source of this edge and $x$ be the destination. If both $u$ and $w$ are in attached sets, then there is a path from $u$ to $w$ in $\mathcal{}R$ (from the previous paragraph). In addition, there is an edge from $w$ to $x$ in $\mathcal{}R$ (since $w$ is the creator node and $x$ is the first node of a future and we explicitly add this edge on line 4). Therefore, there is a path from $u$ to $x$ in $\mathcal{}R$. We can then find the next create_fut or get_fut edge on this path and continue with the induction. Again, we can see this in Figure 5 where there is a path from $C$ to $I$ via $D$ and also a path from $C$ to $L$ via $E,F$ and $G$.

In order to prove Lemma A.4 formally, we will define two kinds of attached sets. Intuitively, prefix-complete sets are those where the first node added to the set is the source node of the set and the set can grow in the forward direction; and suffix-complete sets are those where the first node added is the sink node of the set and the set can grow in the backward direction by unions with unattached sets.

We first understand the structure of prefix-complete attached sets. Consider an attached set $A$ where the first node added to $u$. $A$ is prefix complete if $u$ is either (1) the strand immediately after a get_fut node (line 4); or (2) $u$ the first node in the continuation of a creator node (line 4); or (3) $u$ is the first node of a future function (line 4); or (4) a sync node where both its subdags that are joining are attached (line 4).

Lemma A.5.

If $u$ is the first node added to a prefix-complete attached set $A$, then for all other nodes $v\in A$, we have $u\prec v$. In addition, consider a node $v\in A$ where $A$ is a prefix-complete attached set. (1) If there is an edge $(v,w)$ in $G_{\mathit{full}}$ such that $w$ is not in $A$, then $v$ must be the sink node of $A$. (2) If there is any edge $(w,v)$ in $G_{\mathit{full}}$ where $w$ is not in $A$, then $v$ is either the source or $w$ is in an unattached set.

Proof.

The first statement is clear by construction. Any attached set constructed in one of the ways described above will never union with an unattached set that has nodes that precede $u$. In particular, we can induct on the growth of a prefix-complete set to show all the properties described above. ∎

Consider an attached set $A$ where the first node added to $u$. $A$ is suffix-complete if $u$ is either (1) the strand ending with a create_fut instruction (line 4); or (2) the node immediately preceding the getter node in the SP dag of the getter node (line 4); or (3) the spawn node where both spawned subdags are attached (line 4).

Lemma A.6.

If $u$ is the first node added to a prefix-complete attached set $A$, then for all other nodes $v\in A$, we have $v\prec u$. Consider a node $v\in A$; if there is an edge $(w,v)$ in $G_{\mathit{full}}$ such that $w$ is not in $A$, then $v$ must be the source node of $A$. In addition, if there is any edge $(v,w)$ in $G_{\mathit{full}}$ where $w$ is not in $A$, then $v$ is either the sink or $w$ is in an unattached set.

Proof.

Again, we can induct on the growth of sets created by the above methods. ∎

The following is a surprising lemma. Basically, a suffix-complete attached set is never an unattached set’s attached successor or predecessor.

Lemma A.7.

If an attached set $A$ is an attached predecessor or an attached successor of an unattached set $U$, then $A$ must be prefix-complete.

Proof.

A set $A$ is set as an attached successor (on line 4) when a join node $j$ unions with $A$. In this case, $A$ is clearly growing in the forward direction and must be prefix complete. The first node of the entire computation, is by definition, prefix-complete. After this, we can see that attached predecessor is always prefix-complete by inducting on the execution. ∎

We now consider nodes in unattached sets and argue that they have the correct relationship with their predecessors. If $u$ is in an unattached set, then we use $u.\mathit{attPred}$ as a proxy for $u$ when we do the query. The following lemma argues that it is always correct to use this proxy.

Lemma A.8.

At any point during the execution, for an unattached set $U$, if $A=U.\mathit{attPred}$, then for all $u\in A$ and $v\in U$, we have $u\prec_{SP}v$. In addition, there is no incoming create_fut or get_fut edge on any node in the path from $u$ to $v$ (not including $u$).

Proof.

First, recall that $A$ must be a prefix-complete set (Lemma A.7), and the only edges leaving in $G_{\mathit{full}}$ can be from its sink node. Therefore, if any node $u$ in $A$ precedes $v$, then they all must.

The fact that some node $v$ in $A$ must precede $u$ can be seen by induction. If $v$ has only one immediate predecessor $w\in\text{SP-Dag}(v)$, then $v$’s attached predecessor is set as $w$’s attached predecessor (lines 4 and 4). If $v$ has two immediate predecessors ($v$ is a join node), then $v$ is either in an attached set (lines 4 and 4) or it is in the same set with both its predecessors. ∎

We can also see this from our examples. The example of set $X$ is particularly interesting. Note that its attached predecessor is not $C$ — this is because $C$ was not an attached set when $X$ executed — it only became an attached set later. However, note that all nodes in $A$ are in fact before all nodes in $X$ and there is no intervening incident non-SP edge. Similar observations can be made for set $Z$ whose attached predecessor is $A$ instead of $K$ since node 26 was not in $K$ when $Z$ executed (as seen in Figure 9 (right)). However, it is still correct for $Z$’s attached predecessor to be $A$ since every node in $A$ precedes every node in $Z$ and there is no non-SP edge on any path from a node in $A$ to a node in $Z$.

We can now prove that $\mathcal{}R$ has the correct relationships between attached sets.

Lemma A.4 0.

Consider nodes $u$ and $v$, where $A_{u}=\textnormal{Find}(D_{NSP},u)$ and $A_{v}=\textnormal{Find}(D_{NSP},v)$ are distinct attached sets. Then $u\prec_{\mathit{full}}v$ iff $\textnormal{Find}(D_{NSP},u)\prec_{\mathcal{}R}\textnormal{Find}(D_{NSP},v)$.

Proof.

We first argue that if $\textnormal{Find}(D_{NSP},u)\prec_{R}\textnormal{Find}(D_{NSP},v)$, then $u\prec_{\mathit{full}}v$. We can induct on order in which edges are added in $\mathcal{}R$. Let $A_{u}=\textnormal{Find}(D_{NSP},u)$ and $A_{v}=\textnormal{Find}(D_{NSP},v)$. If $v$ is the first node added to $A_{v}$ via $\textnormal{Attachify}(v)$, then all the incoming edges to $A_{v}$ are from $v.\mathit{attPred}$ — therefore, from Lemma A.8, all paths into $A_{v}$ are correct. If $A_{v}$ is directly created (lines 4, 4, and 4) then we explicitly only add the edges into $A_{v}$ in $\mathcal{}R$ which are correct in $G_{\mathit{full}}$. Also, at this point, either $A_{v}$ has no outgoing edges or the correct outgoing edges are explicitly added.

When we execute a sync, we may union unattached sets into attached sets, and we must ensure that the property still holds. (1) When both subdags of an SP dag are unattached, they are both unioned into the set containing the source and the join is also unioned into the same set (lines 4–4). In this case, the only things that can precede these unattached sets also precede the source. (2) When both subdags are attached, no unions happen. (3) When one subdag is attached, the join node $j$ is added to the set that contains one of the predecessor of $j$ (line 4) — therefore, it must be the case that a node that precedes the predecessor of the join node also precedes $j$. In addition, no node succeeds $j$ yet, so the other direction is trivial. The source node union (line 4) is the interesting case. Here $s$ is unioned into a suffix-complete attached set $s_{a}$. Therefore, $s_{a}$ has only one incoming edge and by definition, it is from $s$. Therefore, anything that precedes nodes in $s_{a}$ must also precede $s$ and anything that succeeds nodes in $s_{a}$ must also succeed $s$.

Now we argue that if $u\prec_{\mathit{full}}v$, then either $u$ and $v$ are in the same attached set or the set containing $u$ precedes the set containing $v$ in $\mathcal{}R$. First observation is that $\mathcal{}R$ is always a connected dag — this is easy to see since whenever we add a node in $\mathcal{}R$, we also add an arc to it.

Second, if $u$ and $v$ are in the same SP-dag, and they are not in the same attached set, then there is a path from $A_{u}$ to $A_{v}$ in $\mathcal{}R$. We can again see this by induction on composition of SP dags. In the base case, $u$ and $v$ are in different attached sets, we immediately add an edge from $u$ to $v$. After this, assuming there is always an edge from the source to sink in the smaller sp dag, we always either merge the entire sp-dag into the same set (lines 4–4), or add edges from source to both sub dag sources (lines 4–4) and from subdag sinks to the sink (lines 4–4) or we merge the source into one of the subdag sources (line 4) and sink to one of the subdag sinks (line 4).

If $u$ and $v$ are in different SP dags, we induct on the path from $u$ to $v$. Let $w$ be the last node in $\text{SP-Dag}(u)$ and $x$ be the node immediately after $w$ in the path from $u$ to $v$. Both $w$ and $x$ are in attached sets and there is a path from $u$ to $w$ in $\mathcal{}R$ (from the previous paragraph) and an edge from $w$ to $x$ in $\mathcal{}R$ (since $w$ is the creator node and $x$ is the first node of a future and we explicitly add this edge on line 4). Therefore, there is a path from $u$ to $x$. We can then induct on this path and keep moving forward until we get to the dag containing $v$. ∎

Finally, we must make claims about attached successors of unattached sets. We first show a structural property of unattached sets.

Lemma A.9.

For a node $u$, let $C_{u}$ be the closest completed series-parallel dag which is a parallel composition and whose sink node has already executed. If $u$ belongs to an unattached set with no attached successor, then all nodes of $C_{u}$ belong to this same unattached set.

Proof.

When a sink node of a parallel composition following an unattached set executes, the unattached set either gets an attached successor line 4, or all the nodes of the parallel composition are unioned into the same set lines 4–4. ∎

The following lemma claims that if a node $u$ has an attached successor, then there is a path from $u$ to the last node of the attached successor.

Lemma A.10.

Consider a node $u$ where $U_{u}=\textnormal{Find}(D_{NSP},u)$ is unattached. If $U_{u}$ has an attached successor $A$, then $u\prec_{SP}v$ where $v$ is the current sink of this attached successor $A$. In addition, consider any node $w\not\in U_{u}$. If $u\prec_{\mathit{full}}w$ then $v\prec_{\mathit{full}}w$. Finally, we have $u\prec w$ for any node $w$ added to $A$ after it becomes $U_{u}$’s attached successor.

Proof.

Attached successor is set on line 4 where the attached successor always contains the sync node $j$ following the $U_{u}$. Since an unattached set is a complete series-parallel dag with no incident create_fut or get_fut edges (Lemma A.2), any path from $u$ must go through this node $j$ from the property of series-parallel dags. At this point $j$ is the current sink of $A$. Any nodes $w$ subsequently added to $A$ must have the property that $j\prec w$ from the construction of attached sets(Lemma A.3). Therefore, the property remains true by induction. ∎

The important subtlety here is that not all nodes of $U_{u}$’s attached successor have to be after $u$ — consider the set $Z$ in our example with attached successor $L$. Node 28 does not follow $Z$, but $L$ becomes $Z$’s attached successor only after node 33 is added to $L$. (Notice that $L$ is not $Z$’s attached successor in Figure 9 (right) since 33 has not yet executed.)

Now we can argue about the correctness of the query $\textnormal{Query}(u,v)$ where both $u$ and $v$ may be parts of unattached sets. Say $u$ has an attached successor $A_{1}$ and $v$ has an attached predecessor $A_{2}$ and there is no path from $u$ to $v$ that contains only series-parallel edges (otherwise, the first part of the query will give the correct answer), but there is a path $p$ from $u$ to $v$ containing create_fut and get_fut edges. This path must go through the last node of $A_{1}$ (Lemma A.10. In addition, since there are no incident non-SP edge between nodes in $A_{2}$ and $v$ (Lemma A.8), this path must also go through $A_{2}$. Therefore, it is sufficient to check the relationship between $A_{1}$ and $A_{2}$ to check the relationship between $u$ and $v$. In a similar manner, we can also show that we get the correct answer when only one of $u$ and $v$ are in unattached sets.

This final lemma handles the case where $u$ does not have an attached successor. This is where we utilize the condition that the program is executing in depth-first eager order and that $v$ is the currently executing node. The intuition for this lemma is as follows: Since $u$ is in an unattached set, no node in this unattached set has any outgoing non-SP edges. In addition, the nearest join after this set hasn’t executed since it doesn’t have an attached successor. Therefore, all no node $v$ where $u\prec v$ can be executing right now since all such nodes are in the same $P$ bag as $u$. 888We also use this fact when we are querying the $D_{SP}$ data structure since the correctness of Lemma A.1 also depends on eager execution.

Lemma A.11.

Consider a node $u$ where $U_{u}=\textnormal{Find}(D_{NSP},u)$ is unattached and $U_{u}$ does not have an attached successor. If $u$ is an $P$ bag, $u$ is in parallel with the currently executing node $v$.

Proof.

Say $u$ was a strand of function $F$ and its operating function is $G$ ($F$ and $G$ could be the same). Therefore, $u$ is in $G$’s $P$ bag and $G$ is not active, but has returned. Moreover, $G$ has not synced with its parent function. In addition $G$’s last strand $w$ is in the same unattached set as $u$ (Lemma A.9). Since no node of this unattached set has outgoing non-SP edges, no node that is sequentially after $u$ has any incident non-SP edges. Therefore, from Lemma A.1, there can not be any get_fut edges on any path after $u$ at this point. Therefore $u$ is in parallel with $v$. ∎

We can now prove the main theorem by combining Lemmas A.1, A.4, A.8, A.10, and A.11.

Theorem 5.2 0.

If the program is executed in a depth first eager execution order, $\textnormal{Query}(u,v)$ returns true iff $u\prec v$ in $G_{\mathit{full}}$.

If the path from $u$ to $v$ has no get_fut edge, then Lemmas A.1 applies. In addition, Lemma A.4 argues that the second part of the query (lines 3–3) answers all questions correctly between two nodes in attached sets. Finally, Lemmas A.8, A.10, and A.11 show that using attached predecessors and successors for nodes in unattached sets gives the correct answer when the first part of the query (using $D_{SP}$) returns false.

Appendix B Artifact Appendix

B.1. Abstract

This artifact contains source code for the compiler, runtime system, and benchmarks used in the PPoPP 2019 paper Efficient Race Detection with Futures, plus shell scripts that compile everything and run the benchmarks. The hardware requirements are any modern multicore CPU, while the software requirements include a relatively recent Linux distribution (tested on Ubuntu 16.04), the datamash package, and the GNU gold linker. To validate the results, run the test scripts and compare the results to figures 6, 7, and 8 in the paper.

B.2. Artifact check-list (meta-information)

• •

**Program: ** C/C++ code.

• •

**Compilation: ** Modified fork of clang++ with -O3 -flto flags. To fully reproduce the reproduce the results, we recommend installing the GNU gold linker as ld.

• •

**Data set: ** The dedup benchmark uses publicly available data sets. Scripts in the repository will download and setup all data sets.

• •

**Run-time environment: ** Tested on Ubuntu 16.04, but expected to work on any modern Linux.

• •

**Hardware: ** Any modern multicore CPU; tested on an Intel®Xeon® CPU E5-2665 with hyperthreading disabled. Enabling hyperthreading may change results.

• •

**Metrics: ** Runtime (in seconds).

• •

**Output: ** Runtime and standard deviation for all benchmarks, each run with 12 configurations which determine what kind of futures and which race detection algorithm are used and what level of instrumentation/race detection is turned on — baseline, reachability only, reachability + memory instrumentation, and full race detection.

• •

**How much disk space required (approximately)?: ** 13GB.

• •

**How much time is needed to prepare workflow (approximately)?: ** 1.5 hours.

• •

How much time is needed to complete experiments (approximately)?: 4 hours.

• •

**Publicly available?: ** Yes

• •

**Code/data licenses (if publicly available)?: ** MIT.

B.3. Description

B.3.1. How delivered

The project is available on Gitlab at https://gitlab.com/wustl-pctg-pub/futurerd2.git.

B.3.2. Hardware dependencies

Any modern multicore CPU. It was tested on an Intel®Xeon®CPU E5-2665.

B.3.3. Software dependencies

The project was tested on Ubuntu 16.04, but it is expected to run correctly in other Linux distributions. To fully reproduce the results, link-time optimization should be used (-flto) with the GNU gold linker installed as ld. On our system we make /usr/bin/ld a shell script that forwards its arguments to gold whenever the USE_GOLD environment variable is set and the original ld otherwise.

The benchmark script requires GNU datamash, which can be installed using apt-get in Ubuntu 14+ or can be obtained from https://www.gnu.org/software/datamash. Bash 4+ should be used to run the scripts.

B.3.4. Data sets

All required datasets are downloaded by scripts included in the distribution.

B.4. Installation

The setup.sh script in the project repository will build our modified compiler, the modified Cilk Plus runtime, and all the benchmarks.

B.5. Experiment workflow

• •

Clone the source code to your machine:

⬇

1$ git clone

2> https://gitlab.com/wustl-pctg-pub/futurerd2.git

3$ cd futurerd2

• •

Install GNU gold as your linker. Modern versions of the GNU binutils package include gold, though for our purposes the system ld should point to gold. Installing gold also installs a header called plugin-api.h, usually in either /usr/include or /usr/local/include. Find this file and replace the BINUTILS_PLUGIN_DIR variable in build-llvm-linux.sh with this path.

• •

Install other software dependencies. In Ubuntu 14+, this is as simple as

⬇

1$ sudo apt-get install datamash zlib1g zlib1g-dev openssl

and making sure you have Bash 4+.

• •

Build the necessary components. The setup.sh script will build the compiler and download and unpack the necessary data sets.

• •

Run the benchmark script (bench/run.sh). The script compiles the runtime library and race detection library, and compiles and runs each configuration of each benchmark. Tuning parameters can be found in bench/time.sh (which the run.sh script uses) — feel free to examine the script and change parameters, such as the number of iterations for each benchmark.

⬇

1$ cd bench

2$ ./run.sh

• •

Observe the results. Once completed, full results can be found in the files times.ss.csv (benchmarks used MultiBags race detection algorithm with structured futures), times.ns.csv (benchmarks used MultiBags+ algorithm with structured futures), and times.nn.csv (benchmarks used MultiBags+ algorithm with general futures).

B.6. Evaluation and expected result

Although absolute times will differ on your machine, you should see similar relative overhead for the benchmarks. Compare the results to figures 6, 7, and 8 in the paper.

B.7. Notes

Please send feedback or file issues at our gitlab repository (https://gitlab.com/wustl-pctg-pub/futurerd2).

B.8. Methodology

Submission, reviewing and badging methodology:

• •

http://cTuning.org/ae/submission-20180713.html

• •

http://cTuning.org/ae/reviewing-20180713.html

• •

https://www.acm.org/publications/policies/artifact-review-badging