unmap() guaranteed to succeed?

[Marcus Brinkmann]

Hi,

I try to understand if (and if yes, why) unmap() in L4 architecture
implementations is guaranteed to succeed.  I hesitate to say I
understood the description in Marcus Völp, Design and Implementation
of the Recursive Virtual Address Space Model for Small Scale
Multiprocessor Systems, but at least I skimmed through it and have
developed sort of a mental picture of the post-order node processing.
Bernhard Kauer in L4.sec Implementation also refers to this work.

I understand there are substantial variations of L4 implementations,
and I don't have a complete picture of which one uses which algorithm.

In any case, I am worried about the following scenario, and wonder if
you can share with me your insight on the question if this is a valid
concern or not:

Let's say there is a mapping of the same page from A to B and from A
to C.  Now, unmap() proceeds in post-order, and deletes the mapping
from A to C.  Then it is preempted, and a restart point at B is noted.
Next B maps the page to B', which updates the restart point to be at
B'.  Now, unmap() proceeds by deleting the mapping from B to B'.
Again, the unmap operation is preempted, with the restart point being
B.  The cycle continues.

There are variations of this, where B' creates a mapping to B'', which
creates a mapping to B''' etc, n times in total, and unmap() undos the
last k such mappings before it is preempted.  As long as n >= k, the
B's can create new mappings as fast or faster as unmap can delete
them, so there doesn't seem to be a way for unmap() to succeed
eventually.

I have the feeling that this is an obvious threat scenario and thus is
probably addressed already, but I can't find where.  I might be
missing something obvious.

Thanks,
Marcus