diff options
Diffstat (limited to 'src/pkg/runtime/proc.p')
| -rw-r--r-- | src/pkg/runtime/proc.p | 526 |
1 files changed, 0 insertions, 526 deletions
diff --git a/src/pkg/runtime/proc.p b/src/pkg/runtime/proc.p deleted file mode 100644 index f0b46de61..000000000 --- a/src/pkg/runtime/proc.p +++ /dev/null @@ -1,526 +0,0 @@ -// Copyright 2011 The Go Authors. All rights reserved. -// Use of this source code is governed by a BSD-style -// license that can be found in the LICENSE file. - -/* -model for proc.c as of 2011/07/22. - -takes 4900 seconds to explore 1189070 states -with G=3, var_gomaxprocs=1 -on a Core i7 L640 2.13 GHz Lenovo X201s. - -rm -f proc.p.trail pan.* pan -spin -a proc.p -gcc -DSAFETY -DREACH -DMEMLIM'='4000 -o pan pan.c -pan -w28 -n -i -m500000 -test -f proc.p.trail && pan -r proc.p.trail -*/ - -/* - * scheduling parameters - */ - -/* - * the number of goroutines G doubles as the maximum - * number of OS threads; the max is reachable when all - * the goroutines are blocked in system calls. - */ -#define G 3 - -/* - * whether to allow gomaxprocs to vary during execution. - * enabling this checks the scheduler even when code is - * calling GOMAXPROCS, but it also slows down the verification - * by about 10x. - */ -#define var_gomaxprocs 1 /* allow gomaxprocs to vary */ - -/* gomaxprocs */ -#if var_gomaxprocs -byte gomaxprocs = 3; -#else -#define gomaxprocs 3 -#endif - -/* queue of waiting M's: sched_mhead[:mwait] */ -byte mwait; -byte sched_mhead[G]; - -/* garbage collector state */ -bit gc_lock, gcwaiting; - -/* goroutines sleeping, waiting to run */ -byte gsleep, gwait; - -/* scheduler state */ -bit sched_lock; -bit sched_stopped; -bit atomic_gwaiting, atomic_waitstop; -byte atomic_mcpu, atomic_mcpumax; - -/* M struct fields - state for handing off g to m. */ -bit m_waitnextg[G]; -bit m_havenextg[G]; -bit m_nextg[G]; - -/* - * opt_atomic/opt_dstep mark atomic/deterministics - * sequences that are marked only for reasons of - * optimization, not for correctness of the algorithms. - * - * in general any code that runs while holding the - * schedlock and does not refer to or modify the atomic_* - * fields can be marked atomic/dstep without affecting - * the usefulness of the model. since we trust the lock - * implementation, what we really want to test is the - * interleaving of the atomic fast paths with entersyscall - * and exitsyscall. - */ -#define opt_atomic atomic -#define opt_dstep d_step - -/* locks */ -inline lock(x) { - d_step { x == 0; x = 1 } -} - -inline unlock(x) { - d_step { assert x == 1; x = 0 } -} - -/* notes */ -inline noteclear(x) { - x = 0 -} - -inline notesleep(x) { - x == 1 -} - -inline notewakeup(x) { - opt_dstep { assert x == 0; x = 1 } -} - -/* - * scheduler - */ -inline schedlock() { - lock(sched_lock) -} - -inline schedunlock() { - unlock(sched_lock) -} - -/* - * canaddmcpu is like the C function but takes - * an extra argument to include in the test, to model - * "cannget() && canaddmcpu()" as "canaddmcpu(cangget())" - */ -inline canaddmcpu(g) { - d_step { - g && atomic_mcpu < atomic_mcpumax; - atomic_mcpu++; - } -} - -/* - * gput is like the C function. - * instead of tracking goroutines explicitly we - * maintain only the count of the number of - * waiting goroutines. - */ -inline gput() { - /* omitted: lockedm, idlem concerns */ - opt_dstep { - gwait++; - if - :: gwait == 1 -> - atomic_gwaiting = 1 - :: else - fi - } -} - -/* - * cangget is a macro so it can be passed to - * canaddmcpu (see above). - */ -#define cangget() (gwait>0) - -/* - * gget is like the C function. - */ -inline gget() { - opt_dstep { - assert gwait > 0; - gwait--; - if - :: gwait == 0 -> - atomic_gwaiting = 0 - :: else - fi - } -} - -/* - * mput is like the C function. - * here we do keep an explicit list of waiting M's, - * so that we know which ones can be awakened. - * we use _pid-1 because the monitor is proc 0. - */ -inline mput() { - opt_dstep { - sched_mhead[mwait] = _pid - 1; - mwait++ - } -} - -/* - * mnextg is like the C function mnextg(m, g). - * it passes an unspecified goroutine to m to start running. - */ -inline mnextg(m) { - opt_dstep { - m_nextg[m] = 1; - if - :: m_waitnextg[m] -> - m_waitnextg[m] = 0; - notewakeup(m_havenextg[m]) - :: else - fi - } -} - -/* - * mgetnextg handles the main m handoff in matchmg. - * it is like mget() || new M followed by mnextg(m, g), - * but combined to avoid a local variable. - * unlike the C code, a new M simply assumes it is - * running a g instead of using the mnextg coordination - * to obtain one. - */ -inline mgetnextg() { - opt_atomic { - if - :: mwait > 0 -> - mwait--; - mnextg(sched_mhead[mwait]); - sched_mhead[mwait] = 0; - :: else -> - run mstart(); - fi - } -} - -/* - * nextgandunlock is like the C function. - * it pulls a g off the queue or else waits for one. - */ -inline nextgandunlock() { - assert atomic_mcpu <= G; - - if - :: m_nextg[_pid-1] -> - m_nextg[_pid-1] = 0; - schedunlock(); - :: canaddmcpu(!m_nextg[_pid-1] && cangget()) -> - gget(); - schedunlock(); - :: else -> - opt_dstep { - mput(); - m_nextg[_pid-1] = 0; - m_waitnextg[_pid-1] = 1; - noteclear(m_havenextg[_pid-1]); - } - if - :: atomic_waitstop && atomic_mcpu <= atomic_mcpumax -> - atomic_waitstop = 0; - notewakeup(sched_stopped) - :: else - fi; - schedunlock(); - opt_dstep { - notesleep(m_havenextg[_pid-1]); - assert m_nextg[_pid-1]; - m_nextg[_pid-1] = 0; - } - fi -} - -/* - * stoptheworld is like the C function. - */ -inline stoptheworld() { - schedlock(); - gcwaiting = 1; - atomic_mcpumax = 1; - do - :: d_step { atomic_mcpu > 1 -> - noteclear(sched_stopped); - assert !atomic_waitstop; - atomic_waitstop = 1 } - schedunlock(); - notesleep(sched_stopped); - schedlock(); - :: else -> - break - od; - schedunlock(); -} - -/* - * starttheworld is like the C function. - */ -inline starttheworld() { - schedlock(); - gcwaiting = 0; - atomic_mcpumax = gomaxprocs; - matchmg(); - schedunlock(); -} - -/* - * matchmg is like the C function. - */ -inline matchmg() { - do - :: canaddmcpu(cangget()) -> - gget(); - mgetnextg(); - :: else -> break - od -} - -/* - * ready is like the C function. - * it puts a g on the run queue. - */ -inline ready() { - schedlock(); - gput() - matchmg() - schedunlock() -} - -/* - * schedule simulates the C scheduler. - * it assumes that there is always a goroutine - * running already, and the goroutine has entered - * the scheduler for an unspecified reason, - * either to yield or to block. - */ -inline schedule() { - schedlock(); - - mustsched = 0; - atomic_mcpu--; - assert atomic_mcpu <= G; - if - :: skip -> - // goroutine yields, still runnable - gput(); - :: gsleep+1 < G -> - // goroutine goes to sleep (but there is another that can wake it) - gsleep++ - fi; - - // Find goroutine to run. - nextgandunlock() -} - -/* - * schedpend is > 0 if a goroutine is about to committed to - * entering the scheduler but has not yet done so. - * Just as we don't test for the undesirable conditions when a - * goroutine is in the scheduler, we don't test for them when - * a goroutine will be in the scheduler shortly. - * Modeling this state lets us replace mcpu cas loops with - * simpler mcpu atomic adds. - */ -byte schedpend; - -/* - * entersyscall is like the C function. - */ -inline entersyscall() { - bit willsched; - - /* - * Fast path. Check all the conditions tested during schedlock/schedunlock - * below, and if we can get through the whole thing without stopping, run it - * in one atomic cas-based step. - */ - atomic { - atomic_mcpu--; - if - :: atomic_gwaiting -> - skip - :: atomic_waitstop && atomic_mcpu <= atomic_mcpumax -> - skip - :: else -> - goto Lreturn_entersyscall; - fi; - willsched = 1; - schedpend++; - } - - /* - * Normal path. - */ - schedlock() - opt_dstep { - if - :: willsched -> - schedpend--; - willsched = 0 - :: else - fi - } - if - :: atomic_gwaiting -> - matchmg() - :: else - fi; - if - :: atomic_waitstop && atomic_mcpu <= atomic_mcpumax -> - atomic_waitstop = 0; - notewakeup(sched_stopped) - :: else - fi; - schedunlock(); -Lreturn_entersyscall: - skip -} - -/* - * exitsyscall is like the C function. - */ -inline exitsyscall() { - /* - * Fast path. If there's a cpu available, use it. - */ - atomic { - // omitted profilehz check - atomic_mcpu++; - if - :: atomic_mcpu >= atomic_mcpumax -> - skip - :: else -> - goto Lreturn_exitsyscall - fi - } - - /* - * Normal path. - */ - schedlock(); - d_step { - if - :: atomic_mcpu <= atomic_mcpumax -> - skip - :: else -> - mustsched = 1 - fi - } - schedunlock() -Lreturn_exitsyscall: - skip -} - -#if var_gomaxprocs -inline gomaxprocsfunc() { - schedlock(); - opt_atomic { - if - :: gomaxprocs != 1 -> gomaxprocs = 1 - :: gomaxprocs != 2 -> gomaxprocs = 2 - :: gomaxprocs != 3 -> gomaxprocs = 3 - fi; - } - if - :: gcwaiting != 0 -> - assert atomic_mcpumax == 1 - :: else -> - atomic_mcpumax = gomaxprocs; - if - :: atomic_mcpu > gomaxprocs -> - mustsched = 1 - :: else -> - matchmg() - fi - fi; - schedunlock(); -} -#endif - -/* - * mstart is the entry point for a new M. - * our model of an M is always running some - * unspecified goroutine. - */ -proctype mstart() { - /* - * mustsched is true if the goroutine must enter the - * scheduler instead of continuing to execute. - */ - bit mustsched; - - do - :: skip -> - // goroutine reschedules. - schedule() - :: !mustsched -> - // goroutine does something. - if - :: skip -> - // goroutine executes system call - entersyscall(); - exitsyscall() - :: atomic { gsleep > 0; gsleep-- } -> - // goroutine wakes another goroutine - ready() - :: lock(gc_lock) -> - // goroutine runs a garbage collection - stoptheworld(); - starttheworld(); - unlock(gc_lock) -#if var_gomaxprocs - :: skip -> - // goroutine picks a new gomaxprocs - gomaxprocsfunc() -#endif - fi - od; - - assert 0; -} - -/* - * monitor initializes the scheduler state - * and then watches for impossible conditions. - */ -active proctype monitor() { - opt_dstep { - byte i = 1; - do - :: i < G -> - gput(); - i++ - :: else -> break - od; - atomic_mcpu = 1; - atomic_mcpumax = 1; - } - run mstart(); - - do - // Should never have goroutines waiting with procs available. - :: !sched_lock && schedpend==0 && gwait > 0 && atomic_mcpu < atomic_mcpumax -> - assert 0 - // Should never have gc waiting for stop if things have already stopped. - :: !sched_lock && schedpend==0 && atomic_waitstop && atomic_mcpu <= atomic_mcpumax -> - assert 0 - od -} |