Efficient Linearizability Checking for Actor-based Systems

From the initial enabled set, the systematic random scheduler chooses a random receive and executes it. This may enable new receives to add to the previously enabled ones to pick from, and the process repeats until no enabled receives remain. From there, the scheduler backtracks to the initial state and initial enabled set and repeats until a timeout.

One straightforward approach to exploring systems is to explore schedules depth first. This algorithm non-deterministically picks an enabled receive that has not been marked explored and performs the associated action. When the enabled set is empty on some path, it outputs a schedule which later is transformed into a history. Then, it backtracks to the earliest point in time where other, unexplored, receives remain and it repeats this procedure. To bound execution time, all schedulers have to be stopped at some point, e.g. at some count of schedules generated. Hence, in practice, this policy will tend to mostly make some initial choices of receives, and it will aggressively explore reorderings of the “deepest” enabled receives before timing out. As a result, in our experience, this approach tends to explore similar schedules (before timing out), so it produces many but similar histories.

All of the remaining schedulers are based on Exhaustive DFS. They cut the search space by overriding methods that refine the scheduler behavior to prune receives causing redundant schedules/histories.

The delay-bounded scheduler ⁴⁶ extends the Exhaustive DFS scheduler, and it mainly explores schedules similarly but randomly delaying some receives. The scheduler starts with a fixed delay budget $D$. As it explores, for each receive $r$, it picks a random natural number d, $0\leq d\leq D$. If $d>0$ then the scheduler skips over $d$ agents that have enabled receives in the enabled set in a round robin order, and it explores the next agent’s enabled receive. The sum of chosen values of $d$ along in a schedule is bounded to $D$.

Dynamic partial order reducing (DPOR ²⁰) scheduler prunes schedules that reorder independent receives that affect different actors. If two receives target the same actor, then they are considered dependent since the order they are applied in can influence the behavior of that agent (and transitively those it communicates with). In Figure 4, for example, when exploring a state of the system, there are two enabled receives; $r_{1}$ destined to agent $A$ and $r_{2}$ destined to agent $B$. The scheduler picks one of them non-deterministically (here $r_{1}$), and it executes the transition, producing $r_{3}$ destined to $B$. In the new state, it then chooses to execute $r_{3}$. Notice that $r_{2}$ and $r_{3}$ are independent so only one interleaving needs to be explored. However, when $r_{2}$ is chosen and executed, the scheduler notices that the previously chosen $r_{1}$ is dependent, so it determines that it must explore the receives in the opposite order as well. Hence, the scheduler first checks if $r_{2}$ is enabled in the state from which $r_{1}$ was executed. If so, it adds it to the first state’s backtracking set, which tracks the remaining receives that need be explored after completing the current path. It only needs to do costly branching if the receives are dependent.

One complication arises in DPOR (shown in Figure 4) is that it is possible that $r_{2}$ is not in the enabled set of the top state (labeled start). That is, two receives can be dependent, but they might not always be in one enabled set. This situation is due to a later executed receive enabling $r_{2}$. In that case, DPOR takes all receives that executed between the dependent state (i.e. a previous state from which a receive destined to the same agent as the current receive was executed) and the current one, and filters them based on whether they were enabled in the dependent state, returning only those that were enabled in the dependent state. Then, the entire set of filtered receives is added to the dependent state’s backtracking set to explore later. This is where TransDPOR and IRed improve over DPOR, by being more careful about which one from the filtered set of receives is added to the dependent state’s backtracking set.

The key idea in TransDPOR ⁸ that differentiates it from DPOR is that when a receive becomes enabled that is dependent with a receive earlier in the schedule, it is added to the backtracking set of that earlier state (the dependent state) in the schedule only if that state’s backtracking set is empty. TransDPOR always over approximates the root enabler receive (the receive that enabled the current one whether directly or transitively) by always adding the first receive in the schedule after the one executed from the dependent state to the dependent state’s backtracking set.

IRed is based on TransDPOR, and improves over it in one specific aspect. It tracks causality (i.e. the root enabler receive) with perfect precision by scanning for the causal chain backwards starting from the current receive until the first one that enabled it in the schedule. Then it adds that root enabler receive, if found, to the dependent state’s backtracking set. Otherwise, if a root enabler was not found, it does not update the backtracking set. More concretely, during the scan, it checks for the predicate (and keeps track of the earliest receive executed in the schedule that satisfies it) whether the current receive’s sender is the same as the previous receive’s receiver. The earliest receive that satisfies it becomes the current root enabler receive. The scanner continues in this manner until it reaches the dependent state, or the predicate is no more satisfied and the last root enabler receive detected was enabled (co-enabled) in the dependent state. In which case, the last root enabler receive is the the one to explore when the algorithm backtracks to that specific state. The sequence of receives starting at the root enabler up to and including the current receive is called causal chain, and the root enabler is the first receive in this sequence. This causal chain pattern is characteristic of actors and purely sequential communicating processes. This reverse traverse for the root enabler also filters away many unrelated receives effectively, and it improves backtracking in the presence of retries. This is where our algorithm thrives in complexity that is common in distributed systems.

Our second algorithm is based on IRed and is focused on revealing linearizability violations by redefining the dependence relation of concurrent key-value stores. Linearizability is compositional ^{14, 13, 47}. However, the only time this was exploited for verifying linearizability is in P-Compositionality work ¹⁴ at the history level. In addition, we realized that a linearizability violation is a race condition on an actor/agent having two interfering receives (due to network re-ordering) or transitively between the actors/agents composing the distributed ADT (and, hence, a data race on the collective state of actors composing the ADT) that is exposed clients. We used this fact to restrict the number of interesting schedules that may produce linearizability bugs by applying it at the schedule generation stage. This was done by first augmenting the harness with additional internal messaging info, and then overriding the dependence relation to restrict dependent states to those that satisfy all of the following: (1) the receive executed from that state has to be targeting the same agent/receiver (same as before); and (2) the receives have to target a certain key in the distributed key-value store (compositionality of linearizability). So, the hypothesis about our algorithm (LiViola) is that it is expected to perform the worst in a single key-value store (e.g. a map that has one key, a register, or a single element set) and perform the best as more keys are added to the distributed ADT. Hence, our two algorithms above should thrive on complexity more than the other algorithms. In addition, it is noted in WGL paper ⁴⁵ that WGL suffers the most when there are more keys; however, our algorithms should reduce the number of schedules the most when there are more keys. In other words, the more WGL has to deal with more keys interleaving, the fewer schedules our algorithms produce in comparison to others and the more complimentary they are to WGL checking.

While IRed algorithm’s improvement is generic to all problems, LiViola is specialized to linearizability. As a result, IRed enables a whole class of algorithms that extend it and can be specialized in-lieu LiViola to more precisely address different problems. That can be done by overriding one/both of the $\textit{areDependent(receive1,receive2)}\rightarrow\textit{Boolean}$ and $\textit{didEnable(receive1,receive2)}\rightarrow\textit{Boolean}$ methods.

As explained in our operational semantics paper ³², the global state of an actor system is a distributed system state in DS2 terms, and here it is symbolized as $s\in\mathbb{S}$, where $\mathbb{S}$ is the set of all possible states in a system. Each state $s=\langle\alpha,m\rangle$ is comprised of a map $\alpha:\mathbb{A}\rightarrow\mathbb{L}$ where $\mathbb{A}$ is the set of all possible agents/actors identifiers in the system, and $\mathbb{L}$ are possible local states. In that state, $m\in\mathbb{M}$ is the set of all pending messages, while $\mathbb{M}$ is the set of all possible messages in the system.We, also, use $pending(s)$ to indicate the set of pending messages for a state $s\in\mathbb{S}$.

Each actor processes each received message atomically since it does not share any state with any other actor/agent.

That processing step is called a transition (or processing a receive). Processing a transition $t\in\tau$, where $\tau$ is the set of all possible transitions in a system, may lead to one of the three outcomes (or a combination of them) depending on the agent’s/actor’s local state and constrains imposed by its implementation logic. These outcomes are the following: changing its local state, sending out new messages (we call this enabling new receives/transitions), and/or creating new agent(s)/actor(s).

Note that the above definition is still verbatim as in TransDPOR paper, only symbols and the way it was stated differs a little. The message processed causing the transition $t_{m}$ be executed is denoted as $\textit{msg}(t_{m})=m$, the actor/agent (also called destination of the receive) that performed the transition is denoted as $\textit{actor}(t_{m})=a$, the message(s) sent out due to executing the transition is denoted $\textit{out}(t_{m})$, and actors created as $\textit{new}(t_{m})$. Further, we add our definitions to simplify the resulting pseudocode and make it more understandable. The sender of a message is denoted as $\textit{sender}(m\in\mathbb{M})$ is the sender actor/agent of that message.

Next, we also keep TransDPOR ⁸ definitions that follow the standard DPOR ²⁰ presentation style. A schedule (a sequence of transitions) is defined in Definition 3.2.

To elaborate on Definition 3.2, A transition sequence $S$ is a finite sequence $t_{1}.t_{2}\dots t_{n}$ of transitions where there exists states $s_{0},s_{1},\dots,s_{n}$ such that $s_{0}$ is the initial state and a series of transformations of that state to intermediate states reaching the terminal state $s_{n}$, as in $s_{0}\xrightarrow{t_{1}}s_{1}\xrightarrow{t_{2}}\dots\xrightarrow{t_{n}}s_{n}$. Two transitions are said to be independent when they are not performed by the same actor/agent.

All independent transitions can be left without permuting their execution order, in as much as the system allows, with respect to each other since they can commute without affecting the resulting state of their different execution orders. Two transitions $t_{i}$ and $t_{j}$ are denoted $\textit{dependent}(t_{i},t_{j})$ if and only if they are dependent, per Definition 3.3 for DPOR/TransDPOR algorithms and per Definition 3.8 for IRed/LiViola. We also override that by using only transitions’ ids to say the same, as in $\textit{dependent}(i,j)$. From that, two schedules are considered equivalent based on whether all that changed between them is the relative re-arrangement(s) of independent transitions. Definition 3.5 defines this relationship between two equivalent schedules. It is crucial, at this point, to define the happens-before relationship in Definition 3.4 for the definition of equivalent schedules (Definition 3.5) to be clear.

The happens-before relation is the first of two constraints that enforces the strict ordering of a subset of the transitions in a schedule based on the system imposed constraints. This is necessary since it is the basis of partial order reduction; it imposes partial ordering on some of the transitions during permuting of schedules. The second constraint is the direct/indirect enablement between two receives/messages, which is defined in Definition 3.6.

We define some auxiliary functions to be used throughout the rest of the paper:

• •

  dom(S) is the set of identifiers assigned to the events in the schedule/trace S to determine their location in the sequence of events/receives..

• •

  out(S) is the messages sent out after executing/processing schedule/trace S events, also overridden for a single event e.g. $\textit{out}(S_{i})$.

The above is TransDPOR’s enablement relation. It differs significantly from our (IRed’s) enablement definition we present shortly. The TransDPOR definition of enablement, shown above in Definition 3.6, states that: 1) if a message $m$ is sent from the transition/receive $S_{i}$, then that receive enabled that message (i.e. enabled the transition that will process it later when received by the agent it is destined to), or 2) if an earlier transition/receive $S_{i}$ enabled another transition/receive $S_{j}$ that, in turn, sends a message $m$, then $S_{i}$ indirectly (but only through one intermediate transition – “exists”) lead to enabling that message $m$. We need to pause at the second part of the definition. It allows only one intermediary transition/receive to enable and indirect enablement of a message/receive. Here is a missed opportunity, i.e. the definition misses partial order reduction opportunities for coarser grained interleaving. In other words, TransDPOR definition of enablement relation, does not capture the full transitivity of the enablement relation defined by IRed. It approximates to the first transition after the dependent transition as the root-enabler. This over-approximation leads to unnecessary additional schedules that are uninteresting. This is crucial to take note of as it is the basis of precise causality tracking of both IRed and LiViola that we define next.

Next we present our new definition of the enablement relation (IRed’s), that is transitive enablement relation (“for all”) in Definition 3.7. It, also, is what we call causal chains. That is, we redefine the enablement relation in the pseudocode to be that of ours, with minimal change to the original TransDPOR algorithm.

Note that Definition 3.7 is significantly different than the way TransDPOR defines the enablement relation. Specifically, it differs in the second case of the definition. Here, we define the transitive enablement relation based on the observation that a sequence of transitions each enabling the next in a certain execution path (sub-schedule or sub-sequence) through the same or different actors, then that sub-sequence may enable a message/receive to eventually but strictly causally be sent out. The specific criteria to detect that pattern is specified by a $\forall j,k$ quantifier over transitions whose indices are $i<j<k$ in that sub-sequence $w$. That sub-sequence $w$, in turn, conforms completely (all its transitions) to the happens-before relation, it is a total order by itself. To recap, the happens-before relation in actors is a relation over transitions each of which is enabled by a received message (a receive). This is why we use transitions and receives interchangeably. This is stated by $i\rightarrow_{S}j$ for the first transition being fixed by the relation and for all $j,k\in\textit{dom}(w)$ such that each $j$ happens-before all $k$’s after it, $j\rightarrow_{S}k$. Further, the message $m$ has to be sent out by the last transition $w_{l}$ ($m\in\textit{out}(w_{l})$) and whose index is the last in the sub-sequence $w$ ($l=\textit{max}\{\textit{dom}(w)\}$).

For better readability of the algorithm presented next, the term $i\xRightarrow{}m$ can be read as “the causal-chain that starts with $i$ and ultimately causes message $m$ to be sent”. For brevity, IRed’s definition of transitive enablement relation means one transition may enable a series of subsequent acyclic transitions/enablements to eventually enable (send out) a certain message $m$. The specific implementation details to detect that pattern will be discussed in context when explaining the IRed algorithm in the next section, §3.1.2.

Next, we explain IRed and Liviola algorithms with respect to TransDPOR in a much similar style as it was done for TransDPOR with respect to DPOR. We chose to stick to the same style as it makes understanding the subtle differences between these algorithms easier to follow, and it binds previous and current publications all together for better documentation of advancements.

In this section we explain the IRed pseudocode shown in Algorithm 1. Again, the underlined parts are the differences between the original TransDPOR algorithm, while the double underlined is the difference between LiViola and IRed. We begin by explaining some notations used in the pseudocode to make explaining the algorithm more streamlined.

For a schedule $S=t_{1}.t_{2}\dots t_{n}$, $\textit{dom}(S)$ is the set of transitions identifiers $\{1,2,\dots,n\}$, while $S_{i}$ for $i\in\textit{dom}(S)$ is the specific transition $t_{i}$ in that schedule $S$. The state $s_{i-1}\in\mathbb{S}$ from which a transition $t_{i}$ is executed is denoted by $\textit{pre}(S,i)$. The state $s_{n}\in\mathbb{S}$ after a schedule $S\in\tau^{*}$ is executed is indicated by $\textit{last}(S)$. Finally, we use $\textit{next}(s_{i}\in\mathbb{S},m)$ to indicate the transition $t$ that processes the message $m$ starting from state $s_{i}$.

As we already know, and like DPOR-based algorithms before it, IRed maintains a backtracking set that keeps track of all receives/transitions that are to be explored from that specific state $s\in\mathbb{S}$ to which they were added. However, just like TransDPOR, that backtracking set can only have one transition/receive at max at all times. That is implemented using the $freeze$ flag, if it is set in that specific state, the algorithm does not add anything to that state’s backtracking set, $\textit{backtrack}(s)$. Otherwise, it adds one transition/receive, and it sets the $freeze$ flag to prevent more receives from being added, as long as it is frozen. When the algorithm backtracks to that specific state $s\in\mathbb{S}$ and $\textit{backtrack}(s)\not=\phi$, it resets the $freeze$ flag and executes the transition/receive from that backtracking set. Just as a reminder, all our algorithms except Systematic Random are depth first search algorithms (DFS).

Next, we explain (line by line) the pseudocode shown in Algorithm 1. IRed starts, like TransDPOR, by finding the current state $s$ for the input sequence/schedule $S$ (line 2). The algorithm then loops over all $\textit{pending}(s)$ messages in state $s$ (line 3) and explores them depth first. Lines 4-10 contain the main logic of the algorithm, while Lines 11-19 contain the recursive step of the algorithm. At line 4, it starts by searching for the latest ($\textit{max}\{\dots\}$) dependent state $\textit{pre}(S,i)$ for the currently being explored transition $\textit{next}(s,m)$ that are may/not be enabled and both are not governed by the enablement relation $i\not\rightarrow_{s}m$. If there is such, the algorithm proceeds to line 5, otherwise it tries with another message $m\in\textit{pending}(s)$. If there is no more messages in the pending set $\textit{pending}(s)$, it jumps to line 11. Assuming there was such dependent state, however, the algorithm will then check if the dependent state’s freeze flag is not set (i.e. reset), $\neg\textit{freeze}(\textit{pre}(S,i))$. If it is set, however, the algorithm proceeds to line 11, again. If the $freeze$ flag is reset, this means the backtracking set of the dependent state does not have any transition/receive in it, and hence the algorithm will attempt to find a candidate transition/receive set to add one from it to the backtracking set, Line 6. At line 6, the algorithm tries to do one or two checks, depending on some criteria to be discussed soon, in order to construct the candidate receives/transitions set (indicated by $E$) from which it adds to the backtracking set of the dependent receive $\textit{backtrack}(\textit{pre}(S,i))$. The first check the algorithm does to find candidate receives/transitions (or similarly messages) to add to $E$. To do this, it checks if the current message being explored is co-enabled with the message processed by the transition executed from the dependent receive, $m^{\prime}\in\textit{enabled}(\textit{pre}(S,i))$. If there is any, that is added to the candidate set $E$.

Before we explain the second check, there is a note we want to make. In TransDPOR pseudocode, there was a redundant conjecture of two terms at the end of the line starting with ($\exists j\in\textit{dom}(S)\ |\ m^{\prime}\dots$). We removed that to make it more readable, since they cause confusion and it is covered by the line that starts with ($j=\textit{min}\{\dots\}$). That conjecture was “$j>i$ and $j\rightarrow_{S}m$”.

In addition, the algorithm does another check so that if there is a message that was enabled directly or transitively (indirectly) through what we called earlier a causal chain, i.e. a series of receives/transitions for which each earlier transition/receive enables a later one to be executed. The algorithm tries to find a transition $S_{k}$ that enabled a message $m$ directly or transitively through later enabled transitions/receives, $k\xRightarrow{}_{S}m$. The said message is found by first extracting a sub-sequence $w$ (Definition 3.7), using the transitive enablement relation, whose all transitions conform to the predicate $\textit{receiver}(w_{k-1})=\textit{sender}(w_{k})$ and whose last transition causes the message $m$ to be sent out. In IRed’s implementation, the predicate is used to extract the sub-sequence $w$ by traversing the transition sequence in reverse (we call it reverse traverse) down to the earliest transition $t_{k}\in w$ that satisfies it. The reason behind this is that the algorithm only knows what transition is caused by which one that happened before only after executing all transitions before it. In other words, the algorithm does not know the future, it only checks the past transitions to detect the root-enabler $t_{j}$ where $j\in\textit{dom}(S)$. That $w$ is a sub-sequence of the schedule $S$, i.e. its transitions is a subset of $S$ transitions, with the same original relative order in $S$, that conform to the said predicate. After the algorithm extracts that sequence, it chooses the first transition of it as the root enabler of the message $m$, and hence considers it a candidate to be added to $E$. All of the above is stated in the pseudocode as: $j=\textit{min}\{k\in\textit{dom}(w)\ |\ k>i$ and $k\xRightarrow{}_{S}m\}$. What was just explained is the more precise tracking of the root enabler (i.e. the first transition in the sub-sequence $w$) that IRed tracks precisely in comparison to TransDPOR’s redundant over-approximation of the root enabler (the first transition/receive that happened after the dependent transition/receive in $S$).

Now, the only difference between LiViola and IRed is that LiViola overrides the $\textit{dependent}(i,j)$ relation and tightens it a bit more than just two receives/transitions are dependent if they are executed/performed by the same receiver actor/agent. It is double underlined in the pseudocode shown in Algorithm 1. Definition 3.8 redefines the dependence relation for LiViola.

Lines 11-19, are the recursive step of the algorithm. In line 11, the algorithm checks if the message under investigation $m$ (that was picked randomly from the pending set) is in the enabled set of the last state in the schedule, $\exists m\in\textit{enabled}(s)$. If not, it tries with other messages $m\in\textit{pending}(s)$ looping back to Line 3. If the message is in the enabled set of that last state $s$, the algorithm proceeds to update the backtracking set of $s$ to the randomly picked message $m$, $\textit{backtrack}(s):=\{m\}$ (Line 12). The reason behind this is that the algorithm always checks the backtracking set for the next message to explore, it simplifies the implementation. At line 13, the algorithm resets the new state’s explored set $done$ so that it marks future to-be-explored receives/transitions. The loop in line 14, then, recurses over all messages that are in the backtracking set of the latest state but that were not explored before, $\exists m\in(\textit{backtrack}(s)\setminus\textit{done})$. Each message $m$ is marked as explored, $\textit{add}\ m\ to\ \textit{done}$ (line 15). Then the state is marked as unfrozen, i.e. the algorithm can update its backtracking set by future transitions/receives, $\textit{freeze}(s):=\textit{false}$ (line 16). Finally, the algorithm recurses on the next state resulting from processing the message $m$ (as in performing the transition/receive), $\textit{Explore}(\textit{S.next}(s,m))$, and appending the resulting transition to the transition sequence/schedule $S$ (Line 17). The algorithm continues until there are no more messages in the pending set.

The next section will detail our experiments for evaluating the performance of all the mentioned algorithms.

Synthetic clients created by schedulers are empty agents without any behavior. The scheduler creates a client per request. Each client submits one request in its lifetime and receives at most one response. The scheduler then picks these responses and appends them to the schedule at hand. After done generating all schedules, the accumulator construct that tracks these schedules and their associated data statistics generates the histories from the schedules. It is up to the construct implementation that is accumulating schedules to decide how to use these schedules as a post-processing step to transform these schedules.

Beyond the actor system itself, linearizability checking requires some set of client invocations of the ADT methods so that algorithms can observe the outcomes and produce histories to check. Different patterns of client requests have different trade offs. Simple harnesses with few invocations may not produce buggy histories, while complex harnesses with many invocations may suffer state space explosion. Hence, we explore a few small harnesses chosen for each specific ADT that attempts to mix method invocations that observe state with those that mutate it.

Linearizability is defined on what clients observe, so harnesses only make sense if they generate multiple invocations that observe the target state. Furthermore, bugs are most likely to manifest when those observations could have been affected by interfering mutation operation(s). For the register, we start with a simple harness that generates two read() operations and a write(v) operation (we call this harness the 2r+1w harness). We also use a harness that includes a second write(v^′) operation (2r+2w), since concurrent mutations are often a source of bugs. The latter case with mutating operations can timeout, so it finds fewer bugs than first harness.

Each harness has six sections. The first specifies the initial state of the sequential specification and whether the ADT is a MAP or a SET (a register is a one-key key-value map). The second section specifies sets of target agents’ identifiers in order to distinguish them from other agents (e.g. synthetic clients). The next three sections indicate how the agents should be initialized, and it provides patterns that bind messages to message categories that the scheduler can understand. For example, it provides patterns that let it recognize read, write, and replication messages and their acknowledgments in agents’ queues. The final section is provided specifically for LiViola to indicate which messages are of interest to interleave, where the key lies in the payload of these messages (if it is not known until runtime, then a wildcard of -1 can be provided), whether it is a read-related/write-related/both message. The final section also contains some exclusions for messages; only LiViola respects these; it does not shuffle these excluded messages with rest, which helps it control state space explosion. The messages should only be excluded from interleaving if all the following conditions apply: receiving that message at the destination

• •

  should not interfere or cause potentially interfering messages to be sent back into the ADT cluster (to ADT agents);

• •

  should not mutate agent state (e.g. change the key-value pair);

• •

  should not change the observed value at the client (even if it blue change the state in question).

That being said, we could not apply any exclusions to the correct distributed register harness. Also, note that excluding a message does not mean that it is not executed, LiViola just does not shuffle it; it executes in whatever order it occurs. These exclusions are both problem specific (i.e. linearizability in this case) and implementation specific. The source code gives the precise format and details of the harness format.

In virtually all cases, configurations avoid an explosion of runtime in checking histories using the exponential WGL algorithm ($\textit{TC}\approx 0$). Some of the configurations produce several unique histories ($\textit{UH}\in[6,3557]$, Figure 8c), but since the harness is constrained to just a handful of invocations, checking all of them is still nearly instantaneous ($\ll$ 1 second). Hence, though we were worried the complexity of checking histories would be problematic (poor quality), the explosion in schedulers state space seems to be a more serious issue (poor progression) (Figure 8a and 9a).

This suggests, just as in conventional model checking, smarter pruning or direction of scheduling is more important in finding bugs than reducing history checking time. This also reinforces our decision to focus our efforts on improving schedulers for linearizability checking rather than focusing on improving linearizability checking itself as others have done ¹⁴.

The Systematic Random scheduler is ineffective in finding bugs (Figure 8b). It progresses well, and it produces many unique histories quickly (Figure 8d). However, even after doubling its cutoff to let it explore more schedules, it still finds only one bug in one configuration (the second harness of Open Chord), where other approaches find many more.

Coupled with the previous conclusion, this suggests that simply generating more histories alone is not sufficient to find bugs. This also suggests that any approach that simply tries to maximize “coverage” in the space of schedules or in the space of histories is not likely to yield bugs unless it is efficient enough to provide near-full coverage, which is unlikely due to the exponential explosion of exploration space.

Exhaustive DFS (EX) and Delay-Bounded (DB) perform similarly in most cases and metrics, even though DB uses some bounded randomness. By delaying events, DB reorders the space of schedules, but without a cutoff, EX eventually explores the same schedules in a different order. So, DB’s limited randomness does little to change the set of schedules explored.

Both approaches do well at finding bugs with the first harness (2r+1w). In the other harness (2r+2w), they hit the cutoff rather quickly (Figure 8a), which indicates they generated too many fruitless schedules from the state space. This is reflected in their poor precision ($\textit{NL}/S$, Figure 8f) and progression ($\textit{UH}/S$, Figure 8d) ratios. If we removed the cutoff, they will find bugs in the second benchmark but only after generating large numbers of uninteresting schedules, which indicates they are not effective exploring larger state spaces.

An important observation is that chronological uniqueness of histories (involved in many measures), indicated by an asterisk ‘*’ in graphs of Figures 8 and 9) causes an issue. It causes redundancy in the counts of unique histories particularly so for schedulers exploring more redundant schedules (e.g. SR and DB). It amplifies the illusion of their effectiveness in generating more unique histories. The following is the list of all schedulers, ordered from most to least affected by this issue: SR, DB, EX, DP, TD, IR, LV. As we go from left to right in that list, the less amplification effect we get because there are fewer repeated chronologically unique histories; hence, the more credible the measures are of that specific scheduler. LiViola is the best due to being the least redundant. Unique histories it produced tended to have the most diversity among all. Even with this diversity, in Open Chord benchmarks, for example, LV produced four non-linearizable histories out of 17 unique histories on the smaller harness. When we cross-checked them with the larger harness we saw that they are the same history (i.e. the same exact bug), shown in Figure 7, and explained by the schedule shown in Listing 1. Note that the other write call of the second harness is on a different key ($k_{2}$); hence, not shown, since it does not affect LV. However, it does affect all others’ results. If the $k_{2}$ related invocation and response are placed at the end of the history, one can imagine how many internal schedules that can be repeating the bug before it.

Another example on the other (most affected) extreme in Open Chord benchmarks, DB produces 3,557 unique histories and that reduce to 357 buggy ones while EX (which covers the same exhaustive state space), produces 325 unique histories that reduce to 15 buggy histories. None of them is more exhaustive than the other but DB is more repetitive than EX. The reason behind this is when the bug happens to be closer to the root of the exploration tree and the scheduler is interleaving things closer to leaves, the prefix containing the bug repeats as many times as the leaves. That has an amplification effect on bugs reported especially when the later interleavings after the prefix result in more chronologically unique histories.

In the distributed register, the three algorithms DPOR, TransDPOR, and IRed did better than EX and DB on both harnesses. DPOR, however, did slightly less favorably than TD and IR in terms of timing. The latter two did exactly the same. Otherwise, IR did not show any improvements over TD because this implementation is strongly causally consistent; hence, IR does not get an advantage over TD’s over-approximation of the root enabler. So, TD represents the worst-case scenario for IR.

In the second benchmark, DP and TD did mostly the same except for few differences on the 3 invocation test. DP produced fewer quality unique histories to catch bugs as indicated by $\textit{NL}/\textit{UH}$, and it is less precise as indicated by $\textit{NL}/S$ than TD. However, results show it is more precise than IR. This is tempered by what we mentioned regarding repetitive chronological uniqueness of histories. TD was significantly faster at making progress towards unique schedules than DP. As for IR in the second benchmark, precision, quality and progression are slightly less than TD, but TD is more repetitive.

LV performance numbers should have been exactly like IR’s on the register benchmarks, since they are one-key stores. LV enables developers to tweak the harness with interleaving exclusions (within the constraints we mentioned in §4.1 to assure soundness) to indicate which messages are the focus on during exploration (i.e. potentially interfere) which lead to significant improvements. It explores only 88 schedules in comparison to the second highest runners’ (IR and TD) 2,906 on the smaller harness, and does not approach the cutoff on the 4-invocations test, at 7,236 schedules. Meanwhile, IRed ran for over 203 hrs and still never terminated. However, developers should practice caution using this feature as we will see why in the next benchmark.

In the second benchmark, IR and LV were the best of the algorithms, too. They performed similarly except LV scored significantly better but were 2 seconds slower. In the third benchmark, LV performance was the worst-case scenario showing exact statistics as IR. Note that on the buggy version of this third (not shown here), when we tweaked the harness aggressively, LV outperformed all others by a large margin in the first harness. However, for the second test, it missed all bugs and prematurely terminated at a bit over 10K schedules stating it did not find bugs; when it should not miss bugs. So, we reverted these tweaks and passed a plain harness, i.e. with no tweaks, and re-run the experiments, shown in the Figures 8 and 9. This is an example of why developers are to practice caution when tweaking the harness while still conforming to the criteria presented in §4.1. The reader is encouraged to look at the rest of the numbers in tables in Appendix A for raw numbers, the best results we observed are for Open Chord.