[ZweZeya]

Stacked on #2 (fix/lift-lower-crashes).

What this changes

Closes the three soundness defects in docs/audit.md, each of which could make a queue look single-producer or single-consumer when it is not:

• Spawn in a loop counted as one thread. A site now counts as possibly many when it is in a loop or a CFG cycle, or in a function that may itself run more than once.
• main had no thread, so its accesses were dropped. It has one now.
• Parameter index was ignored (argument zero was taken for every parameter). Each instance records its call site and binds parameter i to argument i.

Also two precision fixes: resolution follows every instance on a thread, not just the first; thread contexts are computed to a fixed point instead of recursion over a cache seeded with empty placeholders.

Indirect calls are still not followed, but no longer invisible: a function whose address escapes, or that nothing calls, runs on an "unknown" thread, and every queue it touches is UNKNOWN. A spawn's entry is the first function-address argument, not operand zero (the sret slot on x86-64). Output follows IR order.

How it was checked

23 of 23 pass, no warnings. The eight new or rewritten defect tests fail against the parent, each for the reason it names (worker pool called SPSC; main's push dropped, SPMC instead of MPMC; b's context lost under mutual recursion; second parameter's queue attributed to the first). The prototype's example, compiled for AArch64 and x86-64, gives SPSC for q1 and MPMC for q2 on both.

Checklist

• CI is green
• New behaviour has a test; a fixed bug has a test that failed before
• No file moves or renames mixed in with substantive changes
• The pinned LLVM revision is untouched, or this PR does nothing else

🤖 Generated with Claude Code

[apaznikov]

Closing as superseded by #10. The three soundness defects this closes (a spawn in a loop counted as one thread, main without a thread, the parameter index ignored) are closed there too, by a shared thread-instance walk (ThreadInstanceWalk) that every analysis on that branch now uses: threads are spawn instances under a call string, a spawn that may run more than once stands for many, and parameters bind by index through the call that produced the instance. The fixed-point thread contexts and the "unknown" thread for address-taken code have their counterparts there as well (speculative instances). Keeping two ownership analyses would have meant two answers to the same question.