SCALE: Source Code Analyzer for Locating Errors

Author: Florian, Mihai

Year: 2010

Degree: Master's thesis

Advisors: Holzmann, Gerard J.; Chandy, K. Mani

Committee Member: None, None

Option: Computer Science

DOI: 10.7907/KXWA-7Y81

Abstract

This thesis presents the design and implementation of SCALE, a tool for systematic software testing multi-threaded C applications that use the pthread library. SCALE exhaustively explores the non determinism introduced by thread schedulings and tries to find violations of safety properties. We have designed SCALE to be flexible so that it is easy to add and combine different exploration and state space reduction algorithms. In this thesis we describe the currently implemented reduction algorithms, of which the most important ones are local execution cycle detection and super step partial order reduction. To exemplify how SCALE can be used, we have applied it to a few multi-threaded applications, measured its performance and compared the results to those obtained by other tools. While checking the implementation of a non-blocking queuing algorithm, we were able to find a previously unknown bug that appears only in some unexpected thread inter-leavings.

Files