Implementation detail of Revisit Monitoring

Basic idea of revisit monitoring

The idea of revisit monitoring is simple but more scalable in real world programs.  The method consists of two components: a state slicing process to determine which variables should be recorded for a state, and adaptive state recording strategy to compare the recorded states.

State slicing

Considering the case "while (a >= 7) {olda = a; a = b; b = olda + 1;}" , in which only if a < 7 , the loop can terminate. Obviously,  the variable olda is not responsible for the termination since it is a temporary variable and is not necessary to be recorded. Therefore, we make a variable slicing for the target loop to remove such redundant context. The procedure is as follows.

1.  Given a path 𝜏,  we choose all the variable in condition as a candidate state variable set, denoted as S. 

2. For each variable v  in S, we make a end to up detection to search for the variables  which affected v, denoted as v',  and add these variables into S.

3. Repeat step 2 until no new v' is found.

4. Filter out the unrelated variables from S, i.e., constant variables,  unchanged variable, and the temporary variables~(e.g., the variables allocated within the loop). Finally we can get the sliced variables as the state which will be recorded by state monitor.

Adaptive State Recording

We propose an adaptive strategy to determine the period of state recording. Our strategy is based on an interval I, where we record the states at This interval is dynamically updated based on the number of loop iterations:

Hash Algorithm

To reduce the overhead of variable comparisons, EndWatch only records  the hash value for all the sliced variables in the state. We adopt SHA-256 algorithm to make hash for sliced variables of a state. The following figure shows the hash process for a target state. Given a state with multiple variables, we first convert them to string type. Then combine them and take `\0' as connections. Finaly, we use Hash Algorithm (SHA-256) to get their hash value as a signature. The recorder only record this signature rather than a sequence of variables, by which the checker only needs to compare the hash value in each loop iteration.