تشغيل كل الجداول يثبت برنامجًا صغيرًا لكنه يكلّف عدد التداخلات. وتسلك الأدوات الحقيقية اختصارين. كاشف التسابق يراقب تشغيلًا واحدًا ويبلغ عن المتغيرات التي قد تتسابق في جدول آخر. ومدقق النماذج يتذكر الحالات التي رآها. لخيطين من 10 خطوات يكون ذلك 184756 جدولًا مقابل 121 حالة.
أثر وسؤال
لا يشغّل كاشف التسابق خيوطًا. إنه يقرأ أثرًا: كل قراءة وكتابة للبيانات المشتركة وكل اكتساب وتحرير لقفل. تصبح برامجنا قوائم من هذه العمليات وتحوّل interleave برنامجًا وجدولًا إلى أثر ذلك التشغيل. خيطان يقرأ كل منهما x ويكتبه بلا قفل يعطيان الأحداث الأربعة أدناه. وفي هذا الجدول ينتهي الخيط 0 قبل أن يبدأ الخيط 1 فيرى الاختبار الجواب الصحيح. أما سؤال الكاشف فمختلف: هل كان يمكن أن يتداخل الخيطان؟
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')]
مجموعة الأقفال: أي قفل يحمي هذا المتغير؟
يستعمل الكاشف الأول انضباطًا: ينبغي أن يحمي كل متغير مشترك قفل ما يكون ممسوكًا عند كل وصول. تتتبع قاعدة مجموعة الأقفال الأقفال التي يمسكها كل خيط وتقاطع لكل متغير مجموعات الأقفال الممسوكة عند وصولاته. فإن لمس المتغير خيطان على الأقل وكتبه أحدهما وكان التقاطع فارغًا فلا يحميه قفل واحد: تُبلَّغ حالة تسابق محتملة. يُعلَّم العدّاد بلا قفل ولا يُعلَّم العدّاد بقفل. القاعدة رخيصة وقد تعطي إنذارًا كاذبًا. في التسليم أدناه يكتب الخيط 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']
تُبلَّغ عن متغير حين يصل إليه خيطان ويكتب أحدهما ولا يكون أي قفل ممسوكًا عند كل وصولاته. تجد غياب انضباط الأقفال من تشغيل واحد مع إنذارات كاذبة حيث يأتي الترتيب من شيء غير قفل مشترك.
يحدث قبل: ما الذي يمكن أن يتداخل فعلًا
يطرح الكاشف الثاني السؤال الدقيق: هل توجد سلسلة ترتيبات من الوصول الأول إلى الثاني؟ هناك نوعان من الأضلاع: الترتيب داخل خيط واحد والزوج تحرير ثم اكتساب للقفل نفسه. وعلاقة يحدث قبل هي الإغلاق لكليهما. ويسجّل ساعة متجهية لكل خيط ما رآه الخيط؛ يخزّن التحرير الساعة في القفل ويأخذ الاكتساب الأعظم عنصرًا بعنصر معها. والوصول تسابق إن كان لوصول سابق متعارض من خيط آخر عصر لم تره الساعة الحالية. في التسليم يصل التحرير والاكتساب الكتابة بالقراءة فلا تسابق. لا يبلّغ إلا عن التسابقات الحقيقية لكن في الوصولات التي رآها فقط.
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 علاقة يحدث قبل لأنها لا تعطي إنذارات كاذبة على الأثر الذي ترى. وقاعدة مجموعة الأقفال هي الطريقة الأرخص لإيجاد متغير لا يحميه أحد قط وفحص أول جيد. ولا تغني أيٌّ منهما عن مدقق النماذج في بنية بلا أقفال لا تأتي صحتها من الأقفال أصلًا.
ما حجم الفضاء؟
يزور مدقق النماذج البرنامج نفسه لكنه يتذكر الحالات. في برامجنا الحالة هي مدى تقدم كل خيط فقط فمع خيوط من 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
يكفي أثر تسلسلي واحد للكاشفين لإيجاد القفل الناقص والبرنامج المقفل نظيف. وميزة مدقق النماذج على القوة الغاشمة هي النسبة بين 1820 و65 وتنمو بلا حدّ: لـ10 و10 خطوات تكون 184756 مقابل 121. ولهذا يستطيع التحقق من النماذج تغطية برامج لا يبلغها التعداد البسيط أبدًا بينما يكلّف كاشف التسابق مرورًا واحدًا على تشغيل.
تذكّر حالة في أول مرة تُبلَغ ولا توسّعها أبدًا مرتين. تصل جداول كثيرة إلى الحالة نفسها فتنخفض الكلفة من عدد الجداول إلى عدد الحالات.
ما ستبنيه
يتبع المختبر الدرس: أثر تشغيل وقاعدة مجموعة الأقفال وقاعدة يحدث قبل بالساعات المتجهية وعدّ الحالات وبرامج خيوط العدّ ودراسة الكاشفين وحجمي الفضاء على أيام صعود 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
الموضوع التالي: للشيفرة بلا أقفال خطر إضافي لا يصلحه كاشف ولا مدقق بعد وقوعه: حين يحرّر خيط عقدة لا يزال خيط آخر يقرؤها. مؤشرات الخطر واسترجاع العصور تبني الطريقتين الكلاسيكيتين لتحرير الذاكرة بأمان ويُظهر المستكشف استعمالًا بعد التحرير تحت كل جدول لم تمنعه.
المختبر: ما الذي يُقيَّم
6 مهام · 100 نقطة- أثر تشغيل10 نقطة
- قاعدة مجموعة الأقفال25 نقطة
- يحدث قبل بالساعات المتجهية30 نقطة
- حالات مدقق النماذج5 نقطة
- خيوط العدّ5 نقطة
- الدراسة على جدول SPY25 نقطة