Screen concurrent C for race candidates

[jserv]

Adds analyze_concurrency, a Level-0 screen over the loaded project's C sources that reports concurrent events, lexical lock order, and pairs of conflicting accesses it cannot order. Everything it claims is syntax, so it reports candidates and never verdicts: there is deliberately no status meaning "not a race", because the strongest thing a lexical lockset supports is that two accesses name one lock, which is evidence rather than protection. The series also carries the supporting changes that came out of building it, each revertible on its own: the verdict predicates move out of analysis.rs (6,181 lines to 5,660), the stdio suite's thread count is pinned where it actually runs, dead_code is denied rather than warned, and a Frama-C that dies mid-session now reports its pid, liveness and log tails instead of only "connection closed".

Verified with scripts/run-gates.sh at the tip: 18 of 18 gates, RUNNER_EXIT=0, including 648 unit tests, 157 stdio tests at the pinned four threads, and the tutorial corpus at 28/28 under -wp-cache none, so those proofs are computed rather than replayed. Every commit builds under cargo check --all-targets, checked by checking each one out, so the series bisects. Three of the fixes were mutation-tested rather than trusted: reverting the trylock handling, the lockset intersection on block exit, and reading threads_detected off spawn tokens each makes its own regression fail, and the file was restored byte-identical afterwards.

Deliberately left out. docs/design/concurrency-ast/ specifies re-founding this tool on the Frama-C AST, which answers by construction what the scanner answers by heuristic, but that is a design only and none of it is implemented here. Two measured cleanups are also deferred to it: interning the strings an Event repeats, and memoizing thread attribution per function. One maintenance hazard is recorded and not fixed: the "a transport went" predicate is spelled twice in server.rs, once negated.

---

Summary by cubic

Adds analyze_concurrency, a Level-0 screen over the loaded project's C sources that reports concurrent events, lexical lock order, and pairs of conflicting accesses it cannot order. Everything it claims is syntax, so it reports candidates and never verdicts: there is deliberately no status meaning "not a race", because the strongest thing a lexical lockset supports is that two accesses name one lock, which is evidence rather than protection.

Screening behavior

• Comments and literals are blanked with columns kept, so actions on a line order by position; accesses are per token occurrence, and braces are positioned actions in the same stream, so } else { falls out rather than being special-cased.
• Leaving a block intersects locksets rather than restoring the enclosing one, so a lock released inside a block stays released; thread attribution walks a call graph from each entry.
• Whether the program is concurrent is read off pthread_create tokens rather than resolved entries, since a wrapped argument list resolves to nothing.
• The scan checks its own deadline in both the emission and pairing phase; an early stop is reported and every count it emits is a floor.
• Three shapes previously screened raceless now name their regression: a call inside an initializer, a loop body beside its head, and a non-regular input file that consumed the whole budget while reading.

Supporting changes

• Verdict predicates move out of analysis.rs into verdicts.rs; the stdio suite's thread count is pinned to four, with a guard that the workflow and runner agree; dead_code is denied rather than warned.
• A Frama-C that dies mid-session now reports its pid, liveness, and log tails instead of only "connection closed", and a reload that moved its sources no longer announces a lost process.
• The concurrency limits' defaults and clamps are documented, and the stdio pin guard reads across wrapped commands.

Verified at the tip: 18 of 18 gates pass, including 648 unit tests, 157 stdio tests, and the tutorial corpus at 28/28 under -wp-cache none, so those proofs are computed rather than replayed.

^{Written for commit c585f53. Summary will update on new commits.}