Hey I'm just curious...how do you detect if a memory page mapped by a page table has been written to or accessed?
I imagine if you're writing a filesystem task, such information would help you know when to flush data back to disk or which pages to keep around if things get tight.
I hope this isn't a stupid question.
You (or some other code block) needs to look at how the memory pages are marked in the TLB system. One way is to mark the page read only then on a write handle the exception validate the writer and mark the page writable for that context. Then mark a bit that the page needs to be pushed to disk.
Filesystem code also flows through code that can mark it as dirty and needing to be pushed to media. Since some file writes are well managed with exclusion flags at the open some things get easy.
Assumptions can be made as well on the last close and push any page in memory back to disk.
It is possible for user space file system code to do bookkeeping and tell the OS that pages have been modified. i.e. the content of the file belong to user space. Meta data and the block list for the file belong to the protected code in the kernel.
Without a TLB protection and exception there is no way to "know" and other code must do the book keeping.
Big cautions about multi processor, multi user, access control lists, files with holes (blocks of NULL) and as always meta data including extended meta data. Least I forget filesystem design is difficult.
On Wed, Aug 12, 2015 at 5:36 PM, Raymond Jennings shentino@gmail.com wrote:
Hey I'm just curious...how do you detect if a memory page mapped by a page table has been written to or accessed?
I imagine if you're writing a filesystem task, such information would help you know when to flush data back to disk or which pages to keep around if things get tight.
I hope this isn't a stupid question.
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
On Wed, Aug 12, 2015 at 8:15 PM, Tom Mitchell mitch@niftyegg.com wrote:
You (or some other code block) needs to look at how the memory pages are marked in the TLB system. One way is to mark the page read only then on a write handle the exception validate the writer and mark the page writable for that context. Then mark a bit that the page needs to be pushed to disk.
Filesystem code also flows through code that can mark it as dirty and needing to be pushed to media. Since some file writes are well managed with exclusion flags at the open some things get easy.
Assumptions can be made as well on the last close and push any page in memory back to disk.
It is possible for user space file system code to do bookkeeping and tell the OS that pages have been modified. i.e. the content of the file belong to user space. Meta data and the block list for the file belong to the protected code in the kernel.
Without a TLB protection and exception there is no way to "know" and other code must do the book keeping.
Big cautions about multi processor, multi user, access control lists, files with holes (blocks of NULL) and as always meta data including extended meta data. Least I forget filesystem design is difficult.
On Wed, Aug 12, 2015 at 5:36 PM, Raymond Jennings shentino@gmail.com wrote:
Hey I'm just curious...how do you detect if a memory page mapped by a page table has been written to or accessed?
I imagine if you're writing a filesystem task, such information would help you know when to flush data back to disk or which pages to keep around if things get tight.
I hope this isn't a stupid question.
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
-- T o m M i t c h e l l
So basically there's no way to actually peek at the page table or otherwise ask the microkernel if the page is accessed/dirty?
I was also asking about the accessed bit.
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.
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.
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...
On Wed, Aug 12, 2015 at 8:37 PM, Raymond Jennings shentino@gmail.com wrote:
On Wed, Aug 12, 2015 at 8:15 PM, Tom Mitchell mitch@niftyegg.com wrote:
You (or some other code block) needs to look at how the memory pages are marked in the TLB system. One way is to mark the page read only then on a write handle the exception validate the writer and mark the page writable for that context. Then mark a bit that the page needs to be pushed to disk.
Filesystem code also flows through code that can mark it as dirty and needing to be pushed to media. Since some file writes are well managed with exclusion flags at the open some things get easy.
Assumptions can be made as well on the last close and push any page in memory back to disk.
It is possible for user space file system code to do bookkeeping and tell the OS that pages have been modified. i.e. the content of the file belong to user space. Meta data and the block list for the file belong to the protected code in the kernel.
Without a TLB protection and exception there is no way to "know" and other code must do the book keeping.
Big cautions about multi processor, multi user, access control lists, files with holes (blocks of NULL) and as always meta data including extended meta data. Least I forget filesystem design is difficult.
On Wed, Aug 12, 2015 at 5:36 PM, Raymond Jennings shentino@gmail.com wrote:
Hey I'm just curious...how do you detect if a memory page mapped by a page table has been written to or accessed?
I imagine if you're writing a filesystem task, such information would help you know when to flush data back to disk or which pages to keep around if things get tight.
I hope this isn't a stupid question.
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
-- T o m M i t c h e l l
So basically there's no way to actually peek at the page table or otherwise ask the microkernel if the page is accessed/dirty?
I was also asking about the accessed bit.
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...
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.commailto: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.systemsmailto: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.
On Thu, Aug 13, 2015 at 5:48 AM, Adrian Danis adrian.danis@nicta.com.au wrote:
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.
This is why I was asking if having mapping rights on the page descriptor/page table would be sufficient. If you can change which physical page a virtual address refers to, you could probably also have enough privilege to be trusted with dirty/accessed bit.
Is this the sort of "within the capability model" you are referring to?
So to be specific on the whole accessed/dirty bit topic.
My first intention was to ask how to do it presently, if possible.
When I found out it wasn't...I'd like to make it a suggestion for a future version.
I'm brand new to this list, so is this the proper way to make suggetions?
On Thu, Aug 13, 2015 at 1:47 PM, Raymond Jennings shentino@gmail.com wrote:
On Thu, Aug 13, 2015 at 5:48 AM, Adrian Danis adrian.danis@nicta.com.au wrote:
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.
This is why I was asking if having mapping rights on the page descriptor/page table would be sufficient. If you can change which physical page a virtual address refers to, you could probably also have enough privilege to be trusted with dirty/accessed bit.
Is this the sort of "within the capability model" you are referring to?
The classic paper on dealing with paging without access to reference bits is:
“Converting a swap-based system to do paging in an architecture lacking page-referenced bits” http://dl.acm.org/citation.cfm?id=806595
Note: Basically, hardware dirty/reference bits are really only a performance optimisation.
You still have to implement page-based virtual memory on top of seL4, i.e. something that provides virtual memory and paging to external storage, for whatever your applications are, etc….
Given an implementation of page-based virtual memory (and a replacement algorithm such as “2nd chance clock”), the difference between having access to hardware bits and simulating bits is pretty minor.
We can look into supporting querying the hardware bits, but lack of access to them is not preventing building a specific system due to ease of emulation.
- Kevin
From: Devel [mailto:devel-bounces@sel4.systems] On Behalf Of Raymond Jennings Sent: Friday, 14 August 2015 7:21 AM To: Adrian Danis Adrian.Danis@nicta.com.au Cc: devel@sel4.systems Subject: Re: [seL4] Detecting dirty/accessed page tables
So to be specific on the whole accessed/dirty bit topic.
My first intention was to ask how to do it presently, if possible.
When I found out it wasn't...I'd like to make it a suggestion for a future version.
I'm brand new to this list, so is this the proper way to make suggetions?
On Thu, Aug 13, 2015 at 1:47 PM, Raymond Jennings <shentino@gmail.commailto:shentino@gmail.com> wrote: On Thu, Aug 13, 2015 at 5:48 AM, Adrian Danis <adrian.danis@nicta.com.aumailto:adrian.danis@nicta.com.au> wrote: 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.
This is why I was asking if having mapping rights on the page descriptor/page table would be sufficient. If you can change which physical page a virtual address refers to, you could probably also have enough privilege to be trusted with dirty/accessed bit.
Is this the sort of "within the capability model" you are referring to?
________________________________
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.
So basically you use denied permissions to trap the access, and then emulate the access bits yourself?
On Thu, Aug 13, 2015 at 7:19 PM, Kevin Elphinstone < Kevin.Elphinstone@nicta.com.au> wrote:
The classic paper on dealing with paging without access to reference bits is:
“*Converting a swap-based system to do paging in an architecture lacking page-referenced bits”*
http://dl.acm.org/citation.cfm?id=806595
Note: Basically, hardware dirty/reference bits are really only a performance optimisation.
You still have to implement page-based virtual memory on top of seL4, i.e. something that provides virtual memory and paging to external storage, for whatever your applications are, etc….
Given an implementation of page-based virtual memory (and a replacement algorithm such as “2nd chance clock”), the difference between having access to hardware bits and simulating bits is pretty minor.
We can look into supporting querying the hardware bits, but lack of access to them is not preventing building a specific system due to ease of emulation.
Kevin*From:* Devel [mailto:devel-bounces@sel4.systems] *On Behalf Of *Raymond Jennings *Sent:* Friday, 14 August 2015 7:21 AM *To:* Adrian Danis Adrian.Danis@nicta.com.au *Cc:* devel@sel4.systems *Subject:* Re: [seL4] Detecting dirty/accessed page tables
So to be specific on the whole accessed/dirty bit topic.
My first intention was to ask how to do it presently, if possible.
When I found out it wasn't...I'd like to make it a suggestion for a future version.
I'm brand new to this list, so is this the proper way to make suggetions?
On Thu, Aug 13, 2015 at 1:47 PM, Raymond Jennings shentino@gmail.com wrote:
On Thu, Aug 13, 2015 at 5:48 AM, Adrian Danis adrian.danis@nicta.com.au wrote:
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.
This is why I was asking if having mapping rights on the page descriptor/page table would be sufficient. If you can change which physical page a virtual address refers to, you could probably also have enough privilege to be trusted with dirty/accessed bit.
Is this the sort of "within the capability model" you are referring to?
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.
In short, yes.
- Kevin
From: Raymond Jennings [mailto:shentino@gmail.com] Sent: Friday, 14 August 2015 12:35 PM To: Kevin Elphinstone Kevin.Elphinstone@nicta.com.au Cc: Adrian Danis Adrian.Danis@nicta.com.au; devel@sel4.systems Subject: Re: [seL4] Detecting dirty/accessed page tables
So basically you use denied permissions to trap the access, and then emulate the access bits yourself?
On Thu, Aug 13, 2015 at 7:19 PM, Kevin Elphinstone <Kevin.Elphinstone@nicta.com.aumailto:Kevin.Elphinstone@nicta.com.au> wrote: The classic paper on dealing with paging without access to reference bits is:
“Converting a swap-based system to do paging in an architecture lacking page-referenced bits” http://dl.acm.org/citation.cfm?id=806595
Note: Basically, hardware dirty/reference bits are really only a performance optimisation.
You still have to implement page-based virtual memory on top of seL4, i.e. something that provides virtual memory and paging to external storage, for whatever your applications are, etc….
Given an implementation of page-based virtual memory (and a replacement algorithm such as “2nd chance clock”), the difference between having access to hardware bits and simulating bits is pretty minor.
We can look into supporting querying the hardware bits, but lack of access to them is not preventing building a specific system due to ease of emulation.
- Kevin
From: Devel [mailto:devel-bounces@sel4.systemsmailto:devel-bounces@sel4.systems] On Behalf Of Raymond Jennings Sent: Friday, 14 August 2015 7:21 AM To: Adrian Danis <Adrian.Danis@nicta.com.aumailto:Adrian.Danis@nicta.com.au> Cc: devel@sel4.systemsmailto:devel@sel4.systems Subject: Re: [seL4] Detecting dirty/accessed page tables
So to be specific on the whole accessed/dirty bit topic.
My first intention was to ask how to do it presently, if possible.
When I found out it wasn't...I'd like to make it a suggestion for a future version.
I'm brand new to this list, so is this the proper way to make suggetions?
On Thu, Aug 13, 2015 at 1:47 PM, Raymond Jennings <shentino@gmail.commailto:shentino@gmail.com> wrote: On Thu, Aug 13, 2015 at 5:48 AM, Adrian Danis <adrian.danis@nicta.com.aumailto:adrian.danis@nicta.com.au> wrote: 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.
This is why I was asking if having mapping rights on the page descriptor/page table would be sufficient. If you can change which physical page a virtual address refers to, you could probably also have enough privilege to be trusted with dirty/accessed bit.
Is this the sort of "within the capability model" you are referring to?
________________________________
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.
As Kevin said - yes. One good place to research and look at this is the MIPS processor. The MIPS hardware is minimum the interesting parts are done in software. The exception handler works with a richer table of qualities that it manages. The transition from user space to privileged space in the exception handler sets the stage for all that might be needed.
I/O is difficult, a generation of Intel hardware had MTTR registers and address spaces for I/O coherency. Today PAT (page attribute table) is used. https://en.wikipedia.org/wiki/Page_attribute_table Kernel and user space atomic operations are always in the critical path and are not a given. One last detail... I/O devices can modify memory in ways the CPU set of multiple cores cannot seen in a coherent way unless the cache control bits are correctly set. Physical, I/O and virtual mapped memory can have mismatched control bits.
VM is difficult... it helped me to start with the MIPS model and look at what can be crafted on top of a minimum but sufficient foundation. Linux has support for multiple processors yet the user space sees a common model.
On Thu, Aug 13, 2015 at 7:34 PM, Raymond Jennings shentino@gmail.com wrote:
So basically you use denied permissions to trap the access, and then emulate the access bits yourself?
On Thu, Aug 13, 2015 at 7:19 PM, Kevin Elphinstone < Kevin.Elphinstone@nicta.com.au> wrote:
The classic paper on dealing with paging without access to reference bits is:
“*Converting a swap-based system to do paging in an architecture lacking page-referenced bits”*
http://dl.acm.org/citation.cfm?id=806595
Note: Basically, hardware dirty/reference bits are really only a performance optimisation.
You still have to implement page-based virtual memory on top of seL4, i.e. something that provides virtual memory and paging to external storage, for whatever your applications are, etc….
Given an implementation of page-based virtual memory (and a replacement algorithm such as “2nd chance clock”), the difference between having access to hardware bits and simulating bits is pretty minor.
We can look into supporting querying the hardware bits, but lack of access to them is not preventing building a specific system due to ease of emulation.
Kevin*From:* Devel [mailto:devel-bounces@sel4.systems] *On Behalf Of *Raymond Jennings *Sent:* Friday, 14 August 2015 7:21 AM *To:* Adrian Danis Adrian.Danis@nicta.com.au *Cc:* devel@sel4.systems *Subject:* Re: [seL4] Detecting dirty/accessed page tables
So to be specific on the whole accessed/dirty bit topic.
My first intention was to ask how to do it presently, if possible.
When I found out it wasn't...I'd like to make it a suggestion for a future version.
I'm brand new to this list, so is this the proper way to make suggetions?
On Thu, Aug 13, 2015 at 1:47 PM, Raymond Jennings shentino@gmail.com wrote:
On Thu, Aug 13, 2015 at 5:48 AM, Adrian Danis adrian.danis@nicta.com.au wrote:
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.
This is why I was asking if having mapping rights on the page descriptor/page table would be sufficient. If you can change which physical page a virtual address refers to, you could probably also have enough privilege to be trusted with dirty/accessed bit.
Is this the sort of "within the capability model" you are referring to?
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 Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
I think that allowing the hardware bits to be queried (and probably changed atomically while being read) would be useful.
Would such a feature be added in the future? I have a crazy hunch (but nowhere near the experience to prove it) that avoiding such "canary" style page faults could optimize things.
On Thu, Aug 13, 2015 at 7:19 PM, Kevin Elphinstone < Kevin.Elphinstone@nicta.com.au> wrote:
The classic paper on dealing with paging without access to reference bits is:
“*Converting a swap-based system to do paging in an architecture lacking page-referenced bits”*
http://dl.acm.org/citation.cfm?id=806595
Note: Basically, hardware dirty/reference bits are really only a performance optimisation.
You still have to implement page-based virtual memory on top of seL4, i.e. something that provides virtual memory and paging to external storage, for whatever your applications are, etc….
Given an implementation of page-based virtual memory (and a replacement algorithm such as “2nd chance clock”), the difference between having access to hardware bits and simulating bits is pretty minor.
We can look into supporting querying the hardware bits, but lack of access to them is not preventing building a specific system due to ease of emulation.
Kevin*From:* Devel [mailto:devel-bounces@sel4.systems] *On Behalf Of *Raymond Jennings *Sent:* Friday, 14 August 2015 7:21 AM *To:* Adrian Danis Adrian.Danis@nicta.com.au *Cc:* devel@sel4.systems *Subject:* Re: [seL4] Detecting dirty/accessed page tables
So to be specific on the whole accessed/dirty bit topic.
My first intention was to ask how to do it presently, if possible.
When I found out it wasn't...I'd like to make it a suggestion for a future version.
I'm brand new to this list, so is this the proper way to make suggetions?
On Thu, Aug 13, 2015 at 1:47 PM, Raymond Jennings shentino@gmail.com wrote:
On Thu, Aug 13, 2015 at 5:48 AM, Adrian Danis adrian.danis@nicta.com.au wrote:
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.
This is why I was asking if having mapping rights on the page descriptor/page table would be sufficient. If you can change which physical page a virtual address refers to, you could probably also have enough privilege to be trusted with dirty/accessed bit.
Is this the sort of "within the capability model" you are referring to?
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.
Hi Raymond,
I think that allowing the hardware bits to be queried (and probably changed atomically while being read) would be useful.
Would such a feature be added in the future? I have a crazy hunch (but nowhere near the experience to prove it) that avoiding such "canary" style page faults could optimize things.
As Kevin said: it’s an optimisation that was until recently only available on x86 processors. Because its an optimisation, it adds no functionality, only performance.
We take performance very seriously. In fact, while seL4’s design is driven primarily by security, our philosophy is also that security is no excuse for bad performance.
But, as Kevin also said, we’ve yet to see an important use case that will significantly benefit from this optimisation. There is no reason why we couldn’t support this optimisation, but, until someone convinces us that it’ll make a real difference, we have far more important work to do. A “would be nice” is not sufficient, I’m afraid.
So, if you have an important and convincing use case that depends on this, then let us know. If you can come up with funding for the work, and we’re convinced it really helps, we’ll increase the priority.
Soon (probably later today) I’ll post our development roadmap on announce@sel4.systemsmailto:announce@sel4.systems. You’ll see that we’ve got plenty on our plate, all of which is important functionality that indisputably adds to seL4’s real-world usefulness, and therefore has priority. In fact, if we had more people, we would put them on accelerating the roadmap before we work on nice-to-haves.
Gernot
________________________________
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.
Greatly appreciated.
I'll definitely be taking a look at it.
As far as funding, I'm actually just a hobbyist interested in microkernels and I am not here in any corporate or business capacity.
I suppose someone could always add A/D bit access themselves by submitting a pull request on github?
On Fri, Aug 14, 2015 at 6:56 AM, Gernot Heiser gernot@nicta.com.au wrote:
Hi Raymond,
I think that allowing the hardware bits to be queried (and probably changed atomically while being read) would be useful.
Would such a feature be added in the future? I have a crazy hunch (but nowhere near the experience to prove it) that avoiding such "canary" style page faults could optimize things.
As Kevin said: it’s an optimisation that was until recently only available on x86 processors. Because its an optimisation, it adds no functionality, only performance.
We take performance very seriously. In fact, while seL4’s design is driven primarily by security, our philosophy is also that security is no excuse for bad performance.
But, as Kevin also said, we’ve yet to see an important use case that will significantly benefit from this optimisation. There is no reason why we couldn’t support this optimisation, but, until someone convinces us that it’ll make a real difference, we have far more important work to do. A “would be nice” is not sufficient, I’m afraid.
So, if you have an important and convincing use case that depends on this, then let us know. If you can come up with funding for the work, and we’re convinced it really helps, we’ll increase the priority.
Soon (probably later today) I’ll post our development roadmap on announce@sel4.systems. You’ll see that we’ve got plenty on our plate, all of which is important functionality that indisputably adds to seL4’s real-world usefulness, and therefore has priority. In fact, if we had more people, we would put them on accelerating the roadmap before we work on nice-to-haves.
Gernot
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.
Btw, just wante dto say I really love microkernels. I like how clean they keep things by having packages of code neatly contained and isolated.
Good work, guys.
On Fri, Aug 14, 2015 at 10:50 AM, Raymond Jennings shentino@gmail.com wrote:
Greatly appreciated.
I'll definitely be taking a look at it.
As far as funding, I'm actually just a hobbyist interested in microkernels and I am not here in any corporate or business capacity.
I suppose someone could always add A/D bit access themselves by submitting a pull request on github?
On Fri, Aug 14, 2015 at 6:56 AM, Gernot Heiser gernot@nicta.com.au wrote:
Hi Raymond,
I think that allowing the hardware bits to be queried (and probably changed atomically while being read) would be useful.
Would such a feature be added in the future? I have a crazy hunch (but nowhere near the experience to prove it) that avoiding such "canary" style page faults could optimize things.
As Kevin said: it’s an optimisation that was until recently only available on x86 processors. Because its an optimisation, it adds no functionality, only performance.
We take performance very seriously. In fact, while seL4’s design is driven primarily by security, our philosophy is also that security is no excuse for bad performance.
But, as Kevin also said, we’ve yet to see an important use case that will significantly benefit from this optimisation. There is no reason why we couldn’t support this optimisation, but, until someone convinces us that it’ll make a real difference, we have far more important work to do. A “would be nice” is not sufficient, I’m afraid.
So, if you have an important and convincing use case that depends on this, then let us know. If you can come up with funding for the work, and we’re convinced it really helps, we’ll increase the priority.
Soon (probably later today) I’ll post our development roadmap on announce@sel4.systems. You’ll see that we’ve got plenty on our plate, all of which is important functionality that indisputably adds to seL4’s real-world usefulness, and therefore has priority. In fact, if we had more people, we would put them on accelerating the roadmap before we work on nice-to-haves.
Gernot
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.
On Thu, Aug 13, 2015 at 12:03 AM, Raymond Jennings shentino@gmail.com wrote: ......
Would having a capability for the page directory in question suffice to assure security?
Not sure I can answer this. I am inclined to think that a policy that had this capability would only be secure if the capability was not assigned to anything. For debugging some troubling things are sometimes necessary but production is another world.
-
Adrian Danis -
Gernot Heiser -
Kevin Elphinstone -
Raymond Jennings -
Tom Mitchell