Re: Detection of locking one lock twice

[Josh Triplett <josh@joshtriplett.org>]

On Tue, Dec 22, 2009 at 01:09:27AM +0100, Petr Muller wrote:
> I'm playing with sparse a bit, especially the context/locking problem
> detecting stuff. I'm trying to create simple context updating
> lock/unlock, everything works as I would expect except for this case
> (I've reduced it as much as possible) :
> 
> #ifdef __CHECKER__
>   #define __acquires(x) __attribute__((context (x, 0, 1)))
>   #define __releases(x) __attribute__((context (x, 1, 0)))
>   #define __acquire(x) __context__(x,1)
>   #define __release(x) __context__(x,-1)
> #else
> (...)
> #endif
> 
> (...)
> 
> void lock(void)
>   __acquires(i)
> {
>   __acquire(i);
> }
> 
> void unlock(void)
>   __releases(i)
> {
>   __release(i);
> }
> 
> void fction(int a)
> {
>   lock();
>   lock();
>   unlock();
>   unlock();
> }
> 
> int main(void){
>   fction(1);
>   return 0;
> }
> 
> Sparse gives no warning in this code - I would expect that second call
> to lock() would violate the 'in' limit of __acquires attribute, but it
> does not. I'm wondering if this is actually a problem in sparse, or am I
> doing something wrong? 

As far as I know, Sparse currently treats the "in" context as a minimum
requirement, not an exact requirement.  Thus, a context of 0 ends up
meaning "may or may not hold the lock", while 1 means "must hold the
lock at least once".

I think that needs fixing.

- Josh Triplett