Re: [Xen-devel] missing lock in percpu_rwlock? (Was: Re: New Defects reported by Coverity Scan for XenProject)

[Andrew Cooper <andrew.cooper3@xxxxxxxxxx>]

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-admin@xxxxxxxxxxxx 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.crossley@xxxxxxxxxx>
>>>> 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.
>
>> 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.

~Andrew

_______________________________________________
Xen-devel mailing list
Xen-devel@xxxxxxxxxxxxx
http://lists.xen.org/xen-devel