Success messages with topological sorting from deadlock analysis

[sim642]

In the same vein as #1577, when our deadlock analysis proves the program deadlock-free, there's no explanation or proof of the fact. Whereas in the case of possible deadlocks we output a locking cycle.

The proof of the locking graph being non-cyclic would be a topological sorting of its nodes. When requested, we could compute the topological ordering and output it as a group message, just like locking cycles are outputted as group messages (meaning a cycle instead).