unmap() guaranteed to succeed?
marcus.brinkmann at ruhr-uni-bochum.de
Mon Dec 11 18:26:02 CET 2006
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
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.
More information about the l4-hackers