Sound and efficient concurrency bug prediction

Yan Cai, Yun Hao, Jinqiu Wang, Lei Qiao, Jens Palsberg

202127 citationsDOI

Abstract

Concurrency bugs are extremely difficult to detect. Recently, several dynamic techniques achieve sound analysis. M2 is even complete for two threads. It is designed to decide whether two events can occur consecutively. However, real-world concurrency bugs can involve more events and threads. Some can occur when the order of two or more events can be exchanged even if they occur not consecutively. We propose a new technique SeqCheck to soundly decide whether a sequence of events can occur in a specified order. The ordered sequence represents a potential concurrency bug. And several known forms of concurrency bugs can be easily encoded into event sequences where each represents a way that the bug can occur. To achieve it, SeqCheck explicitly analyzes branch events and includes a set of efficient algorithms. We show that SeqCheck is sound; and it is also complete on traces of two threads.

Topics & Concepts

ConcurrencyComputer scienceSequence (biology)Set (abstract data type)Programming languageEvent (particle physics)Isolation (microbiology)Concurrent computingTheoretical computer scienceDistributed computingGeneticsBiologyPhysicsMicrobiologyQuantum mechanicsParallel Computing and Optimization TechniquesSoftware Testing and Debugging TechniquesAdvanced Malware Detection Techniques