Bbs: A Phase-Bounded Model Checker for Asynchronous Programs

Abstract. A popular model of asynchronous programming consists of a singlethreaded worker process interacting with a task queue. In each step of such a program, the worker takes a task from the queue and executes its code atomically to completion. Executing a task can call “normal” functions as well as post additional asynchronous tasks to the queue. Additionally, tasks can be posted to the queue by the environment. Bouajjani and Emmi introduced phase-bounding analysis on asynchronous programs with unbounded FIFO task queues, which is a systematic exploration of all program behaviors up to a fixed task phase. They showed that phase-bounded exploration can be sequentialized: given a set of recursive tasks, a task queue, and a phase bound L > 0, one can construct a sequential recursive program whose behaviors capture all states of the original asynchronous program reachable by an execution where only tasks up to phase L are executed. However, there was no empirical evaluation of ...

• Type: Journal
• Year: 2015
• Where: CAV
• Authors: Rupak Majumdar, Zilong Wang
• Keywords: CAV 2015, Hardware