Abstract
dc:description.abstractProgrammers often have to spend a significant amount of time inspecting the software code and execution traces to identify the root cause of a software bug. For a multithreaded program, debugging is even more challenging due to the subtle interactions between concurrent threads and the often astronomical number of possible interleavings. In this work, we propose a logical constraint-based symbolic analysis method to aid in the diagnosis of concurrency bugs and find their root causes, which can be later used to recommend repairs. In our method, the diagnosis process is formulated as a set of constraint solving problems. By leveraging the power of constraint satisfiability (SAT) solvers and a bounded model checker, we perform a semantic analysis of the sequential computation as well as the thread interactions. The analysis is ideally suited for handling software with small to medium code size but complex concurrency control, such as device drivers, synchronization protocols, and concurrent data structures. We have implemented our method in a software tool and demonstrated its effectiveness in diagnosing subtle concurrency bugs in multithreaded C programs.
Degree
thesis:*- Name thesis:degree_name
- Master of Science
- Level thesis:degree_level
- masters
- Discipline thesis:degree_discipline
- Computer Engineering
- Department dc:contributor.department
- Electrical and Computer Engineering
- Grantor dc:publisher
- Virginia Tech
- Year dc:date.issued
- 2015
Author and committee
dc:creator, dc:contributor.*- Author dc:creator
-
- Khoshnood, Sepideh
- Chair dc:contributor.committeechair
-
- Wang, Chao
- Committee members dc:contributor.committeemember
-
- Hsiao, Michael S.
- Ravindran, Binoy
Subjects
dc:subject × 4Rights
dc:rights- Statement dc:rights
-
- In Copyright
- Licence dc:rights.uri
Identifiers
dc:identifier.*- Dc Identifier Other
- vt_gsexam:5293
- OAI identifier oai:identifier
- oai:vtechworks.lib.vt.edu:10919/52784