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