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.
Thu 26 OctDisplayed time zone: Tijuana, Baja California change
15:30 - 17:00 | |||
15:30 22mTalk | A Model for Reasoning about JavaScript Promises OOPSLA Magnus Madsen University of Waterloo, Ondřej Lhoták University of Waterloo, Canada, Frank Tip Northeastern University DOI | ||
15:52 22mTalk | Robust and Compositional Verification of Object Capability Patterns OOPSLA David Swasey MPI-SWS, Germany, Deepak Garg Max Planck Institute for Software Systems, Derek Dreyer MPI-SWS DOI | ||
16:15 22mTalk | A Verified Messaging System OOPSLA DOI | ||
16:37 22mTalk | Who Guards the Guards? Formal Validation of the ARM v8-M Architecture Specification OOPSLA Alastair Reid Arm Ltd DOI |