formalregress.tex is using mixed use of SEL4 and seL4. SEL4 is used 8 times, while seL4 is used twice over the entire repository. That said, seL4 seems the intended name since their website[1] uses the name. Use seL4 consistently. [1] https://sel4.systems/ Signed-off-by: SeongJae Park <sj38.park@xxxxxxxxx> --- Changes from v1 - Use seL4 instead of SEL4 future/formalregress.tex | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/future/formalregress.tex b/future/formalregress.tex index b1a39b29..63c9021f 100644 --- a/future/formalregress.tex +++ b/future/formalregress.tex @@ -118,23 +118,23 @@ that the compiler is correct. An alternative approach is to take the binary produced by the C compiler as input, thereby accounting for any relevant compiler bugs. This approach has been used in a number of verification efforts, -perhaps most notably by the SEL4 +perhaps most notably by the seL4 project~\cite{ThomasSewell2013L4binaryVerification}. \QuickQuiz{ Given the groundbreaking nature of the various verifiers used - in the SEL4 project, why doesn't this chapter cover them in + in the seL4 project, why doesn't this chapter cover them in more depth? }\QuickQuizAnswer{ - There can be no doubt that the verifiers used by the SEL4 + There can be no doubt that the verifiers used by the seL4 project are quite capable. - However, SEL4 started as a single-CPU project. - And although SEL4 has gained multi-processor + However, seL4 started as a single-CPU project. + And although seL4 has gained multi-processor capabilities, it is currently using very coarse-grained locking that is similar to the Linux kernel's old Big Kernel Lock (BKL)\@. There will hopefully come a day when it makes sense to add - SEL4's verifiers to a book on parallel programming, but + seL4's verifiers to a book on parallel programming, but this is not yet that day. }\QuickQuizEnd -- 2.17.1
