לדלג לתוכן

פתרון סדרים אטומיים וגבולותיהם

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

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

המתנה לפי ערך

הפרסום החד־פעמי יכול להיכתב כך:

#include <atomic>
#include <cassert>
#include <string>
#include <thread>

int main() {
    std::string payload;
    std::atomic<bool> ready{false};
    std::jthread reader([&] {
        ready.wait(false, std::memory_order_acquire);
        assert(payload == "published");
    });
    payload = "published";
    ready.store(true, std::memory_order_release);
    ready.notify_one();
    reader.join();
}

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

שינוי שחוזר לאחור

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

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

משמעות הדוח הניסויי

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