Siyao Meng created HDDS-16427:
---------------------------------
Summary: Formal verification for Ozone OM write path (double
buffer and client Ratis write) with TLA+
Key: HDDS-16427
URL: https://issues.apache.org/jira/browse/HDDS-16427
Project: Apache Ozone
Issue Type: Sub-task
Reporter: Siyao Meng
Use TLA+ (via the Specula pipeline) to model and verify the OM write path: the
OM double buffer flush and ordering, and the client side Ratis write commit and
retry path. Model check the specification and validate real OM traces against
it. Bugs found by this effort are linked under this issue.
h3. Run environment
{noformat}
Ozone commit: 9fbf9ee0cb1bd2f5f5d437b6719ebbe5309351fb
Specula: v1.1.0 (commit c6aa3dfa)
Agent/model: claude-code, Claude Opus 4.8 (1M context)
{noformat}
h3. Coverage
||Target||Effort||Guidance||Result||
|om-double-buffer|high|{{campaigns/ozone-9fbf9ee/targets/007-om-double-buffer/.prompt-extra.md}}|No
findings|
|client-ratis-write|high|{{campaigns/ozone-9fbf9ee/targets/002-client-ratis-write/.prompt-extra.md}}|No
findings|
h3. Reproduce
{code:none}
specula run --agent=claude-code --effort=high --keep-original --max-parallel=2 \
--enable-reviews --confirm-debate --tlc-memory-limit=28G --tlc-worker-limit=8
\
"<target>|apache/ozone|Java|Use the target-specific .prompt-extra.md"
{code}
h3. Bugs
None. Both targets model checked clean at the pinned commit.
Generated with Specula (Claude Opus 4.8).
--
This message was sent by Atlassian Jira
(v8.20.10#820010)
---------------------------------------------------------------------
To unsubscribe, e-mail: [email protected]
For additional commands, e-mail: [email protected]
