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

From: Andrea Parri
Date: Tue Nov 27 2018 - 06:56:00 EST


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: slides.pdf
Description: Adobe PDF document