On 18 Mar 2020, at 11:59, Demi Obenour mailto:demiobenour@gmail.com> wrote:
Also, why is verifying fine-grained locking so difficult? CertiKOS managed
to do it, so I am probably missing something.
CertiKOS is a toy system, with almost no useful functionality, see https://dl.acm.org/doi/pdf/10.1145/3341301.3359641?casa_token=UXRlNw-GWUgAAA...
It’s about an order-of-magnitude slower than seL4 to start with. On top, their multicore version imposes further requirements that wold be unacceptable for seL4, such as any data access (incl R/O) must be locked.
We have no plans of destroying seL4’s image by verifying a slow kernel.
Gernot
