Invalidating mapped flexpages in pagers

[Paul Boddie]

Hello,

I have been trying to implement a pager in L4Re where the pager employs a 
memory region of limited size to satisfy map requests for a dataspace 
occupying a larger virtual memory region. Upon receiving a map request, the 
pager identifies the dimensions of the flexpage to be sent to the task 
experiencing the page fault, and it populates the flexpage's memory with the 
appropriate data.

What this accomplishes so far is that when page faults occur in a task 
accessing the dataspace, mappings from virtual memory addresses are 
established in the task referring to the memory region populated by the pager. 
The task can read from page to page and keep getting new data.

However, as each new map request comes in, I want to be able to invalidate the 
mappings previously made by the pager. Otherwise, I get many pages in the 
task's address space referring to the same memory, which is obviously not what 
I intend.

Is it possible to send a flexpage from the pager in such a way that the 
mappings previously established by Fiasco.OC for the memory region are 
invalidated? Or have I missed some other mechanism for achieving what I am 
attempting? The L4Re documentation isn't helping me so much here, and I can't 
seem to find examples of this kind of thing in the source distribution.

Thanks for any help anyone can give!

Paul