summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--TRICKS140
-rwxr-xr-xcuth48
-rwxr-xr-xpr.pl36
-rwxr-xr-xprintpcs14
-rwxr-xr-xshow13
-rwxr-xr-xsign.pl19
-rw-r--r--sleep1.p134
-rwxr-xr-xspinp16
8 files changed, 0 insertions, 410 deletions
diff --git a/TRICKS b/TRICKS
deleted file mode 100644
index 8d1439f..0000000
--- a/TRICKS
+++ /dev/null
@@ -1,140 +0,0 @@
-This file lists subtle things that might not be commented
-as well as they should be in the source code and that
-might be worth pointing out in a longer explanation or in class.
-
----
-
-[2009/07/12: No longer relevant; forkret1 changed
-and this is now cleaner.]
-
-forkret1 in trapasm.S is called with a tf argument.
-In order to use it, forkret1 copies the tf pointer into
-%esp and then jumps to trapret, which pops the
-register state out of the trap frame. If an interrupt
-came in between the mov tf, %esp and the iret that
-goes back out to user space, the interrupt stack frame
-would end up scribbling over the tf and whatever memory
-lay under it.
-
-Why is this safe? Because forkret1 is only called
-the first time a process returns to user space, and
-at that point, cp->tf is set to point to a trap frame
-constructed at the top of cp's kernel stack. So tf
-*is* a valid %esp that can hold interrupt state.
-
-If other tf's were used in forkret1, we could add
-a cli before the mov tf, %esp.
-
----
-
-In pushcli, must cli() no matter what. It is not safe to do
-
- if(cpus[cpu()].ncli == 0)
- cli();
- cpus[cpu()].ncli++;
-
-because if interrupts are off then we might call cpu(), get
-rescheduled to a different cpu, look at cpus[oldcpu].ncli,
-and wrongly decide not to disable interrupts on the new cpu.
-
-Instead do
-
- cli();
- cpus[cpu()].ncli++;
-
-always.
-
----
-
-There is a (harmless) race in pushcli, which does
-
- eflags = readeflags();
- cli();
- if(c->ncli++ == 0)
- c->intena = eflags & FL_IF;
-
-Consider a bottom-level pushcli.
-If interrupts are disabled already, then the right thing
-happens: read_eflags finds that FL_IF is not set,
-and intena = 0. If interrupts are enabled, then
-it is less clear that the right thing happens:
-the readeflags can execute, then the process
-can get preempted and rescheduled on another cpu,
-and then once it starts running, perhaps with
-interrupts disabled (can happen since the scheduler
-only enables interrupts once per scheduling loop,
-not every time it schedules a process), it will
-incorrectly record that interrupts *were* enabled.
-This doesn't matter, because if it was safe to be
-running with interrupts enabled before the context
-switch, it is still safe (and arguably more correct)
-to run with them enabled after the context switch too.
-
-In fact it would be safe if scheduler always set
- c->intena = 1;
-before calling swtch, and perhaps it should.
-
----
-
-The x86's processor-ordering memory model
-matches spin locks well, so no explicit memory
-synchronization instructions are required in
-acquire and release.
-
-Consider two sequences of code on different CPUs:
-
-CPU0
-A;
-release(lk);
-
-and
-
-CPU1
-acquire(lk);
-B;
-
-We want to make sure that:
- - all reads in B see the effects of writes in A.
- - all reads in A do *not* see the effects of writes in B.
-
-The x86 guarantees that writes in A will go out
-to memory before the write of lk->locked = 0 in
-release(lk). It further guarantees that CPU1
-will observe CPU0's write of lk->locked = 0 only
-after observing the earlier writes by CPU0.
-So any reads in B are guaranteed to observe the
-effects of writes in A.
-
-According to the Intel manual behavior spec, the
-second condition requires a serialization instruction
-in release, to avoid reads in A happening after giving
-up lk. No Intel SMP processor in existence actually
-moves reads down after writes, but the language in
-the spec allows it. There is no telling whether future
-processors will need it.
-
----
-
-The code in fork needs to read np->pid before
-setting np->state to RUNNABLE. The following
-is not a correct way to do this:
-
- int
- fork(void)
- {
- ...
- np->state = RUNNABLE;
- return np->pid; // oops
- }
-
-After setting np->state to RUNNABLE, some other CPU
-might run the process, it might exit, and then it might
-get reused for a different process (with a new pid), all
-before the return statement. So it's not safe to just
-"return np->pid". Even saving a copy of np->pid before
-setting np->state isn't safe, since the compiler is
-allowed to re-order statements.
-
-The real code saves a copy of np->pid, then acquires a lock
-around the write to np->state. The acquire() prevents the
-compiler from re-ordering.
diff --git a/cuth b/cuth
deleted file mode 100755
index cce8c0c..0000000
--- a/cuth
+++ /dev/null
@@ -1,48 +0,0 @@
-#!/usr/bin/perl
-
-$| = 1;
-
-sub writefile($@){
- my ($file, @lines) = @_;
-
- sleep(1);
- open(F, ">$file") || die "open >$file: $!";
- print F @lines;
- close(F);
-}
-
-# Cut out #include lines that don't contribute anything.
-for($i=0; $i<@ARGV; $i++){
- $file = $ARGV[$i];
- if(!open(F, $file)){
- print STDERR "open $file: $!\n";
- next;
- }
- @lines = <F>;
- close(F);
-
- $obj = "$file.o";
- $obj =~ s/\.c\.o$/.o/;
- system("touch $file");
-
- if(system("make CC='gcc -Werror' $obj >/dev/null 2>\&1") != 0){
- print STDERR "make $obj failed: $rv\n";
- next;
- }
-
- system("cp $file =$file");
- for($j=@lines-1; $j>=0; $j--){
- if($lines[$j] =~ /^#include/){
- $old = $lines[$j];
- $lines[$j] = "/* CUT-H */\n";
- writefile($file, @lines);
- if(system("make CC='gcc -Werror' $obj >/dev/null 2>\&1") != 0){
- $lines[$j] = $old;
- }else{
- print STDERR "$file $old";
- }
- }
- }
- writefile($file, grep {!/CUT-H/} @lines);
- system("rm =$file");
-}
diff --git a/pr.pl b/pr.pl
deleted file mode 100755
index 46905bd..0000000
--- a/pr.pl
+++ /dev/null
@@ -1,36 +0,0 @@
-#!/usr/bin/perl
-
-use POSIX qw(strftime);
-
-if($ARGV[0] eq "-h"){
- shift @ARGV;
- $h = $ARGV[0];
- shift @ARGV;
-}else{
- $h = $ARGV[0];
-}
-
-$page = 0;
-$now = strftime "%b %e %H:%M %Y", localtime;
-
-@lines = <>;
-for($i=0; $i<@lines; $i+=50){
- print "\n\n";
- ++$page;
- print "$now $h Page $page\n";
- print "\n\n";
- for($j=$i; $j<@lines && $j<$i +50; $j++){
- $lines[$j] =~ s!//DOC.*!!;
- print $lines[$j];
- }
- for(; $j<$i+50; $j++){
- print "\n";
- }
- $sheet = "";
- if($lines[$i] =~ /^([0-9][0-9])[0-9][0-9] /){
- $sheet = "Sheet $1";
- }
- print "\n\n";
- print "$sheet\n";
- print "\n\n";
-}
diff --git a/printpcs b/printpcs
deleted file mode 100755
index 81d039b..0000000
--- a/printpcs
+++ /dev/null
@@ -1,14 +0,0 @@
-#!/bin/sh
-
-# Decode the symbols from a panic EIP list
-
-# Find a working addr2line
-for p in i386-jos-elf-addr2line addr2line; do
- if which $p 2>&1 >/dev/null && \
- $p -h 2>&1 | grep -q '\belf32-i386\b'; then
- break
- fi
-done
-
-# Enable as much pretty-printing as this addr2line can do
-$p $($p -h | grep ' -[aipsf] ' | awk '{print $1}') -e kernel "$@"
diff --git a/show1 b/show1
deleted file mode 100755
index e0d3d83..0000000
--- a/show1
+++ /dev/null
@@ -1,3 +0,0 @@
-#!/bin/sh
-
-runoff1 "$@" | pr.pl -h "xv6/$@" | mpage -m50t50b -o -bLetter -T -t -2 -FLucidaSans-Typewriter83 -L60 >x.ps; gv --swap x.ps
diff --git a/sign.pl b/sign.pl
deleted file mode 100755
index d793035..0000000
--- a/sign.pl
+++ /dev/null
@@ -1,19 +0,0 @@
-#!/usr/bin/perl
-
-open(SIG, $ARGV[0]) || die "open $ARGV[0]: $!";
-
-$n = sysread(SIG, $buf, 1000);
-
-if($n > 510){
- print STDERR "boot block too large: $n bytes (max 510)\n";
- exit 1;
-}
-
-print STDERR "boot block is $n bytes (max 510)\n";
-
-$buf .= "\0" x (510-$n);
-$buf .= "\x55\xAA";
-
-open(SIG, ">$ARGV[0]") || die "open >$ARGV[0]: $!";
-print SIG $buf;
-close SIG;
diff --git a/sleep1.p b/sleep1.p
deleted file mode 100644
index af69772..0000000
--- a/sleep1.p
+++ /dev/null
@@ -1,134 +0,0 @@
-/*
-This file defines a Promela model for xv6's
-acquire, release, sleep, and wakeup, along with
-a model of a simple producer/consumer queue.
-
-To run:
- spinp sleep1.p
-
-(You may need to install Spin, available at http://spinroot.com/.)
-
-After a successful run spin prints something like:
-
- unreached in proctype consumer
- (0 of 37 states)
- unreached in proctype producer
- (0 of 23 states)
-
-After an unsuccessful run, the spinp script prints
-an execution trace that causes a deadlock.
-
-The safe body of producer reads:
-
- acquire(lk);
- x = value; value = x + 1; x = 0;
- wakeup(0);
- release(lk);
- i = i + 1;
-
-If this is changed to:
-
- x = value; value = x + 1; x = 0;
- acquire(lk);
- wakeup(0);
- release(lk);
- i = i + 1;
-
-then a deadlock can happen, because the non-atomic
-increment of value conflicts with the non-atomic
-decrement in consumer, causing value to have a bad value.
-Try this.
-
-If it is changed to:
-
- acquire(lk);
- x = value; value = x + 1; x = 0;
- release(lk);
- wakeup(0);
- i = i + 1;
-
-then nothing bad happens: it is okay to wakeup after release
-instead of before, although it seems morally wrong.
-*/
-
-#define ITER 4
-#define N 2
-
-bit lk;
-byte value;
-bit sleeping[N];
-
-inline acquire(x)
-{
- atomic { x == 0; x = 1 }
-}
-
-inline release(x)
-{
- assert x==1;
- x = 0
-}
-
-inline sleep(cond, lk)
-{
- assert !sleeping[_pid];
- if
- :: cond ->
- skip
- :: else ->
- atomic { release(lk); sleeping[_pid] = 1 };
- sleeping[_pid] == 0;
- acquire(lk)
- fi
-}
-
-inline wakeup()
-{
- w = 0;
- do
- :: w < N ->
- sleeping[w] = 0;
- w = w + 1
- :: else ->
- break
- od
-}
-
-active[N] proctype consumer()
-{
- byte i, x;
-
- i = 0;
- do
- :: i < ITER ->
- acquire(lk);
- sleep(value > 0, lk);
- x = value; value = x - 1; x = 0;
- release(lk);
- i = i + 1;
- :: else ->
- break
- od;
- i = 0;
- skip
-}
-
-active[N] proctype producer()
-{
- byte i, x, w;
-
- i = 0;
- do
- :: i < ITER ->
- acquire(lk);
- x = value; value = x + 1; x = 0;
- release(lk);
- wakeup();
- i = i + 1;
- :: else ->
- break
- od;
- i = 0;
- skip
-}
-
diff --git a/spinp b/spinp
deleted file mode 100755
index db9614b..0000000
--- a/spinp
+++ /dev/null
@@ -1,16 +0,0 @@
-#!/bin/sh
-
-if [ $# != 1 ] || [ ! -f "$1" ]; then
- echo 'usage: spinp file.p' 1>&2
- exit 1
-fi
-
-rm -f $1.trail
-spin -a $1 || exit 1
-cc -DSAFETY -DREACH -DMEMLIM=500 -o pan pan.c
-pan -i
-rm pan.* pan
-if [ -f $1.trail ]; then
- spin -t -p $1
-fi
-