Revamp Deadlock-Detection to work incrementally and consider MHP information

[michael-schwarz]

Another issue that we discussed at Gobcon some weeks ago, adding it here so we don't lose track.

Things that would need to be done:

• Incrementalize the collection of lock-order constraints (the approach from Incremental TD3: optimize write-only unknown restarting #634 by @sim642 should work here)
• Replace Cil.location with Node.t
• Maybe: Incrementalize the building of the locking graph (?)
• Make use of MHP information to exclude some cycles. (Naively, this would require collecting lock/unlock pairs for mutexes to exclude cycles where the cycle in the locking order is excluded by MHP information, e.g.
  • T1 locks a and then b,
  • T2 locks b and then a
  • But T2 is not started yet when T1 does the locking)

This would then be a second class of concurrency bug that we can find with Goblint.

[sim642]

A very quick Google search yielded this article: https://arxiv.org/abs/1607.06927. They point out of the lack of sound static analysis tools for deadlock analysis, so it might be good to have a maintained deadlock analysis indeed. Also they claim to have evaluated theirs on an extensive set of pthread programs, which would be of great interest to our benchmarking. Moreover, they have something called "non-concurrency analysis" which sounds a lot like our MHP, so another thing to look at there.

[sim642]

• Maybe: Incrementalize the building of the locking graph (?)

I'm not sure what you mean by this. In #655 the locking order graph is implicitly constructed at the end, based on the information in the global invariant. This is the same as how we construct the race graph.
Both are constructed from scratch each time, based on the incremental global invariant. I'm not sure there is any other way, because somehow storing more of the graph in another derived global invariant would also require somehow subtracting/restarting parts of it, which makes it more involved than just set removal. Also since the locking order graph involves transitivity, removing one edge might require the removal of many derived edges, which isn't really possible without having the non-transitive graph around.

• Make use of MHP information to exclude some cycles. (Naively, this would require collecting lock/unlock pairs for mutexes to exclude cycles where the cycle in the locking order is excluded by MHP information [...])

I'm thinking we should somehow be able to reuse most of our existing access implementations for may_race. Most of them (like MHP, but also mutex (must-lockset)) are just about concurrency and independent of the variable being accessed. Just like we record MCPAccess.A for each access, we could record it for each locking event. Then later when traversing the graph, the same information can be checked pairwise like may_race.

The question is how to nicely allow the access implementations to work for both, while having variable information for actual accesses, but just program point concurrency information for locking events. In particular, to have the two without having to duplicate the access functions, MCPAccess.A and another module in each Spec.

Would be helpful if you could suggest an example program, where MHP information should exclude a deadlock, so it'd be easier to experiment with. (EDIT: Nevermind, the paper I linked above has one for common mutexes and one for create-join).

[michael-schwarz]

In #655 the locking order graph is implicitly constructed at the end, based on the information in the global invariant. This is the same as how we construct the race graph.

I was thinking along the lines of maybe re-using (unchanged) SCCs or something, but unless this actually becomes a bottleneck, I agree it is probably not worth thinking about it too much.

Would be helpful if you could suggest an example program, where MHP information should exclude a deadlock, so it'd be easier to experiment with.

I thought up some examples on the way to work, so if they would still be helpful, let me know!

[sim642]

I thought up some examples on the way to work, so if they would still be helpful, let me know!

I added MHP support directly to #655, so feel free to just add your examples to that PR. That should already be able to handle them.