An Approach To Detecting Concurrency Bugs Based On Constraint Solving

To guarantee the correctness, the sequence of statements in a method or code block of concurrent programs must be atomic. An atomicity violation occurs when there is an unexpected interleaving between the execution of statements which must be atomic and statement executed by other threads and the execution result of interleaving differs from that result of atomic execution. Atomicity violation is one of the most common concurrency bug and often lead to reading and writing inconsistency or reading intermediate results and etc. Existing atomicity violation detection techniques mostly adopt a conservative concurrent program execution model, this yielding false positives and false negatives.To improve the atomicity violation detection capability, this paper presents an approach to detecting atomicity violations based on constraint solving which has a good detection capability and generally does not generate false positives. The cooperation of program control flow informations with detection process increases the interleaving space which the detecting approach can search, improves the detection capability. In the detection process, this approach firstly transforms control flow informations and the feasibility of the interleaving into a set of constraints, then solving constraints to detect atomicity violations. This paper also proposes an approximate optimization algorithm for the feasibility relaxation of branch events which is used to remove unnecessary constraints for detecting atomicity violations, reduces the time for constraint solving, improving detection efficiency.Based on the above work, this paper implements detecting atomicity violations based on constraint solving tool ConAV, and compares with concurrency bugs detection based on bug patterns tool PECAN to verify the effectiveness of ConAV. Experimental results are as follows:(1) ConAV can detect more atomicity violations than PECAN, in 14 experimental programs, ConAV detects about twice number of atomicity violations than PECAN; (2) The optimization algorithm for the feasibility relaxation of branch events reduces maximum 19%of detection time, optimizes the detection performance.