Invalidating mapped flexpages in pagers

Philipp Eppelt philipp.eppelt at
Mon Mar 18 13:38:36 CET 2019

On 3/18/19 11:31 AM, Paul Boddie wrote:
> On Monday 18. March 2019 08.35.56 Philipp Eppelt wrote:
>> AFAIK, you cannot unmap a page during a page fault reply.
> I had looked into this and couldn't see a way of returning items that would 
> provide the necessary information for unmapping previously mapped pages. I 
> imagine that one could specify a flexpage with an appropriate base address and 
> size, but then it isn't clear how its invalidation would be communicated.
> I looked at the kernel code somewhat to see how it processes map items, but it 
> also wasn't clear how such items might be able to cause unmapping.
>> However, your pager can track the pages you mapped and call task->unmap()
>> explicitly.
>> E.g.
>> // assuming pagee_task of type L4::Cap<L4::Task>
>> pagee_task->unmap(
>>   l4_fpage(addr_of_prev_page, L4_PAGESIZE, L4_FPAGE_RWX),
> I guess that the pager needs to know the identity of the task for which it is 
> performing paging. As far as I understand it, this information isn't 
> automatically available via the normal IPC interactions because it would 
> expose the sender to potentially undesirable operations (such as the one being 
> described) purely because it communicated with another task.
> So, I imagine that the task must first provide its identity to the pager 
> before paging begins. Then, any unmapping can take place as necessary.

Actually, there is a unmap flag which allows you to unmap all child
mappings of a memory fpage. So assume you have three address spaces, A,
B, and C, and A maps a page FP to B as FP' and B maps FP' to C as FP".

So if B decides to call unmap on its own mapping FP' with
L4_FP_OTHER_SPACES [0], it will just unmap FP" in C's address space.
If A decides to call `L4Re::Env::env()->task()->unmap(FP,
L4_FP_OTHER_SPACES)` it will unmap FP' in B and FP" in C.

I suppose that's the way for your pager to eliminate the mapping in its

To put it into code:
  l4_fpage(addr_in_this_task, L4_PAGESIZE, L4_FPAGE_RWX),



philipp.eppelt at - Tel. 0351-41 883 221

Kernkonzept GmbH.  Sitz: Dresden.  Amtsgericht Dresden, HRB 31129.
Geschäftsführer: Dr.-Ing. Michael Hohmuth

More information about the l4-hackers mailing list