Re: [PATCH 7/7] future/formalregress: Use SEL4 consistently

[SeongJae Park <sj38.park@gmail.com>]

On Sat, 2 Dec 2023 11:29:45 -0800 "Paul E. McKenney" <paulmck@kernel.org> wrote:

> On Sat, Dec 02, 2023 at 09:26:14AM -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.  Use SEL4
> > for the consistency.  Note that use of seL4 in swtools.bib is not
> > changed by this commit.
> > 
> > Signed-off-by: SeongJae Park <sj38.park@gmail.com>
> 
> Nice, thank you!

You're very welcome, Paul!

> 
> I queued and pushed all but this one.  Their website [1] says seL4.
> At least I *think* that this is their website.

Agreed :)

> 
> Either way, I agree that this should be consistent with their naming.

Sure, I will send a new revision soon.

> 
> On the Promela/spin change, should a similar change be applied in the
> Formal Verification chapter?

I already finished the translation of the chapter, but hopefully I will revisit
it soon :)  Don't wait for me, though!


Thanks,
SJ

> 
> 							Thanx, Paul
> 
> [1] https://sel4.systems/
> 
> > ---
> >  future/formalregress.tex | 2 +-
> >  1 file changed, 1 insertion(+), 1 deletion(-)
> > 
> > diff --git a/future/formalregress.tex b/future/formalregress.tex
> > index b1a39b29..40bf2b35 100644
> > --- a/future/formalregress.tex
> > +++ b/future/formalregress.tex
> > @@ -701,7 +701,7 @@ so they are all yellow with question marks.
> >  	Indeed there are!
> >  	This table focuses on those that Paul has used, but others are
> >  	proving to be useful.
> > -	Formal verification has been heavily used in the seL4
> > +	Formal verification has been heavily used in the SEL4
> >  	project~\cite{ThomasSewell2013L4binaryVerification},
> >  	and its tools can now handle modest levels of concurrency.
> >  	More recently, Catalin Marinas used Lamport's
> > -- 
> > 2.17.1
> > 
> >