פתרון שיטת חקירה

פתרון ראשון

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

פתרון שני

הערך המרבי של מספר בלתי חתום ברוחב שישים וארבע סיביות עובר פענוח, אך אינו ניתן להכפלה בשתיים באותו טיפוס. השגיאה חוזרת אחרי רכישת המכסה ולפני ההפחתה במימוש הפגום. זהו אותו מבנה בקרה עם סיבה אחרת לכשל.

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

פתרון שלישי

נוסיף למימוש המתוקן את הבדיקה הבאה. היא משתמשת בטיפוסים שהוגדרו בהרצאה ומאמתת את האינווריאנט בנקודות מעבר.

#[test]
fn permits_match_accounting() {
    let budget = Budget { used: Cell::new(0), limit: 2 };
    let first = budget.acquire().unwrap();
    let second = budget.acquire().unwrap();
    assert_eq!(budget.used.get(), 2);
    assert!(budget.acquire().is_err());
    drop(first);
    assert_eq!(budget.used.get(), 1);
    assert!(request(&budget, "bad").is_err());
    assert_eq!(budget.used.get(), 1);
    drop(second);
    assert_eq!(budget.used.get(), 0);
    assert_eq!(request(&budget, "9"), Ok(18));
}

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