18 Mar
2020
18 Mar
'20
12:16 p.m.
On 18 Mar 2020, at 11:59, Demi Obenour <demiobenour@gmail.com<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