Currently there is no support in seL4 for taking advantage of hardware support for detecting dirty/accessed pages. If you want this then you must emulate this in software by changing the access writes on pages and handling the resulting page faults.

The reason for not supporting any underlying hardware features for this is the original, and verified, platform that seL4 was written, an armv6, did not have hardware support for tracking this.

Since porting seL4 to x86 and newer ARM architectures that have support for this there has not been any perceived need for this, so it has not been done. There is certainly no reason requesting such information could not be done within the capability model.

Adrian

On Thu 13-Aug-2015 5:03 PM, Raymond Jennings wrote:
I know that in linux, pages aren't necessarily marked dirty/accessed immediately, but rather they are unmapped from page tables, and when the pte's are removed, any accessed/dirty bits from the pte are pasted into the page struct for the page in question.

On Wed, Aug 12, 2015 at 11:30 PM, Tom Mitchell <mitch@niftyegg.com> wrote:
The accessed bit is a file system + OS feature. If it works in ways
you expect life is good.  OS meta data  may live above the microkernel 
and needs to be checked.

Oh I agree that it's a filesystem/OS feature, but afaik, only the microkernel actually knows about it.

Especially if you aren't writing to a file, but have the file mmap'ed as writable, especially in a shared context.

My main curiosity is how to let an OS take advantage of this extra information to optimize page handling.

Asking the microkernel might be possible with an ioctl() to
a driver you craft.  The page table is both in memory and in the 
processor so knowing what to ask from user space is not obvious.
There are security issues with all of these.   Ity is also very dynamic.

I do not think of the page table as one table.   It is a complex
multi layered structure managed by privileged code and extracting
the portions any security model might allow seem a complex risk.

Would having a capability for the page directory in question suffice to assure security?
 
Debugging tools might let you see what you want.  Debugging tools
need their own framework and support.

Do not ignore cache architecture and MTTR and PAT...
 


_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel



The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.