On Sat, 2007-07-07 at 03:30 +0100, Al Viro wrote:
> On Sat, Jul 07, 2007 at 03:11:52AM +0100, Al Viro wrote:
> > Still not expressive enough... Consider e.g.
> >
> > struct foo *lookup_foo(char *s); // lookup by name, return NULL if failed
> > // or pointer to struct foo with ->mutex
> > // held. Caller should unlock.
> >
> > It's legitimate, not particulary rare and AFAICS can't be expressed.
>
> Another fun problem: consider a structure with pair of methods - ->start()
> and ->stop(). The only locking requirement is that calls are inverse wrt
> locking (i.e. foo->start();foo->stop(); leaves the locking state unchanged).
> Different instances may deal with different locks, different _kinds_ of
> locks or no locks at all. How do you annotate ->start() and ->stop()?
>
> We have just such a beast in the kernel - seq_operations (see fs/seq_file.c
> for code that calls these methods and grep for seq_operations to see users).
Yeah, I've used seq_file. I'd suggest treating this as two separate
problems:
1. How do you express the semantic of function pointers that
represent a paired context in a seq_file? For this case, I
suggest just saying that start and stop acquire and release the
seq_operations structure itself, or some similar dummy context
specific to the instance of the structure. Any caller that
calls the function pointers in a seq_operations struct would
then need to properly pair them. If you wrote a function that
took a seq_operations and didn't properly manage the context
with paired calls, Sparse would warn about it, just as if the
contexts applied to local function pointers or pointers from any
other struct.
2. Does Sparse need to enforce any requirement that the functions
you assign to the function pointers actually acquire and release
some context? If so, you'd have to do some kind of unification.
However, I don't think Sparse needs to enforce that requirement.
Either your particular seq_operations need pairing for some
context reason, in which case you can specify a particular
context on them, or they don't need pairing for some reason, in
which case you don't need to specify a context on them.
Meanwhile, any actual callers of those functions using the
function pointers will get warnings as appropriate based on the
solution to problem 1.
- Josh Triplett
-
To unsubscribe from this list: send the line "unsubscribe linux-sparse" in
the body of a message to majordomo@xxxxxxxxxxxxxxx
More majordomo info at http://vger.kernel.org/majordomo-info.html
