Add sound loop thread-join coverage analysis

[michael-schwarz]

Summary

• add a new threadJoinsPool analysis for proving that loop-created threads have all been joined
• track outstanding join obligations per scalar or partitioned-array slot, including non-unique abstract thread IDs
• conservatively retain lost obligations after overwrites, copies, escapes, detach, unsupported storage, and multiple creation
• propagate clean-exit summaries so joining a worker pool does not hide unjoined descendants
• enable the previously skipped loop-join regression and add 16 focused positive and adversarial tests

Approach

This is a new side-car abstract interpretation rather than the value-domain change prototyped in #1180.

Each successfully created joinable thread introduces an outstanding obligation. For supported fixed-size local pthread_t arrays, obligations are stored in a length-aware partitioned array domain. Partition movement across loop induction-variable updates represents the created or joined prefix/suffix, allowing the analysis to distinguish multiple dynamic instances even when they share one non-unique abstract thread ID.

A permanent lost may-set preserves soundness whenever one-to-one coverage is no longer known. A thread is reported as must-joined only when it is absent from every live slot and from lost, and its thread summary establishes that all descendants exited cleanly.

The precise supported idiom is a fixed-size local array indexed by constants or plain local scalar variables, with joins performed through the same direct slots that received the handles. More complex copies, aliases, index expressions, global/escaped storage, non-default attributes, detach, and multiple creation are handled conservatively.

This directly addresses the completeness hole noted in #1180: proving every array entry is marked joined is insufficient unless every created dynamic thread was represented by a distinct canonical obligation.

Validation

• opam exec -- dune build src/goblint.exe
• ./scripts/update_suite.rb group threadjoins -s — all 28 tests pass
• ./scripts/update_suite.rb group synch -s — all tests pass
• git diff --check

The new tests cover complete and partial joins, repeated slots and repeated joins, overwritten and recreated handles, detach, copies, multiple creation, two independent pools, nested clean and dirty workers, separate scoped indices, reverse joins, and conservatively unsupported index forms.

AI disclosure

This PR was AI-generated with Codex. I burned through most of my Codex token allocation for this week while implementing, reviewing, hardening, and testing it.

[Copilot]

Pull request overview

Adds join-obligation analysis for loop-created thread pools, complementing existing thread-join tracking.

Changes:

• Implements partitioned-array and scalar join-obligation tracking.
• Propagates clean-exit summaries for nested threads.
• Adds extensive positive and adversarial regression coverage.

Reviewed changes

Copilot reviewed 20 out of 20 changed files in this pull request and generated 2 comments.

Show a summary per file

File	Description
src/analyses/threadJoinsPool.ml	Implements pool join analysis.
src/autoTune.ml	Registers analysis for tuning.
src/goblint_lib.ml	Exposes the analysis module.
tests/regression/10-synch/16-join_loop_nr.c	Enables loop-join regression.
tests/regression/51-threadjoins/13-pool-prefix.c	Tests partial joins.
tests/regression/51-threadjoins/14-pool-repeated-slot.c	Tests repeated-slot creation.
tests/regression/51-threadjoins/15-pool-two-arrays.c	Tests independent pools.
tests/regression/51-threadjoins/16-pool-overwrite.c	Tests copied-over handles.
tests/regression/51-threadjoins/17-pool-detach.c	Tests detached threads.
tests/regression/51-threadjoins/18-pool-recreate.c	Tests post-join recreation.
tests/regression/51-threadjoins/19-pool-nested-dirty.c	Tests unjoined descendants.
tests/regression/51-threadjoins/20-pool-nested-clean.c	Tests joined descendants.
tests/regression/51-threadjoins/21-pool-copy-detach.c	Tests detached aliases.
tests/regression/51-threadjoins/22-pool-preexisting-overwritten.c	Tests overwritten preexisting handles.
tests/regression/51-threadjoins/23-pool-repeated-join.c	Tests duplicate joins.
tests/regression/51-threadjoins/24-pool-multiple-create.c	Tests multiple creation.
tests/regression/51-threadjoins/25-pool-scoped-indices.c	Tests distinct loop indices.
tests/regression/51-threadjoins/26-pool-reverse-join.c	Tests reverse joining.
tests/regression/51-threadjoins/27-pool-struct-index.c	Tests unsupported struct indices.
tests/regression/51-threadjoins/28-pool-indirect-index.c	Tests indirect indices.

Suppressed comments (1)

src/analyses/threadJoinsPool.ml:430

• Unsupported output storage is marked only for the newly spawned ID; the write's overwritten obligations are left canonical. A supported ids[0] obligation followed by pthread_create(&ids[cursor.index], ...) (an unsupported struct-field index which may be zero) leaves the old obligation in ids[0]. Because the value domain may evaluate that slot to both old and new IDs, a later direct join can consume the old obligation even on executions where its handle was overwritten. Poison/invalidate the destination before recording the new ID as lost.

          | `Array (v, _)
          | `Scalar v -> add_unsafe_var v (unsupported ())
          | `OtherRoot _
          | `Indirect -> unsupported ()

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.