Messages in this thread | | | Date | Tue, 27 Nov 2018 12:55:37 +0100 | From | Andrea Parri <> | Subject | Re: Q&A from "Concurrency with tools/memory-model" |
| |
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. > [unhandled content-type:application/pdf] | |