unmap() guaranteed to succeed?

[Marcus Voelp]

Hi Marcus,

in short: you are right. Both L4.sec and my solution have this problem. 
Fiasco does not. Details below.

Best regards

    Marcus

Marcus Brinkmann wrote:
> 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.
>   
You are right, there are different implementations in the various 
kernels. To my knowledge none is currently using the algorithm I 
described in my diploma thesis.
> 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.
>   
In my approach the rights have to be removed in preorder (don't remember 
whether this is  already in the thesis). This way B cannot generate 
mapping that still have to be traversed by the unmapping thread and thus 
the restart point remains at B (and not at B'). The mapping node itself 
must not be removed until it is passed in the post-order sweep. What may 
still happen is that while the pre-order sweep is processing node A, a 
concurrent map creates a new mapping B -> B' and then while the unmap 
processes B, a concurrent map creates B' -> B'' and so on. The 
consequence is that unless you restrict the mapping tree size or play 
some nasty tricks with priorities you cannot give an upper bound on the 
duration of unmap.

L4.Sec works has the same problems, however, we use subtree helping 
locks instead of restart point tracking to synchronize concurrent unmaps.

Fiasco implements a different algorithm which does not show the above 
problems. In Fiasco the entire mapping tree corresponding of a page is 
locked via a helping lock that must be taken for both mapping and 
unmapping nodes in this tree. When splitting a superpage, additional 
locks are established for the smaller pages. The unmapping process takes 
and holds the lock corresponding to the root node of its mapping tree 
and all locks of smaller pages. To obtain this lock it may have to take 
temporarily locks corresponding to larger page sizes but these are freed 
once the smaller-page locks are taken. As a consequence, once the lock 
is held, the tree size is fixed and the unmap operation will finish in a 
bounded time. All other threads will first help out this unmap operation 
before they modify the tree. To obtain this lock, in the worst case all 
previously started operations must be helped out. This time is bounded 
as well but can potentially be very large.
> ...
> I have the feeling that this is an obvious threat scenario and thus is
> probably addressed already, but I can't find where.  
So far we mostly ignored this problem as far as the main-stream 
implementations go. One of the reasons I think was that map and unmap 
were not used by real-time tasks so their potentially unbounded 
execution time was not much of a problem. Volkmar's Beleg discusses some 
ideas how to solve this problem.

 From a security perspective this may really be a problem. Do you know 
how other systems solve it? Like Eros e.g., implements immediate 
revocation by destruction of the intermediate objects. However, 
internally they also have a list  in which address spaces a capability 
is mapped.

Best regards

    Marcus

-- 
Marcus Völp

Technische Universität Dresden
Department of Computer Science
Institute for System Architecture 

Tel: +49 (351) 463 38350
Fax: +49 (351) 463 38284

Email: voelp at os.inf.tu-dresden.de
Web: http://os.inf.tu-dresden.de/~voelp