Modern event-driven applications, such as, web pages and mobile apps, rely on asynchrony to ensure smooth end-user experience. Unfortunately, even though these applications are executed by a single event-loop thread, they can still exhibit nondeterministic behaviors depending on the execution order of interfering asynchronous events. As in classic shared-memory concurrency, this nondeterminism makes it challenging to discover errors that manifest only in specific schedules of events. In this work we propose the first stateless model checker for event-driven applications, called R4. Our algorithm systematically explores the nondeterminism in the application and concisely exposes its overall effect, which is useful for bug discovery. The algorithm builds on a combination of three key insights: (i) a dynamic partial order reduction (DPOR) technique for reducing the search space, tailored to the domain of event-driven applications, (ii) conflict-reversal bounding based on a hypothesis that most errors occur with a small number of event reorderings, and (iii) approximate replay of event sequences, which is critical for separating harmless from harmful nondeterminism. We instantiate R4 for the domain of client-side web applications and use it to analyze event interference in a number of real-world programs. The experimental results indicate that the precision and overall exploration capabilities of our system significantly exceed that of existing techniques.
Wed 28 OctDisplayed time zone: Eastern Time (US & Canada) change
10:30 - 12:00 | |||
10:30 22mTalk | Detecting Redundant CSS Rules in HTML5 Applications: A Tree Rewriting Approach OOPSLA Anthony Widjaja Lin Yale-NUS College, Singapore, Matthew Hague Royal Holloway University of London, UK, C.-H. Luke Ong University of Oxford, UK Link to publication | ||
10:52 22mTalk | SATCheck: SAT-Directed Stateless Model Checking for SC and TSO OOPSLA Link to publication | ||
11:15 22mTalk | Programming with Enumerable Sets of Structures OOPSLA Ivan Kuraj Massachusetts Institute of Technology, USA, Viktor Kunčak EPFL, Switzerland, Daniel Jackson Massachusetts Institute of Technology, USA DOI | ||
11:37 22mTalk | Stateless Model Checking of Event-Driven Applications OOPSLA Casper Svenning Jensen Aarhus University, Denmark, Anders Møller Aarhus University, Veselin Raychev ETH Zurich, Switzerland, Dimitar Dimitrov ETH Zurich, Switzerland, Martin Vechev ETH Zurich, Switzerland DOI |