Research On Data Race And Atomicity Of Aerospace C Programs With Multiple Interruptions

In Aerospace C programs with multiple interruptions, the interleaving of interruptions may cause some unexpected interleaving executions and even wrong execution results. A kind of frequently occurred errors is that data race and the atomicity of programs is violated because of shared variables. It has realistic significance to solve this kind of problem for ensuring the correctness of Aerospace and other safety strict requirements software.The goal of this thesis is to explore the technique of checking data race and atomicity of Aerospace C programs with multiple interruptions. Firstly we present a data race and atomicity analysis method based on abstract interpretation. This analysis method, which is suit for checking atomicity of C programs without lock synchronic mechanism, checks the atomicity of software from the relation of concurrent accessing shared variables. This analysis is complete for data race and atomicity analysis, i.e. there will be no data race or violate atomicity ignored. Secondly, in order to deal with the high complexity of the execution of interrupt program, improve the efficient of analysis process, we introduce an optimize method based on function summary. This optimization analysis can not only reduce the state space which is needed to traverse in the static analysis but also still hold the analysis completeness. Finally, we design and implement a data race and atomicity prototype checker named MIDAC. The experimental results demonstrate its effectiveness on several large scale practical programs.