11:00 - 11:30

• ReCBuLC: Reproducing Concurrency Bugs Using Local Clocks

  Multi-threaded programs play an increasingly important role in current multi-core environments. Exposing concurrency bugs and debugging such multi-threaded programs have become quite challenging due to their inherent non-determinism. In order to eliminate such non-determinism, many approaches such as record-and-replay and other similar bug reproducing systems have been proposed. However, those approaches often suffer significant performance degradation because they require a large amount of recorded information and/or long analysis and replay time. In this paper, we propose an effective approach, ReCBuLC, to take advantage of the hardware clocks available on modern processors. The key idea is to reduce the recording overhead and analyzing events' global order by using time stamps recorded in each thread. Those timestamps are used to determine the global orders of shared accesses. To avoid the large overhead incurred in accessing system-wide global clock, we opt to use local per-core clocks that incur much less access overhead. We then propose techniques to resolve differences among local clocks and obtain an accurate global event order. By using per-core clocks, state-of-the-art bug reproducing systems such as PRES and CLAP can reduce the recording overheads by 1% ~85%, and the analysis time by 84.66%~99.99%, respectively.

Xiang Yuan; Chenggang Wu; Zhenjiang Wang; Jianjun Li; Pen-Chung Yew; Jeff Huang; Xiaobing Feng; Yanyan Lan; Yunji Chen; Yong Guan

Chinese Academy of Sciences, China; University of Minnesota at Twin-Cities, USA; Texas A&M University, USA; Capital Normal University, China

11:30 - 12:00

• Dynamic Generation of Likely Invariants for Multithreaded Programs

  We propose a new method for dynamically generating likely invariants from multithreaded programs. While existing invariant generation tools work well on sequential programs, we found they are ineffective at reasoning about multithreaded programs both in terms of the number of real invariants generated and in terms of their usefulness in helping programmers. We address this issue by developing a new dynamic invariant generator consisting of an LLVM based code instrumentation front end, a systematic thread interleaving explorer, and a customized invariant inference engine. We show that efficient interleaving exploration strategies can be used to generate a diversified set of executions with little runtime overhead. Furthermore, we show that focusing on a small subset of thread-local transition invariants is often sufficient for reasoning about the concurrency behavior of programs. We have evaluated our new method on a set of open-source multithreaded C/C++ benchmarks. Our experiments show that our method can generate invariants that are significantly higher in quality than the previous state-of-the-art.

   

  Preprint available:

Markus Kusano; Arijit Chattopadhyay; Chao Wang

Virginia Tech, USA

12:00 - 12:30

• GPredict: Generic Predictive Concurrency Analysis

  Predictive trace analysis (PTA) is an effective approach for detecting subtle bugs in concurrent programs. Existing PTA techniques, however, are typically based on adhoc algorithms tailored to low-level errors such as data races or atomicity violations, and are not applicable to high-level properties such as "a resource must be authenticated before use" and "a collection cannot be modified when being iterated over". In addition, most techniques assume as input a globally ordered trace of events, which is expensive to collect in practice as it requires synchronizing all threads. In this paper, we present GPredict: a new technique that realizes PTA for generic concurrency properties. Moreover, GPredict does not require a global trace but only the local traces of each thread, which incurs much less runtime overhead than existing techniques. Our key idea is to uniformly model violations of concurrency properties and the thread causality as constraints over events. With an existing SMT solver, GPredict is able to precisely predict property violations allowed by the causal model. Through our evaluation using both benchmarks and real world applications, we show that GPredict is effective in expressing and predicting generic property violations. Moreover, it reduces the runtime overhead of existing techniques by 54% on DaCapo benchmarks on average.

   

  Preprint available:

Jeff Huang; Qingzhou Luo; Grigore Rosu

Texas A&M University, USA; University of Illinois at Urbana-Champaign, USA