From: Ben Pfaff Date: Sun, 3 Jul 2005 22:09:19 +0000 (+0000) Subject: Basic Eraser support. X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=a03e6f1ca6bb324d2f5bba70982e493e40faf4f5;p=pintos-anon Basic Eraser support. --- diff --git a/doc/debug.texi b/doc/debug.texi index 1c6d7a3..555cc9d 100644 --- a/doc/debug.texi +++ b/doc/debug.texi @@ -9,6 +9,7 @@ introduces you to a few of them. * ASSERT:: * Function and Parameter Attributes:: * Backtraces:: +* Automatic Race Detection with Checkbochs:: * gdb:: * Debugging by Infinite Loop:: * Modifying Bochs:: @@ -232,6 +233,123 @@ backtrace kernel.o Call stack: 0xc0106eff 0xc01102fb 0xc010dc22 0xc010cf67 0xc0102319 0xc010325a 0x804812c 0x8048a96 0x8048ac8. @end example +@node Automatic Race Detection with Checkbochs +@section Automatic Race Detection with Checkbochs + +In the Pintos projects, especially projects 3 and 4, proper +synchronization is essential for avoiding race conditions. There is +no substitute for good design, but sometimes tools can help with +debugging an implementation. + +We provide a tool called Checkbochs to help find race conditions in +your implementation. Checkbochs is a version of Bochs which has been +modified by Sorav Bansal to implement the Eraser race-detection +algorithm (@bibref{Eraser}). + +Before you can use Checkbochs to to detect data races in your code, +you must first apply a patch to your Pintos source tree. FIXME + +Once you have applied the Checkbochs patch, you can use Checkbochs +simply by adding @option{--checkbochs} to the @command{pintos} command +line. You can usefully use @option{--checkbochs} in conjunction with +@option{--monitor} or @option{--gdb}, but not @option{--qemu} or +@option{--gsx}. The only immediate effect of @option{--checkbochs} is +that your run will produce an extra log file, called +@file{checkbochs.log} by default (use @option{--logfile} to change +it). The log file is a plaintext log of accesses to memory locations +shared by multiple threads. + +After you have a log file, use @command{checkbochs-trace} to interpret +it. First run it without any options, which causes it to report how +many potential race conditions were detected. If any were detected, +it also tells you the address of the data involved in the race and +writes backtraces for access to data for the first race it detected to +@file{btrace}. If more than one race was detected, you can request +information about the @var{n}th race, instead, using @option{-n +@var{n}}. + +The @file{btrace} file lists a backtrace for each access to the data +item implicated in a race. Each backtrace is listed across several +lines. Each backtrace line is divided into several columns containing +a source file name, function name, and line number. The first line in +each backtrace also identifies the thread (as the physical address of +its @struct{thread}, followed by the state transition of the memory +location in the format @samp{->}. More +information on the state transition can be found in @bibref{Eraser}. + +You can save the trouble of reading the backtraces and looking up +their source file location by hand by using the @option{--cscope} +option to @command{checkbochs-trace}. This brings up the backtrace +info in @command{cscope}, a program for interactively exploring code, +which lets you quickly view the source lines implicated in each +backtrace. + +@menu +* Debugging Race Conditions:: +* Checkbochs Limitations:: +@end menu + +@node Debugging Race Conditions +@subsection Debugging Race Conditions + +Once you know that there is a race condition at memory location +@var{addr}, you need to know at least two things to debug it. First, +you need to know what data corresponds to @var{addr}. If it is global +or @code{static} data, then @command{checkbochs-trace} will normally +print the variable's name. Otherwise, for automatic (local) or +heap-allocated data, you will have to figure it out by looking at the +backtrace. + +Second, you need to know the various points in time during code +execution at which the data variable was accessed, and which thread +made each access. You can figure this out from the backtraces: +@file{btrace} contains both the types of accesses made and the tids of +the accessing threads. + +@node Checkbochs Limitations +@subsection Limitations + +Checkbochs can be useful for debugging race conditions, but it has +several limitations. + +Checkbochs is subject to false negatives, that is, it will not find +all potential races. For example, Checkbochs will not detect races +that result from failing to recheck a condition that might have +changed while a lock was released. Suppose that @code{lock} is a lock +that controls acquisition and release of a resource, such as a page of +memory. The following code then has a race, because @code{owner} is +not re-checked after releasing and re-acquiring @code{lock}. +Checkbochs fails to detect this race because @code{lock} is always +held when @code{owner} is accessed: + +@example +struct thread *owner = NULL; /* Initially no owner. */ +struct lock lock; /* Controls changes to @var{owner}. */ + +@dots{} + +lock_acquire (&lock); +if (owner == NULL) + @{ + lock_release (&lock); + @dots{} + lock_acquire (&lock); + owner = thread_current (); + lock_release (&lock); + @} +@end example + +Checkbochs is also subject to false positives, that is, not every race +it reports is really a race. (This is why they have been called +``potential'' races throughout this section.) This will occur when +accesses to data are synchronized in a way not visible to Checkbochs. +For example, Checkbochs does not understand all uses of semaphores, +so synchronization via semaphores may be reported as races. + +Checkbochs is a dynamic checker, meaning that it actually runs the +code that it checks. This also means that code that doesn't get run +doesn't get checked, so you can also get false negatives that way. + @node gdb @section @command{gdb} diff --git a/doc/references.texi b/doc/references.texi index 78c6b8c..cb46422 100644 --- a/doc/references.texi +++ b/doc/references.texi @@ -107,3 +107,10 @@ Interface---DRAFT---24 April 2001}. A draft of a revised version of M.@: K.@: McKusick, K.@: Bostic, M.@: J.@: Karels, J.@: S.@: Quarterman, @cite{The Design and Implementation of the 4.4@acronym{BSD} Operating System}. Addison-Wesley 1996. + +@bibdfn{Eraser} +S.@: Savage, M.@: Burrows, G.@: Nelson, P.@: Sobalvarro, T.@: Anderson, +``Eraser: a dynamic data race detector for multi-threaded programs,'' +ACM Transactions on Computer Systems 15 (1997):4, pages 391--411. +Also in Proceeding of the 16th ACM Symposium on Operating Systems +Principles (1997), pages 27--37. diff --git a/src/Makefile b/src/Makefile index 6dd4610..33e0321 100644 --- a/src/Makefile +++ b/src/Makefile @@ -22,3 +22,8 @@ TAGS:: tags:: ctags -T --no-warn $(TAGS_SOURCES) +cscope.files:: + echo $(TAGS_SOURCES) > $@ + +cscope.out:: cscope.files + cscope -bk diff --git a/src/utils/pintos b/src/utils/pintos index 348c6ab..f282ec8 100755 --- a/src/utils/pintos +++ b/src/utils/pintos @@ -9,6 +9,9 @@ use Getopt::Long qw(:config bundling); # Command-line options. our ($sim); # Simulator: bochs, qemu, or gsx. our ($debug) = "none"; # Debugger: none, monitor, or gdb. +our ($checkbochs) = 0; # Use checkbochs race detector? +our ($checkbochs_logfile) # Log file for checkbochs. + = "checkbochs.log"; our ($mem) = 4; # Physical RAM in MB. our ($serial_out) = 1; # Send output to serial port? our ($vga); # VGA output: window, terminal, or none. @@ -54,6 +57,9 @@ sub parse_command_line { "monitor" => sub { set_debug ("monitor") }, "gdb" => sub { set_debug ("gdb") }, + "checkbochs" => \$checkbochs, + "logfile=s" => \$checkbochs_logfile, + "m|memory=i" => \$mem, "j|jitter=i" => sub { set_jitter (@_) }, "r|realtime" => sub { set_realtime () }, @@ -102,8 +108,12 @@ Simulator selection: --gsx Use VMware GSX Server 3.x as simulator Debugger selection: --no-debug (default) No debugger - --monitor Debug with simulator's monitor - --gdb Debug with gdb + --monitor Debug with simulator's monitor (Bochs or qemu only) + --gdb Debug with gdb (Bochs or qemu only) +Race detector (Bochs only; may be combined with debugger): + --no-checkbochs (default) Do not use race detector + --checkbochs Use race detector + --logfile=FILE Set checkbochs log file (default: checkbochs.log) Display options: (default is both VGA and serial) -v, --no-vga No VGA display -s, --no-serial No serial output @@ -358,15 +368,10 @@ sub run_vm { # Runs Bochs. sub run_bochs { - # Select Bochs binary based on the chosen debugger. - my ($bin); - if ($debug eq 'none') { - $bin = 'bochs'; - } elsif ($debug eq 'monitor') { - $bin = 'bochs-dbg'; - } elsif ($debug eq 'gdb') { - $bin = 'bochs-gdb'; - } + # Select Bochs binary based on checkbochs and debugger settings. + my ($bin) = $checkbochs ? 'checkbochs' : 'bochs'; + $bin .= '-dbg' if $debug eq 'monitor'; + $bin .= '-gdb' if $debug eq 'gdb'; # Write bochsrc.txt configuration file. open (BOCHSRC, ">", "bochsrc.txt") or die "bochsrc.txt: create: $!\n"; @@ -394,6 +399,7 @@ EOF } else { print BOCHSRC "display_library: term\n"; } + print BOCHSRC "logfile: $checkbochs_logfile\n" if $checkbochs; close (BOCHSRC); # Compose Bochs command line. @@ -435,6 +441,8 @@ sub run_qemu { if $vga eq 'terminal'; print "warning: qemu doesn't support jitter\n" if defined $jitter; + print "warning: qemu doesn't support race detection\n" + if $checkbochs; my (@cmd) = ('qemu'); for my $iface (0...3) { my ($option) = ('-hda', '-hdb', '-hdc', '-hdd')[$iface]; @@ -464,6 +472,7 @@ sub run_gsx { gsx_unsup ("--no-vga") if $vga eq 'none'; gsx_unsup ("--terminal") if $vga eq 'terminal'; gsx_unsup ("--jitter") if defined $jitter; + gsx_unsup ("--checkbochs") if $checkbochs; unlink ("pintos.out");