{'fraction_non_alphanumeric': 0.03563883020126765, 'fraction_numerical': 0.013343711775825643, 'mean_word_length': 4.299970533346429, 'pattern_counts': {'":': 0, '<': 1, '<?xml version=': 0, '>': 1, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 17, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Atomicity Checking in Linear Time using Vector Clocks

Multi-threaded programs are challenging to write. Developers often need to reason about a prohibitively large number of thread interleavings to reason about the behavior of software. A non-interference property like atomicity can reduce this interleaving space by ensuring that any execution is equivalent to an execution where all atomic blocks are executed serially. We consider the well studied notion of conflict serializability for dynamically checking atomicity. Existing algorithms detect violations of conflict serializability by detecting cycles in a graph of transactions observed in a given execution. The size of such a graph can grow quadratically with the size of the trace making the analysis not scalable. In this paper, we present AeroDrome, a novel single pass linear time algorithm that uses vector clocks to detect violations of conflict serializability in an online setting. Experiments show that AeroDrome scales to traces with a large number of events with significant speedup.


Introduction
Writing correct multi-threaded programs is extremely difficult. It is the class of software that is most prone to errors. Reasoning about multi-threaded programs is notoriously challenging due to the inherent nondeterminism that arises from thread scheduling in such systems. If the program satisfies certain fundamental properties then reasoning about them becomes easier, and if such properties are violated then it is often symptomatic of more serious bugs in the software. Atomicity is one such classical concurrency property, which guarantees that a programmer reasoning about a concurrent program can assume that atomic blocks of code can be executed sequentially without any context switches in between. Atomicity allows programmers to reason about atomic blocks without worrying about the effects of other threads. Unfortunately, violation of atomicity specifications is quite common and is the root cause in a majority of real-world bugs [13,28].
Various approaches to identifying atomicity violations have been explored. Static analysis based approaches for atomicity checking are usually conservative, computationally expensive, and often rely on user annotations, like type annotations [5,14,20,21,40,47]. The advantage of static analysis approaches is that they may successfully prove that a program satisfies all its atomicity requirements. Dynamic analysis for atomicity violations, on the other hand, have the advantage that they are fully automated and are computationally less expensive [6,12,13,19,30,52]. Though they cannot prove that a program satisfies its atomicity specification, dynamic analysis can be used to check if an observed trace is witness to the violation of atomicity. Given their scalability, dynamic analysis techniques for detecting atomicity violations have proved to be very useful in practice.
In this paper, we will focus on sound and precise dynamic analyses; unsound dynamic analyses have the disadvantage that they report many false alarms 1 . Most sound and precise dynamic analyses [6,12,19] for atomicity violation are based on checking the conflict serializability of an observed program execution. An execution is conflict serializable if it can be transformed into an equivalent execution, where all statements in an atomic block are executed consecutively without context switches, by commuting adjacent, non-conflicting operations of different threads. Here conflicting operations are either two operations by the same thread, two accesses (at least one of which is a write access) to a common memory location, or acquires and releases of common locks. Determining if an execution is conflict serializable can be reduced to checking for the existence of a cycle in a graph called the transaction graph. The transaction graph has atomic blocks (a.k.a. transactions) as vertices, and edges between blocks that contain non-commutable events. A path from atomic block A to B indicates that A must be executed before B in a serial execution, and so a cycle in such a graph indicates that the execution is not equivalent to a serial one. All current sound and precise dynamic analyses for conflict serializability [6,19] rely on this idea and thus have an asymptotic complexity of cubic time -each new event of the trace requires updating the transaction graph, and checking for cycles; the number of edges in the graph can be quadratic in the number of events, giving a quadratic processing time per event.
The central question motivating this paper is the following: Is a cubic running time necessary for checking conflict serializability? Or are there sub-cubic algorithms for this problem? The main result of this paper is a new, linear time algorithm for checking conflict serializability.
For other concurrency specifications, like data race detection, that admit sound and precise linear time algorithms, the key to achieving an efficient algorithm is the use of vector clocks [22,26,31,32]. Such algorithms rely on computing vector timestamps for events in a streaming fashion as the trace is generated, and using these timestamps to recover the causal order between a pair of events. However, generalizing such an algorithmic principle to conflict serializability checking is far from straightforward. This is because checking conflict serializability requires identifying causal orders between transactions (or atomic blocks) and not individual events. For this reason, Flanagan-Freund-Yi [19], in fact, dismiss the possibility of a vector clock based algorithm for conflict serializability checking: "The traditional representation of clock vectors [32] is not applicable because our happens-before relation is over compound transactions and not individual operations. " The challenge is to discover a way to associate a single timestamp with a transaction, even though new causal dependencies are discovered as each individual event in the trace is processed. This is further complicated by the following observation. Vector timestamps implicitly summarize the set of all events that must be ordered before. However, the set of transactions that must be executed before a transaction T might be known only well after all the events of T have been seen (see Example 2). These observations suggest that a scheme of assigning vector timestamps to transactions may only be computed if the algorithm makes multiple streaming passes over the trace, which may result in an algorithm that is not linear time.
We address these challenges by assigning vector timestamps to individual events in a trace. The induced order on events is then used to discover the ordering relationship between transactions, and thereby determining if a trace is conflict serializable. For a trace containing a bounded number of variables, threads, and locks, our algorithm, AeroDrome, is a single pass, streaming algorithm that runs in linear time 2 . As with standard vector clock algorithms, such as those used in data race detection [15,37], our algorithm summarizes information in vector clocks and thus does not need to store the timestamp of all the events in the trace to detect serializability violations.
We have implemented AeroDrome in our tool R [3] and have compared its performance against the Velodrome [19] algorithm on various benchmark programs. Atomicity specifications (i.e., which blocks of code should be regarded as atomic) are hard to come by. One naïve specification is to consider each method call to be atomic. Since often there is a main method for each thread, this means that the entire computation of each thread should be atomic. Programs are unlikely to satisfy such strong atomicity specifications, but running detection algorithms against these, gives us a baseline. We use such naïve specifications for some programs in our benchmark. For such benchmarks, conflict serializability is trivially violated in a small prefix of the observed trace. The resulting transaction graph is thus small, the overhead of maintaining vector clocks outweighs the benefits of a linear time algorithm, and Velodrome slightly outperforms AeroDrome. For other programs in our benchmark, we use the more realistic atomicity specifications given in [6]. Here transactions consist of smaller blocks of code, and the resulting transaction graph has many transactions. For such examples, our algorithm significantly outperforms Velodrome. This suggests that on realistic atomicity specifications, the benefits of having a linear time algorithm can be significant.
The rest of the paper is organized as follows. In Section 2, we discuss preliminary notations such as that of concurrent program traces and the definition of conflict serializability. In Section 3, we use motivating examples to illustrate the challenges involved in developing a linear time vector clock algorithm for dynamically checking conflict serializability. In Section 4, we discuss AeroDrome, a single pass linear time vector clock algorithm for checking conflict serializability, which is also the main contribution of 2 Vector clock based algorithms are linear time under the computational assumption that arithmetic operations take constant time. This is a reasonable assumption in practice because even for traces with billions of events, the numbers involved in vector clocks can be stored in a single word, and so addition and subtraction of such numbers can be reasoned to be constant time. the paper. Section 4 also discusses the correctness and complexity guarantees of the algorithm and optimizations for improving the performance of AeroDrome. Our implementation of AeroDrome in our tool R and its performance evaluation on a suite of benchmark programs is discussed in Section 5. We discuss closely related work in Section 6 and present concluding remarks in Section 7. Some proofs and additional discussion can be found in the full version [2].

Preliminaries
An execution trace (or simply trace) of a concurrent program is a sequence of events. We will use σ , ρ 1 , ρ 2 , . . . to denote traces. Each event in a trace is a pair e = t, op , where t denotes the thread that performs e and op is the operation performed by e; we will use thr(e) to denote t and op(e) to denote op. Operations can be one of r(x), w(x) (read from or write to variable/memory location x), acq(ℓ), rel(ℓ) (acquire or release of lock object ℓ), fork(u), join(u) (fork or join of thread u), ⊲ or ⊳ (denoting the begin or end of an atomic block). Traces are assumed to be well-formedall lock acquires and releases are well matched, a lock is not acquired by more than one thread at a time, all begin and end events are well matched, fork events occur before the first event of the child thread and join events occur after the last event of the child thread. A transaction T in thread t is a maximal subsequence 3 of events of thread t that starts with t, ⊲ and ends with the matching t, ⊳ , and we say e ∈ T if the event e belongs to this maximal subsequence; in this case, txn(e) denotes the transaction T to which e belongs. In a trace σ , we will say that a transaction T is completed in σ if the corresponding end transaction event ·, ⊳ ∈ σ . If T is not completed in σ , it is said to be active.
Given a trace σ , we denote by ≤ σ tr the total order on events induced by σ -for events e, e ′ in σ , we say e ≤ σ tr e ′ iff either e = e ′ or e occurs before e ′ in the sequence σ . Two events e, e ′ are said to be conflicting if either (a) thr(e) = thr(e ′ ), (b) e = t, fork(u) and thr(e ′ ) = u, (c) thr(e) = u and e ′ = t, join(u) , (d) there is a common memory location x such that both op(e), op(e ′ ) are one of {w(x), r(x)} and not both are r(x), or (e) there is a lock ℓ such that op(e) = rel(ℓ) and op(e ′ ) = acq(ℓ). Given a trace σ , conflict-happens-before ≤ σ CHB is the smallest reflexive, transitive relation such that for every pair of conflicting events e ≤ σ tr e ′ , we have e ≤ σ CHB e ′ . Atomicity is closely related to the property of conflict serializability. Informally, this property requires that an execution be equivalent to a serial execution by commuting adjacent non-conflicting events; an execution is serial if for every thread t in the trace and for every transaction T of thread t, there are no events of any other thread between the begin and end events of T . In this context, if two events r(z) 10 ⊳ Figure 1. Trace ρ 1 . Taking T i to be the transaction of thread e and e ′ are ordered by ≤ CHB , then their order is the same in all equivalent executions. To capture conflict serializability, such a causal relationship needs to be lifted to transactions. Consider two transactions T and T ′ with events e ∈ T and e ′ ∈ T ′ such that e ≤ σ CHB e ′ . If the goal in a serial execution is to schedule all events of T consecutively, given that e is before e ′ in all equivalent executions, it must be the case that every event of T should happen before each event of T ′ . Thus, transaction T must happen before transaction T ′ in trace σ (denoted T ⋖ σ Txn T ′ ) if there are events e ∈ T and e ′ ∈ T ′ such that e ≤ σ CHB e ′ . We now present the definition of conflict serializability (which implies atomicity) from [19].
Definition 1 (Conflict Serializability [19]). A trace σ is conflict serializable if there is no sequence of k > 1 distinct transactions T 0 ,T 1 . . . T k−1 such that for every 0 ≤ i ≤ k−1, we have T i ⋖ σ Txn T (i +1) mod k . If σ is not conflict serializable, then such a sequence T 0 , . . . ,T k−1 is said to be a witness to the violation.
Example 1. Consider the trace ρ 1 in Figure 1. This trace is a sequence of 10 events, performed by three different threads t 1 , t 2 and t 3 . In all our examples, we will use e i to denote the i th event in the trace. This trace has three transactions -transaction T 1 = e 1 e 2 e 9 e 10 is performed in t 1 , transaction T 2 = e 3 e 4 e 5 is performed in t 2 and transaction T 3 = e 6 e 7 e 8 is performed in t 3 . All pairs of events, both of which are performed by the same thread (such as (e 1 , e 2 ) or (e 2 , e 10 ) in ρ 1 ) are conflicting. In addition, (e 2 , e 4 ) and (e 7 , e 9 ) are conflicting pairs of events in ρ 1 and we use an explicit arrow ( ) to depict such interthread conflicting pairs. We have T 1 ⋖ CHB e 5 . Finally, the trace ρ 1 is conflict serializable and the equivalent serial execution is the sequence ρ serial 1 = e 6 e 7 e 8 e 1 e 2 e 9 e 10 e 3 e 4 e 5 , in which the order of transaction is T 3 T 1 T 2 . Observe that the relative order of conflicting events in ρ serial 1 is the same as in the original trace ρ 1 .
Based on Definition 1, a cyclic dependency on transactions using ⋖ σ Txn suggests that σ does not have an equivalent serial execution and hence the program does not satisfy its atomicity specification. Previous techniques [6,19] for checking conflict serializability dynamically, rely on constructing a directed graph. The vertices in such a graph are the different transactions in the observed trace, the edges correspond to the order imposed by ⋖ Txn and checking violations of conflict serializability reduces to searching for a cycle in this graph. These algorithms run in time that is quadratic in the length of the observed trace as they check for cycles each time a new edge is added in the graph.

Challenges in Designing a Vector Clock Algorithm
Vector clocks have been very useful in designing linear time algorithms for dynamic analysis of multi-threaded systems [15,23,26,31,37]. The broad principle behind these algorithms, is to assign vector timestamps to events as the trace is generated/observed so that the ordering between these assigned timestamps captures causal ordering. Notice that, conflict serializability is defined in terms of the relation ⋖ Txn on transactions (Definition 1), and thus, the most straightforward vector clock algorithm would rely on assigning timestamps to transactions in such a way that the timestamp of transaction T 1 is less than or equal to timestamp of transaction T 2 if and only if T 1 ⋖ Txn T 2 . However, since a transaction is a sequence of events (and not a single event), the first challenge is figuring out how to assign and update timestamps of transactions when individual events are being continuously generated by the execution; this is one of the reasons why such algorithms were deemed impossible for atomicity in [19]. However, there is a deeper and more fundamental challenge with assigning timestamps to transactions, as illustrated in the following example.
Example 2. Consider again the trace ρ 1 in Figure 1. Notice that there is a "path" from T 3 to T 2 (via T 1 ) using ⋖ ρ 1 Txn , even though T 3 starts after T 2 is completed in the trace ρ 1 . Further the discovery that T 3 has a path to T 2 can be made only after the event e 9 is generated in the trace, and at that point, both T 2 and T 3 have completed. This poses serious challenges when designing a vector clock algorithm. A vector clock algorithm assigning a timestamp to transaction T that is consistent with ⋖ Txn , needs to know (explicitly or implicitly) the set of transactions that have a path to T ; this is because the algorithm needs to ensure that the timestamp assigned to T is ordered There is a cycle in the transaction graph that can be realized by a path using ≤ CHB -edges that begins and ends in the same transaction.
after the timestamps assigned to all these "predecessor" transactions. However, as transaction T 2 in trace ρ 1 illustrates, this may require knowing future events and transactions.
Example 2 illustrates that transactions T ′ that have a ⋖ Txnpath to a transaction T may only be determined by events that appear after T itself. This suggests that one is unlikely to get a linear time streaming algorithm that assigns timestamps to transactions for detecting atomicity violations.
Therefore, we explore the possibility of an algorithm that assigns timestamps to events (not transactions), but which can nonetheless enable checking conflict serializability. The first key question to address is which relation among events should the timestamps try to capture implicitly? Recall that, the relation ⋖ Txn (on transactions) is defined in terms of the relation ≤ CHB (on events), and therefore, a natural first step to explore, is to see if computing ≤ CHB is sufficient to detect atomicity violations.
Example 3. Consider the trace ρ 2 in Figure 2 with two transactions T 1 and T 2 in threads t 1 and t 2 respectively. Here, we have, T 1 ⋖ ρ 2 Txn T 2 and T 2 ⋖ ρ 2 Txn T 1 , thus giving us a violation of conflict serializability with the sequence T 1 ,T 2 witnessing the violation. Now consider the following ≤ CHB path in the trace - This path, in fact, is symptomatic of the atomicity violation because it starts and ends in the same transaction (transaction T 1 ) and passes through another transaction (transaction T 2 ).
The atomicity violation in trace ρ 2 in Example 3 can be deduced based on the observation that there are 3 events e, f , (e 1 , e 5 , e 7 in ρ 2 , specifically) such that txn(e) = txn( ), txn(e) txn(f ), and e ≤ CHB f ≤ CHB . If we can prove that this is equivalent to Definition 1, then all we need to do is to compute (implicitly using vector clocks) the ≤ CHB ordering. Unfortunately, this is not true, i.e., violations of conflict serializability cannot be detected by simply using ≤ CHB ordering and searching for the above kind of ≤ CHB paths. We illustrate this in the next example.
There is no ≤ CHB path that starts and ends in the same transaction.
Example 4. Consider trace ρ 3 in Figure 3. As before, let T 1 , T 2 be the two transactions by threads t 1 and t 2 respectively.
, thus giving us a conflict serializability violation. However, there is no ≤ CHB -path that starts and ends in the same transaction. If vector timestamps are used to compute ≤ CHB , then violations of conflict serializability cannot be detected by checking ordering of vector timestamps of events.
Example 4 demonstrates that ≤ CHB is not the right relation on events to detect violations of conflict serializability. Then, what is the right relation to track? In order to identify that, we will first recast Definition 1 in terms of events.
We will say that there is a path from event e to f through for every i < k. Using the notion of path between events through transactions, we can recast the notion of conflict serializability as follows. Though * −→ σ gives us a characterization of conflict serializability, it is not clear how to compute it algorithmically in a single pass over the trace. The reasons are technical and therefore, skipped. Instead, what we will compute is a slight restriction of the relation * −→ σ , defined as follows.
Definition 2. For events e, f in trace σ , we say e⋖ σ E f , if there is an event in σ such that e ≤ σ CHB and either (a) = f , The following theorem formalizes how we can check for conflict serializability violations using the new relation. The proof of this theorem is presented in [2].
Each transaction is a ⋖ Txn predecessor of the other.
Theorem 2. For a transaction T , letT ⊲ denote the begin transaction event ·, ⊲ of T . The following observations hold.
1. Any trace σ with a transaction T , events e and f such that f ∈ T , e T , T ⊲ ⋖ σ E e and e ⋖ σ E f , is not conflict serializable. 2. Let σ be a trace that is not conflict serializable with a witness T 0 , . . .T k−1 such that each T i , except possibly one, is complete in σ . Then there is a transaction T and events e, f in σ such that f ∈ T , e T , T ⊲ ⋖ σ E e and e ⋖ σ E f . We conclude this section with examples illustrating both the definition ⋖ E and the use of Theorem 2.
Example 6. Consider trace ρ ′ 1 in Figure 4; this is a slight modification of trace ρ 1 from Figure 1 that now has an atomicity violation. Again e i denotes the i th event, and σ i denotes the prefix upto event e i . Notice that in prefix σ 11 , e 1 ⋖ σ 11 E e 5 (because e 1 ≤ σ 11 CHB e 5 ) and e 5 ⋖ σ 11 E e 11 (because e 5 * −→ σ 11 e 11 and txn(e 5 ) is complete in σ 11 ). Thus by Theorem 2, there is a violation of conflict serializability.

Vector Clock Algorithm
Based on intuitions developed in Section 3, we will now describe our vector clock based algorithm called AeroDrome, for checking violations of conflict serializability. Before presenting the algorithm itself, we recall some notation and concepts related to vector clocks that will be useful.
Let us fix the set of threads in the trace/program to be Thr. A vector time (or timestamp) is a vector of non-negative integers, whose size/dimension is |Thr| (number of threads). For a thread t ∈ Thr, we denote the t th component of a vector time V by V (t). We say a vector time V 1 is less than (or ordered before or simply before) another time V 2 (of the same dimension), denoted In this case, we say that V 2 is greater than, ordered after or after V 1 . The minimum vector time on threads Thr is ⊥ Thr = λt . 0, and we will often use ⊥ when Thr is clear from context. Next, the join of two vector times V 1 and V 2 is the time Vector clocks are variables (or place holders) for vector timestamps. That is, vector clocks are variables that take values from the space of vector times, and will be used in our algorithm to compute the timestamps associated with various events in a trace. All the operations on vector times can be naturally thought of as applying to vector clocks as well.

The AeroDrome Algorithm
Our algorithm AeroDrome is a single pass linear time algorithm. It processes events in the trace as they are generated and (implicitly) assigns vector timestamps to each of these events. Broadly, the goal of the algorithm will be to assign vector timestamps that capture the relation ⋖ E (Definition 2) and use Theorem 2 to discover conflict serializability violations. The exact invariant maintained by the algorithm is technical and is postponed to later. Similar to other vector clock algorithms, such as those used in data race detection [15,37], AeroDrome does not explicitly store the timestamps of each event in the trace; it instead maintains the timestamps of constantly many events using constantly many vector clocks. This small set of vector clocks is adequate for detecting conflict serializability violations.
Pseudocode for AeroDrome is shown in Algorithm 1. It processes events in the trace based on their operation, calling the appropriate handler. As mentioned before, the algorithm uses several vector clocks, which we will depict using the black-board font -C, L, W, R, etc. Let us assume for now that every event in the trace is part of some transaction, and that transactions are not nested; later in this section, we will describe how to efficiently handle nested transactions and unary transactions, i.e., events not enclosed within a begin and end atomic block.

Vector Clocks and Other Data in the State
The most crucial set of clocks maintained by the algorithm are those of the form C t , for each thread t ∈ Thr. The clock C t , intuitively, stores the timestamp of the last event performed by the thread t so far. That is, when performing an event e = t, op , the timestamp assigned to e by AeroDrome is, in fact, determined by the value of the clock C t right after e was processed by the algorithm. This is similar in spirit to vector clock algorithms for data race detection such as the standard D + [37] or its derivatives like F T [15]. The algorithm also checks for violations of conflict serializability using the characterization in Theorem 2, which relies on the timestamp of the begin event of a transaction. The algorithm, therefore, also maintains another clock C ⊲ t which intuitively stores the timestamp of the last begin event performed by thread t.
The goal of these vector timestamps is to capture the relation ⋖ E . Since ⋖ E is defined using ≤ CHB , we need to ensure that the vector timestamps reflect the orderings induced by ≤ CHB . In order to capture the intra-thread dependencies imposed by ≤ CHB and ⋖ E , the algorithm ensures that for each thread t, the vector clock C t increases monotonically as new events arrive in the trace. However, to capture other dependencies of the ≤ CHB relation, we need auxiliary clocks. Consider an event e of the form t, acq(ℓ) . All previously encountered events with operations on lock ℓ are ≤ CHB -before e. Hence the timestamp of e must be after those assigned to such events. To do this, AeroDrome will maintain a vector clock L ℓ for each lock ℓ, that stores the timestamp of the last rel(ℓ) seen so far; this will be read to ensure that the timestamp of e is appropriately larger. Similarly, we need to ensure that the timestamp of every write event is after the timestamp of all previous writes and reads to the same variable, and that of a read event is after the timestamp of previous writes. Therefore, for every variable x, AeroDrome has a clock W x that stores the timestamp of the last write w(x)-event and a clock R t, x that stores the time of the last t, r(x) -event. Notice that when considering paths between events through transactions ( * −→), we need to make sure that consecutive transactions along the path are different. To be able to track this constraint, AeroDrome will also maintain scalar variables lastRelThr ℓ and lastWThr x , which store the identifier of the thread that performed the last release on ℓ and write on x, respectively. Each of the clocks C t are initialized with the time ⊥[1/t], all other clocks are initialized to ⊥, and all the scalar variables are initialized to a default value of NIL.

Updates to the State
As new events are observed in the trace, the algorithm updates these vector clocks in a manner that is consistent with tracking the ⋖ E -relation.
When processing a begin event e = t, ⊲ , the algorithm first increments the local component of C t (line 35 -'C t := C t [C t (t)+1]'). To understand why, let e prev be some event in for t ∈ Thr do R t, x := ⊥; 9: procedure A G (clk, t) 10: if C ⊲ t ⊑ clk and t has an active transaction then 11: declare 'conflict serializability violation'; 12: C t := C t ⊔ clk; 13: procedure (t, ℓ) 14: if lastRelThr ℓ t then

40:
A G (C t , u); 41: for ℓ ∈ Locks do 42: for x ∈ Vars do 44: for u ∈ Thr do 46: the previous transaction (if any) by the same thread t. Further, let e ′ be some event performed by a different thread t ′ t such that (a) e prev ⋖ E e ′ , and (b) ¬(e ⋖ E e ′ ). The increment of the local component ensures that this relationship between e, e prev and e ′ can be accurately inferred from their timestamps by ensuring that the local component of the timestamp of e is strictly greater than that of e prev . Finally, AeroDrome updates C ⊲ t with the timestamp of the current event e stored in C t .
When processing an acquire event e = t, acq(ℓ) , the algorithm makes sure that the timestamp of e is ordered after the last release event e ℓ of lock ℓ. This is achieved by updating 'C t := C t ⊔ L ℓ ' in the procedure A G when invoked at line 15; the procedure A G also checks for conflict serializability violation before updating C t , but more on that later. Of course, if e ℓ is performed by the same thread t (condition in line 14), then, this is already ensured and no explicit update is required.
At a write event e = t, w(x) , AeroDrome ensures that the timestamp of e is ordered after all the prior reads and writes on x by calling A G in lines 29 and 31. The algorithm then updates W x to be the timestamp of e (see line 32) and lastWThr x to t, thus preserving the semantics of the clock W x and the scalar variable lastWThr x . The updates performed at a read event are similar.
At a fork event e = t, fork(u) , the algorithm updates the clock of the child thread u ('C u := C u ⊔ C t '; line 20) so that all events of u are ordered after e. At a join event e = t, join(u) , the algorithm updates C t to C t ⊔ C u so that all events of thread u are ordered before e.
Let us now consider the updates performed at an endtransaction event e = t, ⊳ . Let e ⊲ denote the matching begin transaction event. Observe that if for an event f , e ⊲ ⋖ E f , then since txn(e) is completed in σ , e ⋖ E f . That is, all future events that are ⋖ E -after e ⊲ must be assigned a timestamp after that of e. This is ensured by updating clocks C u for all threads u that satisfy C ⊲ t ⊑ C u (lines [38][39][40], and clocks L ℓ , W x , and R u, x (lines 41-46).

Checking Violations of Atomicity
The algorithm detects violations of atomicity at various points by a call to the procedure A G . The checks can be broadly classified into two categories. First, the algorithm can report a violation at an event e = t, op such that there is an earlier event e ′ (performed by a thread t ′ t) that conflicts with e. In this case, if e ⊲ ⋖ E e ′ (where e ⊲ is the begin event of txn(e)), then conditions in Theorem 2 are satisfied to demonstrate a violation. This check is performed at acquire events (line 15), at read events (line 25) and at write events (lines 29 and 31). Second, the algorithm reports atomicity violations when processing an end event e = t, ⊳ (with a matching begin event e ⊲ ). The algorithm detects a violation when there is another thread u t with an active transaction whose begin event is e ⊲ u , whose last event is e u and e ⊲ u ⋖ E e and e ⊲ ⋖ E e u (line 40). These checks for violations of conflict serializability are performed in A G , which takes two arguments: clk (a vector timestamp) and t (a thread identifier), and declares a violation if (a) thread t has an active transaction, and (b) clk is ordered after C ⊲ t , which is the timestamp of the begin event of the (active) transaction of t (line 10). It then updates the value of the clock C t to C t ⊔ clk (line 12).

Nested and Unary Transactions
Let us now consider the cases of nested and unary transactions that we postponed. In the case of nested transactions, it is enough to only consider the outermost transactions and ignore the inner transactions. This is because there if there is a cycle involving a transaction T that is nested inside another transaction T ′ , then there is clearly also a cycle involving T ′ . As a result, we simply ignore the begin and end events that have a non-zero nesting depth.
Events that are not enclosed by begin and end transaction events consitute a trivial atomic block, namely, one consisting of only that single event. These are called unary transactions. The pseudocode in Algorithm 1 works correctly even in the presence of unary transactions. Notice that a unary transaction corresponding to a read, write, acquire or join event can only correspond to a cycle that involves another non-unary transactions. Our algorithm, in fact, does not detect a violation at these unary transactions (in the procedure A G , line 10) as unary transactions are not active transactions. Figure 6. AeroDrome on Trace ρ 3 .
We conclude this section with a theorem stating the correctness of Algorithm 1 (proof can be found in [2]).
Theorem 3. On any trace σ , Algorithm 1 reports a violation of conflict serializability iff σ is not conflict serializable.

AeroDrome on Example Traces
Let us illustrate AeroDrome's workings on the traces from Section 3. Even though these examples do not use any synchronization primitives like locking, they contain all the features needed to highlight the subtle aspects of AeroDrome.
Let us begin with the simplest trace ρ 2 from Figure 2. We show the values of the relevant vector clocks in Figure 5. In this figure, we only depict the value of a vector clock in row i if its value has changed after processing the i th event e i in the trace. We do not show the values of the clocks R t 1 , x , R t 2 , x . R t 1 , or R t 1 , as they are not important here. There are two threads and thus the size of each vector clock is 2. The clocks C t 1 and C t 2 are initialized to the timestamps 1,0 and 0,1 respectively, and all other clocks are initialized to ⊥= 0,0 . The local clocks increment after a begin event (line 35 in Algorithm 1) and thus the clocks C t 1 and C t 2 become 2,0 and 0,2 after e 2 . Further, these are also the values of the clocks C ⊲ t 1 and C ⊲ t 2 from this point onwards until the end of the execution. After processing e 3 = t 1 , w(x) , the value of the clock W x becomes 2,0 (line 32). At event e 4 , the call to A G (see line 25) with arguments ( 2,0 , t 2 ) updates the clock C t 2 to 2,2 (line 12). The clock W gets updated to C t 2 = 2,2 after processing e 5 . Finally, at event e 6 , the algorithm calls A G with arguments ( 2,2 , t 1 ). In this procedure, the algorithm asserts that C ⊲ t 1 ⊑ W and declares an atomicity violation. Let us next consider the trace ρ 3 from Figure 3. AeroDrome's run on this trace is shown in Figure 6. Updates corresponding to the first four events are straightforward. In event e 5 , C t 1 gets updated to 2,2 because of the call to A G in line 25. Notice that this call does not raise any violation of atomicity because at this point, C ⊲ t 1 = 2,0 and the clock W is 0,2 thus failing the check C ⊲ t 1 ⊑ W in line 10. The same explanation applies to the r(x) event e 6 in 2,0,0 0,2,0 0,2,0 2,2,0 2,2,0 0,0,2 2,2,2 2,2,2 Conf. serializ. violation (C ⊲ t1 ⊑ W z ) Figure 7. AeroDrome on Trace ρ ′ 1 .
t 2 and thus no atomicity violation is reported here as well. Next, the algorithm processes the end event e 7 = t 1 , ⊳ . At this point, the algorithm checks if any event in the currently active transaction of t 2 is ordered after e 1 (condition C ⊲ t 1 ⊑ C t 2 in line 39 of Algorithm 1). This check succeeds since C ⊲ t 1 = 2,0 and C t 2 = 2,2 at this point. The algorithm then checks if C ⊲ t 2 ⊑ C t 1 in the procedure A G and thus declares an atomicity violation. This illustrates the subtlety in how the algorithm reports atomicity violations at an end event.
We will now illustrate how Algorithm 1 detects the atomicity violation in the more involved trace ρ ′ 1 from Figure 4. This example illustrates how AeroDrome handles dependencies between transactions introduced by future events. The run of AeroDrome on ρ ′ 1 is shown in Figure 7. We omit the updates to the clocks R t i ,u (i ∈ {1, 2, 3}, u ∈ {x, , z}) as they do not play a significant role in this example. All vector clocks have dimension 3 because there are three threads in ρ ′ 1 . As before, the clocks are initialized as follows -C t 1 = 1,0,0 , C t 2 = 0,1,0 and C t 3 = 0,0,1 ; all other clocks are initialized to 0,0,0 . The begin events result in incrementing of local clocks and thus C t 1 = 2,0,0 after e 1 . Further, the clock W x gets updated to the value of C t 1 at the end of e 2 . The next two events e 3 and e 4 are processed in a similar fashion. At event e 5 = t 2 , r(x) , the clock C t 2 gets updated to 2,2,0 as in line 12. After this, the transaction in t 2 ends. The clocks of none of the threads is updated because of e 6 as neither thread t 1 nor t 2 have clock values larger than C ⊲ t 2 (line [38][39][40]. However the write and read clocks are updated. Specifically, the clock W maintaining the timestamp to the last write to is such that C ⊲ t 2 ⊑ W and thus, the algorithm updates W to W ⊔ C t 2 = 2,2,0 (line 44 in Algorithm 1). Event e 7 is a begin event and updates C t 3 to 0,0,2 . Now at the r( ) event e 8 , the clock C t 3 gets updated with W which at this point evaluates to 2,2,0 , thus giving C t 3 = 2,2,2 . The write clock W z then gets updated to 2,2,2 after e 9 . Further, significant clock updates are performed at the end event e 10 . Finally, the algorithm detects an atomicity violation at event e 11 = t 1 , r(z) -the algorithm checks if the clock W z knows some event in t 1 (C ⊲ t 1 ⊑ W z ) and concludes that there is a violation of conflict serializability as this check passes.

Reducing the number of Read Clocks
Recall that Algorithm 1 maintains, a vector clock R t, x for every pair of thread t and memory location x. Therefore, the number of such vector clocks that need to be tracked in the basic algorithm is O(|Thr|V ), where |Thr| is the number of threads and V is the number of memory locations. Storing and updating these many clocks can be expensive, when the number of memory locations that need to be tracked is prohibitively large, as is the case for most real world software. We tackle this using our optimization to reduce the number of clocks from O(|Thr|V ) to O(V ). The role of the clocks R t, x is two-folds. First, these clocks help detect atomicity violation -at a write event e = t, w(x) , the algorithm checks if there is a thread u t such that C ⊲ t ⊑ R u, x (line 10 in Algorithm 1). Second, these clocks are used to update C tat a write event e = t, w(x) , we set C t := u t C t ⊔ R u, x (line 12 called iteratively in the loop at line 30).
The reduction in clocks is achieved by instead maintaining a single clock (per memory location) for each of the above two purposes instead of maintaining O(|Thr|) many clocks (per memory location). First, for updating clocks correctly at write events, we will maintain a single clock R x for each location x. This clock stores the value u R u, x at each point while processing the trace. Next, to perform checks for violations of conflict serializability, we will have another clock R x (check read). This clock will store the value u R u, x [0/u] at each point in the analysis. Based on the invariants maintained by the algorithm, one can show that checking C ⊲ t ⊑ u t R u, x is equivalent to checking C ⊲ performance of AeroDrome, are outlined in greater detail in [2].
We now state the time and space complexity for the optimized version discussed in this section. We will use n non-end and n end as the number of non-end events and end events in the trace (and therefore n = n non-end + n end is the size of the trace). We will denote by |Thr|, V and L the number of threads, memory locations and locks in the input trace. Further, all arithmetic operations are assumed to take constant time.
The complexity observations easily follow from the description of the algorithm.

Experimental Evaluation
In this section, we describe our implementation of AeroDrome and the results of evaluating it on benchmark programs.

Implementation
We have implemented AeroDrome in a prototype tool R , available publicly [3]. R is written in Java and analyzes traces generated by concurrent programs and detects violations of conflict serializability. The primary goal of the evaluation is to assess if the theoretical bound (linear time) of the algorithm also translates to effective performance in practice, or in other words, does our vector clock algorithm perform better than existing approaches such as the classical graph based algorithm (Velodrome) proposed in [19]? We emphasize that the primary purpose of the evaluation is to compare different algorithms for checking atomicity instead of comparing different tools that implement these algorithms.

Logging.
In order to evaluate our algorithm against the above objective and to ensure a fair comparison with other approaches, we must ensure that all competing candidate algorithms analyze the same trace. However, the dynamic behavior of a concurrent program can vary significantly across different runs, even when starting with the same input. In order to ensure fairness, we compare the performance of the different algorithms on the same dynamic execution. Our tool R therefore first extracts an execution trace from a concurrent programs and then analyzes the same trace against all candidate algorithms. We use RoadRunner [16] to log traces from our set of benchmark programs. RoadRunner uses load time program instrumentation and can be extended to log various events -read and write accesses to memory locations, acquire and release of synchronization objects (locks), forks and joins of threads, and events generated at the entry and exit of each method, which we respectively mark as transaction begin (⊲) and end (⊳) events.

Velodrome.
The Velodrome algorithm [19] runs in (worst case) quadratic time and analyzes traces by building a directed graph, with transactions as nodes in the graph and where the edges correspond to ⋖ Txn relation between transactions. There was no publicly available implementation of Velodrome that analyzes logged executions. Thus, we also implement this algorithm in R . We use the Java graph library JGraphT [33] to implement various graph operations (adding nodes and edges, cycle detection, etc.,) in Velodrome algorithm. In our implementation of Velodrome, we also incorporate garbage collection as an optimization suggested in [19] -transactions with no incoming edges do not participate in cycles and can be deleted from the graph. In line with the objective of our evaluation, we analyze AeroDrome and Velodrome on the same trace (generated by RoadRunner) to ensure a fair comparison.
Other techniques. The tool DoubleChecker [6] is a state-of-the-art tool for checking conflict serializability in a sound and complete manner. DoubleChecker implements a two-phase analysis -the first phase performs a fast but imprecise analysis and reports an over-approximation of the actual set of cycles in the transaction graph. The second phase then filters out the false positives from this set with a more fine grained analysis. DoubleChecker's performance crucially relies on the first phase being carried out while the program executes. Therefore, one cannot get performance data for DoubleChecker on a logged trace. As a result, there can be no fair comparison between our algorithm and DoubleChecker as one cannot guarantee that the two analyses run on the same trace. In order to gauge if DoubleChecker will significantly outperform our implementation of AeroDrome, we ran Dou-bleChcker's publicly available implementation [1] on a subset of our benchmarks. On these benchmarks, DoubleChecker's performance was slower by an order of magnitude. While these experiments do not indicate that DoubleChecker performs worse than our algorithm, they do suggest that our algorithm will be competitive against DoubleChecker. We choose not to present these numbers in this paper, because they are not an apples-to-apples comparison.

Atomicity Specifications.
In general, the logging mechanism in RoadRunner instruments and tracks all events corresponding to entering and exiting methods. A naïve atomicity specification would be to mark all method boundaries as atomic. However, as expected, not all methods are intended to be atomic. For example, default methods like run in Java, or the static main methods are often not intended to be atomic. Thus, atomicity specifications need to be specially identified by developers, by supplying manual annotations [20]. In the absence of such static annotations, we use atomicity specifications from prior work [6] whenever possible (Table 1). For the benchmarks (Table 2) for which no specifications were available, we declare all methods except the main and run methods to be atomic.

Benchmarks and Setup.
Our benchmark programs (Table 1 and Table 2) are derived from the DaCaPo benchmark suite [7] adapted to run with RoadRunner [16], Java Grande Forum [43] and microbenchmarks from [45] and have been used in prior work [6]. Our experiments were conducted on a 2.6GHz 64-bit Linux machine with Java 1.8 as the JVM and 30GB heap space. In each table, Column 1 depicts the name of the benchmark. Column 2 reports the number of events in the trace generated from the corresponding benchmark program in Column 1.
Observe that the number of events in the execution traces can vary from a few hundred to billions of events and our algorithm can scale to such large traces. Column 3, 4 and 5 report the number of distinct threads, locks and variables accessed in the trace generated. Column 6 reports the number of transactions in the trace. Column 7 reports '✗' if an atomicity violation was detected and reports '✓' otherwise. Columns 8 and 9 report the time (in seconds) taken by respectively the Velodrome algorithm and AeroDrome introduced in this article to analyze the trace generated; a 'TO' represents timeout after 10 hours. Column 10 reports the speed-up of AeroDrome over Velodrome.

Evaluation Results
For the first set of benchmarks (Table 1), we use the atomicity specification obtained from prior work [6]. For the second set of benchmarks (Table 2), we use default atomicity specifications (all methods except main and run are assumed to be atomic). The specifications from [6] are carefully crafted to ensure that spurious atomicity violations are not reported.
In the absence of careful specifications, we can expect that the violations will be reported early on in executions. Let us first consider the first set of benchmarks from Table 1. On most of these benchmarks, the violations of atomicity are discovered late in the trace. This is expected as the specifications are realistic and do not declare all methods to be atomic. The performance of AeroDrome is significantly better than that of Velodrome. Velodrome times out on most of these benchmarks (time limit was set to be 10 hours). This is because of the prohibitively large number of transactions that get accumulated in these traces. Consider, for example, the case of sunflow for which AeroDrome takes less than a second, while Velodrome spends about 68 seconds. Here, the number of nodes in the graph analyzed by Velodrome is about 9000. This coupled with the quadratic runtime complexity, results in the notable slowdown. Notice that, the slowdown is despite the garbage collection optimization implemented in Velodrome. Our algorithm, on the other hand, has a linear running time. Similarly, in the benchmark avrora, the number of transactions is more than 393K in the prefix of the trace in which AeroDrome reports an atomicity violation. Any super linear time analysis is unlikely to scale for so many transactions, and Velodrome, in fact, does not return an answer within 10 hours. AeroDrome, on the other hand, scales to traces with more than a billion events (avrora, lusearch, moldyn, raytracer, xalan) and demonstrates the effectiveness of a linear time vector clock algorithm. For the examples on which AeroDrome does not give a huge speedup over Velodrome, we discovered that the number of nodes in Velodrome's graph analysis is fairly small; for example, there were 13 nodes in the graph for pmd, 4 nodes in sor and 13 nodes in xalan.
In the second set of benchmarks, we notice that the performance of our algorithm AeroDrome is comparable to that of Velodrome. This is expected because the atomicity specifications are inadequate and do not reflect realistic onestypically most methods are non-atomic and developers have to identify a smaller set of candidate code blocks that they think are atomic. As a result, on these benchmarks, violations are detected early on in the trace and thus, the size of the transaction graph in Velodrome's analysis is small. A detailed analysis of the traces suggests that in all these benchmarks, the number of transactions did not grow more than 4, except for tomcat, for which the size of the graph grows to 21. In this case, the cost of maintaining vector clocks and updating them at every event overrides their potential benefits, and as a result, the graph based algorithm runs faster.

Related Work
Multi-threaded programs are challenging to write and reason about. Atomicity is a principled concept that lets programmers reason about coarse behaviors of programmers, without being concerned about fine grained thread interleavings. Ensuring atomicity of concurrent program blocks is therefore an important question [28] and has been investigated thoroughly.
Static analysis techniques analyze source code to confirm the atomicity of code blocks marked atomic. Such techniques prominently rely on the design of type systems [18,20]. These type systems rely on commutativity of operations and are inspired from Lipton's theory of reduction [27] and the concept of purity [14]. Extensions to type inference [40] and to programs with non-blocking synchronization [47] have been developed. The work in [18] uses constraint based type system inference for inferring atomicity specifications.
Dynamic analysis algorithms for checking atomicity inspect individual program executions instead of the program source code. Lipton's theory of reduction [27] has been a prominent theme in this space, most notably the analysis employed by Atomizer [13]. This approach however leads to false alarms. The notion of conflict serializability was introduced concurrently by Flanagan et al [19] and Farzan et al [12], with subtle differences on how synchronization events need to be ordered. In particular, Farzan et al [11] do not consider any lock operations in their traces and can lead to both false positives and false negatives. Further, their algorithm relies on maintaining sets of locks, threads and variables, similar to the use of locksets in Goldilocks [10] algorithm for employing HB for race detection, and similar to the case in race detection [15,31], such an algorithm is expected to be orders of magnitude slower than a vector clock algorithm. We refer the reader to [6] for a more thorough analysis of the differences in the two approaches. Conflict serializability has been inspired from the theory of concurrency control in databases [34]. Recently, DoubleChecker [6] proposed a two-pass analysis for efficient detection of conflict serializability violations. Here, a coarse first pass detects potential cycles in the transaction graph. This is followed by a fine grained analysis that tracks more information and ensures the soundness of the overall analysis. The notion of causal atomicity [11] asks for an equivalent trace where a particular transaction is serial.
As with most concurrency bugs, detecting atomicity violations is a challenging problem and is subject to interleaving explosion problem. Techniques such as that in CTrigger [36] and AVIO [30] resort to directed exploration of thread interleavings to expose subtle atomicity violations. Penelope [44] detects 2 thread atomicity violations using directed interleaving exploration. The work in [4,29,48,49] is also based on exercising specific thread schedules. SMT solving based predictive analysis techniques [46] have been developed, but tend to not scale. The work of Samak et. al. [39] synthesizes directed unit tests for catching atomicity violations. The work in [11,41] develop techniques for model checking concurrent programs for exposing atomicity violations. The use of random sampling and thread scheduling have also been proposed previously in the literature [25,35]. Jin et. al. [24] study the problem of synthesizing bug patches for fixing atomicity bugs.

Conclusions
In this paper, we considered the problem of checking atomicity in concurrent programs. Conflict serializability of traces is a popular notion for checking atomicity dynamically. We present the first linear time, vector clock algorithm for checking violations of conflict serializability on traces of concurrent programs. Our experimental evaluation demonstrates the power of a linear time algorithm, in that, it scales well to large executions and is often faster than existing graph based algorithms. Interesting avenues for future work include extending the insights developed in our paper to design efficient algorithms for other notions of atomicity, including causal atomicity [11], view serializability [48] or reduction based atomicity characterizations as in [13,49]. Other promising lines of work include improving the efficiency of the proposed dynamic analysis for atomicity by incorporating ideas from data race detection. This includes the classic epoch optimizations [15], static analysis for redundancy elimination [17] and optimal check placement [38], and other advances concerning instrumentation [8,9,50,51].