Analysis of asynchronous programs with event-based synchronization

Abstract

Asynchronous event-driven programming has become a central model for building responsive and efficient software systems, from low-level kernel modules, device drivers, and embedded systems, to consumer application on platforms such as.Net, Android, iOS, as well as in the web browser. Being fundamentally concurrent, such systems are vulnerable to subtle and elusive programming errors which, in principle, could be systematically discovered with automated techniques such as model checking. However, current development of such automated techniques are based on formal models which make great simplifications in the name of analysis decidability: they ignore event-based synchronization, and they assume concurrent tasks execute serially. These simplifications can ultimately lead to false positives, in reporting errors which are infeasible considering event-based synchronization, as well as false negatives, overlooking errors which arise due to interaction between concurrent tasks. In this work, we propose a formal model of asynchronous event-driven programs which goes a long way in bridging the semantic gap between programs and existingmodels, in particular by allowing the dynamic creation of concurrent tasks, events, task buffers, and threads, and capturing precisely the interaction between these quantities.We demonstrate that (1) the analogous program analysis problems based on our new model remain decidable, and (2) that our new model is strictly more expressive than the existing Petri net based models. Our proof relies on a class of high-level Petri nets called Data Nets, whose tokens carry names taken from an infinite and linearly ordered domain. This result represents a significant expansion to the decidability frontier for concurrent program analyses.