On Mon, Nov 20, 2017 at 01:55:35PM -0500, Tim Hansen wrote:
> On Sun, Nov 19, 2017 at 09:28:49PM +0000, Al Viro wrote:
> > On Sun, Nov 19, 2017 at 03:02:10PM -0500, Tim Hansen wrote:
> > > Adds hlist_first_rcu and hlist_next_rcu for safe access
> > > to the hlist in seq_hlist_next_rcu.
> > >
> > > Found on linux-next branch, tag next-20171117 with sparse.
> >
> > Frankly, I'm tempted to take sparse RCU annotations out for good -
> > they are far too noisy and I'm not sure sparse is suitable for the
> > analysis needed to prove safety of that stuff, so unless you (or
> > somebody else) figures out how to use them in a reasonably clean
> > way, we'd probably be better off just dropping them.
>
> Can you detail how sparse is insufficent to prove RCU saftey?
> I'm not an RCU expert by any means but I don't know of any
> complaints regarding the capabilities of sparse to detect RCU
> correctness in the community. That however could just be my
> own ignornace. As far as I know these sparse RCU annotations
> are used widely across other subsystems.
>
> I'd defer to other people more knowledgable on sparse to chime
> in regarding the "correctness" of it's capability on the RCU.
Hi,
[not knowing much about RCU's needs here but knowing quite a bit
about sparse]
I think the issue here is mainly about the use of the address space.
For kernel space vs. __user vs. __iomem, address space works quite
well: a pointer points either to a kernel address or to userland
or to some device or bus memory. It's an exclusive thing.
So you can annotate the pointer with __user or __iomem, it's a
kind of extension of the typing system, and you can let sparse
do its job.
For the endianness annotations, it's very similar: a variable
either points to a native value or to a big or little endian
value, only one can (should!) be correct. The __be32/__le32/...
annotations are once again an extension of the typing system.
Fine for sparse.
For RCU, the impression I have is that things are completly
different: it's more a question of transient state than
something exclusive. The choice to use another address space
imposes the need of a lot of artificial annotation. And to
make sparse able to do its job, a lot of artificial helpers
are needed to cast variable in and out of the __rcu address
space.
-- Luc Van Oostenryck
From 1584612444485600336@xxx Mon Nov 20 18:56:29 +0000 2017
X-GM-THRID: 1584526039726552067
X-Gmail-Labels: Inbox,Category Forums,HistoricalUnread