Linearizability Verification And Data Race Detection

Concurrent program execution is uncertain and the interleaving space is large,which makes it difficult to detect concurrency defects.Linear consistency is one of the criteria for the correctness of concurrent objects,and detection of linearization usually requires searching the corresponding abstract specification in an exponentially growing execution trace space.To solve this problem,a shared memory access pattern is proposed to speed up the process of linear conformance verification.The main idea is to automatically extract the memory access pattern through the correspondence between the fine grained execution trace of a few concurrent objects and the linear consistent abstract trace.The memory access pattern is the correspondence between the fine-grained shared memory access sequence and the abstract specification sequence,and the memory pattern is used to accelerate the generation of the corresponding abstract specification trace for the finegrained traces detected.This algorithm can detect the linear consistency of concurrent objects with fixed linearization points,future mechanism and help mechanism.In the experiment,the linear consistency of the six concurrent algorithms is checked.Compared with the on-the-fly refinement check algorithm,the memory access mode method has a certain advantage in time.Concurrency errors are mostly caused by data competition defects.In this paper,the convolutional neural network model is used to predict the data competition defects.Firstly,570 source programs were obtained through Git Hub search,and 570 programs with data competition defects were obtained through program variation of the obtained source programs.There were 1140 files in the dataset,1026 of which were isolated for model training and verified on 114 files.The experimental results showed that the accuracy,accuracy and recall rate reached 78.2%,72.6% and 74.1% during training.And 40 source programs that are not in the data set are predicted,which proves that the deep learning model trained in this paper can successfully detect data competition defects...