Imported Upstream version 60upstream/60

1 files changed, 526 insertions, 0 deletions

diff --git a/src/pkg/runtime/proc.p b/src/pkg/runtime/proc.p
new file mode 100644
index 000000000..f0b46de61
--- /dev/null
+++ b/src/pkg/runtime/proc.p
@@ -0,0 +1,526 @@
+// 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
+}