Date: Wed, 31 Jul 1996 15:07:14 +0900 (JST) From: Michael Hancock <michaelh@cet.co.jp> To: FreeBSD Hackers <Hackers@FreeBSD.ORG> Subject: kernel assertions (Rev. 1) Message-ID: <Pine.SV4.3.93.960731135230.12103C-100000@parkplace.cet.co.jp>
next in thread | raw e-mail | index | archive | help
This is a more concrete example of code specifications via assertions with
changes based on the discussions earlier.
Global Macros
-------------
The assertion macros can have levels associated with them to allow the
code author to choose which assertions go into the production build.
ASSERT_LEVEL == 0 - All assertions are preprocessed out.
ASSERT_LEVEL == 1 - Level 1 assertions are applied. (default)
REQUIRE1, ENSURE1
ASSERT_LEVEL == 2 - Level 2 assertions are additionally applied
REQUIRE1, ENSURE1
REQUIRE2, ENSURE2
Example ...
/*
* remove the buffer from the appropriate free list
*/
void
bremfree(struct buf * bp)
{
int s = splbio();
REQUIRE2(bp, "Expected bp to point to something")
REQUIRE1(bp->b_qindex != QUEUE_NONE, "Expected a buffer on a
queue");
TAILQ_REMOVE(&bufqueues[bp->b_qindex], bp, b_freelist);
bp->b_qindex = QUEUE_NONE;
ENSURE2(bp->b_qindex == QUEUE_NONE, "Buffer should no longer be on
a queue");
splx(s);
}
Since the ASSERTION_LEVEL is 1, only the original assertion check is
actually compiled into the code.
We were able to add specifications REQUIRE2 and ENSURE2 without adding any
overhead except when running diagnostics.
Note REQUIRE and ENSURE do the same thing. They are named differently for
conceptual reasons.
The ENSURE2 looks redundant in the above example, but for larger functions
without multiple exits and with easily defined resulting states the
assertion is useful. Though I've found that the REQUIRE assertions are
more important.
I personally don't care if they are called REQUIRE, ENSURE or just plain
ASSERT. The REQUIRE and ENSURE names, borrowed from Eiffel, do help make
things clearer.
The REQUIRE2 stuff can replace the
#ifdef DIAGNOSTICS
if (expr)
panic(expl);
#endif
stuff I've seen in the code.
Assertion failures can print out the following:
A stringified expr
The description
Filename
Line number
Mike Hancock
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?Pine.SV4.3.93.960731135230.12103C-100000>