diff options
| author | SeongJae Park <sj38.park@gmail.com> | 2023-12-02 13:33:46 -0800 |
|---|---|---|
| committer | Paul E. McKenney <paulmck@kernel.org> | 2023-12-14 09:58:29 -0800 |
| commit | 23553e431f641abc7b79493f9e5015b8a6b4bad4 (patch) | |
| tree | f20566629c641f4f7c1ab8b4d987aba0c03cd137 | |
| parent | 4e380fbb497669a0c1dbc133581969b6fe0f1e16 (diff) | |
| download | perfbook-23553e431f641abc7b79493f9e5015b8a6b4bad4.tar.gz | |
future/formalregress: Use seL4 consistently
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@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
| -rw-r--r-- | future/formalregress.tex | 12 |
1 files 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 |