Q&A from "Concurrency with tools/memory-model"

Q&A from "Concurrency with tools/memory-model"

[Paul E. McKenney]

Hello!

Good turnout and some good questions here in Vancouver BC, please see
below for rough notes.  ;-)

							Thanx, Paul

------------------------------------------------------------------------

"Concurrency with tools/memory-model"

Andrea Parri presenting.

Rough notes of Q&A.

o	Want atomic bit operation.

o	But smp_read_barrier_depends() not there, so how to note pairing?
	A:  Note the dependency as the other end of the pairing.

o	Speculation barriers, as in Spectre and Meltdown?  A: This would
	require adding timing, not in the immediate future.

o	What ordering does system calls provide?  A: None that we know of.
	Boqun: Userspace needs to explicitly provide the needed ordering
	when interacting with the kernel.  Some architectures do provide
	full barriers, but not to be counted on.

o	Why herd7?  A: Based on other formalizations -- note that herd7
	had a number of hardware models.  Paul: Plus the founder of the
	LKMM project is a co-author of herd, which might have had some
	effect.

o	Why not also model interrupts and NMIs?  Promela and spin have
	been used for this.  A: Cannot currently model them.  You can
	emulated them with additional threads and locks, if you wish.
	Vincent Nimal and Lihao Liang have done some academic work on
	these topics.

Re: Q&A from "Concurrency with tools/memory-model"

[Andrea Parri]

[-- Attachment #1: Type: text/plain, Size: 1551 bytes --]

On Thu, Nov 15, 2018 at 02:56:30PM -0800, Paul E. McKenney wrote:
> Hello!
> 
> Good turnout and some good questions here in Vancouver BC, please see
> below for rough notes.  ;-)

Thanks for the notes.  I attach here the slides used for the talk
(so let's see how many typos I've left...).

  Andrea


> 
> 							Thanx, Paul
> 
> ------------------------------------------------------------------------
> 
> "Concurrency with tools/memory-model"
> 
> Andrea Parri presenting.
> 
> Rough notes of Q&A.
> 
> o	Want atomic bit operation.
> 
> o	But smp_read_barrier_depends() not there, so how to note pairing?
> 	A:  Note the dependency as the other end of the pairing.
> 
> o	Speculation barriers, as in Spectre and Meltdown?  A: This would
> 	require adding timing, not in the immediate future.
> 
> o	What ordering does system calls provide?  A: None that we know of.
> 	Boqun: Userspace needs to explicitly provide the needed ordering
> 	when interacting with the kernel.  Some architectures do provide
> 	full barriers, but not to be counted on.
> 
> o	Why herd7?  A: Based on other formalizations -- note that herd7
> 	had a number of hardware models.  Paul: Plus the founder of the
> 	LKMM project is a co-author of herd, which might have had some
> 	effect.
> 
> o	Why not also model interrupts and NMIs?  Promela and spin have
> 	been used for this.  A: Cannot currently model them.  You can
> 	emulated them with additional threads and locks, if you wish.
> 	Vincent Nimal and Lihao Liang have done some academic work on
> 	these topics.
> 

[-- Attachment #2: slides.pdf --]
[-- Type: application/pdf, Size: 137134 bytes --]