[インデックス 18302] ファイルの概要

このコミットは、Goランタイムからsrc/pkg/runtime/proc.pファイルを削除するものです。このファイルは、Goスケジューラの動作を検証するために使用されていたPromelaモデルの定義を含んでいました。

コミット

commit 0e027fca428a893ceeb49e4f833f9a923c5f201d
Author: Dmitriy Vyukov <dvyukov@google.com>
Date:   Tue Jan 21 12:49:55 2014 +0400

    runtime: delete proc.p
    It's entirely outdated today.
    
    R=golang-codereviews, bradfitz, gobot, r
    CC=golang-codereviews
    https://golang.org/cl/43500045
---
 src/pkg/runtime/proc.p | 526 -------------------------------------------------
 1 file changed, 526 deletions(-)

diff --git a/src/pkg/runtime/proc.p b/src/pkg/runtime/proc.p
deleted file mode 100644
index f0b46de611..0000000000
--- 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,\n- * 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
-}

GitHub上でのコミットページへのリンク

https://github.com/golang/go/commit/0e027fca428a893ceeb49e4f833f9a923c5f201d

元コミット内容

このコミットの元々の内容は、runtime: delete proc.p です。コミットメッセージには「It's entirely outdated today.」と簡潔に記されており、このファイルがもはやGoランタイムの現状に合致せず、不要になったことを示しています。

変更の背景

src/pkg/runtime/proc.pは、Goランタイムのスケジューラを形式的に検証するために使用されていたPromela言語で書かれたモデルファイルでした。Promelaは、並行システムのモデル検査ツールであるSPINで使用される言語です。

Goのスケジューラは、ゴルーチン（G）、論理プロセッサ（P）、OSスレッド（M）からなるM:P:Gモデルを採用しています。このモデルは、ゴルーチンを効率的にOSスレッドに割り当て、並行処理を管理するためのものです。初期のGo開発段階では、このような複雑な並行システムの正確性を保証するために、形式手法を用いた検証が試みられていました。proc.pはその一環として、スケジューラのロジックを抽象化し、デッドロックやライブネスなどの特性をSPINで検証するためのモデルとして機能していました。

しかし、Goランタイムのスケジューラは時間の経過とともに進化し、その設計や実装は初期のモデルとは大きく異なっていきました。コミットメッセージにある「It's entirely outdated today.」という記述は、このPromelaモデルが現在のGoスケジューラの複雑性や最適化を正確に反映しておらず、もはや検証ツールとしての価値を失っていたことを示唆しています。Goのスケジューラは継続的に改善されており、その検証手法も変化していったと考えられます。

前提知識の解説

Goランタイムスケジューラ (M:P:Gモデル)

Goのランタイムスケジューラは、Goプログラムの並行性を管理する上で非常に重要な役割を担っています。その中心にあるのがM:P:Gモデルです。

G (Goroutine): Goにおける軽量な実行単位です。Goキーワードを使って作成され、Goランタイムによって管理されます。OSスレッドよりもはるかに軽量で、数百万のゴルーチンを同時に実行することも可能です。
M (Machine/OS Thread): オペレーティングシステムのスレッドです。Goコードやランタイムコード、システムコールを実行する責任を持ちます。MはOSによって管理されます。
P (Processor/Context): 論理プロセッサ、またはコンテキストとも呼ばれます。MがGoコードを実行するために必要なリソース（スケジューラやメモリ割り当ての状態など）を提供します。Pの数は通常、GOMAXPROCS環境変数によって設定され、各Pは実行準備ができたゴルーチン（G）のローカル実行キューを持っています。

スケジューラの主な役割は、実行可能なゴルーチン（G）を、利用可能なOSスレッド（M）に効率的に分散させることです。MがGoコードを実行するには、Pを取得する必要があります。Pはまた、ワークスティーリング（work-stealing）を容易にします。これは、アイドル状態のPが、他のビジーなPのローカル実行キューからゴルーチンを「盗む」ことで、リソースの効率的な利用を保証するメカニズムです。

Promelaと形式検証

Promela (Process Meta Language) は、並行システムの形式検証に使用されるモデリング言語です。SPIN（Simple Promela Interpreter）というモデル検査ツールと組み合わせて使用されます。形式検証は、ソフトウェアやハードウェアの設計が特定の要件（安全性、ライブネスなど）を満たしていることを数学的に証明する手法です。

Promelaでは、システムを並行に動作するプロセス（proctype）の集合として記述します。これらのプロセスは、チャネルを介したメッセージパッシングや共有変数を通じて相互作用します。SPINは、Promelaモデルのすべての可能な状態遷移を探索し、デッドロックの発生やアサーション違反などの問題がないかをチェックします。

proc.pファイルは、Goスケジューラの主要な要素（ゴルーチン、M、P、ロック、キューなど）をPromelaの構文で抽象的に表現していました。これにより、実際のGoコードを実行することなく、スケジューラのロジックに潜在する並行性の問題を早期に発見しようとしていたと考えられます。

技術的詳細

proc.pファイルの内容を見ると、Goスケジューラの主要な概念がPromelaのプリミティブにマッピングされていることがわかります。

#define G 3: ゴルーチンの最大数を3に設定しています。これはモデル検査の探索空間を限定するためのものです。
byte gomaxprocs = 3;: GOMAXPROCSの値を設定しています。var_gomaxprocsが定義されている場合、実行中にこの値が変化する可能性もモデル化されています。
byte mwait; byte sched_mhead[G];: 待機中のM（OSスレッド）のキューを表現しています。
bit gc_lock, gcwaiting;: ガベージコレクタの状態をモデル化しています。
byte gsleep, gwait;: スリープ中または実行待ちのゴルーチンの数を表現しています。
bit sched_lock;: スケジューラのロックを表現しています。
inline lock(x) { d_step { x == 0; x = 1 } }: ロックの取得をアトミックな操作として定義しています。d_stepは、そのブロック内の操作が不可分であることをSPINに伝えます。
inline gput() / inline gget(): ゴルーチンをランキューに入れる/取り出す操作をモデル化しています。
inline entersyscall() / inline exitsyscall(): システムコールへの出入りをモデル化し、スケジューラとの相互作用を表現しています。
proctype mstart(): 新しいM（OSスレッド）のエントリポイントを定義し、ゴルーチンの実行、システムコール、ガベージコレクション、GOMAXPROCSの変更などの動作をシミュレートしています。
active proctype monitor(): スケジューラの状態を初期化し、不可能な条件（例：利用可能なプロセッサがあるのにゴルーチンが待機している）をアサート（assert 0）することで、モデルの正しさを検証しています。

このPromelaモデルは、Goスケジューラの初期の設計段階における概念的な検証を目的としていました。しかし、実際のGoランタイムは非常に動的で複雑であり、この抽象化されたモデルでは現在のスケジューラの挙動を完全に捉えることができなくなったため、削除されたと考えられます。Goのスケジューラは、ワークスティーリング、ネットワークポーラーとの統合、非同期プリエンプションなど、多くの高度な機能が追加されており、これらをPromelaで正確にモデル化し続けることは困難であったと推測されます。

コアとなるコードの変更箇所

このコミットのコアとなる変更は、単一のファイルの削除です。

src/pkg/runtime/proc.p ファイルが完全に削除されました。

これにより、526行のコードが削除されています。

コアとなるコードの解説

削除されたproc.pファイルは、GoランタイムのスケジューラをPromela言語で記述したモデルでした。このファイル自体はGoの実行可能バイナリには含まれておらず、Goランタイムのビルドプロセスの一部でもありませんでした。これは、Goスケジューラの設計段階で、その並行動作の正しさを形式的に検証するための外部ツール（SPINモデルチェッカー）で使用されるための補助的なファイルでした。

ファイルが削除されたということは、このPromelaモデルが現在のGoスケジューラの設計と乖離し、もはやその検証に役立たないと判断されたことを意味します。Goのスケジューラは継続的に最適化され、新しい機能が追加されてきたため、初期の抽象化されたモデルでは現実の複雑性を捉えきれなくなったのでしょう。

この削除は、Goランタイムのコードベースをクリーンアップし、もはやメンテナンスされていない、または関連性のないファイルを排除する一般的なプラクティスの一環と見なすことができます。

comemo