On Wed, 2016-02-03 at 12:24 +0000, Andrew Cooper wrote: > On 03/02/16 12:21, Andrew Cooper wrote: > > On 03/02/16 11:00, Ian Campbell wrote: > > > On Wed, 2016-02-03 at 10:50 +0000, Andrew Cooper wrote: > > > > On 03/02/16 10:45, Ian Campbell wrote: > > > > > On Tue, 2016-02-02 at 20:23 -0800, scan-ad...@coverity.com wrote: > > > > > > * CID 1351223: Concurrent data access > > > > > > violations (MISSING_LOCK) > > > > > > /xen/include/xen/spinlock.h: 362 in _percpu_write_unlock() > > > > > Coverity seems to think this is new in 41b0aa569adb..9937763265d, > > > > > presumably due to > > > > > > > > > > commit f9dd43dddc0a31a4343a58072935c1b5c0cbbee > > > > > Author: Malcolm Crossley <malcolm.cross...@citrix.com> > > > > > Date: Fri Jan 22 16:04:41 2016 +0100 > > > > > > > > > > rwlock: add per-cpu reader-writer lock infrastructure > > > > Expected behaviour. writer_activating is expected to only be > > > > written > > > > under lock, but read without lock. > > > I suppose this is something we should eventually model? > > Short of annotating the source code with Coverity comments (which has > > already been objected to), I don't see a way. > > > > This issue is Coverity (correctly) observing the behaviour of the > > function, and coming to the wrong conclusion. The modelling file is > > used to correct the interpretation of the behaviour of the function. > > > > > Would you typically mark this as "False positive" or "Intentional"? > > I would err on the side of Intentional. > > > > The analysis of the issue was correct; that data was accessed both with > > and without the lock, and that this usually means a data race > > condition. > > > > In this case, it is a deliberate algorithm decision to have the data > > access like this.
Done. I linked to your explanation in the comments. > > > > > I just marked a couple of libxl ones about taking ctx->lock (which is > > > recursive) twice as "False positive", but perhaps "Intentional" is > > > the > > > correct designation there? > > There is an attempt to model this in the model file, but it clearly > > isn't taking. > > (I meant to say as well) > > This I would err in the side of false positive, with "modelling > required" as a reason. The lock is a recursive lock and Coverity should > be able to spot this fact, but can't for some reason. Good idea, I'll update those. Ian _______________________________________________ Xen-devel mailing list Xen-devel@lists.xen.org http://lists.xen.org/xen-devel
