Fault Localization in Multi-Threaded C Programs using Bounded Model Checking (extended version)

TL;DR

This paper presents a novel approach for fault localization in multi-threaded C programs by transforming them into sequential programs and applying fault-diagnosis methods, leveraging bounded model checking to improve debugging efficiency.

Contribution

It introduces a new method that transforms multi-threaded programs into sequential ones for fault localization, extending existing techniques to handle concurrency.

Findings

Effective fault localization in multi-threaded programs

Code transformation leverages counterexamples from bounded model checkers

Sequential fault-localization methods can be adapted for multi-threaded contexts

Abstract

Software debugging is a very time-consuming process, which is even worse for multi-threaded programs, due to the non-deterministic behavior of thread-scheduling algorithms. However, the debugging time may be greatly reduced, if automatic methods are used for localizing faults. In this study, a new method for fault localization, in multi-threaded C programs, is proposed. It transforms a multi-threaded program into a corresponding sequential one and then uses a fault-diagnosis method suitable for this type of program, in order to localize faults. The code transformation is implemented with rules and context switch information from counterexamples, which are typically generated by bounded model checkers. Experimental results show that the proposed method is effective, in such a way that sequential fault-localization methods can be extended to multi-threaded programs.