On Sat, Dec 02, 2023 at 01:33:46PM -0800, SeongJae Park wrote: > 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> Queued, and thank you very much! Thanx, Paul > --- > 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 >
