תרגול אימות מערכת מקבילית

הרחיבו את המודל כך שיבדיל בין שגיאת הגשה לבין פעולה שהתקבלה. שגיאת הגשה אינה יוצרת חבילת completion, אבל צריכה ליצור תוצאה סופית אחת עבור הקורא.

הוסיפו מונה פרסום תוצאה ומצאו מסלול פגום שבו הצלחה מיידית מתפרסמת גם מתוך פונקציית ההגשה וגם מתוך חבילת completion. תקנו את המדיניות עבור מצב הודעות ההשלמה הרגיל של הפרק.

צרו טבלת בדיקות למנוע האמיתי עם לפחות שמונה סדרי אירועים מוגדרים. עבור כל בדיקה ציינו מה נשלט על ידי backend מדומה ומה דורש מערכת Windows אמיתית.

הגישו גם invariant אחד של חיים, invariant אחד של ספירה והוכחת memory order אחת. כתבו במפורש מה לא הוכח על ידי המודל, כגון התקדמות של driver או התנהגות תחת כשל חומרה.