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 programs
Speaker:Johannes Kloos
coming from:Max Planck Institute for Software Systems
Speakers Bio:
Event Type:SWS Student Defense Talks - Thesis Defense
We use this to send out email in the morning.
Level:Public Audience
Date, Time and Location
Date:Thursday, 14 June 2018
Duration:60 Minutes
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.

This model is widely used because it provides the performance benefits of
concurrency together with easier programming than multi-threading. While
there is ample work on how to implement asynchronous programs, and
significant work on testing and model checking, little research has been
done on handling asynchronous programs that involve heap manipulation, nor
on how to automatically optimize code for asynchronous concurrency.

This thesis addresses the question of how we can reason about asynchronous
programs while considering the heap, and how to use this to optimize
programs. The work is organized along the main questions:

(i) How can we reason about asynchronous programs, without ignoring the heap?
(ii) How can we use such reasoning techniques to optimize programs involving
asynchronous behavior?
(iii) How can we transfer these reasoning and optimization techniques to other settings?

The unifying idea behind all the results in the thesis is the use of an
appropriate model encompassing global state and a promise-based model of
asynchronous concurrency. For the first question, we start from refinement
type systems for sequential programs and extend them to perform precise
resource-based reasoning in terms of heap contents, known outstanding
tasks and promises. This extended type system is known as Asynchronous
Liquid Separation Types, or ALST for short. We implement ALST in for OCaml
programs using the Lwt library.

For the second question, we consider a family of possible program
optimizations, described by a set of rewriting rules, the DWFM rules. The
rewriting rules are type-driven: We only guarantee soundness for programs
that are well-typed under ALST. We give a soundness proof based on a
semantic interpretation of ALST that allows us to show behavior inclusion
of pairs of programs.

For the third question, we address an optimization problem from industrial
practice: Normally, JavaScript files that are referenced in an HTML file
are be loaded synchronously, i.e., when a script tag is encountered, the
browser must suspend parsing, then load and execute the script, and only
after will it continue parsing HTML. But in practice, there are numerous
JavaScript files for which asynchronous loading would be perfectly sound.
First, we sketch a hypothetical optimization using the DWFM rules and a
static analysis.

To actually implement the analysis, we modify the approach to use a
dynamic analysis. This analysis, known as JSDefer, enables us to analyze
real-world web pages, and provide experimental evidence for the efficiency
of this transformation.
Video Broadcast
Video Broadcast:YesTo Location:Saarbr├╝cken
To Building:E1 5To Room:029
Tags, Category, Keywords and additional notes
Attachments, File(s):
Created:Maria-Louise Albrecht/MPI-KLSB, 05/28/2018 02:12 PM Last modified:Maria-Louise Albrecht/MPI-KLSB, 06/07/2018 09:27 AM
  • Maria-Louise Albrecht, 06/07/2018 09:27 AM
  • Maria-Louise Albrecht, 06/06/2018 10:54 AM
  • Maria-Louise Albrecht, 05/28/2018 02:38 PM -- Created document.