Re: Sparse "context" checking..

[Linus Torvalds <torvalds@osdl.org>]

On Sat, 30 Oct 2004, Roland Dreier wrote:
>
>     Linus> In particular, this is designed for doing things like
>     Linus> matching up a "lock" with the pairing "unlock", and right
>     Linus> now that's exactly what the code does: it makes each
>     Linus> spinlock count as "+1" in the context, and each spinunlock
>     Linus> count as "-1", and then hopefully it should all add up.
> 
> Do you have a plan for how to handle functions like spin_trylock()?  I
> notice in the current tree you just didn't annotate spin_trylock().

Actually, the _current_ tree does actually annotate spin_trylock() (as of
just before I sent out the email). It looks like

	#define spin_trylock(lock)      __cond_lock(_spin_trylock(lock))

where __cond_lock() for sparse is

	include/linux/compiler.h:# define __cond_lock(x)        ((x) ? ({ __context__(1); 1; }) : 0)

ie we add a "+1" context marker for the success case.

NOTE! This works with sparse only because sparse does immediate constant 
folding, so if you do

	if (spin_trylock(lock)) {
		..
		spin_unlock(lock);
	}

sparse linearizes that the right way unconditionally, and even though 
there is a data-dependency, the data depenency is constant. However, if 
some code does

	success = spin_trylock(lock);
	if (success) {
		..
		spin_unlock(lock);
	}

sparse would complain about it, because sparse doesn't do any _real_ data 
flow analysis.

So sparse can follow all the obvious cases, including trylock and
"atomic_dec_and_lock()".

			Linus