A Model for Reasoning about JavaScript Promises

In JavaScript programs, asynchrony arises in situations such as web-based user-interfaces, communicating with servers through HTTP requests, and non-blocking I/O. Event-based programming is the most popular approach for managing asynchrony, but suffers from problems such as lost events and event races, and results in code that is hard to understand and debug. Recently, ECMAScript 6 has added support for promises, an alternative mechanism for managing asynchrony that enables programmers to chain asynchronous computations while supporting proper error handling. However, JavaScript promises are complex and error-prone in their own right, so programmers would benefit from techniques that can reason about the correctness of promise-based code. Since the ECMAScript 6 specification is informal and intended for implementors of JavaScript engines, it does not provide a suitable basis for formal reasoning. This paper presents lambda_P, a core calculus that captures the essence of EcmaScript 6 promises. Based on lambda_P, we introduce the promise graph, a program representation that can assist programmers with the debugging of promise-based code. We then report on a case study in which we investigate how the promise graph can be helpful for debugging errors in promise-based code fragments reported on the StackOverflow forum. As another application of lambda_P, we systematically derive a static analysis that can be used to compute an over-approximation of the promise graph.