Siyao Meng created HDDS-16434:
---------------------------------
Summary: Formal verification for Ozone Recon OM data sync with TLA+
Key: HDDS-16434
URL: https://issues.apache.org/jira/browse/HDDS-16434
Project: Apache Ozone
Issue Type: Sub-task
Reporter: Siyao Meng
Use TLA+ (via the Specula pipeline) to model and verify Recon OM data
synchronization: delta and full snapshot sync from OM, the OM lineage epoch,
the async reprocess of derived tables, and crash before reprocess durability.
Model check the specification and validate real Recon 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||
|recon-om-sync|medium|{{campaigns/ozone-9fbf9ee/targets/023-recon-om-sync/.prompt-extra.md}}|1
reproduced Critical, 1 env-limited Critical|
h3. Reproduce
{code:none}
specula run --agent=claude-code --effort=medium --keep-original
--max-parallel=2 \
--enable-reviews --confirm-debate --tlc-memory-limit=28G --tlc-worker-limit=8
\
"recon-om-sync|apache/ozone|Java|Use the target-specific .prompt-extra.md"
{code}
h3. Bugs (link via "Testing discovered")
* (REPRODUCED, Critical) BUG_RECON_MC2: a full snapshot swap onto an earlier OM
lineage plus a crash before the async reprocess becomes durable leaves Recon
derived tables permanently built against the old OM lineage, because
reconciliation is epoch blind. [recon-om-sync MC-2]
* (ENV_LIMITED, Critical) BUG_RECON_MC1: real defect reachable only outside the
modeled configuration; classify by consequence. [recon-om-sync MC-1]
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]
