[
https://issues.apache.org/jira/browse/RATIS-2542?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18102989#comment-18102989
]
Anony Mouse commented on RATIS-2542:
------------------------------------
Following the Specula publication above - that covers the proofs half of this
ticket, so offering the empirical half in case it is useful: we have built a
working Jepsen harness for Ratis.
https://github.com/hooji/ratis-jepsen (Apache-2.0)
What it does today: a 5-node Ratis deployment in Docker with a small KV state
machine, driven through the real {{RaftClient}}. Linearizable register and
exactly-once counter workloads. Fault injection covering partitions,
crash-restart, process pause, leadership transfer, membership churn against a
node pool, snapshot churn that forces the install-snapshot path, and
storage-durability faults via lazyfs (un-synced discard on a minority and
cluster-wide, plus torn writes). Checkers for linearizability, counter
semantics, liveness, and - deliberately - *evidence*: a snapshot-churn run that
never actually performed an install fails as a broken test rather than passing
as a green one.
41 reference runs against 3.2.2 and the 3.3.0 RC2 artifacts are committed in
the repository with checker verdicts, histories, and CI links, so the results
can be read without running anything. Runs that are supposed to fail - a seeded
stale-read bug, and a demonstration of the documented retry-cache expiry
boundary - are labelled as such and exist to prove the harness convicts a
system that lies.
Three things it turned up, filed separately on their own merits: RATIS-2656
({{BaseStateMachine.pause()}} closing divisions on streamed installs),
RATIS-2657 (install retry with no backoff), and a mechanism plus candidate
one-line fix for the listener {{STARTING}} problem, commented on RATIS-1825.
On the two specific targets named in this ticket's description:
{{notifyInstallSnapshot}} correctness is exercised by the snapshot-churn
scenario with the evidence assertion described above, and repliedIndex
linearizability is what the exactly-once counter workload tests - retried
non-idempotent increments across leader kills, where the retry cache is what
has to make them exactly-once. The counter runs held at the default 60 s
retry-cache window; a deliberate red run brackets the documented expiry
boundary.
Honest scope, since this ticket asks about both testing and proofs: this is
Jepsen only - no model checking, and no coverage of the one durability edge
that would need rename-level fault injection (recorded in the repo's backlog as
an open question, not a finding). The state machine under test is one we wrote,
so results are strongest where the faults exercise Ratis's own paths -
replication, elections, snapshot transfer, membership - and weaker as a claim
about arbitrary integrator state machines.
The harness is available for anyone to run, and I am happy to point it at a
build of your choosing if that would be useful.
> Distributed System Testing in Ratis
> -----------------------------------
>
> Key: RATIS-2542
> URL: https://issues.apache.org/jira/browse/RATIS-2542
> Project: Ratis
> Issue Type: Test
> Components: test
> Reporter: Ivan Andika
> Assignee: Ivan Andika
> Priority: Major
>
> This is a parent task for the effort to introduce distributed system testing
> to test the correctness of Ratis implementation as well provide proofs for
> Ratis-specific implementation (e.g. notifyInstallSnapshot correctness,
> repliedIndex linearizability proof, metadata entry, ratis group remove, etc).
> This would help to catch distributed system regressions and formalize
> implementation.
> Distributed system testing tools:
> * Jepsen, Ellen, Maelstorm
> * Fray
> * Hypothesis (Hegel)
> * Antithesis (paid)
> Distributed system proofs
> * TLA+
> ** Specula (https://github.com/specula-org/Specula) : AI generated TLA+
> already used to find some Raft bugs
> * Lean4
> * P frameworks
--
This message was sent by Atlassian Jira
(v8.20.10#820010)
