Stateless model checking of event-driven applications

4 years 6 months ago
Stateless model checking of event-driven applications
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 ...
Casper Svenning Jensen, Anders Møller, Vese
Added 16 Apr 2016
Updated 16 Apr 2016
Type Journal
Year 2015
Authors Casper Svenning Jensen, Anders Møller, Veselin Raychev, Dimitar Dimitrov, Martin T. Vechev
Comments (0)