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

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 <[email protected]>

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
>