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

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

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

מודל קטן של בעלות

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

#include <cassert>
#include <iostream>
#include <queue>
#include <string>
#include <utility>
#include <vector>

struct State {
    bool cancel = false;
    bool completed = false;
    bool consumed = false;
    bool destroyed = false;
};

struct Node {
    State state;
    std::vector<std::string> path;
};

bool find_failure(bool buggy) {
    std::queue<Node> pending;
    pending.push({{}, {"submitted"}});
    while (!pending.empty()) {
        Node node = std::move(pending.front());
        pending.pop();
        const auto state = node.state;
        if (state.destroyed && !state.consumed) {
            for (const auto& step : node.path) std::cout << step << ' ';
            std::cout << '\n';
            return true;
        }
        if (state.destroyed) continue;
        auto add = [&](State next, const char* label) {
            auto path = node.path;
            path.emplace_back(label);
            pending.push({next, std::move(path)});
        };
        if (!state.cancel && !state.consumed) {
            auto next = state;
            next.cancel = true;
            add(next, "cancel-requested");
        }
        if (!state.completed) {
            auto next = state;
            next.completed = true;
            add(next, "kernel-completed");
        }
        if (state.completed && !state.consumed) {
            auto next = state;
            next.consumed = true;
            add(next, "completion-consumed");
        }
        if (state.consumed || (buggy && state.cancel)) {
            auto next = state;
            next.destroyed = true;
            add(next, "destroyed");
        }
    }
    return false;
}

int main() {
    assert(find_failure(true));
    assert(!find_failure(false));
}

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

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

הוכחות קטנות לפני עומס גדול

נרשום invariants שניתנים לבחינה: כל בקשה פעילה רשומה פעם אחת; כל חבילת completion מתאימה לבקשה חיה; מספר ההשלמות הסופיות אינו עובר את מספר ההגשות שהתקבלו; ו־buffer אינו חוזר למאגר לפני תוצאתו הסופית. עבור תור SPSC נוסיף את שתי שרשראות הפרסום ואת הגבלת מספר היצרנים והצרכנים.

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

הזרקת כשל בגבול הנכון

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

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

הפרעת תזמון ועומס

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

כלי בדיקת races או model checker צריכים להתאים לשפה, לספרייה ולפלטפורמה. אין להניח שכלי מסוים תומך בכל גרסת MSVC, ב־WinAPI או בקורוטינות. אפשר לבדוק רכיב C++ טהור במודל מתאים, ואז לבדוק את גבול Windows בניסויים נפרדים. היקף הכלי נרשם לצד המסקנה.

דוח שאפשר להשתמש בו

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

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

קריאה להעמקה

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