[PATCH v2] future/formalregress: Use seL4 consistently

[PATCH v2] future/formalregress: Use seL4 consistently

[SeongJae Park]

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>
---
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

Re: [PATCH v2] future/formalregress: Use seL4 consistently

[Paul E. McKenney]

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@gmail.com>

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
>