We should aim to support recursive mutexes more thoroughly: We could e.g. maintain an interval expressing how many times a recursive mutex is locked, or alternatively just maintain if it locked once or multiple times.
This part remains open.
Such an analysis that knows if a mutex is recursive or not would also allow us to warn in case of double-locking of non-recursive mutexes. This part was done as part of #839.