אימות ותזמון של מנוע עבודה מקבילי¶
נניח שבדיקה מקבילית עברה אלף פעמים. ייתכן שהקוד נכון, וייתכן שפשוט לא קיבלנו את סדר האירועים שבו הוא נשבר. שגיאות של פרסום וביטול נוטות להסתתר בחלונות קצרים, ולכן נרצה כלי שמחליף חלק מהאקראיות בחקירה שיטתית של סדרי ביצוע קטנים.
הכלי Loom מספק גרסאות בדיקה של primitives ומריץ מודל תחת סדרי תזמון שונים לפי יכולותיו. הוא אינו רואה אוטומטית כל פעולה של std, ולכן צריך להשתמש בטיפוסים המכשוריים במקום שבו רוצים לחקור אינטראקציה. נוסיף לפרויקט בדיקה את התלות הבאה.
הבדיקה הבאה נמצאת ב־tests/publication.rs. היא בודקת פרסום של נתון בעזרת release/acquire, בלי לולאת המתנה בלתי חסומה שמגדילה את מרחב החקירה ללא צורך.
use loom::sync::{Arc, atomic::{AtomicBool, AtomicUsize, Ordering}};
use loom::thread;
#[test]
fn publication_preserves_payload() {
loom::model(|| {
let state = Arc::new((AtomicUsize::new(0), AtomicBool::new(false)));
let producer_state = Arc::clone(&state);
let producer = thread::spawn(move || {
producer_state.0.store(42, Ordering::Relaxed);
producer_state.1.store(true, Ordering::Release);
});
if state.1.load(Ordering::Acquire) {
assert_eq!(state.0.load(Ordering::Relaxed), 42);
}
producer.join().unwrap();
});
}
התנאי מאפשר לקורא להגיע לפני הפרסום, ובמקרה כזה אין טענה שהוא חייב לראות תוצאה מוכנה. אם הוא כן ראה את הפרסום, הוא חייב לראות את הנתון המתאים. זאת בדיקת חוזה מדויקת יותר מהנחה שהמפיק תמיד הספיק לרוץ לפני שורה מסוימת.
שנו את ordering של הדגל ל־Relaxed והריצו שוב את המודל. אנחנו מחפשים דוגמת נגד שמתארת סדר אירועים מותר שבו ההנחה נשברת. תוצאת כלי תלויה במה שמודדנו ובגבולות החקירה, ולכן נשמור את גרסת Loom, מספר התהליכונים וההגדרות. בדיקה קטנה שעברה אינה הוכחה לכל קוד המוצר ולכל גודל קלט.
עבור תור נרצה לבדוק גם ליניאריזציה. נרשום התחלה וסיום של פעולות עם מזהים, ונבדוק אם קיימת סדרה חוקית של push ו־pop שמכבדת את יחסי הזמן שאינם חופפים. שתי פעולות שחפפו יכולות להסתדר ביותר מדרך אחת, ולכן בדיקה שמצפה לסדר הדפסה קבוע יכולה לדחות מימוש תקין או לא לזהות שגיאה אמיתית.
בדיקות תזמון ידניות משלימות את המודל. אפשר לעצור מפיק אחרי כתיבת payload ולפני פרסום, לעצור צרכן אחרי קריאה ולפני שחרור חריץ, ולבטל בזמן שמפיק מחכה לתור מלא. כל נקודה בודקת מעבר מצב מוגדר. הוספת sleep אקראי יכולה להגדיל שונות, אבל אינה מבטיחה שהגענו לחלון המסוים.
רק אחרי בדיקת נכונות נמדוד ביצועים. מנוע work stealing מחלק עבודה בין תורים מקומיים ומאפשר לעובדים לגנוב משימות, אבל הוא מוסיף שאלות של איזון, locality וחיי משימות. עבודה שחוסמת worker על קלט ופלט יכולה לפגוע בכל ההנחות של מנוע שנועד למשימות CPU קצרות. נפריד בין סוגי עבודה או נשתמש במנגנון מתאים לפי הדרישות.
יצירת יותר workers ממעבדים זמינים יכולה להוסיף context switches ותחרות על cache בלי להגדיל throughput. לעומת זאת, עבודה שחוסמת לעיתים יכולה לדרוש מדיניות אחרת. נמדוד utilization, זמני המתנה, אורך תור ו־latency של משימה, ולא נבחר מספר עובדים רק לפי מספר הליבות שכתוב על המחשב.
הרצות על ARM64 חשובות כדי לפגוש יעד עם כללי חומרה שונים, אבל גם הן אינן הוכחה למודל השפה. קוד עם ordering שגוי יכול לעבור במשך זמן רב בכל מכונה שניסינו. נשלב טיעון, מודל, בדיקות נגדיות והרצות native, ונציין מה כל כלי מסוגל לבדוק.
הכלים והגבולות מתועדים בתיעוד Loom בגרסה שנבחרה. דוח טוב כולל את רצף הכשל של הגרסה הפגומה, את השינוי שמונע אותו ואת מדידת העלות אחרי שהחוזה חזר להיות תקין.