The Yogi Project

PLDI 2012 (opens in new tab) Tutorial Presentation

Saturday, June 16, 2012, Beijing, China

Tutorial slides

• Part 1 (opens in new tab)
• Part 2 (opens in new tab)
• Part 3 (opens in new tab)

Introduction

Static analysis and testing have always had complementary strengths and weaknesses. With static analysis, we can obtain very good coverage and analyze program paths that are hard to exercise using testing, but we are forced to deal with scalability issues and false errors. With runtime testing, we can obtain only partial coverage, but the approach scales to large programs and every error that is reported is indeed realizable. Thus, attempting to combine the complementary strengths of static analysis and runtime testing is natural. For the past few years, we have been investigating methods for combining static analysis in the style of counter-example driven refinement ala SLAM, with runtime testing and automatic test case generation approaches in the style of concolic execution ala DART. Our first attempt in this direction was the Synergy algorithm [8], which handled single procedure programs with only integer variables. Then, we proposed the Dash algorithm [7], which had new ideas to handle pointer aliasing and procedure calls in programs. Subsequently, we proposed the Smash algorithm [4] that computes may and must information compositionally and also explains the analysis in the large and diverse amount of existing work in the area. More recently, we proposed the Bolt algorithm [1] that uses MapReduce style parallelism to scale up top-down interprocedural analyses. Throughout this evolution, Yogi has been our implementation vehicle to realize and evaluate these algorithms. We have spent over 4 person-years of engineering [5] to make the tool robust and usable. At this point, Yogi has been run over several hundreds of thousands of lines of C code—in particular, it is now routinely used to verify and test several properties of Windows 7 device drivers. In this tutorial, we will present a detailed account of the evolution of Yogi and our experiences engineering this tool.

Objective

Though several verification tools are finding industrial use, the “secret sauce” that makes them scalable and usable is not widely known. The main objective of this tutorial is to give researchers a comprehensive picture of what it takes to design and engineer an industrial strength property checking engine. In particular, we will give:

• A comprehensive treatment of Yogi’s main algorithms Synergy, Dash, Smash and Bolt their evolution
• Various details of how the various algorithms in the tool have been implemented
• A description of all the optimizations built into Yogi which enables the tool to scale and work on industrial strength applications
• Extensive demos that illustrate points 1, 2 and 3. We also plan to make Yogi available for download around March 2012

Description of Yogi

A detailed description of Yogi’s algorithms can be found in [7, 6, 3, 2, 1]. The goal of Yogi is to solve the property checking problem. An instance of the property checking problem consists of a sequential program P and an assertion . An answer to the property checking problem is pass if every run of P satisfies the property . The answer is fail if there exists some run of P that violates .

Static analysis and testing are complementary approaches to the property checking problem. With static analysis, we can obtain very good coverage and analyze program paths that are hard to exercise using testing, but we are forced to deal with scalability issues and false errors. With runtime testing, we can obtain only partial coverage, but the approach scales to large programs and every error that is reported is indeed realizable.

One of the unique features of Yogi is that it simultaneously searches for both a test to establish that the program violates the property, and an abstraction to establish that the program satisfies the property. If the abstraction has a path that leads to the violation of the property, Yogi attempts to focus test case generation along that path. If such a test case cannot be generated, Yogi uses information from the unsatisfiable constraint from the test case generator to refine the abstraction. Thus, the construction of test cases and abstraction proceed hand-in-hand, using error traces in the abstraction to guide test case generation, and constraints from failed test-case generation attempts to guide refinement of the abstraction.

We have engineered Yogi in such a way that it plugs into Microsoft’s Static Driver Verifier (opens in new tab) (SDV) framework. We have used this framework to run Yogi on several Windows 7 device drivers and properties.

Topics covered

• Overview of the current state-of-the-art in property checking – software model checking tools and testing tools
• Description of the Synergy, Dash, Smash and Bolt algorithms
• Architecture of Yogi and integration with Microsoft’s Static Driver Verifier (SDV) toolkit
• Engineering optimizations in Yogi – details on what works and what does not work

Target audience

The target audience includes faculty, graduate students and undergraduate students and anybody who is concerned about software reliability and program correctness.