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
