[
https://issues.apache.org/jira/browse/HDDS-16434?page=com.atlassian.jira.plugin.system.issuetabpanels:all-tabpanel
]
Siyao Meng updated HDDS-16434:
------------------------------
Description:
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) HDDS-16462: 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) HDDS-16463: real defect reachable only outside the
modeled configuration; classify by consequence. [recon-om-sync MC-1]
Generated with Specula (Claude Opus 4.8).
was:
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).
> 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
> Priority: Major
>
> 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) HDDS-16462: 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) HDDS-16463: 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]
