חוזי גישה והבטחות התקדמות

נניח שמבנה נתונים אינו משתמש ב־Mutex, ולכן אנחנו קוראים לו lock-free. זאת עדיין אינה הוכחה. הוא יכול להמתין לדגל של תהליכון מסוים, להקצות דרך מקצה שנחסם או לבצע callback שנועל משאב אחר. הבטחת התקדמות היא טענה על האלגוריתם ועל ההנחות שלו, ולא על היעדר מילה מסוימת בקוד.

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

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

use std::sync::atomic::{AtomicBool, Ordering};
fn main() {
    let occupied = AtomicBool::new(false);
    std::thread::scope(|scope| {
        for _ in 0..2 {
            let occupied = &occupied;
            scope.spawn(move || {
                while occupied.compare_exchange(false, true,
                    Ordering::Acquire, Ordering::Relaxed).is_err() {
                    std::hint::spin_loop();
                }
                std::hint::black_box(123u64);
                occupied.store(false, Ordering::Release);
            });
        }
    });
}

זהו spin lock. אם התהליכון שמחזיק את true נעצר, השני אינו יכול להשלים את הרכישה. העובדה שההמתנה משתמשת רק באטומים אינה הופכת אותו ל־lock-free. יתרון אפשרי של spin קצר תלוי בתזמון ובמשך המקטע, ומול החזקה ארוכה הוא יכול לבזבז מעבד ולהחמיר תחרות.

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

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

הטיפוס UnsafeCell מאפשר לבנות הפשטה שמנהלת שינוי דרך מעטפת משותפת, אבל אינו מתיר data race. אם משתמשים בו עבור חריצי תור, צריך להוכיח שאין שתי גישות מתנגשות לאותו תא באותו זמן. החוזה של head ו־tail צריך לכלול גם wraparound, מלא מול ריק וסדר השמדה של ערכים שלא נצרכו.

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

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

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

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