[PATCH 0/7] future: Trivial fixups

[PATCH 0/7] future: Trivial fixups

[SeongJae Park]

This patchset contains trivial fixups for future/, which found while
doing Korean translation[1].

[1] https://github.com/sjp38/perfbook-ko_KR

SeongJae Park (7):
  future/tm: Remove unnecessary spaces
  future/tm: Add introduction of TM-availabe options for locking
  future/tm: Consistently add dash between reader and writer of
    reader-writer lock
  future/htm: Remove unnecessary extra 'and'
  future/htm: Use \co{} in favor of $$
  future/formalregress: Use \co{} for spin
  future/formalregress: Use SEL4 consistently

 future/formalregress.tex | 6 +++---
 future/htm.tex           | 4 ++--
 future/tm.tex            | 8 +++++---
 3 files changed, 10 insertions(+), 8 deletions(-)

-- 
2.17.1

[PATCH 1/7] future/tm: Remove unnecessary spaces

[SeongJae Park]

A couple of sentences in future/tm.tex are having two spaces between two
words unnecessarily.  Remove one.

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 future/tm.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/future/tm.tex b/future/tm.tex
index e6985099..1de900b8 100644
--- a/future/tm.tex
+++ b/future/tm.tex
@@ -126,7 +126,7 @@ Here are some options for handling of I/O within transactions:
 	However, special handling is required in cases where multiple
 	record-oriented output streams are merged onto a single file
 	from multiple processes, as might be done using the ``a+''
-	option to \co{fopen()} or the \co{O_APPEND}  flag to \co{open()}.
+	option to \co{fopen()} or the \co{O_APPEND} flag to \co{open()}.
 	In addition, as will be seen in the next section, common
 	networking operations cannot be handled via buffering.
 \item	Prohibit I/O within transactions, so that any attempt to execute
@@ -240,7 +240,7 @@ Here are some options available to TM:
 	back, with consequent degradation of performance and scalability.
 	This approach nevertheless might be valuable given long-running
 	transactions ending with an RPC\@.
-	This approach must still restrict  manual transaction-abort
+	This approach must still restrict manual transaction-abort
 	operations.
 \item	Identify special cases where the RPC response may be moved out
 	of the transaction, and then proceed using techniques similar
-- 
2.17.1

[PATCH 2/7] future/tm: Add introduction of TM-availabe options for locking

[SeongJae Park]

'Locking' section provides TM-available options without any introduction
of it, unlike other sections.  Add it.

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 future/tm.tex | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/future/tm.tex b/future/tm.tex
index 1de900b8..8b8efa98 100644
--- a/future/tm.tex
+++ b/future/tm.tex
@@ -775,6 +775,8 @@ programs containing small amounts of locking, they are often completely
 unacceptable for production-quality lock-based programs wishing to use
 the occasional transaction.
 
+Here are some options available to TM:
+
 \begin{enumerate}
 \item	Use only locking-friendly TM implementations~\cite{DaveDice2006DISC}.
 	Unfortunately, the locking-unfriendly implementations have some
-- 
2.17.1

[PATCH 3/7] future/tm: Consistently add dash between reader and writer of reader-writer lock

[SeongJae Park]

The text is using 'reader-writer lock' consistently, but a sentence in
tm.tex is missing the dash.  Add it.

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 future/tm.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/future/tm.tex b/future/tm.tex
index 8b8efa98..db08bcc6 100644
--- a/future/tm.tex
+++ b/future/tm.tex
@@ -864,7 +864,7 @@ Here are some options available to TM:
 \item	Use TM strictly as an optimization in lock-based systems, as was
 	done by the TxLinux~\cite{ChistopherJRossbach2007a} group,
 	and as has been done by more recent work using TM to elide
-	reader writer locks~\cite{PascalFelber2016rwlockElision}.
+	reader-writer locks~\cite{PascalFelber2016rwlockElision}.
 	This approach seems sound, at least on \Power{8}
 	CPUs~\cite{Le:2015:TMS:3266491.3266500}, but leaves the locking
 	design constraints (such as the need to avoid deadlock) firmly
-- 
2.17.1

[PATCH 4/7] future/htm: Remove unnecessary extra 'and'

[SeongJae Park]

A sentence in future/htm.tex is having 'and' unnecessarily.  Probably
just a typo.  Remove it.

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 future/htm.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/future/htm.tex b/future/htm.tex
index 1404169e..7a5e4ed3 100644
--- a/future/htm.tex
+++ b/future/htm.tex
@@ -582,7 +582,7 @@ semantics of locking, but loses locking's time-based messaging semantics.
 
 	On the other hand, it is possible for a non-empty lock-based
 	critical section to be relying on both the data-protection
-	and time-based and messaging semantics of locking.
+	and time-based messaging semantics of locking.
 	Using transactional lock elision in such a case would be
 	incorrect, and would result in bugs.
 }\QuickQuizEndM
-- 
2.17.1

[PATCH 5/7] future/htm: Use \co{} in favor of $$

[SeongJae Park]

A sentence in htm.tex is using $$ for a code snippet.  Use \co{}
instead.

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 future/htm.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/future/htm.tex b/future/htm.tex
index 7a5e4ed3..fd5a81d1 100644
--- a/future/htm.tex
+++ b/future/htm.tex
@@ -628,7 +628,7 @@ semantics of locking, but loses locking's time-based messaging semantics.
 	When worker threads complete their feed, they must disentangle
 	themselves from the rest of the application and place a status
 	value in a per-thread \co{my_status} variable that is initialized
-	to $-1$.
+	to \co{-1}.
 	Threads do not exit; they instead are placed on a thread pool
 	to accommodate later processing requirements.
 	The control thread assigns (and re-assigns) worker threads as
-- 
2.17.1

[PATCH 6/7] future/formalregress: Use \co{} for spin

[SeongJae Park]

formalregress.tex is using \co{} for spin in most cases.  Use it always
for better consistency.

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 future/formalregress.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/future/formalregress.tex b/future/formalregress.tex
index a50df4ad..b1a39b29 100644
--- a/future/formalregress.tex
+++ b/future/formalregress.tex
@@ -155,7 +155,7 @@ testing, which is in fact the topic of this section.
 It is critically important that formal-verification tools correctly
 model their environment.
 One all-too-common omission is the memory model, where a great
-many formal-verification tools, including Promela/spin, are
+many formal-verification tools, including Promela/\co{spin}, are
 restricted to \IXh{sequential}{consistency}.
 The QRCU experience related in
 \cref{sec:formal:Is QRCU Really Correct?}
@@ -359,7 +359,7 @@ What is needed is a tool that gives at least \emph{some} information
 as to where the bug is located and the nature of that bug.
 
 The \co{cbmc} output includes a traceback mapping back to the source
-code, similar to Promela/spin's, as does Nidhugg.
+code, similar to Promela/\co{spin}'s, as does Nidhugg.
 Of course, these tracebacks can be quite long, and analyzing them
 can be quite tedious.
 However, doing so is usually quite a bit faster
-- 
2.17.1

[PATCH 7/7] 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.  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>
---
 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

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

[Paul E. McKenney]

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!

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

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

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

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

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

[SeongJae Park]

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

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

[Paul E. McKenney]

On Sat, Dec 02, 2023 at 01:32:09PM -0800, SeongJae Park wrote:
> 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!

Fair enough!  ;-)

							Thanx, Paul

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