Re: [PATCH] Documentation: fs: fix directory locking proofs

[Al Viro <viro@zeniv.linux.org.uk>]

On Wed, Oct 11, 2023 at 01:28:15PM +0800, Mo Zou wrote:
> Commit 28eceeda130f ("fs: Lock moved directories") acquires locks also for
> directories when they are moved and updates the deadlock-freedom proof
> to claim "a linear ordering of the objects - A < B iff (A is an ancestor
> of B) or (B is an ancestor of A and ptr(A) < ptr(B))". This claim,
> however, is not correct. Because cross-directory rename may acquire two
> parents (old parent and new parent) and two child directories (source
> and target) and the ordering between old parent and target (or new parent
> and source) may not fall into the above cases, i.e. ptr(old parent) <
> ptr(target) may not hold. We should revert to previous description that
> "at any moment we have a partial ordering of the objects - A < B iff A is
> an ancestor of B".

Not quite.  I agree that the proof needs fixing, but your change doesn't
do it.

The thing is, the ordering in "neither is an ancestor of another" case
of lock_two_directories() does, unfortunately, matter.  That's new,
subtle and not adequately discussed.

Another thing is that callers of lock_two_nondirectories() are not
covered at all.

I'll put something together and post it; it's 2:45am here at the moment,
and I'd rather get some sleep first.