linux-kernel.vger.kernel.org archive mirror
 help / color / mirror / Atom feed
From: "Paul E. McKenney" <paulmck@kernel.org>
To: Jonas Oberhauser <jonas.oberhauser@huawei.com>
Cc: Alan Stern <stern@rowland.harvard.edu>,
	Peter Zijlstra <peterz@infradead.org>,
	"parri.andrea" <parri.andrea@gmail.com>, will <will@kernel.org>,
	"boqun.feng" <boqun.feng@gmail.com>, npiggin <npiggin@gmail.com>,
	dhowells <dhowells@redhat.com>, "j.alglave" <j.alglave@ucl.ac.uk>,
	"luc.maranget" <luc.maranget@inria.fr>, akiyks <akiyks@gmail.com>,
	dlustig <dlustig@nvidia.com>, joel <joel@joelfernandes.org>,
	urezki <urezki@gmail.com>,
	quic_neeraju <quic_neeraju@quicinc.com>,
	frederic <frederic@kernel.org>,
	Kernel development list <linux-kernel@vger.kernel.org>
Subject: Re: Internal vs. external barriers (was: Re: Interesting LKMM litmus test)
Date: Thu, 12 Jan 2023 13:57:16 -0800	[thread overview]
Message-ID: <20230112215716.GS4028633@paulmck-ThinkPad-P17-Gen-1> (raw)
In-Reply-To: <07579baee4b84532a76ea8b0b33052bb@huawei.com>

On Wed, Jan 11, 2023 at 05:24:07PM +0000, Jonas Oberhauser wrote:
> 
> 
> -----Original Message-----
> From: Alan Stern [mailto:stern@rowland.harvard.edu] 
> > What is there to try?  As far as I know, the only construct in the cat language that can be used to get the effect of counting is a recursive definition.
> > Such a lemma would have to be based on the other constructs available in the language.  The only things I can think of which even come close are the * and + operators, and they are insufficient (because they are no stronger than regular expressions, which are well known to be too weak
> -- there isn't even a regular expression for strings in which the parentheses are balanced).
> 
> Well, like I said, I don't yet understand rcu-order well enough to have any opinions :D
> You could say that the time period between me asking if you've tried other stuff and thinking that there's probably some impossibility result making that a waste of time were the one minute I used to read the comment above rcu-order and look at the recursion a little :-P, that was barely enough to understand that you're counting stuff which like you say is probably not possible with the other operators.
> 
> Anyways I'll need to take some time to read the definition carefully.

Apologies for the delay, gmail spam-foldered your email again.  :-/

I will risk sharing the intuition behind the rcu-order counting rule.

In the code, an RCU read-side critical section begins with rcu_read_lock()
and ends with the matching rcu_read_unlock().  RCU read-side critical
section may be nested, in which case RCU cares only about the outermost
of the nested set.

An RCU grace period includes at least one moment in time during which
each and every process/CPU/task/whatever is not within an RCU read-side
critical section.  Any period of time spanning a grace period is itself
a grace period.  And synchronize_rcu() waits for a grace period.

Taking the above two paragraphs together, it is forbidden for any RCU
read-side critical section to start before the beginning of a given
grace period and end after the end of that same grace period.

There is no ordering within or between RCU read-side critical sections
other than their separate relationships to any concurrent grace periods
and due to any operations within or between them that may have ordering
effects.  For example, if you have a series of three non-overlapping RCU
read-side critical sections executed by a given process in the absence of
any grace periods (for example, in the absence of any synchronize_rcu()
invocations), and where all other operations executed by that process
are READ_ONCE() and WRITE_ONCE(), without dependencies of any sort,
those memory-reference operations can be executed in any order.

So if a given RCU read-side critical section's first operation follows a
given grace period on some other process, then all of its other operations
might have been executed just after the start of that same grace period.
The start of the grace period must be epsilon before the (reordered)
end of that RCU read-side critical section.

Suppose that one of that critical section's memory references started
just before a memory reference of some other critical section on some
other process.  Then other references in this second critical section
could be reordered to precede the beginning of the grace period.

If you work the other possible examples, you will find that as long as
there are at least as many grace periods as critical sections in a given
candidate cycle, there will be sufficient ordering to prohibit that cycle.

For diagrams, please see Figures 15.14-15.16 here:

https://kernel.org/pub/linux/kernel/people/paulmck/perfbook/perfbook.2022.09.25a.pdf

On the off-chance that this helps...

							Thanx, Paul

  parent reply	other threads:[~2023-01-12 22:08 UTC|newest]

Thread overview: 161+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
     [not found] <20220921173109.GA1214281@paulmck-ThinkPad-P17-Gen-1>
     [not found] ` <YytfFiMT2Xsdwowf@rowland.harvard.edu>
     [not found]   ` <YywXuzZ/922LHfjI@hirez.programming.kicks-ass.net>
     [not found]     ` <114ECED5-FED1-4361-94F7-8D9BC02449B7>
     [not found]       ` <YzSAnclenTz7KQyt@rowland.harvard.edu>
     [not found]         ` <f763bd5ff835458d8750b61da47fe316@huawei.com>
2023-01-03 18:56           ` Internal vs. external barriers (was: Re: Interesting LKMM litmus test) Alan Stern
2023-01-04 15:37             ` Andrea Parri
2023-01-04 20:58               ` Alan Stern
     [not found]             ` <ee186bc17a5e48298a5373f688496dce@huawei.com>
2023-01-05 17:32               ` Paul E. McKenney
     [not found]                 ` <bea712c82e6346f8973399a5711ff78a@huawei.com>
2023-01-11 15:06                   ` Alan Stern
     [not found]                     ` <768ffe7edc7f4ddfacd5b0a8e844ed84@huawei.com>
2023-01-11 17:01                       ` Alan Stern
     [not found]                         ` <07579baee4b84532a76ea8b0b33052bb@huawei.com>
2023-01-12 21:57                           ` Paul E. McKenney [this message]
2023-01-13 16:38                             ` Alan Stern
2023-01-13 19:54                               ` Paul E. McKenney
     [not found]                               ` <06a8aef7eb8d46bca34521a80880dae3@huawei.com>
2023-01-14 17:42                                 ` Paul E. McKenney
     [not found]                             ` <e51c82a113484b6bb62354a49376f248@huawei.com>
2023-01-14 16:42                               ` Alan Stern
2023-01-17 17:48                                 ` Jonas Oberhauser
2023-01-17 21:19                                   ` Alan Stern
2023-01-18 11:25                                     ` Jonas Oberhauser
2023-01-19  2:28                                       ` Alan Stern
2023-01-19 11:22                                         ` Jonas Oberhauser
2023-01-19 16:41                                           ` Alan Stern
2023-01-19 18:43                                             ` Paul E. McKenney
2023-01-23 16:16                                             ` Jonas Oberhauser
2023-01-23 19:58                                               ` Alan Stern
2023-01-23 20:06                                                 ` Jonas Oberhauser
2023-01-23 20:41                                                   ` Alan Stern
2023-01-24 13:21                                                     ` Jonas Oberhauser
2023-01-24 15:54                                             ` Jonas Oberhauser
2023-01-24 17:22                                               ` Alan Stern
     [not found]                     ` <4c1abc7733794519ad7c5153ae8b58f9@huawei.com>
2023-01-13 16:28                       ` Alan Stern
2023-01-13 20:07                         ` Paul E. McKenney
2023-01-13 20:32                           ` Paul E. McKenney
2023-01-14 17:40                             ` Alan Stern
2023-01-14 17:48                               ` Paul E. McKenney
     [not found]                             ` <136d019d8c8049f6b737627df830e66f@huawei.com>
2023-01-14 17:53                               ` Paul E. McKenney
2023-01-14 18:15                                 ` Paul E. McKenney
2023-01-14 19:58                                   ` Alan Stern
2023-01-15  5:19                                     ` Paul E. McKenney
2023-01-14 20:19                                   ` Alan Stern
2023-01-15  5:15                                     ` Paul E. McKenney
2023-01-15 16:23                                       ` Alan Stern
2023-01-15 18:10                                         ` Paul E. McKenney
2023-01-15 20:46                                           ` Alan Stern
2023-01-16  4:23                                             ` Paul E. McKenney
2023-01-16 18:11                                               ` Alan Stern
2023-01-16 19:06                                                 ` Paul E. McKenney
2023-01-16 19:20                                                   ` Alan Stern
2023-01-16 22:13                                                     ` Paul E. McKenney
2023-01-17 11:46                                                       ` Andrea Parri
2023-01-17 15:14                                                         ` Paul E. McKenney
2023-01-17 15:56                                                           ` Alan Stern
2023-01-17 17:43                                                             ` Paul E. McKenney
2023-01-17 18:27                                                               ` Jonas Oberhauser
2023-01-17 18:55                                                                 ` Paul E. McKenney
2023-01-17 20:20                                                                   ` Jonas Oberhauser
2023-01-17 20:15                                                               ` Alan Stern
2023-01-18  3:50                                                                 ` Paul E. McKenney
2023-01-18 16:50                                                                   ` Alan Stern
2023-01-18 19:42                                                                     ` Jonas Oberhauser
2023-01-18 20:19                                                                       ` Paul E. McKenney
2023-01-18 20:30                                                                         ` Jonas Oberhauser
2023-01-18 21:12                                                                           ` Paul E. McKenney
2023-01-18 21:24                                                                             ` Jonas Oberhauser
2023-01-19  0:11                                                                               ` Paul E. McKenney
2023-01-19 13:39                                                                                 ` Jonas Oberhauser
2023-01-19 18:41                                                                                   ` Paul E. McKenney
2023-01-19 19:51                                                                                     ` Alan Stern
2023-01-19 21:53                                                                                       ` Paul E. McKenney
2023-01-19 22:04                                                                                         ` Alan Stern
2023-01-19 23:03                                                                                           ` Paul E. McKenney
2023-01-20  9:43                                                                                         ` Jonas Oberhauser
2023-01-20 15:39                                                                                           ` Paul E. McKenney
2023-01-20 20:46                                                                                             ` Jonas Oberhauser
2023-01-20 21:37                                                                                               ` Paul E. McKenney
2023-01-20 22:36                                                                                                 ` Jonas Oberhauser
2023-01-20 23:19                                                                                                   ` Paul E. McKenney
2023-01-21  0:03                                                                                                     ` Jonas Oberhauser
2023-01-21  0:34                                                                                                       ` Paul E. McKenney
2023-01-20  3:55                                                                                       ` Paul E. McKenney
2023-01-20  9:20                                                                                         ` Jonas Oberhauser
2023-01-20 12:34                                                                                         ` Jonas Oberhauser
2023-01-20 12:51                                                                                           ` Jonas Oberhauser
2023-01-20 15:32                                                                                             ` Paul E. McKenney
2023-01-20 20:56                                                                                               ` Jonas Oberhauser
2023-01-20 21:40                                                                                                 ` Paul E. McKenney
2023-01-20 16:14                                                                                         ` Alan Stern
2023-01-20 17:30                                                                                           ` Paul E. McKenney
2023-01-20 18:15                                                                                             ` Alan Stern
2023-01-20 18:59                                                                                               ` Paul E. McKenney
2023-01-20 10:13                                                                                     ` Jonas Oberhauser
2023-01-20 15:47                                                                                       ` Paul E. McKenney
2023-01-20 22:21                                                                                         ` Jonas Oberhauser
2023-01-20 16:18                                                                                       ` Alan Stern
2023-01-20 21:41                                                                                         ` Jonas Oberhauser
2023-01-21  4:38                                                                                           ` Paul E. McKenney
2023-01-21 17:36                                                                                           ` Alan Stern
2023-01-21 18:40                                                                                             ` Paul E. McKenney
2023-01-21 19:56                                                                                               ` Alan Stern
2023-01-21 20:10                                                                                                 ` Paul E. McKenney
2023-01-21 21:03                                                                                                   ` Alan Stern
2023-01-21 23:49                                                                                                     ` Paul E. McKenney
2023-01-23 11:48                                                                                             ` Jonas Oberhauser
2023-01-23 15:55                                                                                               ` Alan Stern
2023-01-23 19:40                                                                                                 ` Jonas Oberhauser
2023-01-23 20:34                                                                                                   ` Alan Stern
2023-01-18 20:06                                                                     ` Paul E. McKenney
2023-01-18 20:54                                                                       ` Alan Stern
2023-01-18 21:05                                                                         ` Jonas Oberhauser
2023-01-19  0:02                                                                         ` Paul E. McKenney
2023-01-19  2:19                                                                           ` Alan Stern
2023-01-19 11:23                                                                             ` Paul E. McKenney
2023-01-20 16:01                                                                           ` Alan Stern
2023-01-20 17:58                                                                             ` Paul E. McKenney
2023-01-20 18:37                                                                               ` Alan Stern
2023-01-20 19:20                                                                                 ` Paul E. McKenney
2023-01-20 20:36                                                                                   ` Alan Stern
2023-01-20 21:20                                                                                     ` Paul E. McKenney
2023-01-22 20:32                                                                                       ` Alan Stern
2023-01-23 20:16                                                                                         ` Paul E. McKenney
2023-01-24  2:18                                                                                           ` Alan Stern
2023-01-24  4:06                                                                                             ` Paul E. McKenney
2023-01-24 11:09                                                                                               ` Andrea Parri
2023-01-24 14:54                                                                                                 ` Paul E. McKenney
2023-01-24 15:11                                                                                                   ` Jonas Oberhauser
2023-01-24 16:22                                                                                                     ` Paul E. McKenney
2023-01-24 16:39                                                                                                       ` Jonas Oberhauser
2023-01-24 17:26                                                                                                         ` Paul E. McKenney
2023-01-24 19:30                                                                                                           ` Jonas Oberhauser
2023-01-24 22:15                                                                                                             ` Paul E. McKenney
2023-01-24 22:35                                                                                                               ` Alan Stern
2023-01-24 22:54                                                                                                                 ` Paul E. McKenney
2023-01-25  1:54                                                                                                                   ` Alan Stern
2023-01-25  2:20                                                                                                                     ` Paul E. McKenney
2023-01-25 13:10                                                                                                                       ` Jonas Oberhauser
2023-01-25 15:05                                                                                                                         ` Paul E. McKenney
2023-01-25 15:34                                                                                                                           ` Alan Stern
2023-01-25 17:18                                                                                                                             ` Paul E. McKenney
2023-01-25 17:42                                                                                                                               ` Jonas Oberhauser
2023-01-25 19:08                                                                                                                               ` Alan Stern
2023-01-25 19:46                                                                                                                                 ` Paul E. McKenney
2023-01-25 20:36                                                                                                                                   ` Andrea Parri
2023-01-25 21:10                                                                                                                                     ` Jonas Oberhauser
2023-01-25 21:23                                                                                                                                       ` Paul E. McKenney
2023-01-25 20:46                                                                                                                                   ` Alan Stern
2023-01-25 21:38                                                                                                                                     ` Paul E. McKenney
2023-01-25 23:33                                                                                                                                       ` Paul E. McKenney
2023-01-26  1:45                                                                                                                                         ` Alan Stern
2023-01-26  1:53                                                                                                                                           ` Paul E. McKenney
2023-01-26 12:17                                                                                                                                             ` Jonas Oberhauser
2023-01-26 18:48                                                                                                                                               ` Paul E. McKenney
2023-01-27 15:03                                                                                                                                                 ` Jonas Oberhauser
2023-01-27 16:50                                                                                                                                                   ` Paul E. McKenney
2023-01-27 16:54                                                                                                                                                     ` Paul E. McKenney
2023-01-18 19:57                                                                   ` Jonas Oberhauser
2023-01-18 21:06                                                                     ` Paul E. McKenney
2023-01-18  2:15                                                               ` Alan Stern
2023-01-18  5:17                                                                 ` Paul E. McKenney
2023-01-18 16:03                                                                   ` Alan Stern
2023-01-18 16:59                                                                     ` Boqun Feng
2023-01-18 17:08                                                                       ` Alan Stern
2023-01-18 17:41                                                                     ` Paul E. McKenney
2023-01-19 19:07                                                                       ` Paul E. McKenney
2023-01-14 16:55                           ` Alan Stern
2023-01-14 17:35                             ` Paul E. McKenney
     [not found]                         ` <17078dd97cb6480f9c51e27058af3197@huawei.com>
2023-01-14 17:27                           ` Alan Stern

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=20230112215716.GS4028633@paulmck-ThinkPad-P17-Gen-1 \
    --to=paulmck@kernel.org \
    --cc=akiyks@gmail.com \
    --cc=boqun.feng@gmail.com \
    --cc=dhowells@redhat.com \
    --cc=dlustig@nvidia.com \
    --cc=frederic@kernel.org \
    --cc=j.alglave@ucl.ac.uk \
    --cc=joel@joelfernandes.org \
    --cc=jonas.oberhauser@huawei.com \
    --cc=linux-kernel@vger.kernel.org \
    --cc=luc.maranget@inria.fr \
    --cc=npiggin@gmail.com \
    --cc=parri.andrea@gmail.com \
    --cc=peterz@infradead.org \
    --cc=quic_neeraju@quicinc.com \
    --cc=stern@rowland.harvard.edu \
    --cc=urezki@gmail.com \
    --cc=will@kernel.org \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
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).