Re: [PATCH v6] taskstats: fix data-race

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

 



On Thu, Oct 24, 2019 at 03:58:40PM +0200, Dmitry Vyukov wrote:
> On Thu, Oct 24, 2019 at 3:43 PM Andrea Parri <parri.andrea@xxxxxxxxx> wrote:
> >
> > > But why? I think kernel contains lots of such cases and it seems to be
> > > officially documented by the LKMM:
> > > https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git/tree/tools/memory-model/Documentation/explanation.txt
> > > address dependencies and ppo
> >
> > Well, that same documentation also alerts about some of the pitfalls
> > developers can incur while relying on dependencies.  I'm sure you're
> > more than aware of some of the debate surrounding these issues.
> 
> I thought that LKMM is finally supposed to stop all these
> centi-threads around subtle details of ordering. And not we finally
> have it. And it says that using address-dependencies is legal. And you
> are one of the authors. And now you are arguing here that we better
> not use it :) Can we have some black/white yes/no for code correctness
> reflected in LKMM please :) If we are banning address dependencies,
> don't we need to fix all of rcu uses?

Current limitations of the LKMM are listed in tools/memory-model/README
(and I myself discussed a number of them at LPC recently); the relevant
point here seems to be:

1.	Compiler optimizations are not accurately modeled.  Of course,
	the use of READ_ONCE() and WRITE_ONCE() limits the compiler's
	ability to optimize, but under some circumstances it is possible
	for the compiler to undermine the memory model.  [...]

	Note that this limitation in turn limits LKMM's ability to
	accurately model address, control, and data dependencies.

A less elegant, but hopefully more effective, way to phrase such point
is maybe "feel free to rely on dependencies, but then do not blame the
LKMM authors please".  ;-)

Thanks,
  Andrea



[Index of Archives]     [Linux Kernel]     [Kernel Development Newbies]     [Linux USB Devel]     [Video for Linux]     [Linux Audio Users]     [Yosemite Hiking]     [Linux Kernel]     [Linux SCSI]

  Powered by Linux