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: <20190116115752.GB10803@hirez.programming.kicks-ass.net> Date: Wed, 16 Jan 2019 12:57:52 +0100 From: Peter Zijlstra <peterz@...radead.org> To: Alan Stern <stern@...land.harvard.edu> Cc: Andrea Parri <andrea.parri@...rulasolutions.com>, LKMM Maintainers -- Akira Yokosawa <akiyks@...il.com>, Boqun Feng <boqun.feng@...il.com>, Daniel Lustig <dlustig@...dia.com>, David Howells <dhowells@...hat.com>, Jade Alglave <j.alglave@....ac.uk>, Luc Maranget <luc.maranget@...ia.fr>, Nicholas Piggin <npiggin@...il.com>, "Paul E. McKenney" <paulmck@...ux.ibm.com>, Will Deacon <will.deacon@....com>, Dmitry Vyukov <dvyukov@...gle.com>, linux-kernel@...r.kernel.org Subject: Re: Plain accesses and data races in the Linux Kernel Memory Model On Tue, Jan 15, 2019 at 10:19:10AM -0500, Alan Stern wrote: > On Tue, 15 Jan 2019, Andrea Parri wrote: > > > Unless I'm mis-reading/-applying this definition, this will flag the > > following test (a variation on your "race.litmus") with "data-race": > > > > C no-race > > > > {} > > > > P0(int *x, spinlock_t *s) > > { > > spin_lock(s); > > WRITE_ONCE(*x, 1); /* A */ > > spin_unlock(s); /* B */ > > } > > > > P1(int *x, spinlock_t *s) > > { > > int r1; > > > > spin_lock(s); /* C */ > > r1 = *x; /* D */ > > spin_unlock(s); > > } > > > > exists (1:r1=1) > > > > Broadly speaking, this is due to the fact that the modified "happens- > > before" axiom does not forbid the execution with the (MP-) cycle > > > > A ->po-rel B ->rfe C ->acq-po D ->fre A > > > > and then to the link "D ->race-from-r A" here defined. > > Yes, that cycle certainly should be forbidden. On the other hand, we > don't want to insist that C happens before D, given that D may not > happen at all. > > This is a real problem. Can we solve it by adding a modified > "happens-before" which says essentially that _if_ D is preserved _then_ > C happens before D? But then what about cycles involving more than one > possibly preserved access? Or maybe a relation which says that D > cannot execute before C (so if D executes at all, it has to come after > C)? The latter; there is a compiler barrier implied at the end of spin_lock() such that anything later (in PO) must indeed be later. > Now you see why this stuff is so difficult... At the moment, I don't > know how to fix this.
Powered by blists - more mailing lists