Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Heap-based reasoning about asynchronous concurrency
Speaker:Johannes Kloos
coming from:Max Planck Institute for Software Systems
Speakers Bio:
Event Type:SWS Student Defense Talks - Thesis Proposal
We use this to send out email in the morning.
Level:Public Audience
Date, Time and Location
Date:Thursday, 27 October 2016
Duration:-- Not specified --
Asynchronous concurrency is a wide-spread way of writing programs that
deal with many short tasks. It is the programming model behind event-driven
concurrency, as exemplified by GUI applications, where the tasks correspond to event
handlers, web applications based around JavaScript, the implementation of web browsers,
but also of server-side software or operating systems. It provides a middle-ground
between sequential programming and multi-threading, giving the benefits of concurrency while
being easier to program than multi-threading.

While there are languages and libraries that make the construction of
asynchronous programs relatively simple, there is little support for asynchronous
program analysis. Existing working is mostly focused on model checking or performing
specific targeted analyses. The model checking techniques in particular have turned out to
be inefficient and completely ignore the heap.
In this thesis proposal, I will address the question of how we can reason
about asynchronous programs, and how I want to use this to optimize asynchronous programs.
I will address three main questions:
1.      How can we reason about asynchronous programs, without ignoring
the heap?
2.      How can we use such reasoning techniques to optimize programs
involving asynchronous behavior?
3.      How can we scale reasoning and optimization to apply to real-world
In the proposal, I will describe answers to all three questions. The
unifying idea behind all of these results is the use of a appropriate model of global state
(usually, the heap) and a promise-based model of asynchronous concurrency.

To address the first question, I will describe some prior work (ALST,
ECOOP 2015), where we extended the OCaml type system to reason about asynchronous
concurrency. To address the second and third question, I will describe an ongoing project
(JSDefer) about optimization web pages by loading JavaScript asynchronously, and a planned project
about an automated optimization step for OCaml programs to use change synchronous to
asynchronous I/O operations safely.

Video Broadcast
Video Broadcast:YesTo Location:Saarbrücken
To Building:E1 5To Room:105
Meeting ID:
Tags, Category, Keywords and additional notes
Attachments, File(s):

Maria-Louise Albrecht/MPI-KLSB, 12/22/2016 02:45 PM
Last modified:
Maria-Louise Albrecht/MPI-KLSB, 12/22/2016 02:52 PM
  • Maria-Louise Albrecht, 12/22/2016 02:52 PM -- Created document.