Software Model Checking with Explicit Scheduler and Symbolic Threads

摘要

In many practical application domains, the software is organized into a setof threads, whose activation is exclusive and controlled by a cooperativescheduling policy: threads execute, without any interruption, until they eitherterminate or yield the control explicitly to the scheduler. The formal verification of such software poses significant challenges. On theone side, each thread may have infinite state space, and might call forabstraction. On the other side, the scheduling policy is often important forcorrectness, and an approach based on abstracting the scheduler may result inloss of precision and false positives. Unfortunately, the translation of theproblem into a purely sequential software model checking problem turns out tobe highly inefficient for the available technologies. We propose a software model checking technique that exploits the intrinsicstructure of these programs. Each thread is translated into a separatesequential program and explored symbolically with lazy abstraction, while theoverall verification is orchestrated by the direct execution of the scheduler.The approach is optimized by filtering the exploration of the scheduler withthe integration of partial-order reduction. The technique, called ESST (Explicit Scheduler, Symbolic Threads) has beenimplemented and experimentally evaluated on a significant set of benchmarks.The results demonstrate that ESST technique is way more effective than softwaremodel checking applied to the sequentialized programs, and that partial-orderreduction can lead to further performance improvements.