An Approach To Predicting Concurrency Bugs Based On Constraint Solving

To guarantee the correctness,shared variables which have consistency property must be guaranteed to be atomically executed in the execution of concurrent programs.If there is an unexpected interleaving between the access of shared variables which have consistency property and statements executed by other threads,and the execution result differs from the result of atomic execution,then an atomic-set serializability violation occurs.Atomic-set serializability violation is one of the most common concurrency bug and often lead to reading and writing inconsistency or lossing values and ect.Existing atomic-set serializability violation detection techniques mostly adopt conservative concurrent program models which lead to false negative and false positive.To improve the detection ability of the atomic-set serializability violation,this paper proposes an atomicset serializability violation detection method based on constraint solving.This method collects trace during program execution,and then derives other executable interleavings based on the maximal causal model and the collected trace and detects atomic-set serializability violation in these executable interleavings.This method translates the feasibility of the interleaving into a set of constraints,and transforms the detection problem of the atomic-set serializability violation into a constraint solving problem.This method takes into account program control flow informations,which expands the searchable interleaving space,and improves the tool's detection capabilities,reduces false negative rate.Due to this method is based on the constrained solution,so the solution to the atomic-set serializability violation must be true,does not generate false positives.This paper designs an atomic-set serializability violation detection tool named ASVDetector,and compared with concurrency bugs detection tool PECAN.Experimental results show that,ASVDetector can effectively detect atomic-set serializability violations,in 13 experimental programs,ASVDetector detects about twice number of atomic-set serializability violations than PECAN,which significantly reduces the false negative,and there is no false positives.Feasibility relaxation of branch events can further improve its detection ability and reduce the false negative.