On 18 Mar 2020, at 11:59, Demi Obenour <demioben...@gmail.com<mailto:demioben...@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-GWUgAAAAA:eK8fiBxYacpSoQ3NtUJSR8fFoUFz67RpJuYc2-AdOp7IbAzrSyuYVYsxLJwpn1veupeyzJDDIeLxvw 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 _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
