Add may-ever-have-been-locked digests for relational mutex-meet

[sim642]

This is on top of #1278. Also see the discussion there.

It currently implements the digest splitting using ctx.split, although I'm not entirely convinced that does the right thing.

I added the (fixed) test from more-traces for this, although that already passes without maylocksdigest analysis activated, because the LMust optimization is enough to make it pass, just because it's locally known that they're must-overwritten in main.

[sim642]

This is to still be implemented for the new digests. This is called $\mathsf{acc}$ in the paper, but is never defined there (?).

[michael-schwarz]

acc is defined p.17 and eq (7), but it is specific to one instance, namely this thread id one, where things that are compatible digest-wise may still be ruled out as they are "accounted-for" in the local state (e.g. contributions of threads that have been joined).

If one wants to speak at the level of digests, the appropriate notion is $[[u,act]]^\sharp_\mathcal{A}(A_0,A_1)$ being defined or not.

[sim642]

In the implementation this compatible is the only thing that filters any reads out. Also being called "compatible" probably mislead me to think that's all there is to it. I'll rename it to accounted_for in #1278.

[sim642]

The fact that the refinement should happen due to the lock operation of the digest itself, not accounted_for, somehow gets us back at analyses splitting each other's global unknowns.
Or naively, the relational analysis needs to repeat the exact same lock operations on the digests to see which raise Deadcode as the maylocksdigest analysis is already doing to find the new digests.

I suspect the only reasonable way is to implement digests as a functor around an analysis, just like the paper proposes, to have direct and full control over these things in one place.

[sim642]

I suspect the only reasonable way is to implement digests as a functor around an analysis, just like the paper proposes, to have direct and full control over these things in one place.

Actually even that doesn't seem to work because instead of $m_g$-s we implicitly lock and unlock them in each read_global/write_global. But each of those $\mathsf{lock}(m_g)$ operations has to split if there are multiple globals accessed in a single expression. The issue is that our ctx.split is final: for the split-off branch, no more operations in the transfer function are executed, but the actual variable read and $\mathsf{unlock}(m_g)$ also needs to be executed. Not to mention everything that happens after read_global returns to RelationAnalysis to do other global accesses or whatnot.

Even if these digests were fully embedded into the privatization like TIDs have been so far, the same problem comes up: read_global needs to split into all of these cases and continue executing each one. We'd need CPS or list monad or multi-shot continuations to achieve that, all of which are major fundamental design changes.

So I have no more realistic ideas on how to make these digests work at all. Unless anyone else does, we simply won't be able to implement them (especially in time for CAV).

[michael-schwarz]

We can discuss this at the next GobCon. Maybe shooting for the general solution is overly ambitious, and we could investigate how to incorporate specific digests?

[sim642]

This isn't just a matter of going for the general solution because all of these problems have come up even with the specific simple may-ever-have-been-locked digests. Any other non-ego-lane-derived will inevitably have the very same fundamental problems.

[michael-schwarz]

True, but there might be slight generalizations of ego-lane derived digests that maybe limit what is transmitted at m_g locks, which may still be helpful.

The other thing is if we maybe are able to do some bookkeeping for these m_g locks and then dealy the actual split operation until later... But I'll have to think more deeply about it.

[sim642]

Since this is kind of a dead end for now and not worked on, I'll close this.