+++ /dev/null
-// 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
-}