Regression verification for multi-threaded programs (with extensions to locks and dynamic thread creation)

Abstract

Regression verification is the problem of deciding whether two similar programs are equivalent under an arbitrary yet equal context, given some definition of equivalence. So far this problem has only been studied for the case of single-threaded deterministic programs. We present a method for regression verification of multi-threaded programs. Specifically, we develop a proof-rule whose premise requires only to verify equivalence between sequential functions, whereas their consequents are equivalence of concurrent programs. This ability to avoid composing threads altogether when discharging premises, in a fully automatic way and for general programs, uniquely distinguishes our proof rule from others used for classical verification of concurrent programs. We also consider the effect of dynamic thread creation and synchronization primitives.

Appendix 1: k-equivalence of MT programs

The following is a bounded version of the partial equivalence problem for MT programs, i.e., when loops and recursion are bounded. Denote by $P^k$ the program P after all loops are unrolled k times and all recursive calls are unrolled to depth k. In $P^k$, traces that satisfy the loop guard at the last iteration, or reach a recursive call at depth $k+1$, are blocked.⁴ Let R(k) denote the I/O relation of $P^k$. Then:

Definition 10

(k-Equivalence of nondeterministic programs) Two nondeterministic programs P, $P'$ are k-equivalent if $R(k) = R'(k)$.

Since nondeterminism can be eliminated by adding inputs, we can assume that the scheduler decisions can be modeled with additional set of input variables that we denote by s. We call a valuation of s a determinization state. Let $T^k(\overline{in},\overline{s},\overline{out},\overline{v})$ denote the transition relation of $P^k$, where $\overline{in}$ is a vector of input variables, $\overline{s}$ is a vector of determinization variables, $\overline{out}$ is a vector of output variables and $\overline{v}$ is a vector of other variables. k-equivalence of P and $P'$ can be established by validating:

$$\begin{aligned} \begin{array}{l} \forall \overline{in}, \overline{s}\ \exists \overline{s}', \overline{out}, \overline{out}', \overline{v}, \overline{v}'.\ \\ \qquad T^k(\overline{in}, \overline{s}, \overline{out}, \overline{v}) \wedge T'^k(\overline{in}, \overline{s}', \overline{out}', \overline{v}') \wedge \overline{out}= \overline{out}'\;, \end{array} \end{aligned}$$

and

$$\begin{aligned} \begin{array}{l} \forall \overline{in}, \overline{s}'\ \exists \overline{s}, \overline{out}, \overline{out}', \overline{v}, \overline{v}'.\ \\ \qquad T^k(\overline{in}, \overline{s}, \overline{out}, \overline{v}) \wedge T'^k(\overline{in}, \overline{s}', \overline{out}', \overline{v}') \wedge \overline{out}= \overline{out}'\;. \end{array} \end{aligned}$$

As a small experiment, we verified the equivalence of two versions of an MT program based on this formula. Our program had four threads that read and wrote to shared variables, without loops and recursion. We sequentialized the two versions via our tool rek [1], which introduces determinization variables. We then used CBMC to convert the resulting programs to SMT-LIB format, and concatenated them. Finally, we added the quantifiers as prescribed by the two equations above, and used Z3 to discharge it. It took Z3 less than 2 s to prove that the two versions are indeed partially equivalent.