スケジュールを手で試しても、正しいものを当てなければバグは見つかりません。探索器はプログラムをすべてのスケジュールで実行し、すべての結果を並べ、壊したスケジュールを渡してくれます。SPYのリターン10件の上昇日を数える2つのスレッドには210通りのスケジュールがあり、正しい数になるのはそのうち10通りだけです。
スケジュールは何通りあるか
スケジュールは手番の並びで、スレッド t はちょうど lengths[t] 回の手番を取ります。並びの数を数えるには、全手番(長さの合計)を1列に並べる方法の数、つまりその階乗を考え、同じスレッドの2つの手番を入れ替えても新しいスケジュールにならないので、各スレッドの手番数の階乗で割ります。これが多項係数です。急速に増えます。2手番の2スレッドはわずか6通り、3手番の3スレッドは1,680通り、10手番の2スレッドは184,756通りです。ランダムにスケジュールを試して祈るだけでは、並行プログラムを検証できない理由です。
def count_schedules(lengths): total = factorial(sum(lengths)) for n in lengths: total //= factorial(n) return totalprint(count_schedules([2, 2]))print(count_schedules([3, 3, 3]))print(count_schedules([10, 10]))
6 1680 184756
ジェネレータとしてのスレッド
前のラボではスレッドはステップのリストでした。実際のコードは普通のPythonで書くほうが自然なので、ここからスレッドはジェネレータとします。共有辞書を受け取り、共有データにアクセスする前に毎回 yield します。すると next() を1回呼ぶごとにスレッドは次のアクセスまで進んで止まるので、1手番はちょうど、他のスレッドがインターリーブできる1ステップになります。run_threads は各ジェネレータを準備(最初の yield まで実行)し、スケジュールの各エントリが指すスレッドに手番を与え、スケジュールが終わったら未完了のスレッドをスレッド順に終わらせます。all_schedules は、最初に動くスレッドを選び、残りに再帰することで手番の並びをすべて列挙します。次は、1回ずつ増やす2つのスレッドの6通りのスケジュールです。
def all_schedules(lengths): if sum(lengths) == 0: return [[]] out = [] for tid, n in enumerate(lengths): if n: rest = list(lengths) rest[tid] -= 1 out += [[tid] + tail for tail in all_schedules(rest)] return outdef run_threads(make_threads, schedule, shared=None): shared = dict(shared or {}) threads = make_threads(shared) alive = [True] * len(threads) def turn(tid): try: next(threads[tid]) except StopIteration: alive[tid] = False for tid in range(len(threads)): turn(tid) for tid in schedule: if alive[tid]: turn(tid) while any(alive): for tid in range(len(threads)): if alive[tid]: turn(tid) return sharedtwo = lambda shared: [increments(1)(shared), increments(1)(shared)]for schedule in all_schedules([2, 2]): print(schedule, run_threads(two, schedule))
[0, 0, 1, 1] {'x': 2}
[0, 1, 0, 1] {'x': 1}
[0, 1, 1, 0] {'x': 1}
[1, 0, 0, 1] {'x': 1}
[1, 0, 1, 0] {'x': 1}
[1, 1, 0, 0] {'x': 2}6通りのうち2通りは2で終わり、残り4通りは1で終わります。良い2通りは、片方のスレッドが2ステップとも終えてから他方が始まるものです。残り4通りは、どちらかが書く前に両方が読んでしまうもので、前のラボの失われた更新そのものです。今回は推測なしに見つかりました。
探索してから問いを立てる
explore はプログラムをすべてのスケジュールで実行し、各最終状態になるスケジュールの数を数えます。キーは (名前, 値) の組をソートしたタプルで、同じ状態が同じキーになります。find_schedule はバグ報告の問いを立てます。どのスケジュールが私の不変条件を壊すか、です。最初の1つを返し、run_threads は決定的なので、再生・表示・テストへの貼り付けができます。None が返れば、すべてのスケジュールで不変条件が成り立つので、この小さなプログラムについては希望ではなく証明です。
def explore(make_threads, lengths, shared=None): outcomes = {} for schedule in all_schedules(lengths): key = tuple(sorted(run_threads(make_threads, schedule, shared).items())) outcomes[key] = outcomes.get(key, 0) + 1 return outcomesdef find_schedule(make_threads, lengths, check, shared=None): for schedule in all_schedules(lengths): if not check(run_threads(make_threads, schedule, shared)): return schedule return Noneprint(explore(two, [2, 2]))print(find_schedule(two, [2, 2], lambda shared: shared["x"] == 2))
{(('x', 2),): 2, (('x', 1),): 4}
[0, 1, 0, 1]総当たりの列挙は、スレッドあたり数手番までなら使えますが、その先で爆発します。本物の探索器は枝刈りをします。見た状態を覚え、互いに影響しないステップの並べ替えだけが違うスケジュールを飛ばします。考え方は同じなので、ここで作るものが正しいメンタルモデルです。
returns = [float(r) for r in load_bars()["close"].pct_change().dropna()][:10]ups = [sum(1 for r in returns[start::2] if r > 0) for start in (0, 1)]lengths = [2 * k for k in ups]many = lambda shared: [increments(k)(shared) for k in ups]print(ups, count_schedules(lengths))print({dict(key)["x"]: n for key, n in explore(many, lengths).items()})
[2, 3] 210
{5: 10, 4: 70, 3: 104, 2: 26}正しい答え x = 5 になるのは210通り中10通り、約5%だけです。プログラムを1回、あるいはスレッドがこのように重なることがまれな実機で100回実行するテストは、ほぼ毎回通ってもバグを出荷してしまいます。探索器は見逃せず、find_schedule が最初の犯人 [0, 0, 0, 1, 0, 1, 1, 1, 1, 1] を渡してくれます。
スケジュールによらず成り立つべきデータについての主張。並行プログラムは、不変条件がすべてのスケジュールで成り立つときに正しく、小さなケースでそれを確かめる方法が全スケジュールの探索です。
これから作るもの
ラボは講義の順に進みます。スケジュールの数、そのすべての一覧、ジェネレータのスレッドをスケジュールの下で動かすマシン、結果を数える探索器、不変条件を壊す最初のスケジュールの検索、そしてSPYの上昇日を数える2スレッドの研究です。
- 関数 · 問い前提
- count_schedules(lengths)プログラムのスケジュールは何通りか?単純な算術
- all_schedules(lengths)順に並べると?単純な算術
- run_threads(make_threads, schedule, shared)1つのスケジュールは何を残すか?単純な算術
- explore(make_threads, lengths, shared)どんな結果がどれだけ起きるか?all_schedulesrun_threads
- find_schedule(make_threads, lengths, check)最初に不変条件を壊すスケジュールは?all_schedulesrun_threads
- study(bars)SPYの計数で失敗するスケジュールはいくつか?count_schedulesexplorefind_schedule
次のトピック:探索器でバグが本物だと分かりました。次は直します。アトミック操作とRead-Modify-Writeでは、fetch-and-add や compare-and-swap のように、プロセッサが分割不能な1ステップで行える操作を加え、探索器ですべてのスケジュールでカウンタが正しいことを確かめます。
ラボ:採点される内容
6タスク · 100点- スケジュールの数10点
- すべてのスケジュール15点
- スレッドを動かす25点
- すべての結果を数える20点
- 最初の悪いスケジュール10点
- SPYの表での研究20点