* ASSERT::
* Function and Parameter Attributes::
* Backtraces::
+* Automatic Race Detection with Checkbochs::
* gdb::
* Debugging by Infinite Loop::
* Modifying Bochs::
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{<OldState>-><NewState>}. 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}
# 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.
"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 () },
--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
# 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";
} else {
print BOCHSRC "display_library: term\n";
}
+ print BOCHSRC "logfile: $checkbochs_logfile\n" if $checkbochs;
close (BOCHSRC);
# Compose Bochs command line.
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];
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");
projects / pintos-anon / commitdiff