[
https://issues.apache.org/jira/browse/HDDS-15926?page=com.atlassian.jira.plugin.system.issuetabpanels:all-tabpanel
]
Siyao Meng resolved HDDS-15926.
-------------------------------
Resolution: Done
> Umbrella for Ozone TLA+ verification effort
> -------------------------------------------
>
> Key: HDDS-15926
> URL: https://issues.apache.org/jira/browse/HDDS-15926
> Project: Apache Ozone
> Issue Type: Task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Major
>
> This aims to track the effort on formal/semi-formal verification of each
> aspect in Ozone, with [TLA+|https://github.com/tlaplus/tlaplus],
> [P|https://github.com/p-org/P], etc.
> Readings:
> *
> [https://cacm.acm.org/practice/systems-correctness-practices-at-amazon-web-services/]
> *
> [https://zfhuang99.github.io/github%20copilot/formal%20verification/tla+/2025/05/24/ai-revolution-in-distributed-systems.html]
> h2. Call for help: run a verification target
> Verification runs are independent and parallelizable, so this is easy to
> share out. Each runnable target is filed as its own sub-task under this
> umbrella, labelled {{specula}} and {{help-wanted}}, unassigned, with a
> guidance file attached that defines the scope, the code entry points, and the
> question to investigate. Pick one and run it.
> Find the available ones with:
> {code:none}
> project = HDDS AND parent = HDDS-15926 AND labels = specula AND assignee IS
> EMPTY
> {code}
> h3. How to help
> # Pick an unassigned sub-task and assign it to yourself, so others know it is
> taken.
> # Re-pin the run to the current master head instead of the commit written in
> the sub-task (the pinned commit only records what the description was written
> against). Get it with {{git fetch -q https://github.com/apache/ozone master
> && git rev-parse --short FETCH_HEAD}}, or without a clone with {{git
> ls-remote https://github.com/apache/ozone master}}. Note that hash in the
> sub-task.
> # Point your coding agent (Claude Code, Codex, or similar) at the sub-task
> and have it run [Specula|https://github.com/specula-org/Specula]. The
> sub-task carries the exact command and the attached guidance file. The agent
> does the analysis, spec generation, model checking, trace validation, and
> confirmation.
> # Report back on the sub-task: post the outcome, including the commit you ran
> against. Zero findings is a useful result, because it records the target as
> covered at that commit. For each confirmed bug, file a separate Ozone Bug and
> link it to the sub-task with the "Testing" link type.
> # Optionally, post the generated TLA+ specification. Where to store and
> maintain generated models long term is still an open question, so attaching
> it to the sub-task is fine for now. Opinions on a durable home for them are
> welcome.
> h3. Notes for runners
> * Expect hours of wall clock per target, roughly 28 GB of RAM for TLC, JDK
> 21, and an LLM agent budget.
> * Code entry-point line numbers in a guidance file were captured at an
> earlier commit and may have shifted. Treat them as approximate. Specula
> re-analyzes the source, so a run does not depend on them.
> * Findings are proposals. A model-checking counterexample is a hypothesis
> about the code until it is confirmed against the implementation, and any fix
> still needs human review and testing before merge.
> * Effort level {{medium}} is the tested default for large targets. Higher
> effort can hit per-turn timeouts on the biggest ones.
> h3. Progress so far
> Twenty targets have been verified (OM write path and read consistency, key
> lifecycle and FSO deletion, snapshot diff and GC, SCM ReplicationManager and
> HA catch up, DataNode replication and EC, Recon OM sync). Those produced the
> bugs linked under the sub-tasks of this umbrella, each with a proposed fix
> and test patch attached. The remaining targets are the open {{help-wanted}}
> sub-tasks.
--
This message was sent by Atlassian Jira
(v10.3.26#10030026)
---------------------------------------------------------------------
To unsubscribe, e-mail: [email protected]
For additional commands, e-mail: [email protected]
