Verification Of Concurrent Boolean Programs Based On Thread Transition System

With the rapid development of multi-core processors and concurrent techniques,multithreaded programming has become one of the prevailing paradigms for software development.Concurrent systems have been gradually applied to various fields of people's daily life and provided much convenience.However,the structure of concurrent systems is generally complicated,and the interleaved execution among threads may produce many subtle bugs,which is hard to find with tranditional simulation and test.Model checking is usually used to verify the correctness of concurrent systems.Since the state space of concurrent systems grows exponentially with the increase of the number of concurrent threads,it seriously restricts the effiency of model checking.Predicate abstraction techniques can effectively alleviate the state space explosion problem.It transforms a standard program into a boolean program.As a simple model for program verification,boolean programs optimizes the state space and improves the efficiency of model checking.In this paper,we focus on the reachability analysis on non-recursive concurrent boolean programs with unbounded-thread.Specific work contents are as follows:(1)Studies the basic flow of the backward search algorithm,analyzes the search strategy of the algorithm and the computation of the minimal cover predecessors.Together with the characteristics of boolean programs,we propose a deep first backward search algorithm.It optimizes the computation method of the minimal cover predecessors,and improves the efficiency of reachability analysis of concurrent Boolean programs.(2)Studies the thread transition system of concurrent Boolean programs,on the basis of the deep first backward search,we propose a reachability analysis model based on the thread transition system,which work together with the summarization method and the counter abstraction technique.The model expand the thread transition system of concurrent boolean programs through the over-approximation,then backwardly analyze each path in expanded thread transition system,and summarize the change of each local-state counters effected by the state transitions into presburger formulas.If there's a path can satisfy the formula,we called that the state is reachable.(3)We also elaborate the implemention of the three core modules in the model,including the transition expansion module,the fomula solving module and the expansion algorithm module.After the realization of the model,we verify the correctness and the efficiency of this model through a large amount of experiments.Finally,we summarize the whole work in this paper.The problems need futher improvement and research is also referred.The reachability analysis model based on the thread transition system proposed in this paper can correctly and efficiently analyze the state reachability of the concurrent boolean programs,and verify the correctness of the concurrent boolean program.