בדיקות מודל והזרקת תקלות

לבדוק את המעבר ולא רק את התוצאה הנוחה

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

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

פורמט קטן שאפשר לנתח עד הסוף

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

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

use std::io::{self, Write};

fn checksum(bytes: &[u8]) -> u8 {
    bytes.iter().fold(0_u8, |sum, byte| sum.wrapping_add(*byte))
}

fn append<W: Write>(writer: &mut W, payload: &[u8]) -> io::Result<()> {
    if payload.len() > 64 { return Err(io::Error::other("payload too large")); }
    writer.write_all(&[payload.len() as u8])?;
    writer.write_all(payload)?;
    writer.write_all(&[checksum(payload)])?;
    Ok(())
}

fn recover(bytes: &[u8]) -> (Vec<Vec<u8>>, usize) {
    let mut records = Vec::new();
    let mut offset = 0;
    while let Some(&length) = bytes.get(offset) {
        let length = length as usize;
        if length > 64 { break; }
        let Some(end) = offset.checked_add(length + 2) else { break; };
        let Some(record) = bytes.get(offset..end) else { break; };
        let body = &record[1..1 + length];
        if record[1 + length] != checksum(body) { break; }
        records.push(body.to_vec());
        offset = end;
    }
    (records, offset)
}

struct FaultWriter { bytes: Vec<u8>, remaining: usize }
impl Write for FaultWriter {
    fn write(&mut self, input: &[u8]) -> io::Result<usize> {
        if input.is_empty() { return Ok(0); }
        if self.remaining == 0 { return Err(io::Error::other("injected write failure")); }
        let count = input.len().min(self.remaining).min(3);
        self.bytes.extend_from_slice(&input[..count]);
        self.remaining -= count;
        Ok(count)
    }
    fn flush(&mut self) -> io::Result<()> { Ok(()) }
}

fn main() -> io::Result<()> {
    let mut base = Vec::new();
    append(&mut base, b"old")?;
    let new = b"new-data";
    let complete_size = new.len() + 2;
    for budget in 0..=complete_size {
        let mut writer = FaultWriter { bytes: base.clone(), remaining: budget };
        let result = append(&mut writer, new);
        let (records, valid) = recover(&writer.bytes);
        if budget < complete_size {
            assert!(result.is_err());
            assert_eq!(records, vec![b"old".to_vec()]);
            assert_eq!(valid, base.len());
        } else {
            result?;
            assert_eq!(records, vec![b"old".to_vec(), new.to_vec()]);
            assert_eq!(valid, writer.bytes.len());
        }
        println!("budget={budget} bytes={} valid={valid}", writer.bytes.len());
    }
    Ok(())
}

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

מהו מימוש ייחוס שימושי

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

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

רצף פעולות ומשמעות ההמשך

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

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

כשל כתיבה אינו כשל עמידות

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

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

הזרקה לפי השאלה

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

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

תזמון ומודלים של מקביליות

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

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

תוצאה שניתן לשחזר

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

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