Reduce explicit searching during runtime by caching the program model

McMini is an explicit-state model checker: it performs verification by repeatedly running and re-running the multi-threaded programs it verifies to explore different program outcomes. McMini constructs a model of the program and uses this model to determine how to proceed with verification.

McMini currently only preserves the transitions which produce the current state sequence. That is, given a state sequence S := s_1, s_2, ... , s_{n+1}, McMini tracks the transitions t_1, t_2, ..., t_n where t_i is the transition bringing the multi-threaded program from state s_i to s_{i+1}. If instead we cache the sequence of transitions executed by each thread, we could significantly reduce the number of explicit searching that needs to take place.

To see why, suppose McMini executes the following thread schedule:

thread 1 (1:1)
thread 1 (1:2)
thread 1 (1:3)
thread 2 (2:1)
thread 2 (2:2)
thread 2 (2:3)
thread 3 (3:1)
thread 3 (3:2)
thread 3 (3:3)

McMini will have modeled the transitions 1:1-3, 2:1-3, and 3:1-3. Suppose under DPOR we decide next to explore the following thread schedule:

thread 1 (1:1)
thread 1 (1:2)
thread 1 (1:3) <----- search 3 before 2 (e.g. 3 added to the backtrack set)
thread 3 (3:1) 
thread 3 (3:2)
thread 3 (3:3)
thread 2 (2:1)
thread 2 (2:2)
thread 2 (2:3)

That is, search all the transitions of thread 3 before thread 2. In this case, it is clear that we do not need to re-execute a binary to determine what happens with this trace: McMini already knows what will happen and only enabled-ness can be affected. By definition, transitions define the points in the program which are visible and could enable/disable other threads. Hence, every thread will run the same three transitions ever time!

Essentially, we can reduce explicit searching to cases where the future is unknown. Since the number of possible Mazurkiewicz traces that can be produced grows exponentially with thread depth, this would exponentially reduce the number of fork() system calls we made. We absolutely should attempt to do this.

In particular, we would need at most one call to fork() for every step of every thread, instead of once per branch in the state space. This is a huge savings

mcminickpt / mcmini

Reduce explicit searching during runtime by caching the program model #88