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 
<[email protected]<mailto:[email protected]>> 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
[email protected]<mailto:[email protected]>
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.
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel

Reply via email to