Heap-based reasoning about asynchronous programs
Max Planck Institute for Software Systems
SWS Student Defense Talks - Thesis Defense
14 Jun 2018, 5:00 pm - 6:00 pm
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
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
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
(iii) How can we transfer these reasoning and optimization techniques to other
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
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
First, we sketch a hypothetical optimization using the DWFM rules and a
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.