Detection of locking one lock twice

Detection of locking one lock twice

[Petr Muller]

Hi,

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? 

Thanks,

Petr

Re: Detection of locking one lock twice

[Josh Triplett]

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

Re: Detection of locking one lock twice

[Christopher Li]

On Sun, Jan 3, 2010 at 11:48 PM, Josh Triplett <josh@joshtriplett.org> wrote:
>> void fction(int a)
>> {
>>   lock();
>>   lock();
>>   unlock();
>>   unlock();
>> }
>> 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?

Sorry I am late to the party. I think sparse does not complain on this
code because sparse has no way to track *which* lock it is taking.
Some thing like:

lock(A);
lock(B);
unlock(B);
unlock(A);

It is perfectly fine. So sparse is not suppose to complain there.

> 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".

You can interpret it that way, but that is not how I see it.

The context is not suppose to go to negative, that is why we have 'in' and 'out'
context. When a function perform unlock, you are suppose to give a
positive value in
'in' context to avoid geting negative. As long as the context does not
go negative,
sparse only care about the delta of 'in' and 'out' value. It counts
the context to
the exact number. See the following code:

 	if (insn->opcode == OP_RET)
		return entry != exit ? imbalance(ep, bb, entry, exit, "wrong count
at exit") : 0;

So I don't think it is a bug. If you disagree, please give me more detail.

Chris
--
To unsubscribe from this list: send the line "unsubscribe linux-sparse" in
the body of a message to majordomo@vger.kernel.org
More majordomo info at  http://vger.kernel.org/majordomo-info.html