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.
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.
>