From: Johannes Berg <johannes@sipsolutions.net>
To: Yoann Padioleau <padator@wanadoo.fr>
Cc: linux-sparse@vger.kernel.org
Subject: Re: contextual attributes
Date: Mon, 17 Nov 2008 23:10:28 +0100 [thread overview]
Message-ID: <1226959828.4014.4.camel@johannes.berg> (raw)
In-Reply-To: <8763mmuirz.fsf@aryx.cs.uiuc.edu> (sfid-20081117_224927_421372_B9FEACFC)
On Mon, 2008-11-17 at 15:47 -0600, Yoann Padioleau wrote:
> Is it possible by using the __attribute((context(x,y)) sparse
> attribute to enforce statically that all the callers of
> certain functions do certain actions such as disabling interrupts ?
In theory yes, but only half my patches got merged so no. If you search
the list you'll find a set of patches from myself that allow you to do
this, see below.
I have asked that those patches that got merged are reverted for the
time being until we can work on a decent implementation, but that hasn't
happen either so the current sparse git tree is fairly broken wrt.
context attributes...
> int __assume_disabled_interrupt
> startpoint()
> {
> return 1;
> }
>
>
> int f1ok()
> {
> spin_lock_irq();
> startpoint();
> spin_unlock_irq();
> }
>
>
> int f1bad()
> {
> startpoint();
> }
You'd have to annotate startpoint() with
__attribute__((context(irqsoff,1,1)))
and spin_lock_irq() with __attribute__((context(irqsoff,0,1))) and 1,0
for unlock, in addition to the regular locks.
[or something like that, the syntax isn't firm in my mind right now]
johannes
prev parent reply other threads:[~2008-11-17 22:11 UTC|newest]
Thread overview: 2+ messages / expand[flat|nested] mbox.gz Atom feed top
2008-11-17 21:47 contextual attributes Yoann Padioleau
2008-11-17 22:10 ` Johannes Berg [this message]
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=1226959828.4014.4.camel@johannes.berg \
--to=johannes@sipsolutions.net \
--cc=linux-sparse@vger.kernel.org \
--cc=padator@wanadoo.fr \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.