0On the Verification of Concurrent, Asynchronous Programs with Waiting Queues

Recently, new libraries, such as Grand Central Dispatch (GCD), have been proposed to directly harness the power of multi-core platforms and to make the development of concurrent software more accessible to software engineers. When using such a library, the programmer writes so-called blocks, which are chunks of code, and dispatches them, using synchronous or asynchronous calls, to several types of waiting queues. A scheduler is then responsible for dispatching those blocks among the available cores. Blocks can synchronize via a global memory. In this paper, we propose Queue-Dispatch Asynchronous Systems as a mathematical model that faithfully formalizes the synchronization mechanisms and the behavior of the scheduler in those systems. We study in detail their relationships to classical formalisms such as pushdown systems, Petri nets, FIFO systems, and counter systems. Our main technical contributions are precise worst-case complexity results for the Parikh coverability problem and the termination problem for several subclasses of our model. We also consider an extension of QDAS with a fork-join mechanism. Adding fork-join to any of the subclasses that we have identified leads to undecidability of the coverability problem. This motivates the study of over-approximations. Finally, we consider handmade abstractions as a practical way of verifying programs that cannot be faithfully modelled by decidable subclasses of QDAS