Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
6885392 | Journal of Systems and Software | 2018 | 50 Pages |
Abstract
Atomicity violations are a major source of bugs in concurrent programs. Empirical studies have shown that the majority of atomicity violations are instances of the three-access pattern, where two accesses to a shared variable by a thread are interleaved by an access to the same variable by another thread. This article describes two advancements in atomicity violation detection. First, we describe a new technique that directs the execution of a dynamic analysis tool towards three-access pattern (TAP) instances. The directed search is based on constraint solving and concolic execution. We implemented this technique in a tool called AtomChase. Using 27 benchmarks comprising 5.4 million lines of Java, we compared AtomChase to five other tools. AtomChase found 20% more TAP instances than all five tools combined. Second, we show that not all TAP instances are atomicity violations and present a formally grounded approach to validating the non-atomicity of TAP instances. This approach, called HyperCV, prevents the inclusion of false positives in results presented to users. HyperCV uses a set of provably sufficient conditions for non-atomicity to efficiently validate TAP instances. Using the same benchmarks, HyperCV validated 79% of TAP instances in linear rather than exponential execution time.
Keywords
Related Topics
Physical Sciences and Engineering
Computer Science
Computer Networks and Communications
Authors
Mahdi Eslamimehr, Mohsen Lesani, George Edwards,