Asynchronous programs with prioritized task buffers

Formal programming models are designed to identify and isolate key features in programs. For example, pushdown systems are a natural (and popular) model for sequential recursive programs that isolate the call-return semantics of procedure calls. Isolating features allows an analysis to focus on the key challenges. For concurrent programs, the model of multithreading can sometimes be too general. Consequently, previous work has proposed a model of asynchronous programming where tasks (unit of computation) can be posted to a task buffer and are then executed in a nondeterministically chosen, but serial, order from the buffer.

Guided by real-world applications of asynchronous programming, we propose a new model that enriches the asynchronous programming model by adding two new features: multiple task-buffers and multiple task-priority levels. In our model, tasks can reside in multiple buffers and are served in priority order. Our model allows non-serial execution: tasks with higher priority can preempt tasks with a lower priority, and tasks obtained from different buffers can freely interleave with each other. Modeling these features allows analysis algorithms to detect otherwise uncaught programming errors in asynchronous programs due to inter-buffer interleaving and task-interruption, while correctly ignoring false errors due to infeasible out-of-priority-order executions.

We also give an algorithm for analyzing this new model. Given bounds that restrict inter-buffer task interleaving and intra-buffer task reordering, we give a code-to-code translation from programs in our model to sequential programs, which can then be analyzed by off-the-shelf sequential-program analysis tools. For any given parameter values, the sequential program encodes a subset of possible program behaviors, and in the limit as both parameters approach infinity, the sequential program encodes all behaviors. We demonstrate the viability of our technique by experimenting with a prototype implementation. It is competitive with state-of-the-art verification tools for concurrent programs. Our prototype is able to correctly identify programming errors in simplified asynchronous Windows device driver code, while ignoring infeasible executions.