Q&A from "Concurrency with tools/memory-model"
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.
Quoted 4 lines · Paul E. McKenney
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
Quoted 35 lines
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.