Testing and verification of concurrent programs is hard, as it requires reasoning about all the ways in which operations executed by different processes (or threads) can interfere. Model checking [7, 16] addresses this problem by systematically exploring the state space of a given program and verifying that each reachable state satisfies a given property. A problem in applying model checking to realistic programs is to capture and storing a large number of global states. Two approaches for coping with this problem are abstraction and stateless model checking. Abstraction techniques construct a sound overapproximation ofthe state-transition graph, which can then be tractably analyzed. A pioneering work by Graf and Saidi [12] showed how infinite-state systems can be automatically verified in this way. Stateless model checking (SMC) [11] explores the state space of the program without explicitly storing global states. The technique requires taking control of the scheduler and subsequently executing the program multiple times, each time imposing a different scheduling of the processes. By considering every process at every execution step, however, the number of possible schedulings grows exponentially wrt. the total length of program execution. Consequently, a number of techniques for reducing this number, without unnecessarily sacrificing coverage, have been developed. The most prominent is Partial order reduction (POR) [8, 10, 15, 17], adapted to SMC as Dynamic POR (DPOR) [9], which exploits the fact that schedulings with the same ordering of dependent operations can be regarded as belonging to the same equivalence class (sometimes called a Mazurkiewicz trace), and that it is sufficient to explore one of them. In recent years, several techniques have been develop that further increase the efficiency of stateless model checking. One approach has been to develop techniques that are optimal in the sense that they explore exactly one scheduling in each Mazurkiewicz trace [2]. Corresponding minimization techniques for classical (stateful) model checking were pioneered by Graf and Steffen [13]. Other approaches are based on the observation that the notion of Mazurkiewicz trace is unnecessarily refined for the purpose of determining the outcome of a program scheduling. Hence, coarser equivalences have been defined: e.g., based on mapping each read operation to the corresponding write operation that produces its value [6, 14]. For such coarser equivalences, the question of developing optimal exploration algorithms becomes interesting. In this presentation, we will survey some recent developments and results for making stateless model checking more efficient, also considering different memory models for concurrency [1, 3, 5, 4]. It builds on joint work with Parosh Aziz Abdulla, Stavros Aronis, Mohamed Faouzi Atig, Carl Leonardsson, Magnus Ling, Tuan Phong Ngo, and Konstantinos Sagonas.
展开▼
