סוג האירוע

בחר הכל

הרצאות פומביות

קולוקוויום

סמינרים

כנסים וימי עיון

מועדון IAP

מבחן/תחרות

צהרי יום א'

הרצאות לקהל הרחב

ימים פתוחים וייעוץ

טקסים ואירועים מיוחדים

תחום האירוע

בחר הכל

הפקולטה למדעים מדויקים

ביה"ס למדעי המתמטיקה

ביה"ס לפיזיקה ולאסטרונומיה

המועדון האסטרונומי

ביה"ס לכימיה

מרכז לחקר אינטראקציות אור חומר

פרס סאקלר במדעים הפיזיקליים - כימיה

סימפוזיונים והרצאות מיוחדות

החוג למדעי כדור הארץ

ביה"ס למדעי המחשב

ביה"ס למדעי כדור הארץ

החוג ללימודי הסביבה

The TAU Programming Languages and Systems Seminar - Predicate Abstraction for Remote Memory Access Programs

Yuri Meshman

22 באפריל 2018, 12:30 
בניין שרייבר, חדר 309 
הרצאה לקהל הרחב

Abstract:

 

 

Modern data centers provide support for Remote Memory Access (RMA) as a higher performance alternative (at a similar cost) to message passing and TCP/IP sockets. Yet, it is a Relaxed Memory Model, and programs executing under Relaxed Memory Model are very challenging to verify since they exhibit more intricate behaviors than when executed under the intuitive, concurrent interleaving, SC memory model.

We introduce a novel approach to predicate abstraction based verification and we apply it to programs running on Remote Memory

Access networks.

Remote Memory Access (RMA) networks are an excellent option for future large-scale systems programming, e.g.: MapReduce, distributed operating systems, large-scale runtime systems, but also end-user applications such as scientific computation, control systems, and other parallel applications.

 

Our approach consists of 3 steps.

First, we reduce the problem of verifying a program $P$ running on RMA to the problem of verifying a program $\overline{P}$ that captures an abstraction

of RMA as part of the program.

Second, we present a new technique for discovering both predicates and transformers that enable verification of  $\overline{P}$.

Our key concept is to automatically extrapolate the abstraction proof for sequential consistency (SC), in order to build a sound and precise abstraction of $P$ under RMA.

Third, we perform counterexample based abstraction refinement, using interpolation, for the case where abstraction is too coarse.

 

We implemented our approach and applied it to verifying several challenging concurrent algorithms under RMA. This confirms that the abstraction constructed via extrapolation is precise enough. This is the first time infinite state algorithms are verified for the RMA memory model.

 

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