On Tue, Jun 10, 2025 at 09:21:34AM +0100, Al Viro wrote: > The variant currently in the tree has problems; trying to prove > correctness has caught at least one class of bugs (reparenting > that ends up moving the visible location of reparented mount, due > to not excluding some of the counterparts on propagation that > should've been included). > > I tried to prove that it's the only bug there; I'm still not sure > whether it is. If anyone can reconstruct and write down an analysis > of the mainline implementation, I'll gladly review it; as it is, > I ended up doing a different implementation. Candidate collection > phase is similar, but trimming the set down until it satisfies the > constraints turned out pretty different. > > I hoped to do transformation as a massage series, but that turns out > to be too convoluted. So it's a single patch replacing propagate_umount() > and friends in one go, with notes and analysis in D/f/propagate_umount.txt > (in addition to inline comments). > > As far I can tell, it is provably correct and provably linear by the number > of mounts we need to look at in order to decide what should be unmounted. > It even builds and seems to survive testing... > > Another nice thing that fell out of that is that ->mnt_umounting is no longer > needed. > > Compared to the first version: > * explicit MNT_UMOUNT_CANDIDATE flag for is_candidate() > * trim_ancestors() only clears that flag, leaving the suckers on list > * trim_one() and handle_locked() take the stuff with flag cleared off > the list. That allows to iterate with list_for_each_entry_safe() when calling > trim_one() - it removes at most one element from the list now. > * no globals - I didn't bother with any kind of context, not worth it. > > * Notes updated accordingly; I have not touch the terms yet. > > Signed-off-by: Al Viro <viro@xxxxxxxxxxxxxxxxxx> > --- Reviewed-by: Christian Brauner <brauner@xxxxxxxxxx>