Switch to HoareSet for MayLocks

[michael-schwarz]

Opening this issue so we can refer to it later: It may be advantageous to use a HoareSet for MayLocksets instead of our naive set representation for which the operations are quadratic in the size of the sets.

Independently of this, we need to rethink our approach to MayLocks as it pertains to deadlock detection in general.

[sim642]

The deadlock analysis uses a set of may lock events, consisting of:

1. the mutex,
2. the node where it was locked,
3. the MCPAccess data at that point.

In order to have a Hoare set of these events, there needs to be leq (and other lattice operations) defined for the events, but I'm not sure how that could be done because none of the three components are lattices.
The possibility I can imagine right now would be to use near-equivalent flat lattices for each of them, which allows some things to be forcefully joined together to Top, to essentially ignore those components and reduce the set size. For example, two lock events for the same lock with the same access data at different nodes might be joined together such that the node is forgotten. The exact conditions of when this happens must then be specified though, because it wouldn't come automatically (the flat lattices with lifted values are incomparable either way). So something like a should_join phase is needed to force joining of particular events.

Independently of this, we need to rethink our approach to MayLocks as it pertains to deadlock detection in general.

What do you mean by this?

[michael-schwarz]

What do you mean by this?

We'll give an update at GobCon today.

[sim642]

We'll give an update at GobCon today.

While reviewing #839 I wanted to look up what this was all about, but that day's GobCon notes simply say

TODO: document explanation in issue after GobCon for the future

So I still have no clue what or how this intends to achieve.

[michael-schwarz]

Independently of this, we need to rethink our approach to MayLocks as it pertains to deadlock detection in general.

The idea was that we should be able to handle unknown mutexes in a smarter way.

// may lock set empty
lock(*ptr); // ptr -> {a,b,c}
// ptr is not modified
unlock(*ptr);
// may lock set should be empty again
// currently is {a,b,c}

Currently as soon as we have a non-definite lockset, we can never get rid of any of the elements again.

[sim642]

This probably deserves a separate issue because it's not related to this one, right?

To achieve that, I guess we'd need some kind of var_eq analysis, but with equalities in time, e.g. *ptr@lock == *ptr@unlock.
Maybe symb_locks already achieves something of the sort because it also needs to invalidate things at intermediate modifications. Although there's #434.

[michael-schwarz]

Yes, might make sense to pull it out.

[michael-schwarz]

Unassigning myself, as I am not currently planning on working on this.