Reimplement deadlock analysis and extend with MHP

[sim642]

The refactoring of deadlock analysis for #650 turned into an almost complete rewrite. Extending with common lockset and MHP information was very straightforward.

Changes

1. Use split global constraint unknowns for recording locking orders instead of a global OCaml variable.
2. Replace transitive locking order shortcutting on addition with a locking order graph search (DFS) at the end. This is more flexible and wastes less memory by not actually storing all the edges of the transitive closure.
3. Replace Cil.location with Node for locking events. This makes it incrementally more stable.
4. Improve readability of deadlock warnings by outputting the entire locking order cycle in a grouped message. Previously the transitive shortcutting made cycles longer than 2 difficult to interpret, because intermediate mutexes and locations were omitted.
5. Add Deadlock message category.
6. Exclude deadlocks by access information, which is independent of memory location (common lockset, MHP).

This is directly on master, but I will take care of the merge into #391 when this lands. I already know that will require a few changes to adapt this to #634, which is only on interactive).

Example

Here's how ./regtest.sh 15 03 outputs the three-mutex locking cycle:

[Warning][Deadlock] Locking order cycle:
  lock before: mutex2 with [mhp:{tid=[main, t2@tests/regression/15-deadlock/03-triple_deadlock.c:42:5-42:40]}, thread:[main, t2@tests/regression/15-deadlock/03-triple_deadlock.c:42:5-42:40]] (tests/regression/15-deadlock/03-triple_deadlock.c:20:3-20:30)
  lock after: mutex3 with [mhp:{tid=[main, t2@tests/regression/15-deadlock/03-triple_deadlock.c:42:5-42:40]}, lock:{mutex2}, thread:[main, t2@tests/regression/15-deadlock/03-triple_deadlock.c:42:5-42:40]] (tests/regression/15-deadlock/03-triple_deadlock.c:21:3-21:30)
  lock before: mutex3 with mhp:{tid=[main], {t3@tests/regression/15-deadlock/03-triple_deadlock.c:43:5-43:40}} (tests/regression/15-deadlock/03-triple_deadlock.c:29:3-29:30)
  lock after: mutex1 with [mhp:{tid=[main], {t3@tests/regression/15-deadlock/03-triple_deadlock.c:43:5-43:40}}, lock:{mutex3}] (tests/regression/15-deadlock/03-triple_deadlock.c:30:3-30:30)
  lock before: mutex1 with mhp:{tid=[main], {t1@tests/regression/15-deadlock/03-triple_deadlock.c:41:5-41:40}} (tests/regression/15-deadlock/03-triple_deadlock.c:11:3-11:30)
  lock after: mutex2 with [mhp:{tid=[main], {t1@tests/regression/15-deadlock/03-triple_deadlock.c:41:5-41:40}}, lock:{mutex1}] (tests/regression/15-deadlock/03-triple_deadlock.c:12:3-12:30)

[michael-schwarz]

Also, I think we now get to the point, where we can probably not just ignore double locking anymore. While it may be undefinied behavior in pthreads, I think double locking a mutex that is not configured to support it, also constitutes a deadlock in some philosophical sense, right?

[sim642]

Also, I think we now get to the point, where we can probably not just ignore double locking anymore. While it may be undefinied behavior in pthreads, I think double locking a mutex that is not configured to support it, also constitutes a deadlock in some philosophical sense, right?

That's a good point indeed, especially since recursive mutexes don't self-deadlock (although for the new privatizations we assume they do AFAIK). That should probably be addressed separately too, to have tracking of mutex types and then we could relatively easily simply even warn about that default undefined behavior. This is related to #176.

[michael-schwarz]

although for the new privatizations we assume they do AFAIK

No, iirc we simply assume all mutexes are recursive in the implementation, and in the paper we don't deal with them at all.

[sim642]

Turns out our framework is so great that adding common lockset and MHP information to locking events to exclude some deadlocks was very straightforward, so I added that into this PR. With our existing mutex, mhp and threadJoins analyses, we can deal with the example from here: https://arxiv.org/abs/1607.06927 (also added as regression test).

[michael-schwarz]

I am still adding some examples and checking some smaller things. When I'm done with that (hopefully later today), I'd be cool with merging it and then fixing the issues with Must vs May locks in #662 as you suggested.

[michael-schwarz]

I think the most problematic issue we still have here is threads that end while holding locks. Any future attempt to acquire that lock may result in a deadlock. (Not sure if this is a deadlock according to some definitions that require each thread to be waiting on a resource, but I still think this something we should attempt to catch, maybe we could do it an a separate PR though).

---

Also, I wasted a lot of time trying to come up with an example where one has a deadlock despite not all locking operations pairwise may-happen-in parallel, which turns out was a waste of time.
In the process, I found a (maybe questionable) enhancement of MHP: P1 and P2 may not happen in parallel, if some thread is must-joined at P1 but definitely not created at P2. I now added it and an example for it to this PR, but we can of course also move that to somewhere else.

[michael-schwarz]

I think you already fixed this in ppx_deriving_hash by now, right?

[sim642]

Indeed, but I didn't yet make a new release just for that nor add an opam pin to Goblint to annoy everyone. There's no downside to having a separate named record type here, so I'd just leave it as is for now and change in sometime in the future.

[michael-schwarz]

I think how easy it was to enhance this with MHP information is a good sign we went for the right design here, and as always, I'm impressed with the speed with which you implemented this Simmo!

[michael-schwarz]

Not sure if we want to solve the issue with threads ending while holding mutexes here or make a new issue and PR for it?

[sim642]

Not sure if we want to solve the issue with threads ending while holding mutexes here or make a new issue and PR for it?

I think we should SKIP it here and have a separate issue, because that's a somewhat different form of a deadlock. It's not just about locking order any more.

[sim642]

In the process, I found a (maybe questionable) enhancement of MHP: P1 and P2 may not happen in parallel, if some thread is must-joined at P1 but definitely not created at P2. I now added it and an example for it to this PR, but we can of course also move that to somewhere else.

This is the reason why 15-deadlock-mhp2 doesn't have a deadlock, right? It had no annotations, so I added them, hopefully correctly.

[michael-schwarz]

This is the reason why 15-deadlock-mhp2 doesn't have a deadlock, right?

Yes!