lkml.org 
[lkml]   [2018]   [Nov]   [27]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
Date
From
SubjectRe: 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]
\
 
 \ /
  Last update: 2018-11-27 12:56    [W:0.069 / U:2.372 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site