[CONSAN] Model ConSan mbarrier expect semantics#9958
Conversation
We do so by following the PTX docs and our LLVM lowerings 1. In PTX, a barrier flips when both `arrivals == 0` and `tx-count == 0` 2. In PTX, an expect implies a commit of 1. 3. In triton, we lower `ttng.expect` as an expect on the leader CTA and as a commit of 1 We model all these points in consan.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: fb2364b4f9
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| result = run_in_process(test_async_tma_expect_bytes_mismatch, | ||
| (EXPECT_DELTA, device, False, monkeypatch, num_ctas)) | ||
| assert_expected_cuda_failure(result.exc) | ||
| assert "Deadlock detected" in result.driver_stderr_output |
There was a problem hiding this comment.
Why do we expect deadlock in the case of "under"? We should end up with negative tx-count, right? Should this be flagged as an error rather than causing a deadlock on wait?
There was a problem hiding this comment.
So, this is a bit of a techinicality, but it's correct as-is.
The issue is that expect increments tx-count and complete-tx decrements it. The tx-count is defined to be in the range (-220, 220), and things are well defined there. I agree it's a weird program to first complete and then expect, but it's legal in theory...
There was a problem hiding this comment.
ah, got it! Thanks for the explanation!
We do so by following the PTX docs and our LLVM lowerings 1. In PTX, a barrier flips when both `arrivals == 0` and `tx-count == 0` 2. In PTX, an expect implies a commit of 1. 3. In triton, we lower `ttng.expect` as an expect on the leader CTA and as a commit of 1 We model all these points in consan.
We do so by following the PTX docs and our LLVM lowerings
arrivals == 0andtx-count == 0ttng.expectas an expect on the leader CTA and as a commit of 1We model all these points in consan.