全スケジュールを実行すれば小さなプログラムは証明できますが、コストはインターリーブの数だけかかります。実際のツールは2つの近道を取ります。レース検出器は1回の実行を観察し、別のスケジュールで競合しうる変数を報告します。モデル検査器は見た状態を覚えておきます。10ステップの2スレッドなら、184,756通りのスケジュールに対して状態は121個です。
トレースと問い
レース検出器はスレッドを実行しません。トレースを読みます。共有データのすべての読み書きと、ロックのすべての取得と解放です。私たちのプログラムはそのような操作のリストになり、interleave がプログラムとスケジュールをその実行のトレースに変えます。ロックなしで x をそれぞれ読み書きする2つのスレッドは、下の4つのイベントを生みます。このスケジュールではスレッド0がスレッド1の開始前に終わるので、テストは正しい答えを見ます。検出器の問いは別です。この2つのスレッドは重なりえたか、です。
def interleave(programs, schedule): position = [0] * len(programs) trace = [] for tid in schedule: kind, name = programs[tid][position[tid]] position[tid] += 1 trace.append((tid, kind, name)) return traceunlocked = [[("read", "x"), ("write", "x")], [("read", "x"), ("write", "x")]]trace = interleave(unlocked, [0, 0, 1, 1])print(trace)
[(0, 'read', 'x'), (0, 'write', 'x'), (1, 'read', 'x'), (1, 'write', 'x')]
ロックセット：この変数を守るロックは？
最初の検出器は規律を使います。共有変数はすべて、すべてのアクセスで保持されるあるロックで守られているべきです。ロックセット規則は各スレッドが保持するロックを追い、変数ごとにそのアクセス時に保持されていたロック集合の共通部分を取ります。少なくとも2つのスレッドがその変数に触れ、1つが書き、共通部分が空なら、単一のロックでは守られていません。潜在的な競合として報告します。ロックなしのカウンタは指摘され、ロックありは指摘されません。この規則は安価ですが、誤警報を出すことがあります。下の受け渡しでは、スレッド0が x を書き、ロックを通してスレッド1に渡します。書き込み時にはロックを持っていなかったので規則は文句を言いますが、実際にはアクセスは順序付けられています。
def lockset_races(trace): held = {} accesses = {} for tid, kind, name in trace: locks = held.setdefault(tid, set()) if kind == "acquire": locks.add(name) elif kind == "release": locks.discard(name) else: accesses.setdefault(name, []).append((tid, kind == "write", frozenset(locks))) racy = [] for name, history in accesses.items(): threads = {tid for tid, _, _ in history} writes = any(is_write for _, is_write, _ in history) common = frozenset.intersection(*(locks for _, _, locks in history)) if len(threads) >= 2 and writes and not common: racy.append(name) return sorted(racy)locked = [[("acquire", "m"), ("read", "x"), ("write", "x"), ("release", "m")]] * 2guarded = interleave(locked, [0, 0, 0, 0, 1, 1, 1, 1])handoff = [(0, "write", "x"), (0, "acquire", "m"), (0, "release", "m"), (1, "acquire", "m"), (1, "release", "m"), (1, "read", "x")]print("unlocked:", lockset_races(trace))print("locked: ", lockset_races(guarded))print("handoff: ", lockset_races(handoff))
unlocked: ['x'] locked: [] handoff: ['x']
2つのスレッドがアクセスし、1つが書き、すべてのアクセスで保持されているロックがない変数を報告する規則。1回の実行からロック規律の欠如を見つけますが、順序が共通ロック以外から来る場合には誤警報が出ます。
happens-before：本当に重なりうるもの
2番目の検出器は正確な問いを立てます。最初のアクセスから2番目のアクセスへ順序付けの連鎖があるか。辺は2種類で、スレッド内の順序と、同じロックのreleaseに続くacquireの対です。happens-before関係はその両方の閉包です。スレッドごとのベクタークロックは、そのスレッドが見たものを記録します。releaseはクロックをロックに保存し、acquireはそれとの要素ごとの最大を取ります。別のスレッドの先行する競合アクセスのエポックを現在のクロックが見ていなければ、そのアクセスは競合です。受け渡しでは、releaseとacquireが書き込みと読み出しをつなぐので競合はありません。報告するのは本物の競合だけですが、観察したアクセスの範囲に限られます。
def hb_races(trace): clocks = {} lock_clocks = {} history = {} racy = set() for tid, kind, name in trace: clock = clocks.setdefault(tid, {tid: 1}) if kind == "acquire": for u, value in lock_clocks.get(name, {}).items(): clock[u] = max(clock.get(u, 0), value) elif kind == "release": lock_clocks[name] = dict(clock) clock[tid] += 1 else: is_write = kind == "write" for u, was_write, epoch in history.get(name, []): if u != tid and (is_write or was_write) and clock.get(u, 0) < epoch: racy.add(name) history.setdefault(name, []).append((tid, is_write, clock[tid])) return sorted(racy)print("unlocked:", hb_races(trace))print("locked: ", hb_races(guarded))print("handoff: ", hb_races(handoff))
unlocked: ['x'] locked: [] handoff: []
ThreadSanitizerのような実際のツールは、見たトレースに誤警報が出ないhappens-beforeを使います。ロックセット規則は、誰も守っていない変数を見つけるより安価な方法で、最初の良い検査です。どちらも、正しさがロックにまったく由来しないロックフリー構造のモデル検査の代わりにはなりません。
空間の大きさは？
モデル検査器は同じプログラムを訪れますが、状態を覚えます。私たちのプログラムでは状態は各スレッドがどこまで進んだかだけなので、n ステップのスレッドなら状態は (n1 + 1) × (n2 + 1) × ... 個で、そこに至るスケジュールがいくつあっても変わりません。下のカウンタ用スレッドが実データでの数を、スケジュールと状態を並べて示します。
def count_states(lengths): total = 1 for n in lengths: total *= n + 1 return totaldef counter_programs(ups, locked): programs = [] for count in ups: program = [] for _ in range(count): program += ([("acquire", "m")] if locked else []) + [("read", "x"), ("write", "x")] + ([("release", "m")] if locked else []) programs.append(program) return programsreturns = [float(r) for r in load_bars()["close"].pct_change().dropna()][:6]ups = [sum(1 for r in returns[start::2] if r > 0) for start in (0, 1)]for name, lock in (("unlocked", False), ("locked", True)): programs = counter_programs(ups, lock) lengths = [len(p) for p in programs] trace = interleave(programs, serial_schedule(lengths)) print(name, len(trace), "events", lockset_races(trace), hb_races(trace), count_schedules(lengths), "schedules,", count_states(lengths), "states")
unlocked 8 events ['x'] ['x'] 28 schedules, 21 states locked 16 events [] [] 1820 schedules, 65 states
1本の直列トレースだけで両方の検出器が欠けたロックを見つけ、ロックありのプログラムはきれいです。モデル検査器が総当たりより有利な度合いは1,820と65の比で、これは際限なく広がります。10と10ステップなら184,756対121です。だから、単純な列挙では届かないプログラムもモデル検査なら覆えます。一方でレース検出器のコストは、1回の実行を1周するだけです。
状態は初めて到達したときに記憶し、2度展開しないこと。多くのスケジュールが同じ状態に至るので、コストはスケジュール数から状態数に下がります。
これから作るもの
ラボは講義の順に進みます。実行のトレース、ロックセット規則、ベクタークロックによるhappens-before規則、状態の数え上げ、カウンタ用スレッドのプログラム、そしてSPYの上昇日での両検出器と両空間の大きさの研究です。
- 関数 · 問い前提
- interleave(programs, schedule)何がどの順で起きたか？単純な算術
- lockset_races(trace)共通のロックがない変数は？単純な算術
- hb_races(trace)順序付けられていないアクセスがある変数は？単純な算術
- count_states(lengths)いくつの状態を覚える必要があるか？単純な算術
- counter_programs(ups, locked)カウンタ用スレッドは何をするか？単純な算術
- study(bars)SPYで検出器は一致するか？counter_programsinterleavelockset_raceshb_racescount_states
次のトピック：ロックフリーのコードにはもう1つ、後から検出器にもモデル検査器にも直せない危険があります。別のスレッドがまだ読んでいるノードを、あるスレッドが解放してしまうことです。ハザードポインタとエポックベースの回収では、メモリを安全に解放する2つの古典的な方法を作り、防いでいないスケジュールのすべてでuse-after-freeが起きることを探索器で示します。
ラボ：採点される内容
6タスク · 100点- 実行のトレース10点
- ロックセット規則25点
- ベクタークロックによるhappens-before30点
- モデル検査器の状態5点
- カウンタ用スレッド5点
- SPYの表での研究25点