mirror of
https://github.com/scylladb/scylladb.git
synced 2026-05-02 06:05:53 +00:00
ea172fe531
Use AppendReg instead of ExReg for the state machine. Use a generator which generates a sequence of append operations with unique integers. This implies that the result of every operation uniquely identifies the operation (since it contains the appended integer, and different operations use different integers) and all operations that must have happened before it (since it contains the previous state of the append register), which allows us to reconstruct the "current state" of the register according to the results of operations coming from Raft calls, giving us an on-line linearizability checker with O(1) amortized complexity on each operation completion. We also perform a simple liveness check at the end of the test by ensuring that a leader becomes eventually elected and that we can successfully execute a call.