סוג האירוע

בחר הכל

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

מבחן/תחרות

סמינרים

קולוקוויום

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

צהרי יום א'

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

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

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

מועדון קשרי אקדמיה-תעשייה

תחום האירוע

בחר הכל

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

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

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

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

ביה"ס לכימיה

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

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

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

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

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

The TAU Programming Languages and Systems Seminar - Program logics for asynchronous concurrency

Johannes Kloos, MPI-SWS

19 בנובמבר 2017, 12:30 
בניין שרייבר, חדר 309 
הרצאה לקהל הרחב

Abstract: 

Asynchronous concurrency is a model of execution that sits in between sequential and multithreaded programs. A program in this model consists of a set of tasks; at each point in time, only one task is executing, while all other tasks are kept in a task buffer. An executing task may place new tasks in the task buffer, and when a task terminates or explicitly yields control, a new task to execute is selected from the task buffer. This model underlies many forms of event-based programming, notoriously including the Javascript event model, but also device drivers in various operating system or Android apps.

 

In this talk, I will be presenting work on capturing the semantics of this concurrency model in program logics. I will start by talking about a simple extension to concurrent separation logic that captures the behavior of such programs. After that, I will show how this logic can be extended to relational reasoning: We can use it to define a logic that allows us to provide observational refinement between two asynchronous programs. In particular, we introduce the notion of /delayed refinement/; in contrast to previous notions, which (roughly) required the pair of executions to start and end at the same time, delayed refinement allows us to reason about execution pairs whose components are executed at different times.

 

Bio:

Johannes Kloos is a PhD student at the Max Planck institute for Software System (MPI-SWS) in Kaiserslautern, Germany. He received his Diplom from the University of Kaiserslautern and is about to finish his PhD with Rupak Majumdar. His research interests include concurrency, program logics and type systems on the theoretical side, and the web, especially Javascript, on the practical side.

אוניברסיטת תל-אביב, ת.ד. 39040, תל-אביב 6997801
UI/UX Basch_Interactive