You are viewing a plain text version of this content. The canonical link for it is here.
Posted to commits@hugegraph.apache.org by va...@apache.org on 2026/09/13 07:20:30 UTC
(hugegraph) branch refactor/rust-rewrite-design updated (4b1f238ba -> dc3aede8f)
This is an automated email from the ASF dual-hosted git repository.
zyxxoo pushed a change to branch refactor/rust-rewrite-design
in repository https://gitbox.apache.org/repos/asf/hugegraph.git
from 4b1f238ba docs(build): archive latest validation evidence
new 5846d4c55 feat(tools): add standalone raft linearizability checker
new dc3aede8f docs(test): link standalone linearizability oracle
The 2 revisions listed above as "new" are entirely new to this
repository and will be described in separate emails. The revisions
listed as "add" were already present in the repository and have only
been added to this reference.
Summary of changes:
docs/rust-rewrite-oracle-finalization.md | 2 ++
tools/raft-linearizability/README.md | 17 +++++++++++
tools/raft-linearizability/checker.py | 49 ++++++++++++++++++++++++++++++
tools/raft-linearizability/test_checker.py | 18 +++++++++++
4 files changed, 86 insertions(+)
create mode 100644 tools/raft-linearizability/README.md
create mode 100644 tools/raft-linearizability/checker.py
create mode 100644 tools/raft-linearizability/test_checker.py
(hugegraph) 01/02: feat(tools): add standalone raft linearizability checker
Posted by va...@apache.org.
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 <va...@apache.org>
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]
(hugegraph) 02/02: docs(test): link standalone linearizability oracle
Posted by va...@apache.org.
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 dc3aede8f1d3f4a6c4fb538ebd4811f667bf6cea
Author: vaughn <va...@apache.org>
AuthorDate: Sun Sep 13 15:20:22 2026 +0800
docs(test): link standalone linearizability oracle
---
docs/rust-rewrite-oracle-finalization.md | 2 ++
1 file changed, 2 insertions(+)
diff --git a/docs/rust-rewrite-oracle-finalization.md b/docs/rust-rewrite-oracle-finalization.md
index 28f7c37d9..0c5279b79 100644
--- a/docs/rust-rewrite-oracle-finalization.md
+++ b/docs/rust-rewrite-oracle-finalization.md
@@ -62,6 +62,8 @@
## 完成条件
+已落地一个独立的单寄存器历史 checker：`tools/raft-linearizability/checker.py`。它仅依赖历史输入，通过回溯搜索验证实时顺序和读写语义；测试位于 `tools/raft-linearizability/test_checker.py`。该工具只覆盖 Raft 线性一致性 Oracle 的最小切片，不能替代多分区、多副本和快照恢复验证。
+
只有同时满足以下条件，测试盘点才可称为最终版并允许 Rust 单元替换：
- 所有 CI 实际执行方法均达到 `reviewed` 或明确标记为 `irrelevant`；