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.

In  Foundations of Software Engineering (FSE)

Details

Previous Versions

Michael Emmi, Akash Lal, and Shaz Qadeer. Asynchronous programs with prioritized task buffers, January 2012.