Efficient detection and validation of atomicity violations in concurrent programs
In: Journal of Systems and Software, Jg. 137 (2018-03-01), S. 618-635
Online
unknown
Zugriff:
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.
Titel: |
Efficient detection and validation of atomicity violations in concurrent programs
|
---|---|
Autor/in / Beteiligte Person: | Edwards, George ; Lesani, Mohsen ; Eslamimehr, Mahdi |
Link: | |
Zeitschrift: | Journal of Systems and Software, Jg. 137 (2018-03-01), S. 618-635 |
Veröffentlichung: | Elsevier BV, 2018 |
Medientyp: | unknown |
ISSN: | 0164-1212 (print) |
DOI: | 10.1016/j.jss.2017.06.001 |
Schlagwort: |
|
Sonstiges: |
|