תוכן הקורס ומטרתו
מתכנים רבים מניחים שההתנהגויות של תכניות מקביליות, בהן מספר חוטים ניגשים בו-זמנית לזיכרון משותף, מתקבלות משזירה שרירותית של הפעולות של החוטים השונים. במציאות הנחה זו אינה נכונה. בשל אופטימזציות שמבצעים קומפיילרים והמבנה של ארכיטקטורות זיכרון מודרניות, תכניות מקביליות יכולות להתנהג בצורה שלא מתאימה לאף אחת מהשזירות האפשריות של פעולות החוטים. לימוד פורמלי של הסמנטיקה הנכונה של תכניות מקביליות היא תחום פעיל במחקר של שפות תכנות ואימות תוכנה, הידוע תחת השם "קונסיסטנטיות זיכרון חלשה" (weak memory consistency).
הקורס יציג תחום מחקר זה, ויכלול הגדרות פורמליות של מספר מודלי זיכרון בעלי קונסיסטנטיות חלשה, ותוצאות יסודיות עבורם כמו משפט ה-DRF, הוכחת נכונות של טרנספורמציות על תכניות מקביליות, תרגום ממודל אחד לאחר, ונושאים תיאורטיים ומעשיים באימות תוכנה תחת הנחת מודל זיכרון בעל קונסיסטנטיות חלשה. הקורס יכלול גם תוצאות ממחקר עדכני ואתגרים פתוחים.
הקורס מומלץ לסטודנטים המתעניינים בתיאוריה של שפות תכנות, אימות תוכנה פורמלי ומקביליות.
השתתפות בשיעורים חובה.
טרם פורסם סילבוס מפורט