This is an automated email from the ASF dual-hosted git repository. zyxxoo pushed a commit to branch refactor/rust-rewrite-design in repository https://gitbox.apache.org/repos/asf/hugegraph.git
commit 5846d4c55fd5ba576ea2e392d25e3892cd6d2976 Author: vaughn <[email protected]> AuthorDate: Sun Sep 13 15:19:38 2026 +0800 feat(tools): add standalone raft linearizability checker --- tools/raft-linearizability/README.md | 17 +++++++++++ tools/raft-linearizability/checker.py | 49 ++++++++++++++++++++++++++++++ tools/raft-linearizability/test_checker.py | 18 +++++++++++ 3 files changed, 84 insertions(+) diff --git a/tools/raft-linearizability/README.md b/tools/raft-linearizability/README.md new file mode 100644 index 000000000..cde68a4c1 --- /dev/null +++ b/tools/raft-linearizability/README.md @@ -0,0 +1,17 @@ +# Raft linearizability checker + +`checker.py` is a standalone, dependency-free checker for histories of a single +Raft replicated register. It does not connect to or assume anything about a +Raft implementation. The checker searches for a sequential ordering that +respects real-time precedence (`end <= start`) and register read/write +semantics. It is intentionally small and suitable as a test oracle. + +Each JSON operation has `id`, `op` (`read` or `write`), `value`, `start`, and +`end`; timestamps only need to be comparable. Run: + +```bash +python3 tools/raft-linearizability/checker.py history.json +``` + +Exit status is zero when linearizable and one otherwise. The JSON output +contains a witness operation order or an explanation. diff --git a/tools/raft-linearizability/checker.py b/tools/raft-linearizability/checker.py new file mode 100644 index 000000000..2926b05af --- /dev/null +++ b/tools/raft-linearizability/checker.py @@ -0,0 +1,49 @@ +#!/usr/bin/env python3 +"""Small, dependency-free linearizability checker for a Raft register history.""" +import argparse, json + + +def check(history): + """Return (ok, explanation). History entries: id, op (read|write), value, + start and end (monotonic timestamps).""" + ops = list(history) + ids = {o["id"] for o in ops} + if len(ids) != len(ops): + return False, "duplicate operation id" + for o in ops: + if o["op"] not in ("read", "write") or o["end"] < o["start"]: + return False, "invalid operation" + before = {o["id"]: {p["id"] for p in ops if p["end"] <= o["start"]} + for o in ops} + by_id = {o["id"]: o for o in ops} + + def search(done, value): + if len(done) == len(ops): + return () + candidates = [o for o in ops if o["id"] not in done and + before[o["id"]] <= done] + for o in candidates: + if o["op"] == "read" and o["value"] != value: + continue + nv = o.get("value") if o["op"] == "write" else value + tail = search(done | {o["id"]}, nv) + if tail is not None: + return (o["id"],) + tail + return None + + result = search(set(), None) + return (True, result) if result is not None else (False, "no legal sequential ordering") + + +def main(): + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument("history", help="JSON file containing an array of operations") + args = ap.parse_args() + with open(args.history, encoding="utf-8") as f: + ok, detail = check(json.load(f)) + print(json.dumps({"linearizable": ok, "detail": detail})) + return 0 if ok else 1 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/tools/raft-linearizability/test_checker.py b/tools/raft-linearizability/test_checker.py new file mode 100644 index 000000000..bf43260d3 --- /dev/null +++ b/tools/raft-linearizability/test_checker.py @@ -0,0 +1,18 @@ +import importlib.util +from pathlib import Path + +spec = importlib.util.spec_from_file_location("checker", Path(__file__).with_name("checker.py")) +checker = importlib.util.module_from_spec(spec) +spec.loader.exec_module(checker) + + +def test_valid_concurrent_history(): + h = [{"id": 1, "op": "write", "value": 7, "start": 0, "end": 4}, + {"id": 2, "op": "read", "value": 7, "start": 2, "end": 3}] + assert checker.check(h)[0] + + +def test_invalid_read_before_completed_write(): + h = [{"id": 1, "op": "write", "value": 7, "start": 0, "end": 2}, + {"id": 2, "op": "read", "value": 0, "start": 3, "end": 4}] + assert not checker.check(h)[0]
