lkml.org 
[lkml]   [2018]   [Apr]   [12]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
Date
From
SubjectRe: [PATCH] memory-model: fix cheat sheet typo
On Thu, Apr 12, 2018 at 12:18:13PM +0200, Paolo Bonzini wrote:
> On 12/04/2018 11:23, Andrea Parri wrote:
> >>
> >> - smp_store_mb() is missing
> >
> > Good point. In fact, we could add this to the model as well:
> > following Peter's remark/the generic implementation,
>
> Good idea. smp_store_mb() can save some clock cycles in the relatively
> common idiom
>
> write a write b
> read b read a
> if (b) if (a)
> wake 'em we've been woken
>
> > Yeah, those 'Ordering is cumulative', 'Ordering propagates' could
> > mean different things to different readers... IMO, we may even omit
> > such information; this doc. does not certainly aim for completeness,
> > after all. OTOH, we ought to refrain from making this doc. an excuse
> > to transform (what it is really) high-school maths into some black
> > magic.
> FWIW, what I miss in explanation.txt (and to some extent in the paper)
> is a clear pointer to litmus tests that rely on cumulativity and
> propagation. In the meanwhile I'll send some patches. Thanks for the
> feedback, as it also helps validating my understanding of the model.

The litmus test that first comes to my mind when I think of cumulativity
(at least, 'cumulativity' as intended in LKMM) is:

WRC+pooncerelease+rmbonceonce+Once.litmus

for 'propagation', I could mention:

IRIW+mbonceonces+OnceOnce.litmus

(both tests are availabe in tools/memory-model/litmus-tests/). It would
be a nice to mention these properties in the test descriptions, indeed.

You might find it useful to also visualize the 'valid' executions (with
the main events/relations) associated to each of these tests; for this,

$ herd7 -conf linux-kernel.cfg litmus-tests/your-test.litmus \
-show all -gv

(assuming you have 'gv' installed).

Andrea


>
> Thanks,
>
> Paolo

\
 
 \ /
  Last update: 2018-04-12 13:22    [W:0.107 / U:1.624 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site