Sagar Chaki

Sagar Chaki, Arie Gurfinkel, Ofer Strichman, Proceedings of Formal Methods in Computer-Aided Design (FMCAD), page 137-144, October 20-23, 2013, Portland, OR, USA.

Software: Tools and benchmarks for experiments reported in the paper are here. Read LICENSE.txt for the license, and README.txt for usage.

Abstract: Periodic real-time programs are ubiquitous: they control robots, radars, medical equipment, etc. They consist of a set of tasks, each of which executes (in a separate thread) a specific job, periodically. A common synchronization mechanism for such programs is via Priority Inheritance Protocol (PIP) locks. PIP locks have low programming overhead, but cause deadlocks if used incorrectly. We address the problem of verifying safety and deadlock freedom of such programs. Our approach is based on sequentialization -- converting the periodic program to an equivalent (non-deterministic) sequential program, and verifying it with a model checker. Our algorithm, called PipVerif, is iterative and optimal -- it terminates after sequentializing with the smallest number of rounds required to either find a counterexample, or prove the program safe and deadlock-free. We implemented PipVerif and validated it on a number of examples derived from a robot controller.