חזרה

סילבוס

מספר קורס 0368-4217-01
שם הקורס סמנטיקה של זיכרון משותף
יחידה אקדמית הפקולטה למדעים מדויקים ע"ש ריימונד ובברלי סאקלר -
מדעי המחשב
מרצה פרופ' אורי להבצרו קשר
צור קשר דוא"ל: orilahav@tauex.tau.ac.il
שעות קבלה בתאום מראשבניין: בניין צ'ק פוינט , חדר: 234
אופן ההוראה שיעור
שעות סמסטריאליות 3
סמסטר ב' תשפ"א
יום ד
שעות 10:00-13:00
בניין
חדר
אין סילבוס

תוכן הקורס ומטרתו

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

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

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

השתתפות בשיעורים חובה.



טרם פורסם סילבוס מפורט
מטלות הקורס

עבודת בית

ייתכנו מטלות נוספות
רשימת המטלות המלאה תופיע בסילבוס המפורט של הקורס.

קורסי קדם נדרשיםמודלים חישוביים (03682200) +יס. פורמל. של שפות תכנות (03683241)
קורסים מקבילים
לוגיקה (03682194)

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



tau logohourglass00:00