Testing, runtime verification, and analysis of concurrent programs

Luo, Qingzhou

Permalink

https://hdl.handle.net/2142/87955 Copy

Description

Title

Testing, runtime verification, and analysis of concurrent programs

Author(s)

Luo, Qingzhou

Issue Date

2015-06-02

Director of Research (if dissertation) or Advisor (if thesis)

Rosu, Grigore

Doctoral Committee Chair(s)

Rosu, Grigore

Committee Member(s)

• Marinov, Darko
• Xie, Tao
• Havelund, Klaus

Department of Study

Computer Science

Discipline

Computer Science

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

Ph.D.

Degree Level

Dissertation

Keyword(s)

• Runtime verification
• concurrency
• testing

Abstract

With the development of multi-core processors, concurrent programs are becoming more and more popular. Among several models, the multithreaded shared-memory model is the predominant programming paradigm for developing concurrent programs. However, because of non-deterministic scheduling, multithreaded code is hard to develop and test. Concurrency bugs, such as data races, atomicity violations, and deadlocks, are hard to detect and fix in multithreaded programs. To test and verify multithreaded programs, two sets of techniques are needed. The first one is to enforce thread schedules and runtime properties efficiently. Being able to enforce desired thread schedules and runtime properties would greatly help developers to develop reliable multithreaded code. The second one is to explore the state space of multithreaded programs efficiently. Systematic state-space exploration could guarantee correctness for mul- tithreaded code, however, it is usually time consuming and thus infeasible in most cases. This dissertation presents several techniques to address challenges arising in testing and runtime verification of multithreaded programs. The first two techniques are the IMUnit framework for enforcing testing schedules and the EnforceMOP system for enforcing runtime properties for multithreaded programs. An experimental evaluation shows that our techniques can enforce thread schedules and runtime properties effectively and efficiently, and have their own advantages over existing techniques. The other techniques are the RV-Causal framework and the CAPP technique in the ReEx framework for efficient state-space exploration of multithreaded code. RV-Causal employs the idea of the maximal causal model for state-space exploration in a novel way to reduce the exploration cost, without losing the ability to detect certain types of concurrency bugs. The results show that RV-Causal outperforms existing techniques by finding concurrency bugs and exploring the entire state space much more efficiently.

Graduation Semester

2015-8

Type of Resource

text

Permalink

http://hdl.handle.net/2142/87955

Copyright and License Information

Copyright 2015 Qingzhou Luo

Owning Collections