* Q&A from "Concurrency with tools/memory-model"
@ 2018-11-15 22:56 Paul E. McKenney
2018-11-27 11:55 ` Andrea Parri
0 siblings, 1 reply; 2+ messages in thread
From: Paul E. McKenney @ 2018-11-15 22:56 UTC (permalink / raw)
To: linux-kernel, linux-arch, mingo
Cc: stern, parri.andrea, will.deacon, peterz, boqun.feng, npiggin,
dhowells, j.alglave, luc.maranget, akiyks
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.
^ permalink raw reply [flat|nested] 2+ messages in thread
* Re: Q&A from "Concurrency with tools/memory-model"
2018-11-15 22:56 Q&A from "Concurrency with tools/memory-model" Paul E. McKenney
@ 2018-11-27 11:55 ` Andrea Parri
0 siblings, 0 replies; 2+ messages in thread
From: Andrea Parri @ 2018-11-27 11:55 UTC (permalink / raw)
To: Paul E. McKenney
Cc: linux-kernel, linux-arch, mingo, stern, parri.andrea,
will.deacon, peterz, boqun.feng, npiggin, dhowells, j.alglave,
luc.maranget, akiyks
[-- 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 --]
^ permalink raw reply [flat|nested] 2+ messages in thread
end of thread, other threads:[~2018-11-27 11:56 UTC | newest]
Thread overview: 2+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2018-11-15 22:56 Q&A from "Concurrency with tools/memory-model" Paul E. McKenney
2018-11-27 11:55 ` Andrea Parri
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).