public inbox for gcc-bugs@sourceware.org
help / color / mirror / Atom feed
* [Bug c/59856] New: Support sparse-style context checking, used to validate locking correctness
@ 2014-01-17  9:15 josh at joshtriplett dot org
  0 siblings, 0 replies; only message in thread
From: josh at joshtriplett dot org @ 2014-01-17  9:15 UTC (permalink / raw)
  To: gcc-bugs

http://gcc.gnu.org/bugzilla/show_bug.cgi?id=59856

            Bug ID: 59856
           Summary: Support sparse-style context checking, used to
                    validate locking correctness
           Product: gcc
           Version: unknown
            Status: UNCONFIRMED
          Severity: enhancement
          Priority: P3
         Component: c
          Assignee: unassigned at gcc dot gnu.org
          Reporter: josh at joshtriplett dot org

Created attachment 31866
  --> http://gcc.gnu.org/bugzilla/attachment.cgi?id=31866&action=edit
Sparse test case for context checking

The Sparse static analyzer provides some extensions designed to support static
analysis of locking correctness.  It would help greatly if GCC could support
these extensions as well, to make the warnings more generally available and
visible to developers who aren't using sparse at compilation time.

These extensions consist of a new attribute "context", and a new function-like
construct, "__context__", which manipulate and track numeric "context" values
typically indicating the lock/unlock status of lock variables.

The "context" attribute applies to a function, and takes either two or three
parameters:
__attribute__((context(in, out)))
__attribute__((context(lock_expr, in, out)))

in and out are compile-time-constant unsigned integers, most commonly 0,1 or
1,0.  lock_expr is an arbitrary expression, resolving to a variable used as a
lock; the expression may reference parameters of the function by name.  All
uses of the two-argument form of context are treated as though they all refer
to an identical, anonymous lock_expr, not equivalent to any explicit lock_expr.

Calling a function with the context attribute has two effects: it generates a
warning if the specified context is not at least the value of "in", and it
changes that context by (out-in).  The Linux kernel uses these to define the
following macros:

# define __must_hold(x) __attribute__((context(x,1,1)))
# define __acquires(x)  __attribute__((context(x,0,1)))
# define __releases(x)  __attribute__((context(x,1,0)))

Sample use:

void lock(int l) __acquires(l);
void unlock(int l) __releases(l);
void call_me_with_the_foo_lock_held(void) __must_hold(foo_lock);

The context attribute also implies several checks on the definition of the
function declared with the context attribute: assuming the context on entry to
that function is "in", produce a warning if the function returns with a context
other than "out".

The "__context__" function-like construct takes one or two parameters:

__context__(delta)
__context__(lock_expr, delta)

__context__ may be used anywhere a statement may occur.  It has no associated
runtime effect.  It modifies the specified context (or the anonymous context
for the one-argument form) by the specified delta.  The Linux kernel uses this
to define the following macros:

# define __acquire(x) __context__(x,1)
# define __release(x) __context__(x,-1)
# define __cond_lock(x,c) ((c) ? ({ __acquire(x); 1; }) : 0)

__acquire and __release are commonly used within the body of the most primitive
locking functions, to tell the compiler that the context changed.

__cond_lock supports conditional lock ("trylock") functions, without requiring
special support for them in the compiler, by defining wrapper macros that
invoke the underlying function as the argument to __cond_lock.  Using that
macro in the condition of an if statement will make the context 1 in the body
of the if and 0 in the body of a matching else.

Sparse generates a warning in the following cases, and GCC should do the same:

- Calling a function with the context attribute, if the context is not at least
the "in" value.  (This warns about calling functions that expect a lock to be
held without holding that lock.)

- Causing a context to become negative.  (This warns about an unlock without a
lock.)

- Returning with a non-zero context from a function *not* declared with the
context attribute.  (This warns about a lock without an unlock.)

- Returning from a function declared with the context attribute without having
the specified context match the "out" value.  (This warns when a function
intended to return with a lock held does not do so.)


For a first-pass implementation, it would be acceptable to ignore the lock_expr
entirely, and just treat all contexts as the anonymous context.  This has the
potential to generate false negatives (for instance, by not warning on
"lock(a);unlock(b);"), but it won't generate false positives.

I've attached a test case from Sparse that demonstrates context checking.  a()
and r() are "acquire" and "release" functions.  The functions named good_*
should produce no warnings, while the functions named bad_* should produce
warnings.


^ permalink raw reply	[flat|nested] only message in thread

only message in thread, other threads:[~2014-01-17  9:15 UTC | newest]

Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2014-01-17  9:15 [Bug c/59856] New: Support sparse-style context checking, used to validate locking correctness josh at joshtriplett dot org

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).