lists.openwall.net | lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC | |
Open Source and information security mailing list archives
| ||
|
Message-ID: <20180412112155.GA9154@andrea> Date: Thu, 12 Apr 2018 13:21:55 +0200 From: Andrea Parri <andrea.parri@...rulasolutions.com> To: Paolo Bonzini <pbonzini@...hat.com> Cc: paulmck@...ux.vnet.ibm.com, linux-kernel@...r.kernel.org, Alan Stern <stern@...land.harvard.edu>, Andrea Parri <parri.andrea@...il.com>, Will Deacon <will.deacon@....com>, Peter Zijlstra <peterz@...radead.org>, Boqun Feng <boqun.feng@...il.com>, Nicholas Piggin <npiggin@...il.com>, David Howells <dhowells@...hat.com>, Jade Alglave <j.alglave@....ac.uk>, Luc Maranget <luc.maranget@...ia.fr>, Akira Yokosawa <akiyks@...il.com> Subject: Re: [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
Powered by blists - more mailing lists