Research On Multi-threading Formal Modeling And Deadlock Detection Based On Extended CSP

With POSIX Threads(POSIX Threads,Pthreads)being widely used in various complex concurrent systems,deadlock problems caused by threads competing for resources or pushing the wrong order are becoming more and more common.Deadlocks can cause multi-threading programs to crash or terminate abnormally,which will have catastrophic consequences for industries with high security requirements,so it is of critical importance to effectively detect potential deadlocks in POSIX multi-threading programs.In recent years,the mainstream deadlock detection methods mainly include formal model static deadlock detection analysis and dynamic deadlock detection.Compared with the dynamic deadlock detection,the static deadlock detection based on formal model analysis is highly praised by many scholars because it has perfect mathematical theory and can detect potential deadlock in the program before the software system is compiled.However,there are still some problems in this method that need to be researched:(1)The semantic description of formal language and multi-threading program is very different,and the possibility to directly implement the mapping of multi-threading program semantics to formal models is little;(2)When modeling multi-threadingprograms using formal language,it is easy to make huge model,so that state space explosion will occur in the model detection phase;(3)it is difficult to establish a formal model of equivalent semantics for multi-threading program pointers.Aiming at the above problems,this paper proposes a new method for automatic modeling and deadlock detection of POSIX multi-threading programs based on extended CSP(extended CSP,CSP#),the main work is following:Firstly,a method for mapping POSIX multi-threading programs to CSP#model is proposed.According to the connection between multi-threading program and CSP# modeling language,C++CSP framework language is introduced as a “bridge”,and mapping relation between multi-threading program and C++CSP framework language,mapping relation between C++CSP framework language and CSP# are established respectively.Thus,equivalent semantic mapping of multithreaded programs to CSP# models can be realized.Secondly,based on the independent change and trace theory,a Simplified CSP# Model Algorithm(SCMA)is proposed.By combining the continuous independent transitions of the CSP# model,the number of model transition sequences is reduced,which effectively alleviates the problem of model detection state space explosion.Thirdly,based on pointer alias analysis technology,a Stack Dereference Equivalent Replacement Algorithm(SDERA)is proposed to solve the inconformity of variables description between multi-threading program and CSP# model.Simultaneously,the automatic modeling tool supporting POSIXmulti-threading program,thr2CSP#Tool is designed and implemented,and the PAT(Process Analysis Toolkit)tool is used to automatically perform deadlock detection analysis on the established formal model.Based on the uniform distribution of code size and the use of Pthreads for concurrent operations,this paper selects TCP_server,OpenSSL-server,threadpool,Pfscan,bzip2 smp as test cases.The test cases are analyzed respectively for modeling and model detection.The experimental results show that the proposed method can quickly construct CSP# model for multi-threading programs,and can effectively detect the potential deadlocks,which is suitable for deadlock detection for large-scale multi-threading programs.