lkml.org 
[lkml]   [2018]   [Nov]   [16]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
Date
From
SubjectQ&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.

\
 
 \ /
  Last update: 2018-11-15 23:57    [W:0.051 / U:0.124 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site