BarrierFinder : recognizing ad hoc barriers
- PDF / 1,891,528 Bytes
- 31 Pages / 439.642 x 666.49 pts Page_size
- 86 Downloads / 359 Views
BARRIERFINDER: recognizing ad hoc barriers Tao Wang1 · Xiao Yu1 · Zhengyi Qiu1 · Guoliang Jin1 · Frank Mueller1
© Springer Science+Business Media, LLC, part of Springer Nature 2020
Abstract Ad hoc synchronizations are pervasive in multi-threaded programs. Due to their diversity and complexity, understanding the enforced synchronization relationships of ad hoc synchronizations is challenging but crucial to multi-threaded program development and maintenance. Existing techniques can partially detect primitive ad hoc synchronizations, but they cannot recognize complete implementations or infer the enforced synchronization relationships. In this paper, we propose a framework to automatically identify complex ad hoc synchronizations in full and infer their synchronization relationships. We instantiate the framework with a tool called BARRIERFINDER, which features various techniques, including program slicing and bounded symbolic execution, to efficiently explore the interleaving space of ad hoc synchronizations within multi-threaded programs and collect execution traces. BARRIER F INDER then uses these traces to characterize ad hoc synchronizations into different types with a focus on recognizing barriers. Our evaluation shows that BARRIERFINDER is both effective and efficient in doing this, and BARRIERFINDER is also helpful for programmers to understand the correctness of their implemented ad hoc synchronizations. Keywords Ad hoc synchronizations · Barriers · Program slicing · Symbolic execution · Temporal invariants
1 Introduction 1.1 Motivation In the current multi-core era (Herb 2005; Sutter and Larus 2005), multi-threaded programming has become imperative to leverage the full power of modern CPUs. As multi-threaded Communicated by: Martin Monperrus This work was supported in part by the following grants: Air Force Office of Scientific Research AFOSR-FA9550-12-1-0442 and AFOSR-FA9550-17-1-0205, NSF 1217748 and 1525609, DOE 1403482, Lawrence Livermore National Laboratory subcontracts LLNL-B627261 and LLNL-B631308. Guoliang Jin
guoliang [email protected] Frank Mueller
[email protected] Extended author information available on the last page of the article.
Empirical Software Engineering
programs share resources across threads, programmers rely on proper synchronizations to ensure program correctness and efficiency. While a common set of standard synchronizations, such as mutex and condition variable operations, are provided by different languages or libraries, a recent study (Xiong et al. 2010) finds that programmers frequently choose not to use these standard synchronizations but implement their own ad hoc synchronizations for functionality or performance reasons. Researchers were able to find 6 to 83 ad hoc synchronizations in each of the 12 studied program suites (Xiong et al. 2010). Because of the critical role that synchronizations play in multi-threaded programs, it is important to have an accurate understanding of the semantics of synchronizations and their enforced synchronization relationships. While s
Data Loading...
