Files
scylladb/test
Tomasz Grabiec f582bfd453 Merge "test: raft: randomized_nemesis_test: generator test with linearizability checking" from Kamil
The AppendReg state machine stores a sequence of integers. It supports
`append` inputs which append a single integer to the sequence and return
the previous state (before appending).

The implementation uses the `append_seq` data structure
representing an immutable sequence that uses a vector underneath
which may be shared by multiple instances of `append_seq`.
Appending to the sequence appends to the underlying vector,
but there is no observable effect on the other instances since
they use only the prefix of the sequence that wasn't changed.
If two instances sharing the same vector try to append,
the later one must perform a copy.

This allows efficient appends if only one instance is appending, which
is useful in the following context:
- a Raft server stores a copy in the underlying state machine replica
  and appends to it,
- clients send append operations to the server; the server returns the
  state of the sequence before it was appended to,
- thanks to the sharing, we don't need to copy all elements when
  returning the sequence to the client, and only one instance (the
  server) is appending to the shared vector,
- summarizing, all operations have amortized O(1) complexity.

We use AppendReg instead of ExReg in `basic_generator_test`
with 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 serializability checker with O(1) amortized
complexity on each operation completion.
We also enforce linearizability by checking that every
completed operation was previously invoked.

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.

* kbr/linearizability-v2:
  test: raft: randomized_nemesis_test: check consistency and liveness in basic_generator_test
  test: raft: randomized_nemesis_test: introduce append register
2021-09-23 23:55:13 +02:00
..
2021-09-22 13:13:06 +03:00
2021-09-12 11:32:13 +03:00