Heap-based reasoning about asynchronous concurrency

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
software?
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.