Research On Key Techniques Of Multithreaded Program Verification For Atomicity Of Correlated Variables

During the popularization of the multi-core hardware, the concurrent program has become one of the main programming model s, which utilizes the power of the parallel computation. T here are many applications on the critical safety systems such as aerospace, weapon, traffic, nuclear power, medical instrument and fina ncial management. T he safety of concurrent programs is no doubting the key factor for those applications. In concurrent pr ograms, the atomicity of correlated variables is one of the necessary constraints to be satisfied through the design and implementation. T his condition determines whether the concurrent program executes safely as designers intend ed or not. Therefore, the study of the atomicity of correlated variables is of grea t significance to assure the quality and safety of concurrent programs.This dissertation mainly addresses the key issues on the verification condition and the procedure of program verification. Firstly, the inference of verification condition is researched to retrieve the target of program verification. The research focuses on the confusion problem between the synchronization correlated variables and the atomic correlated variables. Secondly, t he procedure of program verification is studied with respect to the verification target. T he verification is achieved by checking the reachability of error states in the verification target. T he reachable program state is determined by the control dependency and the data dependency. In the control dependency, the rese arch concentrates on the general graph reachability for control flow graph, such as the reachable closure computation for non-spanning-tree edges, the integrity with cycle subgraph components and the parse of unstructured regions. In the data dependency, the research investigates the pointer alias problem, especially for the precision under demand driven strategy. In computing reachable program states, the research emphasizes the granularity of reachable states to improve the efficiency of reducing state sp ace by interpolant subsumption.Firstly, in the automatic inference of the correlated variables, to decrease the false positive rate of correlated variables, this dissertation brings forward the sub-graph mining method based on the simplified PDG. Two steps simplify PDG : the first step is to remove the control flow from PDG relaxing the constraints on the non-dependent order; the second step is to substitute the local predicate checking nodes with the uniform virtual nodes, which increases the possibility of identifying the frequent sub-graphs. After the simplification, the g Span is used to detect the frequent sub-graphs with respect to the correlated variable candidates. T hose candidates are filtered to generate the atomi c correlated variables by the post-process. In the experiment, it is concluded by manual confirmation that the correlated variables mined by simplified PDG has lower false positives than the those mined by the frequent item set algorithm.Secondly, in the graph reachability analysis for CFG:(1) T he current graph reachability algorithms aim at the general sparse and directed acyclic graphs, which do not take into account the particular characteristics of control flow graphs of programs. To solve this problem, the level linearization coding sc heme is presented to make full use of the region structure’s layered sequence to index the vertices with multi- subordinate label. This indexing scheme utilizes the merge character of the region exit vertex to avoid the transitive closure computation for s panning tree’s non-t ree edge in control flow graph. T he time and space cost of index construction is linear with respect to the control flow graph scale. In the experiment on open source benchmarks, the time cost of reachability query of the proposed metho d is similar to constant, and the index construction’s time and space cost are less than Dual Labeling and Tree Cover(2) Aiming at the lack of flow sensitivity for the structuring method based on transform, the virtual region is presented to parse the uns tructured regions. The criterion for structured regions is formalized as the match of split-join nodes. T he virtual join node is inserted in according to the conflict of split node list at join nodes. T he virtual region expresses the hidden logical structu re of unstructured program in a separate and matching form, avoiding transformation on the program. Additionally, virtual regions reserve the statement order and therefore allow the overlying dependent analysis to work directly on it.Thirdly, in pointer alias analysis, to improve the precision, this dissertation proposed a flow-sensitive demand driven pointer alias analysis. T he alias query is translated to the search problem of the pointer variable assignments satisfying the constraints on valid control flows. T he experiments have demonstrated that this presented method improved into the flow sensitivity the precision of alias analysis in demand driven with overhead tolerable.Finally, in reducing the concurrent program reachable states, to conquer the limitation of trace analysis by bounded model checking and the incompleteness of analyzing polling loop, a new symbolic execution algorithm is presented to decrease the representative traces involving loops, and enlarges reachable states of traversed interlea ving. T he traverse of interleaving is formalized as three layered abstraction: over-approximating possible interferences, generalizing the infeasible schedules by dominators and generalizing the reachable states with schedule suffix and local interpolant. T hese three layered abstraction collaborate as an incremental refinement loop to explicitly explore the search space. T he experiments illustrate the effectiveness in the reduction and the completeness in the unfolding of loops.