lkml.org 
[lkml]   [2018]   [Feb]   [3]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
Date
From
SubjectRe: [GIT PULL tools] Linux kernel memory model
On Sat, 3 Feb 2018, Paul E. McKenney wrote:

> Please see below for an initial patch to this effect. This activity
> proved to be more productive than expected for these tests, which certainly
> supports our assertion that locking needs more testing...
>
> MP+polocks.litmus
> MP+porevlocks.litmus
>
> These are allowed by the current model, which surprised me a bit,
> given that even powerpc would forbid them. Is the rationale
> that a lock-savvy compiler could pull accesses into the lock's
> critical section and then reorder those accesses? Or does this
> constitute a bug in our model of locking?
>
> (And these were allowed when I wrote recipes.txt, embarrassingly
> enough...)
>
> Z6.0+pooncelock+poonceLock+pombonce.litmus
>
> This was forbidden when I wrote recipes.txt, but now is allowed.
> The header comment for smp_mb__after_spinlock() makes it pretty
> clear that it must be forbidden. So this one is a bug in our
> model of locking.

I just tried testing these under the most recent version of herd, and
all three were forbidden.

Alan

\
 
 \ /
  Last update: 2018-02-03 23:10    [W:0.220 / U:0.456 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site