[
https://issues.apache.org/jira/browse/HDDS-15926?page=com.atlassian.jira.plugin.system.issuetabpanels:all-tabpanel
]
Siyao Meng updated HDDS-15926:
------------------------------
Description:
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.
was:
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]
> 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
(v8.20.10#820010)
---------------------------------------------------------------------
To unsubscribe, e-mail: [email protected]
For additional commands, e-mail: [email protected]
