Generalizing and accelerating consistency checking for non-transactional distributed storage systems

Generalizing and accelerating consistency checking for non-transactional distributed storage systems

arXiv:2608.17388v1 [cs.DC] 18 Aug 2026

Kotikala Raghav Patel Jay

Aman Hassan RSRS Santhosh

Brian Sajeev Kattikat Abhilash Jindal

Indian Institute of Technology Delhi ajindal@cse.iitd.ac.in Abstract

the clients, called an operation history, is passed to consistency checkers that check for consistency violations. This paper fills two gaps in the current non-transactional consistency checkers. Firstly, distributed storage systems provide various consistency guarantees to their users [6, 13, 14, 31, 37, 46, 61]. However, the current non-transactional consistency checkers, Porcupine [3] and Knossos [36], only check for linearizability. For example, a Jepsen test used Knossos to check the operation histories produced by Zookeeper [33]. However, since Zookeeper does not provide linearizability, the analysis was not considered meaningful [35]. Secondly, these checkers often struggle to scale, since determining whether a history is linearizable is known to be NPcomplete [4]. For example, Porcupine issue#6 [2] reports that a history with just 252 operations causes the checker to hang. The history has a read following many concurrent writes. In such scenarios, the checker may have to consider many permutations of the preceding writes to determine which linearization is consistent with the read’s return value. This paper improves upon both these gaps. To realize a more versatile consistency checker, we generalize the Wing-Gong linearizability checking algorithm. This generalization enables us to check a non-transactional consistency guarantees, stronger than sequential consistency [61], such as ordered sequential consistency (Zookeeper [39]), regular sequential consistency (Gryff-RSC [25]), and bounded staleness consistency (CosmosDB [46, 61]). Further, this improved versatility of our checker enables us to check system-specific consistency guarantees for systems providing strong consistency1 . For instance, say we are testing HoliPaxos [40]. Instead of just checking for linearizability, we can check for “HoliPaxos-linearizability" which poses additional ordering constraints on operations, based on HoliPaxos’ specification, e.g., an operation committed with a lower instance number should execute earlier.

Linearizability checkers check if an operation history, observed by concurrent clients, is linearizable. They are used in testing distributed storage systems, and use the classic WingGong (WG) linearizability checking algorithm. In this paper, we generalize the WG algorithm to make linearizability checkers more versatile: we can check other nontransactional consistency guarantees, like ordered sequential consistency provided by Zookeeper. Equipped with this generalization, we can also check for system-specific consistency guarantees that introduce additional ordering constraints over operations in a history, as per the system’s specification. Our experiments with 8 distributed storage systems show that checking for system-specific consistency guarantees is easy to realize, reduces false negatives in testing, helps debug consistency violations, can be upto 370x faster, and can scale to more concurrent clients within the same checking time budget. We report 6 new consistency violation bugs, out of which 5 could not be found with existing consistency checkers.

1

Introduction

Consistency guarantees constrain the set of behaviors that can be observed by clients, concurrently interacting with a storage system. Distributed storage systems have been often found to violate their consistency guarantees by projects like Jepsen, even though these systems are usually formally specified and verified. These bugs happen because either (a) system’s specification and implementation diverge [28], or (b) the verification process did not consider certain types of faults [18], or (c) the model checker checked a smaller model; the bug reveals itself in longer runs with a particular sequence of interleavings [57]. To find bugs, Jepsen does fault injection testing. It spawns distributed storage system replicas and clients, and introduces “nemeses" that inject server failures, packet delays, network partitions, clock skew, and other real-world disruptions, to stress test the system. The requests and responses observed by

1 Following the definition from [8], we call consistency guarantees

stronger than sequential consistency strong.

1

2.1

To check system-specific consistency guarantees, we add system-specific ordering hints, e.g., instance number for HoliPaxos, within responses. We only consider returning ordering hint that is eagerly available while responding, i.e., providing ordering hints shall not introduce additional network communication and thus additional failure patterns. We empirically demonstrate that we can add such ordering hints for a variety of storage systems in less than 70 lines of code. Because of these additional system-specific ordering constraints over operations, checking for system-specific consistency guarantee is stronger than checking for the basic consistency guarantee. We report 3 bug case studies where the operation histories pass linearizability checking, but fail system-specific consistency checking. We also found that the additional ordering constraints can be helpful in finding the root cause of the problem. Finally, the additional system-specific ordering constraints also help in accelerating the checker, as the checker now has to try fewer operation permutations. In our experiments, we found system-specific consistency checking can be upto 370x faster, and can support more concurrent clients within the same checking time budget, compared to the basic consistency checking. This paper makes the following contributions: • We generalize the WG linearizability checking algorithm to check for a broader set of non-transactional consistency guarantees that are stronger than sequential consistency. We show how this generalized algorithm can be used for various consistency guarantees, such as the ordered sequential consistency provided by Zookeeper. • We propose checking system-specific consistency guarantees as it provides stronger checks, helps in finding rootcausing issues, runs faster, and scales to more concurrent clients. We identify ordering hints and articulate the system-specific consistency guarantees for distributed storage system protocols like Raft, HoliPaxos, EPaxos, LazyLog, Gryff, and Zookeeper. • We implement the ideas presented in this paper in a research prototype Pine. We inject faults into 8 non-transactional distributed storage systems via Jepsen and check operation histories with Pine. We find that checking for systemspecific consistency guarantees makes Pine run upto 370x faster and scales better with increasing number of clients, compared to checking the basic consistency guarantees. • In our experiments, Pine found 6 new consistency violation bugs. Out of them, 5 bugs could not be found by existing checkers. Pine will be made open source.

2

Linearizability

Linearizability is the strongest consistency guarantee, that is typically supported by non-transactional distributed storage systems [26]. Consistency guarantees are defined as constraints on operation histories. An operation history (or a trace) consists of several operations, many of which may be concurrent to one another. Each operation in the history has an invocation time, a return time, the operation’s type and parameters, and the operation’s response2 . For example, Figure 1(a) shows a history H with 4 operations on a concurrent register. op1 puts 0. op3 gets 0. Time advances from left to right; each operation is shown as an interval with an invocation time and a response time. Each horizontal level represents the operations of a single client. The operation history H determines a return-before order between its operations, which we denote as ≺rb H . For example in Figure 1(a), op1 ≺rb op since op returns before op4 starts. 4 1 H rb rb Whereas, neither op2 ≺H op3 nor op3 ≺H op2 holds, because op2 and op3 are concurrent. The return-before order is a total order for sequential histories. Figure 1(b) shows a sequential history. Burckhardt [8] calls a history H linearizable if it satisfies three primitive guarantees: 1. SingleOrder: The history H should be equivalent to a sequential history S i.e., both H and S should have the same set of operations, with identical parameters, operation type, and return values2 . 2. RVal: The equivalent sequential history S must be valid, i.e., read operations return latest written value. rb 3. RealTime: If op1 ≺rb H op2 , then op1 ≺S op2 .

For example, the operation history H in Figure 1(a) is linearizable because: 1. SingleOrder: The history H is equivalent to a sequential history S , shown in Figure 1(b). Both histories have the same 4 operations, and each operation preserves its response. 2. RVal: The sequential history S in Figure 1(b) is valid as each read returns the latest written value. 3. RealTime: The return-before order of operations in S (op1 rb rb ≺rb S op3 ≺S op2 ≺S op4 ) is consistent with the returnbefore order of operations in H (op1 ,op3 ≺rb H op4 ). Whereas, the operation history in Figure 1(d) is not linearizable. It satisfies SingleOrder with the sequential histories in both Figure 1(b) and Figure 1(c) as all of them have the same set of operations. However, when mapping it to Figure 1(b), rb it fails RealTime: op2 ≺rb H op3 , but op3 ≺S op2 . When mapping it to Figure 1(c), it fails RVal: op3 reads 0 which is not the latest written value of 1 by op2 .

Background

For completeness, this section defines linearizability and the interface of a linearizability checker. Readers familiar with them may skip to Section 3.

2 For brevity, we do not discuss incomplete histories, where responses for

some operations are missing. We refer interested readers to [8].

2

put(0) get() = 0 put(1) get() = 1 put(0) get() = 1 op4 • • get() = 0 op3 • put(1) op2 •

op1

op1

op3

op2

op4

(b)

put(0)

put(1) get() = 0 get() = 1

op1

op2

(a)

op3

op4

op1 op2

get() = 0

put(0)

op3

put(1) op4

get() = 1

(d)

(c)

Figure 1: Example histories on a register. (a) A linearizable history. (b) A valid sequential history. (c) An invalid sequential history. (d) A non-linearizable history. 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24

of Wing-Gong (WG) linearizability checking algorithm [65]. Briefly, the WG algorithm inputs the operation history as a doubly linked list. Each operation in the history has a call and a return. All calls and returns are sorted in the doubly linked list by real-time. The algorithm tries to serialize all the operations into a stack. When the algorithm is unable to serialize an operation by the time the operation returns, the algorithm backtracks by popping some operations from the stack, and trying a different sequence of operations. We refer the readers to [28, 41, 65] for more details.

type registerInput struct { op bool // false = put, true = get value int } registerModel := porcupine.Model{ Init: func() interface{} { return 0 }, // Step: takes a state, input, and output, // returns whether it was a legal operation, // along with a new state Step: func(state, input, output interface{}) (bool, interface{}) { regInput := input.(registerInput) if regInput.op == false { return true, regInput.value // always ok to execute a put } else { readCorrectValue := output.(int) == state return readCorrectValue, state // state is unchanged } }, }

3 3.1

Versatility

Distributed storage systems provide a wide variety of consistency guarantees. For example, K-bounded staleness consistency, such as provided by CosmosDB [47], relaxes just the RVal of linearizability to K-BoundedStalenessRVal: a read can return any of the previous K writes. With this change, the previously invalid sequential history in Figure 1(c) is now valid as op3 is now allowed to do a (bounded) stale read of 0. Hence, the non-linearizable history in Figure 1(d) is allowed by 2-bounded staleness consistency, as it satisfies SingleOrder and RealTime with the sequential history in Figure 1(c), which is valid as per 2-BoundedStalenessRVal. Similarly, sequential consistency relaxes RealTime guarantee of linearizability to a PRAM guarantee which itself is composed of three primitive session guarantees: MonotonicReads, MonotonicWrites, and ReadYourWrite [61]. Again, the non-linearizable history in Figure 1(d) is allowed by sequential consistency, as it satisfies SingleOrder and PRAM with the sequential history in Figure 1(b), which is valid as per RVal. Since it is often not obvious how to modify the WG algorithm to check other consistency guarantees, most existing checkers have limited versatility as they just check linearizability. As discussed in Section 1, a Jepsen analysis of Zookeeper was not considered meaningful because Knossos only checks for linearizability, and Zookeeper does not guarantee linearizability. Zookeeper guarantees ordered sequential consistency which is weaker than linearizability, but stronger than sequen-

Listing 1: Sequential specification of a register in the Porcupine linearizability checker, written in Go.

2.2

Limitations of existing checkers

Linearizability checking

A linearizability checker [3, 27, 36, 41, 65] takes as input an operation history and a sequential specification of the object, and determines whether the history is linearizable. The checker must decide whether there exists a valid total order of operations that is consistent with the history’s returnbefore partial order. The sequential specification defines what it means for a total order of operations to be valid. For example, Listing 1 shows a sequential specification of a register initialized to 0. This specification is taken from Porcupine, a state-of-the-art linearizability checker, used by etcd, TiDB, Amazon MemoryDB, and others [3]. The specification allows two operations: a put and a get (lines 1–4). The Step function determines whether a particular operation (input), is allowed to get the specified output in its current state (lines 12–23). For the register, the Step function specifies that the put operation always succeeds and sets the value of the register (lines 16–17) while the get operation is allowed only if it outputs the current state of the register (lines 19–21). Porcupine and others [27, 36] rely on optimized versions 3

tial consistency [39]. op1

3.2

Scalability

op2

The problem of determining whether a concurrent history is linearizable is known to be NP-complete [4]. As discussed in Section 1, Porcupine issue #6 reports that Porcupine hangs while checking a history with just 252 operations [2] since it has to consider many possible permutations of writes. This problem was also acknowledged by the author of Knossos linearizability checker in the same issue:

op3 op4

get() = 0 get() = 1

rev = 1 rev = 0 rev = 2 rev = 3

put(0) rev = 1 op1 put(1) rev = 0 op2 get() = 0 rev = 2 op3 get() = 1 rev = 3 op4 (b)

Figure 2: (a) A linearizable but not etcd-linearizable history. (b) Adjusted input history. This revision number can then be used to provide an additional ordering constraint (say etcd-Ordering): op1 .revision < op2 .revision ⇒ op1 ≺rb S op2 , i.e., the operation with a lower revision number must get serialized first. We call this approach as checking for system-specific consistency guarantee. Instead of checking for the basic consistency guarantee (say linearizability), we are checking for “etcd-linearizability” which strengthens linearizability to SingleOrder ∧ RVal ∧ RealTime ∧ etcd-Ordering. The etcd authors observed significant speedups when checking for etcd-linearizability, over checking for linearizability, i.e., without the etcd-Ordering constraint. In addition to being faster and more scalable, checking for system-specific consistency guarantees is clearly stronger than checking for the basic consistency guarantee. For example, the operation history in Figure 2(a) is linearizable, but not etcd-linearizable. This is because the equivalent sequential history in Figure 1(b) that helps satisfy linearizability, does not preserve the etcd-Ordering constraint: op2 has a lower revision number but is serialized after op1 . In our experiments in Section 5, we indeed found that implementation bugs can lead to histories that satisfy basic consistency guarantees, but not system-specific consistency guarantees. We had to change the experiment setup to make the same bug exhibit operation histories that also violate the basic consistency guarantees. This indicates that checking for the stronger system-specific consistency guarantees is helpful in reducing false negatives. The etcd authors realize etcd-linearizability checker via Porcupine by modifying the input history. For each operation in the original history, either the invocation time is delayed and/or the response time is advanced to generate the modified input history. For example, the operation history in Figure 2(a) is modified using each operation’s order hint (revision number) to the one in Figure 2(b)3 . This approach works well for etcd because the ordering

The suggested workarounds, such as performing frequent reads, are not always feasible when checking real-world histories [43]. For instance, a shared log [45] naturally have readers that lag significantly after writers. Paritioning of the history may also not be possible, such as in a shared log with append/get interface. Finally, reducing concurrency may not be desirable as bugs may appear only at higher-levels of concurrency. For example, in our experiments with EPaxos, out of the 3 bugs found, one appears in concurrency >10, rate >10 ops/s, and another appears in concurrency >10, rate >60 ops/s. We discuss other consistency checkers like Facebook’s [43] in related work in Section 6.

4.1

put(1)

(a)

We hit this in Knossos tests frequently, and while we’ve made as many efforts to optimize constant factors as possible, checking is still O(c!) with respect to concurrency–and concurrency almost always rises in real-world histories. You may be able to work around the issue via careful partitioning of your workload in both time and across distinct objects, reducing the state space, and performing frequent reads to prune the search space often.

4

put(0)

Pine: A more versatile consistency checker System-specific consistency checking

The worst case runtime for strong consistency checkers is determined by the total number of ways in which the operation history can be serialized. While linearizability checkers already struggle to scale, as they must consider a large number of possible operation permutations, checking for weaker consistency guarantees will worsen scalability. This is because weaker consistency guarantees have fewer ordering constraints on the operations. To improve scalability, concurrently with this paper, the etcd authors suggest in Porcupine Issue#35 [56] that the storage system can provide order hints to reduce the number of possible operation permutations, that the checker needs to check. In particular, they suggest that etcd can respond to operations with a revision number, analogous to the committed log index in Raft and the instance number in MultiPaxos.

3 Because we are only delaying invocation times and advancing response times, it can be seen that linearizable points in the modified history will also be valid in the original history, but not vice-versa. In other words, if the modified history is linearizable, then the input history must be linearizable. It can also be seen that the modified history can only reduce the number of operation permutations that may need to be tried for checking linearizability, leading to faster and more scalable checking.

4

op1

op1

1 2

op2

op2

op3

op3

op4

op4

3 4 5 6 7

(a)

8

(b)

Figure 3: Failed attempts to modify the history in Figure 2(a) with two partial ordering constraints: op1 before op2 , and op3 before op4 . (a) A modified history that adds a superfluous return-before order: op1 before op4 . (b) A modified history that loses op3 before op4 order, from the given partial ordering constraints. hints, based on revision numbers, form a total order. However, several systems, like EPaxos, can only provide partial order constraints on their operations. A 2+2 partial order cannot be converted into a modified input history without losing some ordering constraints, as the return-before ordering in operation histories can only express interval orders. For example, it is not possible to adjust the history in Figure 2(a), with op1 before op2 and op3 before op4 ordering constraints, without losing an ordering constraint and without introducing unintended orderings, as illustrated in Figure 3. For some systems, such as LazyLog, we will only be able to provide soft ordering constraints, i.e., in most cases, the operations will complete in the given order but in rare situations, like failovers or errors, they may complete in another order. We now describe a more versatile algorithm that can check different consistency guarantees, such as sequential consistency, K-bounded staleness consistency [46], ordered sequential consistency [39], and regular sequential consistency [25]. The algorithm can check for system-specific strong consistency where system provides additional ordering hints. The algorithm allows both partial and soft ordering constraints.

9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34

kBoundedReadsConsistency := pine.Consistency{ Oracles: {RealTime} Valid: { Init: func(model Model) interface() { return []int{model.Init()} } Step: func(states, input, output interface{}, model Model) (bool, interface{}) { regInput := input.(registerInput) pastStates := states.([]int) if regInput.op { // get // Check if read is valid against // any of last K states for _, s := range pastStates { ok, _ := model.Step(s, input, output) if ok { return ok, pastStates } } return false, pastStates } else { // put l := len(pastStates) ok, newState := model.Step(pastStates[l-1], input, output) // Truncate to K-1 states if l >= K { pastStates = pastStates[l-K+1:] } states = append(pastStates, newState.(int)) return ok, states } }, } }

Listing 2: A consistency model that allows K-bounded stale reads. on the doubly linked list beyond the return of an operation, until the operation is linearized on the stack. Our proposed algorithm continues to require the SingleOrder guarantee, but it generalizes RVal to a Validity guarantee (e.g., K-BoundedStalenessRVal) and RealTime to an Ordering guarantee that must be stronger than PRAM (e.g., RealTime). The basic structure of our proposed algorithm is similar to the WG algorithm. We maintain a stack of currently serialized operations, and backtrack when no further operations can be pushed on the stack.

4.2 A more general algorithm for checking consistency To develop a general algorithm, we observe that the WG algorithm checks all the three primitive guarantees, required by linearizability as follows:

op1 : put(0)

1. SingleOrder: The final stack order determines the total order of the operations.

op2 : put(1)

2. RVal: While pushing every operation in the stack, the algorithm checks whether the sequential specification (Listing 1) allows it on the current state e.g., did this read operation return the latest write in the current state, obtained from applying operations in the stack. If the sequential specification does not allow it, the algorithm backtracks by popping operation(s) from the stack.

op3 : get() = 0

op1 : put(0) op2 : put(1)

op3 : get() = 0

op4 : get() = 1

op4 : get() = 1

(a) Linearizability

(b) Sequential consistency

Figure 4: Operation DAGs for checking if the operation history in Figure 1(d) is allowed by linearizability or sequentially consistency respectively. In (b), we can find a topological order (highlighted by blue arrows), indicating that the history is allowed by sequential consistency.

3. RealTime: The algorithm does not move its entry pointer 5

For a more general Validity checking, instead of passing just the current state to the sequential specification (e.g., to the Step function in Listing 1), we pass a list of all the states from the current serialization. For example, Listing 2 defines a kBoundedReadsConsistency that takes in a model such as registerModel from the sequential specification of the register in Listing 1 to check for K-bounded stale reads in its Valid method. Consistency guarantees can declare Oracles to express more general Ordering guarantees. Each Oracle can take two operations op1 and op2 and return one of 5 ordering outcomes: (1) there is no ordering between op1 and op2 , (2) op1 must precede op2 , which we call a hard constraint: op1 ≺h op2 , (3) op2 ≺h op1 , (4) op1 should usually precede op2 in normal circumstances, but in case of fail overs etc. it may not, which we call a soft constraint: op1 ≺s op2 , and (5) op2 ≺s op1 . For example, Listing 2 declares RealTime ordering Oracle which returns op1 ≺h op2 iff op1 ≺rb H op2 . To check consistency, we maintain the operation history as a DAG instead of as a doubly linked list in the WG algorithm. Each operation is a node in the DAG with hard edges corresponding to ≺h and soft edges corresponding to ≺s orders, as returned by the Oracle. With these changes, the consistency checking boils down to finding a topological order of the input DAG over its hard edges such that the order is valid, as per the Validity guarantee. We modify the standard topological order finding algorithm to prioritize picking operations within the current frontier using the soft edges. Figure 4(a) shows the input DAG for the history in Figure 1(d) when we check it for linearizability, and Figure 4(b) shows the input DAG for the same history when we check it for sequential consistency. When using the RVal validity criteria, we can find a valid topological order for the DAG in Figure 4(b) (highlighted by blue arrows), but not for the DAG in Figure 4(a), indicating that the history is allowed by sequential consistency, but not by linearizability. A naive implementation materializes the full operation DAG, which requires checking ordering hints between every pair of operations. We discuss our optimized algorithm in Section 4.4.

4.3

consistency guarantee. To check system-specific consistency guarantee, we modify this workflow as follows: a The system implementation returns an additional order⃝ ing hint when returning each operation (e.g., revision number for etcd, zxid for ZooKeeper). b The system-specific trace parser is modified to process ⃝ traces augmented with ordering hints. It then uses the operation hints to expose additional ordering constraints between operations through a custom oracle. As discussed already, for any two operations op1 and op2 , the oracle can return 5 types of orders: no ordering, op1 ≺h op2 , op2 ≺h op1 , op1 ≺s op2 , and op2 ≺s op1 . For example, the Zookeeper [31] oracle returns op1 ≺h op2 when op1’s zxid is lesser than that of op2 . When the two zxid are equal, op1 ≺h op2 if op1 is a write and op2 is a read. c The system specifies a system-specific consistency con⃝ taining the Validity specification (e.g., K-bounded staleness validity) and a list of Ordering oracles. For example, Zookeeper-specific consistency declares the ZooKeeper oracle described above, and a RealTimeWW oracle for ordered sequential consistency which only applies return-before real time orders on writes. The consistency checker repeatedly invokes the oracles to build the operation DAG (such as in Figure 4(a)), and then finds a valid topological order in this DAG using the validity specification. Clients and sequential specification remain unmodified. Our proposed modifications are lightweight. Table 1 shows that we can check the system-specific ordering oracles that we add for 8 systems. We could add the order hints in less than 70 lines of code for all the systems.

4.4 Incorporating ordering hints to the operation DAG The consistency model enforces ordering constraints on pair of operations, which can be represented as a DAG with operations as nodes and constraints as edges. A brute-force construction requires O(n2 ) pairwise comparisons, which might be infeasable for large histories. So, we simplify the DAG construction by enforcing that the Ordering guarantee should be stronger than the SessionOrder guarantee: operations from a client must be ordered in the same order as they were issued. So, the DAG is simplified to c chains, one per client. There will be a few cross-client dependencies. We will see that we can represent the cross-client dependencies for each operation with only two edges (one incoming and one outgoing) to each of the other clients. Consider any operation opin , the nth operation from client i. For every other clients j, there exists a maximal range [u, v] of operations from client j are concurrent with opin . Operations before this range have outgoing dependencies to opin and operations after this range have incoming dependencies from opin .

System Design

Figure 5 shows how Pine modifies the consistency checking workflow of Porcupine and Knossos. All the system-specific components are highlighted in green (ignore blue italics text for now). A testing framework like Jepsen [32] spawns stor1 send operations to the age system nodes and lets clients ⃝ 2 system. The clients ⃝ record a trace of all the operations. This trace captures the timestamps of calls and returns for every operation. The trace is sent to the system-specific trace 3 helps build the operation history and sends it parser which ⃝ 4 checks the operto the consistency checker. The checker ⃝ ation history to output if the input history is allowed by the 6

Clients

System implementation def handle(op: Op): idx+=1 1 Ops ⃝ ... return { val: op.ret, a hint: idx ⃝ }

2 Client Traces ⃝ call(op1): put(1), ts: 29 ret(op1): ok, ts: 30, hint=17 call(op4): get(), ts: 33 ret(op4): 0, ts: 36, hint=20

Modified Trace parser

Consistency Checker

4 Fail/ ⃝ Success

3 Build DAG ⃝

Sequential Specification

Validity Checker

Ordering oracles b ≺ (hint1, hint2) ⃝

c System-specific consistency ⃝

Figure 5: System-specific consistency checking with ordering hints. System

Impl.

a LoC ⃝

HoliPaxos [40] etcd [16]

Go Go

3 of 3.1K 0 of 151K

Redis Raft [53]

C

30 of 28K

EPaxos [49]

Go

42 of 7.3K

EPaxos revisited [59]

Go

67 of 5.5K

Erwin [45]

C++

20 of 4.8K

Skyros [20]

C++

42 of 5.6K

Zookeeper [31]

Java

0 of 127K

Gryff-RSC [10]

Go

30 of 18K

b LoC System-specific ordering oracle ⃝ Eager total ordering linearizable systems 28 op1 ≺h op2 : op1 .instance < op2 .instance 24 op1 ≺h op2 : op1 .revision < op2 .revision w1 ≺h w2 : w1 .logidx < w2 .logidx r1 ≺h r2 : r1 .last-applied-instance < r2 .last-applied-instance 30 r ≺h w: r.last-applied-instance < w.logidx w ≺h r: w.logidx ≤ r.last-applied-instance Dependency tracking linearizable systems op1 ≺h op2 : op1 .inst ≤ op2 .deps[op1 .replica] ∧ op2 .inst ̸≤ op1 .deps[op2 .replica] op1 ≺h op2 : op1 .inst ≤ op2 .deps[op1 .replica] ∧ op2 .inst ≤ op1 .deps[op2 .replica] 55 ∧ op1 .seq < op2 .seq In addition to above, 60 op1 ≺s op2 : op1 .timestamp < op2 .timestamp Lazy ordering linearizable systems w1 ≺h w2 : w1 .view < w2 .view w1 ≺h w2 : ∀s ∈ Sequencers: w1 .seqIdx[s] < w2 .seqIdx[s] w ≺h r: ∀s ∈ Sequencers: w.seqIdx[s] ≤ r.idx 80 w1 ≺s w2 : w1 .seqIdx[leader] < w2 .seqIdx[leader] w ≺s r: w.seqIdx[leader] ≤ r.idx op1 ≺h op2 : op1 .view < op2 .view w1 ≺h w2 : w1 .DIdx[leader] < w2 .DIdx[leader] ∧ ∃ Supermajority ⊆ Sequencers : ∀s ∈ Supermajority: w1 .DIdx[s] < w2 .DIdx[s] 60 w ≺h r: w.DIdx[leader] ≤ r.CIdx[leader] r1 ≺h r2 : r1 .CIdx[leader] ≤ r2 .CIdx[leader] w1 ≺s w2 : w1 .DIdx[leader] < w2 .DIdx[leader] Non-linearizable systems op1 ≺h op2 : op1 .zxid < op2 .zxid 30 w ≺h r: w.zxid = r.zxid 18 op1 ≺h op2 : op1 .carstamp < op2 .carstamp

a add ordering hints to the implementation, and to ⃝ b incorporate Table 1: System implementations and lines of changes to ⃝ ordering hints in the system’s trace parser and ordering oracle. Ordering constraints are provided for single key operations. w represents a write operation, r represents a read operation, and op represents any of the two. For HoliPaxos, etcd, Redis Raft, and ZooKeeper the ordering constraints order operations by their position in the consensus log. Redis Raft and Zookeeper do not put reads in the consensus log. So, we order reads after writes when they return with the same last-applied-instance and zxid respectively. For Gryff-RSC, we order operations by their carstamps. For EPaxos, we use the ordering constraint proved by Theorem 5 from the EPaxos proof of correctness [49], which says that if there is a cycle of dependencies, then the operation with the lower sequence number executes first. If there are no cycles, then the dependent operation executes next. Note that all operations conflict for operations to single key. Also note that since sequence numbers can be equal, the order constraint only defines a partial order. EPaxos revisited adds timestamp-ordered queueing. We return this timestamp with each operation and use it for soft order constraints. For Erwin, we use the following hard order constraints: writes that completed in an earlier view happens first, and writes that had lower sequence number from all the sequencers happen first. If a leader does not fail, its sequence number determines the order in which writes are applied. After a failover, writes might get applied in a different order. We therefore use leader’s sequence number only in soft order constraints. For Skyros, we use the following hard-order constraints: operations that complete in an earlier view must precede those that complete in a later view. The index in the durability log orders writes, while the index in the consensus log orders reads. If supermajority of sequencers doesn’t agree on the order of writes from the leader’s durability log, then the writes might be applied in a different order during failover. We therefore relax this supermajority condition and use the resulting ordering as a soft-order constraint.

We record the start of this range as opin .start[ j] = u. We will see why this is helpful but first, we show how can we compute

this faster by making use of total order and transitivity. Suppose opin .start[ j] = u, so for all m < u, the dependency 7

j

opm → opin holds. By SessionOrder, we get the dependency j opin → opin+1 . And by transitivity we get opm → opin+1 . Therefore opin+1 .start[ j] ≥ u. So, we know a lower bound for opin+1 .start[ j]. We need to search only among the operations in client j in the range [u, #Ops from client j]. Since this is a totally ordered set, we can perform binary search on this range. Instead of the standard binary search, we perform exponential search starting from u. This performs better when the range is small. To check any arbitrary consistency model, we first construct the chains and then construct the DAG. Each operation op contains a boolean attribute op.visited which denotes whether op.start has been computed. We initialize opi0 .start for each client i. To find the single order, the checker explores all topological orderings of the DAG. It maintains a frontier, the set of operations with no non-serialized incoming dependencies. This can be easily computed using the start attribute of an operation. At each step, it picks an operation from the frontier and attempts to serialize it against the current model state. The current serialization is stored in a stack which is used for backtracking. The operations from the frontier are explored in the soft-hint order. Within the frontier, the checker compares all pairs of operations to discover the soft orders. This is possible because the size of frontier is at most O(c). When no operation from the frontier is serializable, the checker backtracks, popping an operation from the stack.

5

that Jepsen can inject faults while testing each system. We run each experiment for 2 minutes, three times, where clients send read and write requests in a closed loop. In the second phase, we analyze these histories using Pine, while varying ordering oracles, as well as with Porcupine to detect consistency violations, and to compare their runtime performance. Both implementations are written in Go. All Experiments were performed on a system with an Intel Core i9-12900 CPU (24 logical threads), 32 GB RAM, and a 1TB SK hynix NVMe SSD, running Docker v28.1.1 with Intel VT-x enabled. For finding bugs, we run each storage system with different fault injection scenarios using Jepsen. We use 5, 25, and 125 Jepsen concurrent clients with varying read ratios to send requests. In our setup, the concurrent Jepsen clients are realized by a single Jepsen control node which sends requests with different client IDs. For measuring scalability of consistency checking, we do not use Jepsen clients as it gets bottlenecked by the single Jepsen control node, producing artificially smaller operation histories. We instead use real client threads and run the 5 replicas of each system as 5 processes i.e., not inside the Jepsen’s docker cluster, without any fault injection. We use 8, 12, 16, and 20 concurrent clients with varying read ratios. For each experiment setting, we measure the end-to-end time taken to output a consistency verdict and the peak memory consumption during the checking process. Across all graphs, a x mark indicates that the checker timed out after 2 minutes and failed to produce a verdict. We report averages across the three operation history traces for each setting. For runtime performance of checkers, we only show results for operation histories that were found to be consistent, as inconsistent operation histories do not reflect the true runtime of the checkers. A checker can exit quickly on an inconsistent history, if say it is unable to put just the first two operations in a single order.

Evaluation

We have added ∼900 lines of Go code to Porcupine to realize the ideas in this paper. We call our implementation Pine. In this section, we evaluate the following research questions: 1. Is checking for system-specific consistency guarantees effective in finding bugs which may not be caught otherwise? (Section 5.2)

5.1.1 2. How do hard and soft order constraints influence the runtime and scalability of Pine? (Section 5.3)

For Redis Raft and etcd, we could use their Jepsen clients and server setups. For others, we faced several difficulties in running the systems within Jepsen. The most notable one is Erwin. Instead of using hardware RDMA in their original implementation, we tried to use software RDMA (rxe). In this setup, Erwin encountered RDMA read failures and never progressed to stable end-to-end ordering and storage. In addition, we observed an independent deadlock bug in the shard server’s read path. Due to this, we are only able to report runtime performance of checkers with Erwin where both the storage replicas and the clients are running outside Jepsen’s docker containers. Since Erwin realizes a totally ordered log with append/get operations, it is much harder to linearize than the other systems which we test with a shared register with put/get operations. Due to this, at higher concurrency and

3. Does Pine add memory and time overhead over the Porcupine implementation? (Section 5.4)

5.1

Setup limitations

Evaluation Setup

We follow a two-phase setup for our evaluations. The setup is summarized in Table 2. In the first phase, we generate a comprehensive set of operation histories by running a suite of experiments on various distributed storage systems. Each storage system is modified to respond with operation hints, as was described in Table 1. We deploy each system in Jepsen’s [32] Docker cluster containing 5 nodes, isolated within a virtual Docker network, so 8

Dimension System

Read ratio Client threads Nemesis

Client threads

Values HoliPaxos [63], RedisRaft [42], etcd [17], EPaxos [48], EPaxos-Revisited [60], LazyLog [44], Zookeeper [19], Gryff-RSC [9], Skyros [20] , YugabyteDB [68] 0.01, 0.33, 0.66, 0.99 Runtime performance testing 8, 12, 16, 20 Failure-injection testing Noop, Clock scrambling, Partition (random half), Partition (split one), Hammer-time, Majority ring 5, 25, 125

then op3 . But this linearization is not allowed by HoliPaxoslinearizability, because op2 has a higher instance number than op3 and therefore must happen after op3 . In other words, op3 reads a value that is committed later by the consensus protocol. Upon investigating the replication log, we found that HoliPaxos committed the operation op2 thrice at instance numbers 451, 456, and 461, with only the last instance being returned to the client. In other words, HoliPaxos is not idempotent, i.e., it could apply the same operation multiple times, especially after a new leader is elected (notice that op1 ’s response contained ballot=258, and op2 ’s response contained ballot=770 indicating a leader reelection after the partition). To expose non-idempotent request handling, we changed put operations to increment operations. With this modification, linearizability also failed confirming the bug. We fix the idempotency issue by implementing the ideas from RIFL [38] where clients generate a unique ID for each operation and the servers track and store the result of each operation based on its ID. If the server receives an operation with an ID that it has already executed, it simply returns the stored result of the operation, without re-executing the operation. This fix eliminated the consistency violations.

Table 2: Experiment setup configurations. Each experiment is repeated 3 times and is run for 2 minutes using closed-loop clients. We deploy each storage system with 5 replicas. For failure injection testing, the servers and clients are deployed within Jepsen’s docker cluster. lower read ratios, all checkers timeout with Erwin. We therefore report results with 4, 6, 8, and 10 client threads only. For Gryff-RSC, the client itself does additional bookkeeping of the last observed value to send with the next operation. Instead of moving this client into Jepsen, we send a read-write request from the Jepsen client to Gryff’s client which then forwards it to Gryff servers. We found consistency violation bugs in Gryff-RSC, EPaxos, EPaxos-revisited, and HoliPaxos. We were able to root cause and fix some consistency violations for the last three systems, as we will describe in Section 5.2.1. EPaxos and EPaxos-revisited still had more consistency violations which we are still investigating.

EPaxos-revisited. We found three consistency violation bugs in EPaxos-revisited. All the three bugs revealed themselves, even without any fault injection. The first bug was also present in EPaxos. The last bug could also be caught by linearizability checking, the other two only got caught when checking for EPaxos-linearizability. 1. Inconsistent cycle breaking. Figure 6(b) shows a history that is linearizable, but not EPaxos-linearizable. The dependency order hint returned for the operations show that both the reads op1 and op2 must happen after the two writes op3 and op4 (indicated by the red arrows). However, the operation op1 reads the value written by op3 , and the operation op2 reads the value written by op4 . The order hints revealed the following important details which were useful in root-causing this issue. The two reads op1 and op2 have different command leaders: replica 3 and replica 4 respectively. The two writes op3 and op4 also had different command leaders, replicas 0 and 1 respectively. The two write operations formed a cyclic dependency, both having an equal sequence number of 15380. Therefore, we suspected that the two replicas 3 and 4 which led the two reads, did not execute the two writes in a consistent manner. When EPaxos replicas track dependencies between operations, they can discover that the operation dependencies form a cycle. Each replica independently breaks the cycle by sorting the operations, and then executing them in this sorted order. To realize replicated state machines, all replicas must break dependency cycles in a consistent manner. However, this is where the bug stems from. In the implementation, different replicas can sort the operations with a dependency

5.2 Effectiveness of system-specific consistency checking System-specific consistency guarantees are stronger than basic consistency guarantees. For example, “etcdlinearizability" adds an additional “etcd ordering oracle" based on revision numbers. Evaluation highlights. We found that checking for this stronger guarantee can reduce false negatives and speed up consistency checking as there are fewer possible topological orders to explore. We also found that the operation hints can be a useful tool to debug consistency violations. We discuss the consistency violation bugs and their root causes in Section 5.2.1 and compare checker performance in Section 5.2.2. 5.2.1

Consistency violations

HoliPaxos. When we tested HoliPaxos under network partitions, we found histories that were linearizable but not HoliPaxos-linearizable. Figure 6(a) shows one such example. The history can be linearized into the order op1 , then op2 , 9

network partition

get() = 26762 get() = 26763 op2 • • instance=3:3064, seq:15381 instance=4:3064, seq:15382

op1 op1

put(1309)

put(1320)

op2 • • instance=446, ballot=258 instance=461, ballot=770

op3

get() = 1320

• instance=457, ballot=770

(a) HoliPaxos does not handle operation retries in an idempotent manner, after a new leader gets elected. For this history, op2 was executed three times, at instance number 451, 456, and 461.

put(26762) op3 • instance=0:3101, seq:15380 put(26763) op4 • instance=1:3082, seq:15380

(b) EPaxos replicas break dependency cycles in an inconsistent manner. For this history, replicas 3 and 4 executed the write operations op3 and op4 in different orders, leading to diverging reads.

put(314)

op1 op2 op3

•

•

instance=0:1075

put(307) instance=2:1058 get() = 307 •

instance=2:1059

(c) EPaxos-revisited misses dependent operations, when executing. In this history, replica 2 returns a read operation op3 , before executing the write operation op1 , on which op3 depended upon.

Figure 6: Interesting operations of linearizable histories that violated system-specific consistency guarantees. The linearization shown by the linearization points is disallowed by the systems’ ordering hints, shown by red arrows. cycle in inconsistent orders. The fix is shown in the below Listing, where the sorting comparator did not handle the case where the sequence numbers of two operations can be identical. 1 2 3 4 5 6 7 8 9

func (na nodeArray) Less(i, j int) bool { + if na[i].Seq == na[j].Seq { + if na[i].ReplicaId == na[j].ReplicaId { + return na[i].InstanceNo < na[j].InstanceNo + } + return na[i].ReplicaId < na[j].ReplicaId + } return na[i].Seq < na[j].Seq }

2. Missed operations. After fixing the previous bug, we again found another history that is linearizable but not EPaxoslinearizable. The interesting operations of the history are shown in Figure 6(c). The order hints reveal that the write operation op1 should happen before the read operation op3 , but the read operation returned a stale write by op2 . We could not reproduce this bug with EPaxos. Upon diffing the two source codes, we found that when the execution thread is traversing the dependency graph of operations, if the replica does not yet have the dependent operation or if it has not yet committed the operation, EPaxos would sleep, waiting for the operation to appear and for the commit to happen. EPaxosrevisited changed these sleep to return false as shown in the below Listing. However, when returning false from the strongconnect method, it is mandatory to clear the visited stack, otherwise the operation gets skipped. The fix was to clear the stack, whenever strongconnect returns false. 1 2 3 4 5 6 7 8 9 10 11 12 13

// ... if !e.strongconnect(w, index) { for j := l; j < len(stack); j++ { stack[j].Index = 0 } stack = stack[0:l] return false }

14 15 16 17 18 19 20 21

} // ...

22 23 24

}

3. Blind writes. EPaxos-revisited adds PUT_BLIND writes which return after committing, but before being executed, to measure and contrast commit latency with execution latency. However, the implementation missed declaring that PUT_BLIND conflicts with other writes to the same key. The fix was to add this check as shown in the below Listing. 1 2 3 4 5 6 7 8 9

// src/state/state.go func Conflict(gamma *Command, delta *Command) bool { if gamma.K == delta.K { if gamma.Op == PUT || delta.Op == PUT + || gamma.Op == PUT_BLIND || delta.Op == PUT_BLIND { return true } } }

Takeaway: System-specific consistency checking reduces false-negatives, as they are stronger guarantees than the basic consistency guarantees. The order hints can assist the developers in root-causing the reason for the consistency violation.

func (e *Exec) strongconnect(v *Instance, index *int) bool { // ... for i := e.r.ExecedUpTo[q] + 1; i <= inst; i++ { for e.r.InstanceSpace[q][i] == nil || ... { // change from time.Sleep(1000 * 1000) return false } for e.r.InstanceSpace[q][i].Status != epaxosproto.COMMITTED { // change from time.Sleep(1000 * 1000) return false }

5.2.2

Checker performance

Figure 7 compares the end-to-end runtime when checking for linearizability, and when checking for system-specific consistency guarantee, while varying the number of client threads and read ratios. Due to page limit, we only show results for two representative systems: etcd is a total order system and Erwin is a lazy ordering system. We observe that as number of client threads increase, and when read ratios decrease, the end-to-end runtime increases 10

75

.7x

17 7.8 36 x 6.6 18 x 0.6 x 3.4 x

6

8 10

Threads

.1x

100

.4x

1% 33% 67% 99%

Read Ratio

SSC

22

1% 33% 67% 99%

BC

102

44

1.3 x 0.7 x

19 9.1

x

4

x

Threads

9.8

10 2 8 12 16 20

1.1 x 4.1 x

100

6.4 x 72 .5x

Time (s)

10 2 EPaxos (50% Reads) Erwin (50% Reads) EPaxos (16 Threads) Erwin (8 Threads) 102

Time (sec)

10 .2x 58 .1x

100

4.4 x 64 .7 26 x 7.5 x

Time (s)

10

LIN SSC etcd (50% Reads) Skyros (50% Reads) etcd (16 Threads) Skyros (16 Threads) 2

2 10 Gryff(RSC)ZooKeeper(OSC) Protocols

Read Ratio

Figure 7: Performance comparison for checking basic consistency guarantees (linearizability, ordered sequential consistency, and regular sequential consistency) with checking for system-specific consistency guarantees. System-specific consistency checking can be upto 370x faster and scale better when increasing concurrency and reducing read ratios.

5.3

specific consistency checking. Then, we evaluate the impact of soft order hints (≺s ) on end-to-end runtimes.

10 1

SSC

x

.1x

100

101

31

102

SSC without soft orders

1.0

SSC with DAG

18 3 1.1 .2x x

Time (sec)

LIN SSC with modified history

Time (sec)

for checking linearizability. For higher concurrency and lower read ratios, linearizability checking starts timing out. However, this is not always the case for system-specific consistency checking. For instance, the time it takes to check for etcd-linearizability, as we increase number of client threads and reduce read ratios, only grows from 0.14s to 1.87s. This is because etcd ordering oracle already provides a total order over all the operations using the revision number order hint. For other systems, the time does grow (at a reduced rate) because their ordering oracles only provide partial order constraints. This speed up is also observed when the basic consistency guarantee is not linearizability, as shown in the rightmost plot in Figure 7. In OSC and RSC, Pine without system-specific ordering oracle quickly times out, because these consistency guarantees are even weaker than linearizability, which increases the search space of possible topological orders. Using system-specific consistency guarantees, we found a consistency violation bug in Gryff-RSC which we are still root-causing. For Zookeeper, we did not find any consistency violation bug. Note that existing checkers, like Porcupine and Knossos, cannot check these system setups as they do not guarantee linearizability. Takeaway: System-specific consistency checking can be upto 370x faster when compared to the basic consistency checking. This makes system-specific consistency checking robust in evaluating write-intensive and highly concurrent histories that traditionally bottleneck existing checkers. Pine generalizes to checking other consistency guarantees like ordered sequential consistency and regular sequential consistency which cannot be checked by existing checkers.

10 2 Erwin etcd Protocols

10 3 Erwin Skyros Protocols

(a)

(b)

Figure 8: (a) Modified history algorithm is effective for totalorder hard constraints, such as in etcd, but not for Erwin. Pine’s DAG algorithm is effective for both systems as it does not lose ordering information. (b) Soft order constraints in system-specific consistency checking can provide modest speedups. Figure 8(a) compares the end-to-end runtimes for basic consistency checking, and system-specific consistency checking using the modified history approach and the Pine’s DAGbased algorithm. Due to page limit, we again show results for the three representative systems. We observe that the modified history approach already realizes the large speed up over linearizability checking for etcd. This is because etcd’s ordering oracle provides total order constraints using revision numbers, which can be fully captured by the modified history approach (recall Figure 2(b)). However, Pine’s DAG-based algorithm gives > 180× speed up for Erwin and etcd, over the modified history approach. This is because the modified history approach loses direct ordering relations (i.e., non-transitive) because the modified history approach can only express interval orders, whereas Erwin only provide partial order constraints, which may not form an interval order. Figure 8(b) removes just the soft orders from Erwin (≺s in

Impact of Ordering Oracle’s Strength

We do two evaluations in this section. We compare the effectiveness of Pine’s DAG-based algorithm with the etcd’s modified history approach (Figure 2(b)) for doing system11

Table 1), to measure the impact of soft order on end-to-end runtimes. We observe that soft orders improve runtimes by 1.2× in Erwin. These time differences can be understood by the number of stack pops that happen while serializing the history, as is also shown in Figure 8(b). While hard ordering constraints (≺h ) reduce the number of possible topological orders, soft ordering constraints (≺s ) help Pine prioritize among concurrent operations. Takeaway: Hard order constraints (≺h ) reduce the search space and soft order constraints (≺s ) help prioritize the search. Pine’s DAG algorithm does not lose ordering relations, which are lost by the modified history algorithm. This leads to 183× speed up over the modified history algorithm.

5.4

user trust and revenue [21, 62]. These errors can be due to both protocol bugs [23, 57] and implementation bugs [66, 67]. Protocol bugs have been targeted by formally verifying safety and liveness properties of the system’s specification [12, 29, 54]. Implementation bugs have been targeted by validating the conformance of the implementation with its specification [5] using proof checkers [24], extracting implementation from the specification [64], and using model checkers [66], refinement checkers [15], and trace validation [11, 70] while performing property-based testing [50], fuzzing [51] and fault-injection testing [5, 32] over the implementation. Consistency checkers remain prevalent for checking distributed storage systems [30, 55, 58, 69] as they directly check what is observed by the clients. Consistency checkers do not necessitate writing a proof for the implementation [24], limiting the implementation language [64], writing a complete specification [15, 54], developing new logics [12], keeping the implementation and specification always in-sync with one another [5], and making assumptions about the correctness of unverified libraries, unsafe code, and possible system errors [18]. Pine performs system-specific consistency checking which requires lightweight annotation with order hints on responses: < 100 lines in all the studied systems.

Overhead

Finally, we compare the execution time and peak memory consumption of Porcupine against Pine for linearizability checking i.e., without utilizing any order hints. We report results for operation histories with concurrency set to 16 & 10 respectively for etcd and Erwin and with read ratio 0.5.

Pine

x

Porcupine

1.4

x

We have already discussed linearizability checkers in Section 2. There are also transactional consistency checkers like Elle [34], which are orthogonal to this work on checking nontransactional consistency guarantees. The non-transactional consistency checkers, built at Facebook [43] and HP Labs [1], have differing goals than Pine. These checkers count how often “consistency anomalies" are observed in their eventually consistent storage systems, whereas Pine, Porcupine, and Knossos are typically useful to catch implementation bugs.

1.0

Time (sec)

102 101 100 10 1 etcd

Protocols

Erwin

Figure 9: Pine provides comparable performance to Porcupine for testing linearizability. As shown in Figure 9, when checking linearizability (i.e., no order hints), Pine matches the execution speed of Porcupine. This confirms that Pine’s preprocessing steps, discussed in Section 4.4, adds negligible runtime overhead. We found that Pine’s memory consumption was always lower than that of Porcupine, both when Pine was checking linearizability and when it was checking system-specific consistency guarantees. This is because for both the implementations, the memory consumption is not dominated by the operation history, but rather a bitset that caches the linearizations tried thus far. Takeaway: Pine does not add much time or memory overhead over Porcupine, while providing more general consistency checking algorithm that goes beyond linearizability and supports system-specific consistency guarantees.

6

Both the Facebook and HP Labs checkers extend beyond checking linearizability, but they only extend to “local” consistency guarantees (e.g., per-object sequential consistency, and read-after-write consistency for the Facebook’s checker), where the input operation history can be partitioned into smaller histories (e.g., operations to each key in a key-value store), each of which can then be checked independently. However, operations on many data types, e.g., a totally ordered shared log [45], cannot be partitioned into independent histories. Further, several consistency guarantees, like ordered sequential consistency, are non-local. Such consistency guarantees can not be checked with their checkers. Their checking algorithms only works for shared registers with put and get operations, as they match get operations with their corresponding put operations. Therefore, the storage systems that provide read-modify-write operations [10,25,52], e.g., increment a counter, cannot be checked with their checker.

Related Work

Storage system errors can lead to severe consequences, such as data loss [67], service unavailability [7, 22, 23], loss of 12

7

Conclusion

Giardullo, Sachin Kulkarni, Harry Li, Mark Marchukov, Dmitri Petrov, Lovro Puzar, Yee Jiun Song, and Venkat Venkataramani. Tao: Facebook’s distributed data store for the social graph. In Proceedings of the 2013 USENIX Conference on Annual Technical Conference, USENIX ATC’13, page 49–60, USA, 2013. USENIX Association.

In this paper, we presented a consistency checking approach that generalizes beyond just checking for linearizability. This was possible because of the decomposition of linearizability into more primitive SingleOrder, RVal, and RealTime properties by Burckhardt [8]. Our algorithm generalizes RVal into validity properties and RealTime into ordering properties. With this generalization, we could check for weaker consistency guarantees like ordered sequential consistency and regular sequential consistency. We could also strengthen consistency checking towards system-specific consistency guarantees, where systems provide system-specific hard and soft ordering constraints, over and above their basic consistency guarantee. Our evaluations show that checking for system-specific consistency can be upto 370x faster, and can scale better to challenging scenarios of higher concurrency and lower read ratios. We report 6 new bugs, out of which 5 could not be found with existing consistency checkers.

[7] Marc Brooker, Tao Chen, and Fan Ping. Millions of tiny databases. In Proceedings of the 17th Usenix Conference on Networked Systems Design and Implementation, NSDI’20, page 463–478, USA, 2020. USENIX Association. [8] Sebastian Burckhardt. Principles of Eventual Consistency, volume 1 of Foundations and Trends® in Programming Languages. Now Publishers, principles of eventual consistency edition, October 2014. [9] Matthew Burke, Audrey Cheng, and Wyatt Lloyd. Gryff: A replicated storage system providing low read tail latency. https://github.com/matthelb/gryff, 2020. Accessed: 20 April 2026.

References [10] Matthew Burke, Audrey Cheng, and Wyatt Lloyd. Gryff: unifying consensus and shared registers. In Proceedings of the 17th Usenix Conference on Networked Systems Design and Implementation, NSDI’20, page 591–618, USA, 2020. USENIX Association.

[1] Eric Anderson, Xiaozhou Li, Arif Merchant, Mehul A. Shah, Kevin Smathers, Joseph Tucek, Mustafa Uysal, and Jay J. Wylie. Efficient eventual consistency in Pahoehoe, an erasure-coded key-blob archive. In Proceedings of the 2010 IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), pages 181–190. IEEE, 2010.

[11] Amaury Chamayou and Markus Kuppe. Consensus trace validation. https://github.com/microsoft/C CF/issues/5057, 2023. Accessed: 20 April 2026.

[2] Anish Athalye. Porcupine: Linearizability checker — github issue 6. https://github.com/anishathaly e/porcupine/issues/6. Accessed: 20 April 2026.

[12] Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. Using crash hoare logic for certifying the fscq file system. In Proceedings of the 25th Symposium on Operating Systems Principles, SOSP ’15, page 18–37, New York, NY, USA, 2015. Association for Computing Machinery.

[3] Anish Athalye. Porcupine: A fast linearizability checker in Go. https://github.com/anishathalye/porc upine, 2017. Accessed: 20 April 2026. [4] Anish Athalye. Testing distributed systems for linearizability. https://anishathalye.com/testing-dis tributed-systems-for-linearizability/, 2018. Accessed: 20 April 2026.

[13] Brian F. Cooper, Raghu Ramakrishnan, Utkarsh Srivastava, Adam Silberstein, Philip Bohannon, Hans-Arno Jacobsen, Nick Puz, Daniel Weaver, and Ramana Yerneni. Pnuts: Yahoo!’s hosted data serving platform. Proc. VLDB Endow., 1(2):1277–1288, August 2008.

[5] James Bornholt, Rajeev Joshi, Vytautas Astrauskas, Brendan Cully, Bernhard Kragl, Seth Markle, Kyle Sauri, Drew Schleit, Grant Slatton, Serdar Tasiran, Jacob Van Geffen, and Andrew Warfield. Using lightweight formal methods to validate a key-value storage node in amazon s3. In Proceedings of the ACM SIGOPS 28th Symposium on Operating Systems Principles, SOSP ’21, page 836–850, New York, NY, USA, 2021. Association for Computing Machinery.

[14] James C. Corbett, Jeffrey Dean, Michael Epstein, Andrew Fikes, Christopher Frost, J. J. Furman, Sanjay Ghemawat, Andrey Gubarev, Christopher Heiser, Peter Hochschild, Wilson Hsieh, Sebastian Kanthak, Eugene Kogan, Hongyi Li, Alexander Lloyd, Sergey Melnik, David Mwaura, David Nagle, Sean Quinlan, Rajesh Rao, Lindsay Rolig, Yasushi Saito, Michal Szymaniak, Christopher Taylor, Ruth Wang, and Dale Woodford. Spanner: Google’s globally distributed database. ACM Trans. Comput. Syst., 31(3), August 2013.

[6] Nathan Bronson, Zach Amsden, George Cabrera, Prasad Chakka, Peter Dimov, Hui Ding, Jack Ferris, Anthony 13

[15] Ding Ding, Zhanghan Wang, Jinyang Li, and Aurojit Panda. Runtime protocol refinement checking for distributed protocol implementations. In Proceedings of the 22nd USENIX Symposium on Networked Systems Design and Implementation, NSDI ’25, USA, 2025. USENIX Association.

Conference on Software Engineering: Software Engineering in Practice, ICSE-SEIP ’23, page 1–12. IEEE Press, 2023. [24] Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath Setty, and Brian Zill. Ironfleet: proving practical distributed systems correct. In Proceedings of the 25th Symposium on Operating Systems Principles, SOSP ’15, page 1–17, New York, NY, USA, 2015. Association for Computing Machinery.

[16] etcd Authors. etcd. https://etcd.io/, 2013. Accessed: 1 January 2026. [17] etcd Authors. etcd: A distributed, reliable key-value store for the most critical data of a distributed system. ht tps://github.com/etcd-io/etcd, 2018. Accessed: 20 April 2026.

[25] Jeffrey Helt, Matthew Burke, Amit Levy, and Wyatt Lloyd. Regular sequential serializability and regular sequential consistency. In Proceedings of the ACM SIGOPS 28th Symposium on Operating Systems Principles, SOSP ’21, page 163–179, New York, NY, USA, 2021. Association for Computing Machinery.

[18] Pedro Fonseca, Kaiyuan Zhang, Xi Wang, and Arvind Krishnamurthy. An empirical study on the correctness of formally verified distributed systems. In Proceedings of the Twelfth European Conference on Computer Systems, EuroSys ’17, page 328–343, New York, NY, USA, 2017. Association for Computing Machinery.

[26] Maurice P. Herlihy and Jeannette M. Wing. Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst., 12(3):463–492, July 1990.

[19] Apache Software Foundation. Apache zookeeper: A distributed coordination service for distributed applications. https://github.com/apache/zookeeper, 2008. Accessed: 20 April 2026.

[27] Alex Horn. ahorn/linearizability-checker: Fast linearizability checker. https://github.com/ahorn/lin earizability-checker, 2015. Accessed: 20 April 2026.

[20] Aishwarya Ganesan, Ramnatthan Alagappan, Anthony Rebello, Andrea C. Arpaci-Dusseau, and Remzi H. Arpaci-Dusseau. Exploiting nil-external interfaces for fast replicated storage. ACM Trans. Storage, 18(3), September 2022.

[28] Alex Horn and Daniel Kroening. Faster linearizability checking via p-compositionality, 2015. [29] Heidi Howard, Markus A. Kuppe, Edward Ashton, Amaury Chamayou, and Natacha Crooks. Smart casual verification of the confidential consortium framework. In Proceedings of the 22nd USENIX Symposium on Networked Systems Design and Implementation, NSDI ’25, USA, 2025. USENIX Association.

[21] Haryadi S. Gunawi, Riza O. Suminto, Russell Sears, Casey Golliher, Swaminathan Sundararaman, Xing Lin, Tim Emami, Weiguang Sheng, Nematollah Bidokhti, Caitie McCaffrey, Deepthi Srinivasan, Biswaranjan Panda, Andrew Baptist, Gary Grider, Parks M. Fields, Kevin Harms, Robert B. Ross, Andree Jacobson, Robert Ricci, Kirk Webb, Peter Alvaro, H. Birali Runesha, Mingzhe Hao, and Huaicheng Li. Fail-slow at scale: Evidence of hardware performance faults in large production systems. volume 14, New York, NY, USA, October 2018. Association for Computing Machinery.

[30] Dongxu Huang, Qi Liu, Qiu Cui, Zhuhe Fang, Xiaoyu Ma, Fei Xu, Li Shen, Liu Tang, Yuxing Zhou, Menglong Huang, Wan Wei, Cong Liu, Jian Zhang, Jianjun Li, Xuelian Wu, Lingyu Song, Ruoxi Sun, Shuaipeng Yu, Lei Zhao, Nicholas Cameron, Liquan Pei, and Xin Tang. Tidb: a raft-based htap database. Proc. VLDB Endow., 13(12):3072–3084, August 2020.

[22] Zhenyu Guo, Sean McDirmid, Mao Yang, Li Zhuang, Pu Zhang, Yingwei Luo, Tom Bergan, Madan Musuvathi, Zheng Zhang, and Lidong Zhou. Failure recovery: When the cure is worse than the disease. In 14th Workshop on Hot Topics in Operating Systems (HotOS XIV), Santa Ana Pueblo, NM, May 2013. USENIX Association.

[31] Patrick Hunt, Mahadev Konar, Flavio P. Junqueira, and Benjamin Reed. Zookeeper: wait-free coordination for internet-scale systems. In Proceedings of the 2010 USENIX Conference on USENIX Annual Technical Conference, USENIXATC’10, page 11, USA, 2010. USENIX Association. [32] Kyle Kingsbury. Jepsen: A framework for distributed systems verification, with fault injection. https://gi thub.com/jepsen-io/jepsen. Accessed: 20 April 2026.

[23] Finn Hackett, Joshua Rowe, and Markus Alexander Kuppe. Understanding inconsistency in azure cosmos db with tla+. In Proceedings of the 45th International 14

[33] Kyle Kingsbury. Jepsen: Zookeeper. https://aphy r.com/posts/291-jepsen-zookeeper, 2013. Accessed: 20 April 2026.

shared log abstraction for low-latency applications (artifact). https://github.com/dassl-uiuc/LazyLo g-Artifact, 2024. Accessed: 20 April 2026.

[34] Kyle Kingsbury and Peter Alvaro. Elle: inferring isolation anomalies from experimental observations. Proc. VLDB Endow., 14(3):268–280, November 2020.

[45] Xuhao Luo, Shreesha G. Bhat, Jiyu Hu, Ramnatthan Alagappan, and Aishwarya Ganesan. Lazylog: A new shared log abstraction for low-latency applications. In Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles, SOSP ’24, page 296–312, New York, NY, USA, 2024. Association for Computing Machinery.

[35] Kyle Kingsbury and Jepsen Contributors. jepsenio/zookeeper: Jepsen tests for the zookeeper coordination system. https://github.com/jepsen-io/zook eeper, 2025. Accessed: 20 April 2026.

[46] Microsoft Azure. Azure cosmos db: The industry’s first globally-distributed, multi-model database service. https://azure.microsoft.com/en-us/blog/azu re-cosmos-db-microsofts-globally-distribut ed-multi-model-database-service/, May 2017. Accessed: 20 April 2026.

[36] Kyle Kingsbury and Jepsen Contributors. jepsenio/knossos: Verifies the linearizability of experimentally accessible histories. https://github.com/jepsen-i o/knossos, 2026. Accessed: 20 April 2026. [37] Leslie Lamport, Dahlia Malkhi, and Lidong Zhou. Reconfiguring a state machine. SIGACT News, 41(1):63–73, March 2010.

[47] Microsoft Azure. Consistency levels in Azure Cosmos DB. https://learn.microsoft.com/en-us/az ure/cosmos-db/consistency-levels, 2025. Accessed: 20 April 2026.

[38] Collin Lee, Seo Jin Park, Ankita Kejriwal, Satoshi Matsushita, and John Ousterhout. Implementing linearizability at large scale and low latency. In Proceedings of the 25th Symposium on Operating Systems Principles, SOSP ’15, page 71–86, New York, NY, USA, 2015. Association for Computing Machinery.

[48] Iulian Moraru, David G. Andersen, and Michael Kaminsky. Epaxos: Go implementation of egalitarian paxos. https://github.com/efficient/epaxos, 2013. Accessed: 20 April 2026. [49] Iulian Moraru, David G. Andersen, and Michael Kaminsky. There is more consensus in egalitarian parliaments. In Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles, SOSP ’13, page 358–372, New York, NY, USA, 2013. Association for Computing Machinery.

[39] Kfir Lev-Ari. Ordered Sequential Consistency: Composition and Correctness. PhD thesis, Technion — Israel Institute of Technology, Haifa, Israel, July 2017. [40] Zhiying Liang, Vahab Jabrayilov, Abutalib Aghayev, and Aleksey Charapko. Holipaxos: Towards more predictable performance in state machine replication. Proc. VLDB Endow., 18(8):2505–2518, April 2025.

[50] Madan Musuvathi and Shaz Qadeer. Chess: systematic stress testing of concurrent software. In Proceedings of the 16th International Conference on Logic-Based Program Synthesis and Transformation, LOPSTR’06, page 15–16, Berlin, Heidelberg, 2006. Springer-Verlag.

[41] Gavin Lowe. Testing for linearizability. Concurrency and Computation: Practice and Experience, 29(4), 2017. [42] Redis Ltd. Redisraft: A redis module for creating a consistent raft cluster from multiple redis instances. ht tps://github.com/redislabs/redisraft, 2020. Accessed: 20 April 2026.

[51] Burcu Kulahcioglu Ozkan, Rupak Majumdar, Filip Niksic, Mitra Tabaei Befrouei, and Georg Weissenbacher. Randomized testing of distributed systems with probabilistic guarantees. Proc. ACM Program. Lang., 2(OOPSLA), October 2018.

[43] Haonan Lu, Kaushik Veeraraghavan, Philippe Ajoux, Jim Hunt, Yee Jiun Song, Wendy Tobagus, Sanjeev Kumar, and Wyatt Lloyd. Existential consistency: measuring and understanding consistency at facebook. In Proceedings of the 25th Symposium on Operating Systems Principles, SOSP ’15, page 295–310, New York, NY, USA, 2015. Association for Computing Machinery.

[52] Redis. Redis: An open-source, in-memory data structure store. https://redis.io/, 2009. Accessed: 24 March 2026. [53] Redis Labs. Introducing RedisRaft, a new strongconsistency deployment option. https://multidev.r edis.io/blog/redisraft-new-strong-consist ency-deployment-option/, June 2020. Accessed: 1 January 2026.

[44] Xuhao Luo, Shreesha Bhat, Jiyu Hu, Ramnatthan Alagappan, and Aishwarya Ganesan. Lazylog: A new 15

[54] William Schultz and Murat Demirbas. Design and modular verification of distributed transactions in mongodb. Proc. VLDB Endow., 18(12):5045–5058, August 2025.

Symposium on Operating Systems Design and Implementation - Volume 7, OSDI ’06, page 10, USA, 2006. USENIX Association.

[55] Marek Siarkowicz. On the hunt for etcd data inconsistencies. https://www.youtube.com/watch?v=IIMs 0EjQZHg, 2023. Accessed: 20 April 2026.

[67] Ding Yuan, Yu Luo, Xin Zhuang, Guilherme Renna Rodrigues, Xu Zhao, Yongle Zhang, Pranay U. Jain, and Michael Stumm. Simple testing can prevent most critical failures: an analysis of production failures in distributed data-intensive systems. In Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation, OSDI’14, page 249–265, USA, 2014. USENIX Association.

[56] supahero1. Allow the user to choose order heuristics. https://github.com/anishathalye/porcupine/ issues/35, September 2025. Accessed: 20 April 2026. [57] Pierre Sutra. On the correctness of egalitarian paxos. Information Processing Letters, 156:105901, 2020.

Yugabytedb is a postgresql[68] YugabyteDB Inc. compatible, high-performance, cloud-native, distributed sql database. https://github.com/yugabyte/yuga byte-db, 2016. Accessed: 20 April 2026.

[58] Yacine Taleb, Kevin McGehee, Nan Yan, Shawn Wang, Stefan C. Müller, and Allen Samuels. Amazon memorydb: A fast and durable memory-first cloud database. In Companion of the 2024 International Conference on Management of Data, SIGMOD ’24, page 309–320, New York, NY, USA, 2024. Association for Computing Machinery.

[69] Hamidreza Zare, Viveck Ramesh Cadambe, Bhuvan Urgaonkar, Nader Alfares, Praneet Soni, Chetan Sharma, and Arif A Merchant. Legostore: a linearizable geodistributed store combining replication and erasure coding. Proc. VLDB Endow., 15(10):2201–2215, June 2022.

[59] Sarah Tollman, Seo Jin Park, and John Ousterhout. EPaxos revisited. In 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 21), pages 613–632. USENIX Association, April 2021.

[70] Joshua Zhu. Tla+ trace validation. https://github .com/etcd-io/raft/pull/113, 2023. Accessed: 20 April 2026.

[60] Scott Tollman et al. Epaxos revisited: Evaluation code for the nsdi ’21 paper. https://github.com/platf ormlab/epaxos, 2021. Accessed: 20 April 2026. [61] Paolo Viotti and Marko Vukolić. Consistency in nontransactional distributed storage systems. ACM Comput. Surv., 49(1), June 2016. [62] Mitch Wagner. Amazon web services outage caused by typo. https://www.lightreading.com/it-infra structure/amazon-web-services-outage-cause d-by-typo, 2017. Accessed: 20 April 2026. [63] Zhiying Wang. Holipaxos: Artifact for holipaxos evaluation. https://github.com/Zhiying12/holipaxos -artifect, 2024. Accessed: 20 April 2026. [64] James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas Anderson. Verdi: a framework for implementing and formally verifying distributed systems. SIGPLAN Not., 50(6):357–368, June 2015. [65] Jeannette M. Wing and Chun Gong. Testing and verifying concurrent objects. J. Parallel Distrib. Comput., 17(1–2):164–182, January 1993. [66] Junfeng Yang, Can Sar, and Dawson Engler. Explode: a lightweight, general system for finding serious storage system errors. In Proceedings of the 7th USENIX 16

Related documents

• Making TransactionIsolation Checking Practical#124147
• Analisis Dampak Sistem Berkas terhadap Integritas Data, Pemulihan, dan Ketahanan terhadap Kegagalan pada Server Cloud#1066840
• Coherent File Distribution Protocol#133543
• Pratikriti: A Data Replication Service in the GFFS#649764
• Policy-Compliant Cloud Storage Systems#259376