Checking System Rules Using System-Specific, Programmer-Written Compiler ExtensionsDawson Engler, Benjamin Chelf, Andy Chou, and Seth HallemStanford UniversityChecking System Rules•Model checkers or theorem provers–Pro: Finds error difficult to detect.–Con: Specifications are difficult to construct and do not mirror the code.•Testing–Pro: Simpler and no mirroring problem.–Con: Dynamic•Manual InspectionCompiler Extension•Compilers work with the code itself. Specification is not needed.•Static analysis examines all execution paths.•Need to extend the compiler to include system specific semantic informationSystem Rules•Operations follow a given order•Operations obey contextual restrictions•Sample System Rules–Never/always do X–Always do X before/after Y–Never do X before/after Y–In situation X do (not do) YMetal Overview { #include “linux-includes.h” } sm check_interrupts { // Variables used in patterns decl { unsigned } flags; // Patterns: enable/disable pat enable = { sti(); } | { restore_flags(flags); }; pat disable = { cli(); } // States is_enabled: disable ==> is_disable | enable ==> { err(“double enable”); }; is_disable: enable ==> is_enabled | disable ==> { err(“double disable”); } | $end_of_path$ ==> {err(“exiting w/intr disabled”);}; } /* From Linux 2.3.99 drivers/block/raid5.c */ static struct buffer_head * get_free_buffer( struct stripe_head *sh, int b_size) { struct buffer_head * bh; unsigned long flags; save_flags(flags); cli(); if ((bh = sh->buffer_pool) == NULL) return NULL; sh->buffer_pool = bh->b_next; bh->b_size = b_size; restore_flags(flags); return bh; }Simple Example: assert•Expression in an assert should not have non-debugging side effects.•Assert condition should not fail.Assertion side-effects { #include <assert.h> } sm Assert flow_insensitive { decl { any } expr, x, y, z; decl { any_call } any_fcall; decl { any_args } args; start: { assert(expr); } ==> {mgk_expr_recurse(expr, in_assert); }; in_assert: { any_fcall(args) } ==> { err(“function call”); } | { x = y } ==> { err(“assignment”); } | { z++ } ==> { err(“post-increment”); } | { z-- } ==> { err(“post-decrement”); } ...Checking assertions statically•Use data-flow information to track the value of scalar variables.•Evaluate the assertion expression against these values•Implemented using 100 lines of MetaTemporal Ordering•Many system have requirement in the order of operations.•Sample Extension–Argument copying in kernel system calls–Memory management●Check pointer after memory allocation●Memory not used after free●Deallocate memory on error●Size allocated is not less than assigned pointerGlobal Rules•Kernel cannot lock with interrupt disabled or while holding spin lock–Compute list of possibly blocking routine–Check if potentially blocking routine is called with interrupt disabled or while holding lock•Linux module loading and unloadingResult SummaryCheck Errors False Positives Uses LOCSide-effects 14 2 199 25Static assert 5 0 1759 100Stack check 10 0 332K 53User-ptr 18 15 187 68Allocation 184 64 4732 60Block 123 8 - 131Module ~75 2 - 133Mutex 82 201 14K 64Total ~511 ~292 - 669Conclusion•Many systems have high level system rules that generic compiler cannot check•Use meta information in the form of compiler extensions to check for these system rules•Has advantages over verification, testing, and manual