[prev in list] [next in list] [prev in thread] [next in thread] 

List:       freebsd-hackers
Subject:    kernel assertions (Rev. 1)
From:       Michael Hancock <michaelh () cet ! co ! jp>
Date:       1996-07-31 6:07:14
[Download RAW message or body]

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

[prev in list] [next in list] [prev in thread] [next in thread]