* [PATCH 0/7] future: Trivial fixups
@ 2023-12-02 17:26 SeongJae Park
2023-12-02 17:26 ` [PATCH 1/7] future/tm: Remove unnecessary spaces SeongJae Park
` (6 more replies)
0 siblings, 7 replies; 11+ messages in thread
From: SeongJae Park @ 2023-12-02 17:26 UTC (permalink / raw)
To: paulmck; +Cc: perfbook, 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
^ permalink raw reply [flat|nested] 11+ messages in thread
* [PATCH 1/7] future/tm: Remove unnecessary spaces
2023-12-02 17:26 [PATCH 0/7] future: Trivial fixups SeongJae Park
@ 2023-12-02 17:26 ` SeongJae Park
2023-12-02 17:26 ` [PATCH 2/7] future/tm: Add introduction of TM-availabe options for locking SeongJae Park
` (5 subsequent siblings)
6 siblings, 0 replies; 11+ messages in thread
From: SeongJae Park @ 2023-12-02 17:26 UTC (permalink / raw)
To: paulmck; +Cc: perfbook, 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
^ permalink raw reply related [flat|nested] 11+ messages in thread
* [PATCH 2/7] future/tm: Add introduction of TM-availabe options for locking
2023-12-02 17:26 [PATCH 0/7] future: Trivial fixups SeongJae Park
2023-12-02 17:26 ` [PATCH 1/7] future/tm: Remove unnecessary spaces SeongJae Park
@ 2023-12-02 17:26 ` SeongJae Park
2023-12-02 17:26 ` [PATCH 3/7] future/tm: Consistently add dash between reader and writer of reader-writer lock SeongJae Park
` (4 subsequent siblings)
6 siblings, 0 replies; 11+ messages in thread
From: SeongJae Park @ 2023-12-02 17:26 UTC (permalink / raw)
To: paulmck; +Cc: perfbook, 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
^ permalink raw reply related [flat|nested] 11+ messages in thread
* [PATCH 3/7] future/tm: Consistently add dash between reader and writer of reader-writer lock
2023-12-02 17:26 [PATCH 0/7] future: Trivial fixups SeongJae Park
2023-12-02 17:26 ` [PATCH 1/7] future/tm: Remove unnecessary spaces SeongJae Park
2023-12-02 17:26 ` [PATCH 2/7] future/tm: Add introduction of TM-availabe options for locking SeongJae Park
@ 2023-12-02 17:26 ` SeongJae Park
2023-12-02 17:26 ` [PATCH 4/7] future/htm: Remove unnecessary extra 'and' SeongJae Park
` (3 subsequent siblings)
6 siblings, 0 replies; 11+ messages in thread
From: SeongJae Park @ 2023-12-02 17:26 UTC (permalink / raw)
To: paulmck; +Cc: perfbook, 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
^ permalink raw reply related [flat|nested] 11+ messages in thread
* [PATCH 4/7] future/htm: Remove unnecessary extra 'and'
2023-12-02 17:26 [PATCH 0/7] future: Trivial fixups SeongJae Park
` (2 preceding siblings ...)
2023-12-02 17:26 ` [PATCH 3/7] future/tm: Consistently add dash between reader and writer of reader-writer lock SeongJae Park
@ 2023-12-02 17:26 ` SeongJae Park
2023-12-02 17:26 ` [PATCH 5/7] future/htm: Use \co{} in favor of $$ SeongJae Park
` (2 subsequent siblings)
6 siblings, 0 replies; 11+ messages in thread
From: SeongJae Park @ 2023-12-02 17:26 UTC (permalink / raw)
To: paulmck; +Cc: perfbook, 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
^ permalink raw reply related [flat|nested] 11+ messages in thread
* [PATCH 5/7] future/htm: Use \co{} in favor of $$
2023-12-02 17:26 [PATCH 0/7] future: Trivial fixups SeongJae Park
` (3 preceding siblings ...)
2023-12-02 17:26 ` [PATCH 4/7] future/htm: Remove unnecessary extra 'and' SeongJae Park
@ 2023-12-02 17:26 ` SeongJae Park
2023-12-02 17:26 ` [PATCH 6/7] future/formalregress: Use \co{} for spin SeongJae Park
2023-12-02 17:26 ` [PATCH 7/7] future/formalregress: Use SEL4 consistently SeongJae Park
6 siblings, 0 replies; 11+ messages in thread
From: SeongJae Park @ 2023-12-02 17:26 UTC (permalink / raw)
To: paulmck; +Cc: perfbook, 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
^ permalink raw reply related [flat|nested] 11+ messages in thread
* [PATCH 6/7] future/formalregress: Use \co{} for spin
2023-12-02 17:26 [PATCH 0/7] future: Trivial fixups SeongJae Park
` (4 preceding siblings ...)
2023-12-02 17:26 ` [PATCH 5/7] future/htm: Use \co{} in favor of $$ SeongJae Park
@ 2023-12-02 17:26 ` SeongJae Park
2023-12-02 17:26 ` [PATCH 7/7] future/formalregress: Use SEL4 consistently SeongJae Park
6 siblings, 0 replies; 11+ messages in thread
From: SeongJae Park @ 2023-12-02 17:26 UTC (permalink / raw)
To: paulmck; +Cc: perfbook, 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
^ permalink raw reply related [flat|nested] 11+ messages in thread
* [PATCH 7/7] future/formalregress: Use SEL4 consistently
2023-12-02 17:26 [PATCH 0/7] future: Trivial fixups SeongJae Park
` (5 preceding siblings ...)
2023-12-02 17:26 ` [PATCH 6/7] future/formalregress: Use \co{} for spin SeongJae Park
@ 2023-12-02 17:26 ` SeongJae Park
2023-12-02 19:29 ` Paul E. McKenney
6 siblings, 1 reply; 11+ messages in thread
From: SeongJae Park @ 2023-12-02 17:26 UTC (permalink / raw)
To: paulmck; +Cc: perfbook, 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
^ permalink raw reply related [flat|nested] 11+ messages in thread
* Re: [PATCH 7/7] future/formalregress: Use SEL4 consistently
2023-12-02 17:26 ` [PATCH 7/7] future/formalregress: Use SEL4 consistently SeongJae Park
@ 2023-12-02 19:29 ` Paul E. McKenney
2023-12-02 21:32 ` SeongJae Park
0 siblings, 1 reply; 11+ messages in thread
From: Paul E. McKenney @ 2023-12-02 19:29 UTC (permalink / raw)
To: SeongJae Park; +Cc: perfbook
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
>
>
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: [PATCH 7/7] future/formalregress: Use SEL4 consistently
2023-12-02 19:29 ` Paul E. McKenney
@ 2023-12-02 21:32 ` SeongJae Park
2023-12-02 23:35 ` Paul E. McKenney
0 siblings, 1 reply; 11+ messages in thread
From: SeongJae Park @ 2023-12-02 21:32 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: SeongJae Park, perfbook
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
> >
> >
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: [PATCH 7/7] future/formalregress: Use SEL4 consistently
2023-12-02 21:32 ` SeongJae Park
@ 2023-12-02 23:35 ` Paul E. McKenney
0 siblings, 0 replies; 11+ messages in thread
From: Paul E. McKenney @ 2023-12-02 23:35 UTC (permalink / raw)
To: SeongJae Park; +Cc: perfbook
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
> > >
> > >
^ permalink raw reply [flat|nested] 11+ messages in thread
end of thread, other threads:[~2023-12-02 23:35 UTC | newest]
Thread overview: 11+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2023-12-02 17:26 [PATCH 0/7] future: Trivial fixups SeongJae Park
2023-12-02 17:26 ` [PATCH 1/7] future/tm: Remove unnecessary spaces SeongJae Park
2023-12-02 17:26 ` [PATCH 2/7] future/tm: Add introduction of TM-availabe options for locking SeongJae Park
2023-12-02 17:26 ` [PATCH 3/7] future/tm: Consistently add dash between reader and writer of reader-writer lock SeongJae Park
2023-12-02 17:26 ` [PATCH 4/7] future/htm: Remove unnecessary extra 'and' SeongJae Park
2023-12-02 17:26 ` [PATCH 5/7] future/htm: Use \co{} in favor of $$ SeongJae Park
2023-12-02 17:26 ` [PATCH 6/7] future/formalregress: Use \co{} for spin SeongJae Park
2023-12-02 17:26 ` [PATCH 7/7] future/formalregress: Use SEL4 consistently SeongJae Park
2023-12-02 19:29 ` Paul E. McKenney
2023-12-02 21:32 ` SeongJae Park
2023-12-02 23:35 ` Paul E. McKenney
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).