linux-arch.vger.kernel.org archive mirror
 help / color / mirror / Atom feed
From: Alan Stern <stern@rowland.harvard.edu>
To: "Paul E. McKenney" <paulmck@kernel.org>
Cc: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org,
	kernel-team@fb.com, mingo@kernel.org, parri.andrea@gmail.com,
	will@kernel.org, peterz@infradead.org, boqun.feng@gmail.com,
	npiggin@gmail.com, dhowells@redhat.com, j.alglave@ucl.ac.uk,
	luc.maranget@inria.fr, akiyks@gmail.com
Subject: Re: [PATCH kcsan 9/9] tools/memory-model:  Document locking corner cases
Date: Fri, 4 Sep 2020 15:52:28 -0400	[thread overview]
Message-ID: <20200904195228.GB699781@rowland.harvard.edu> (raw)
In-Reply-To: <20200903234507.GA24261@paulmck-ThinkPad-P72>

On Thu, Sep 03, 2020 at 04:45:07PM -0700, Paul E. McKenney wrote:

> The hope was to have a good version of them completed some weeks ago,
> but life intervened.
> 
> My current thought is to move these three patches out of my queue for
> v5.10 to try again in v5.11:
> 
> 0b8c06b75ea1 ("tools/memory-model: Add a simple entry point document")
> dc372dc0dc89 ("tools/memory-model: Move Documentation description to Documentation/README")
> 0d9aaf8df7cb ("tools/memory-model: Document categories of ordering primitives")
> 35dd5f6d17a0 ("tools/memory-model:  Document locking corner cases")
> 
> These would remain in my v5.10 queue:
> 
> 1e44e6e82e7b ("Replace HTTP links with HTTPS ones: LKMM")
> cc9628b45c9f ("tools/memory-model: Update recipes.txt prime_numbers.c path")
> 984f272be9d7 ("tools/memory-model: Improve litmus-test documentation")
> 7c22cf3b731f ("tools/memory-model: Expand the cheatsheet.txt notion of relaxed")
> 	(But with the updates from the other thread.)
> 
> Does that work?  If not, what would?

That sounds reasonable.

> > > > Just what you want to achieve here is not clear from the context.
> > > 
> > > People who have internalized the "roach motel" model of locking
> > > (https://www.cs.umd.edu/~pugh/java/memoryModel/BidirectionalMemoryBarrier.html)
> > > need their internalization adjusted.
> > 
> > Shucks, if you only want to show that letting arbitrary code (i.e., 
> > branches) migrate into a critical section is unsafe, all you need is 
> > this uniprocessor example:
> > 
> > 	P0(int *sl)
> > 	{
> > 		goto Skip;
> > 		spin_lock(sl);
> > 		spin_unlock(sl);
> > 	Skip:
> > 		spin_lock(sl);
> > 		spin_unlock(sl);
> > 	}
> > 
> > This does nothing but runs fine.  Letting the branch move into the first 
> > critical section gives:
> > 
> > 	P0(int *sl)
> > 	{
> > 		spin_lock(sl);
> > 		goto Skip;
> > 		spin_unlock(sl);
> > 	Skip:
> > 		spin_lock(sl);
> > 		spin_unlock(sl);
> > 	}
> > 
> > which self-deadlocks 100% of the time.  You don't need to know anything 
> > about memory models or concurrency to understand this.
> 
> Although your example does an excellent job of illustrating the general
> point about branches, I am not convinced that it would be seen as
> demonstrating the dangers of moving an entire loop into a critical
> section.

All right, how about this?

	P0(int *sl)
	{
		while (spin_is_locked(sl))
			cpu_relax();
		spin_lock(sl);
		spin_unlock(sl);
	}

Runs normally, even if other threads are doing unknown locking and 
unlocking at the same time.  But:

	P0(int *sl)
	{
		spin_lock(sl);
		while (spin_is_locked(sl))
			cpu_relax();
		spin_unlock(sl);
	}

always goes into an infinite loop.

> > On the other hand, if you want to show that letting memory accesses leak 
> > into a critical section is unsafe then you need a different example: 
> > spin loops won't do it.
> 
> I am not immediately coming up with an example that is broken by leaking
> isolated memory accesses into a critical section.  I will give it some
> more thought.

It may turn out to be a hard challenge.  As far as I know, there are no 
such examples, unless you want to count something like this:

	spin_lock(sl);
	spin_unlock(sl);
	spin_lock(sl);
	spin_unlock(sl);

transformed to:

	spin_lock(sl);
	spin_lock(sl);
	spin_unlock(sl);
	spin_unlock(sl);

You could view this transformation as moving the second spin_lock up 
into the first critical section (obviously dangerous since spin_lock 
involves a loop), or as moving the first spin_unlock down into the 
second critical section (not so obvious since spin_unlock is just a 
memory access).

Okay, so let's restrict ourselves to memory accesses and loops that 
don't touch the spinlock variable itself.  Then we would need something 
more similar to the original example, like this:

	P0(spin_lock *sl, int *x)
	{
		while (READ_ONCE(x) == 0)
			cpu_relax();
		spin_lock(sl);
		spin_unlock(sl);
	}

	P1(spin_lock *sl, int *x)
	{
		spin_lock(sl);
		WRITE_ONCE(x, 1);
		spin_unlock(sl);
	}

This will always run to completion.  But if the loop in P0 is moved into 
the critical section, the test may never end.  Again, you don't need 
fancy memory models to understand this; you just need to know that 
critical sections are mutually exclusive.

But if this example didn't have a loop, allowing the memory access to 
leak into the critical section would be fine.

Alan

      reply	other threads:[~2020-09-04 19:52 UTC|newest]

Thread overview: 30+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2020-08-31 18:20 [PATCH memory-model 0/9] LKMM updates for v5.10 Paul E. McKenney
2020-08-31 18:20 ` [PATCH kcsan 1/9] docs: fix references for DMA*.txt files paulmck
2020-08-31 18:20 ` [PATCH kcsan 2/9] Replace HTTP links with HTTPS ones: LKMM paulmck
2020-08-31 18:20 ` [PATCH kcsan 3/9] tools/memory-model: Update recipes.txt prime_numbers.c path paulmck
2020-08-31 18:20 ` [PATCH kcsan 4/9] tools/memory-model: Improve litmus-test documentation paulmck
2020-08-31 18:20 ` [PATCH kcsan 5/9] tools/memory-model: Add a simple entry point document paulmck
2020-08-31 18:20 ` [PATCH kcsan 6/9] tools/memory-model: Expand the cheatsheet.txt notion of relaxed paulmck
2020-09-02  3:54   ` Boqun Feng
2020-09-02 10:14     ` peterz
2020-09-02 12:37       ` Boqun Feng
2020-09-02 12:47         ` peterz
2020-09-03 23:30         ` Paul E. McKenney
2020-09-04  0:59           ` Boqun Feng
2020-09-04  2:39             ` Paul E. McKenney
2020-09-04  2:47               ` Boqun Feng
2020-09-04 19:56                 ` Paul E. McKenney
2020-08-31 18:20 ` [PATCH kcsan 7/9] tools/memory-model: Move Documentation description to Documentation/README paulmck
2020-08-31 18:20 ` [PATCH kcsan 8/9] tools/memory-model: Document categories of ordering primitives paulmck
2020-08-31 22:34   ` Akira Yokosawa
2020-08-31 23:12     ` Paul E. McKenney
2020-09-01  1:23   ` Alan Stern
2020-09-01  2:58     ` Paul E. McKenney
2020-08-31 18:20 ` [PATCH kcsan 9/9] tools/memory-model: Document locking corner cases paulmck
2020-08-31 20:17   ` Alan Stern
2020-08-31 21:47     ` Paul E. McKenney
2020-09-01  1:45       ` Alan Stern
2020-09-01 17:04         ` Paul E. McKenney
2020-09-01 20:11           ` Alan Stern
2020-09-03 23:45             ` Paul E. McKenney
2020-09-04 19:52               ` Alan Stern [this message]

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=20200904195228.GB699781@rowland.harvard.edu \
    --to=stern@rowland.harvard.edu \
    --cc=akiyks@gmail.com \
    --cc=boqun.feng@gmail.com \
    --cc=dhowells@redhat.com \
    --cc=j.alglave@ucl.ac.uk \
    --cc=kernel-team@fb.com \
    --cc=linux-arch@vger.kernel.org \
    --cc=linux-kernel@vger.kernel.org \
    --cc=luc.maranget@inria.fr \
    --cc=mingo@kernel.org \
    --cc=npiggin@gmail.com \
    --cc=parri.andrea@gmail.com \
    --cc=paulmck@kernel.org \
    --cc=peterz@infradead.org \
    --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).