פתרון אימות מערכת מקבילית

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

כדי למצוא השלמה כפולה, נגדיר מונה published שמתחיל באפס. בגרסה הפגומה הצלחה מיידית מגדילה אותו, ובהמשך צריכת החבילה מגדילה אותו שוב. התנאי published גדול מאחד הוא הפרת החוזה. בגרסה המתוקנת, בתצורת הודעות רגילה, הצלחה מיידית אינה מפרסמת תוצאה; רק ה־dispatcher עושה זאת.

סדרי אירועים שימושיים

בדיקה ראשונה מחזירה שגיאת הגשה לפני שנוצרה פעולה פעילה. בדיקה שנייה מקבלת פעולה ומשלימה אותה מיד לתור, אבל צורכת את החבילה מאוחר יותר. בדיקה שלישית מבקשת ביטול לפני ההשלמה. בדיקה רביעית מבקשת ביטול אחרי שההשלמה כבר ממתינה בתור.

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

ה־backend המדומה שולט בסדר האירועים ובכשלי הקצאה והגשה. מערכת Windows אמיתית נדרשת כדי לבדוק שיוך handle ל־IOCP, תרגום ערכי ההחזרה, חיי OVERLAPPED והתנהגות קובץ קצר. אי אפשר להחליף את הבדיקה הזאת במודל שמניח מראש שהתרגום נכון.

שלוש הוכחות נפרדות

הוכחת החיים אומרת שכל בקשה שהתקבלה נשארת בבעלות המנוע עד צריכת חבילתה. הוכחת הספירה אומרת שהפרש הגשות שהתקבלו והשלמות שנצרכו שווה למספר הפעולות הפעילות. הוכחת סדר הזיכרון בתור SPSC אומרת שכתיבת התא קודמת לפרסום head עם release, וקריאת head עם acquire קודמת לקריאת התא.

המודל אינו מוכיח ש־driver מסוים יגיב לביטול בזמן מוגבל. הוא גם אינו מודל מלא של cache או של תקן C++. ההצהרה על הגבולות אינה חולשה בדוח; היא מונעת שימוש במסקנה מעבר למה שבאמת נבדק.