From e6276088107e814bea95aee42868065dc41c1e8b Mon Sep 17 00:00:00 2001 From: Frans Kaashoek Date: Wed, 24 Jul 2019 09:05:05 -0400 Subject: [PATCH] Delete a few other no-longer relevant files --- TRICKS | 140 ------------------------------------------------------- cuth | 48 ------------------- pr.pl | 36 -------------- printpcs | 14 ------ show1 | 3 -- sign.pl | 19 -------- sleep1.p | 134 ---------------------------------------------------- spinp | 16 ------- 8 files changed, 410 deletions(-) delete mode 100644 TRICKS delete mode 100755 cuth delete mode 100755 pr.pl delete mode 100755 printpcs delete mode 100755 show1 delete mode 100755 sign.pl delete mode 100644 sleep1.p delete mode 100755 spinp 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 = ; - 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 -