syz-verifier: redesigned the analysis program generation and analysis flow (#2908)

Program verification logic is located in one function now.
VMs fetch programs from priority queues, not from the generator.
VMs operate the tasks, not programs now.
For the crashed VM - return error for every program in the queue
*fixed some road errors

10 files changed, 802 insertions, 802 deletions

diff --git a/syz-verifier/execresult.go b/syz-verifier/execresult.go
index d3db18882..9db053a35 100644
--- a/syz-verifier/execresult.go
+++ b/syz-verifier/execresult.go
@@ -21,9 +21,34 @@ type ExecResult struct {
 	// in the generated programs.
 	Info ipc.ProgInfo
 	// Crashed is set to true if a crash occurred while executing the program.
+	// TODO: is not used properly. Crashes are just an errors now.
 	Crashed bool
+	// Source task ID is used to route result back to the caller.
+	ExecTaskID int64
+	// To signal the processing errors.
+	Error error
+}
+
+func (l *ExecResult) IsEqual(r *ExecResult) bool {
+	if l.Crashed || r.Crashed {
+		return false
+	}
+
+	lCalls := l.Info.Calls
+	rCalls := r.Info.Calls
+
+	if len(lCalls) != len(rCalls) {
+		return false
+	}
 
-	RunIdx int
+	for i := 0; i < len(lCalls); i++ {
+		if lCalls[i].Errno != rCalls[i].Errno ||
+			lCalls[i].Flags != rCalls[i].Flags {
+			return false
+		}
+	}
+
+	return true
 }
 
 type ResultReport struct {
@@ -31,6 +56,8 @@ type ResultReport struct {
 	Prog string
 	// Reports contains information about each system call.
 	Reports []*CallReport
+	// Mismatch says whether the Reports differ.
+	Mismatch bool
 }
 
 type CallReport struct {
@@ -69,30 +96,10 @@ func (s ReturnState) String() string {
 	return state
 }
 
-// VeifyRerun compares the results obtained from rerunning a program with what
-// was reported in the initial result report.
-func VerifyRerun(res []*ExecResult, rr *ResultReport) bool {
-	for idx, cr := range rr.Reports {
-		for _, r := range res {
-			var state ReturnState
-			if r.Crashed {
-				state = ReturnState{Crashed: true}
-			} else {
-				ci := r.Info.Calls[idx]
-				state = ReturnState{Errno: ci.Errno, Flags: ci.Flags}
-			}
-			if state != cr.States[r.Pool] {
-				return false
-			}
-		}
-	}
-	return true
-}
-
-// Verify checks whether the Results of the same program, executed on different
-// kernels, are the same. If that's not the case, it returns a ResultReport,
-// highlighting the differences.
-func Verify(res []*ExecResult, prog *prog.Prog, s *Stats) *ResultReport {
+// CompareResults checks whether the ExecResult of the same program,
+// executed on different kernels, are the same.
+// It returns s ResultReport, highlighting the differences.
+func CompareResults(res []*ExecResult, prog *prog.Prog) *ResultReport {
 	rr := &ResultReport{
 		Prog: string(prog.Serialize()),
 	}
@@ -100,7 +107,6 @@ func Verify(res []*ExecResult, prog *prog.Prog, s *Stats) *ResultReport {
 	// Build the CallReport for each system call in the program.
 	for idx, call := range prog.Calls {
 		cn := call.Meta.Name
-		s.Calls[cn].Occurrences++
 
 		cr := &CallReport{
 			Call:   cn,
@@ -119,7 +125,6 @@ func Verify(res []*ExecResult, prog *prog.Prog, s *Stats) *ResultReport {
 		rr.Reports = append(rr.Reports, cr)
 	}
 
-	var send bool
 	pool0 := res[0].Pool
 	for _, cr := range rr.Reports {
 		for _, state := range cr.States {
@@ -127,13 +132,10 @@ func Verify(res []*ExecResult, prog *prog.Prog, s *Stats) *ResultReport {
 			// the pools that executed the program are the same
 			if state0 := cr.States[pool0]; state0 != state {
 				cr.Mismatch = true
-				send = true
+				rr.Mismatch = true
 			}
 		}
 	}
 
-	if send {
-		return rr
-	}
-	return nil
+	return rr
 }
diff --git a/syz-verifier/execresult_test.go b/syz-verifier/execresult_test.go
index aae7bcdac..bddd91042 100644
--- a/syz-verifier/execresult_test.go
+++ b/syz-verifier/execresult_test.go
@@ -10,7 +10,62 @@ import (
 	"github.com/google/syzkaller/prog"
 )
 
-func TestVerify(t *testing.T) {
+func TestIsEqual(t *testing.T) {
+	tests := []struct {
+		name string
+		res  []*ExecResult
+		want bool
+	}{
+		{
+			name: "only crashes",
+			res: []*ExecResult{
+				makeExecResultCrashed(1),
+				makeExecResultCrashed(4),
+			},
+			want: false,
+		},
+		{
+			name: "mismatch because result and crash",
+			res: []*ExecResult{
+				makeExecResultCrashed(1),
+				makeExecResult(2, []int{11, 33, 22}, []int{1, 3, 3}...),
+			},
+			want: false,
+		},
+		{
+			name: "mismatches because of diffent length",
+			res: []*ExecResult{
+				makeExecResult(2, []int{11, 33}, []int{1, 3}...),
+				makeExecResult(4, []int{11, 33, 22}, []int{1, 3, 3}...)},
+			want: false,
+		},
+		{
+			name: "mismatches not found",
+			res: []*ExecResult{
+				makeExecResult(2, []int{11, 33, 22}, []int{1, 3, 3}...),
+				makeExecResult(4, []int{11, 33, 22}, []int{1, 3, 3}...)},
+			want: true,
+		},
+		{
+			name: "mismatches found in results",
+			res: []*ExecResult{
+				makeExecResult(1, []int{1, 3, 2}, []int{4, 7, 7}...),
+				makeExecResult(4, []int{1, 3, 5}, []int{4, 7, 3}...),
+			},
+			want: false,
+		}}
+
+	for _, test := range tests {
+		t.Run(test.name, func(t *testing.T) {
+			got := test.res[0].IsEqual(test.res[1])
+			if diff := cmp.Diff(test.want, got); diff != "" {
+				t.Errorf("ExecResult.IsEqual failure (-want +got):\n%s", diff)
+			}
+		})
+	}
+}
+
+func TestCompareResults(t *testing.T) {
 	p := "breaks_returns()\n" +
 		"minimize$0(0x1, 0x1)\n" +
 		"test$res0()\n"
@@ -54,6 +109,7 @@ func TestVerify(t *testing.T) {
 						4: returnState(22, 3)},
 						Mismatch: true},
 				},
+				Mismatch: true,
 			},
 		},
 		{
@@ -76,6 +132,7 @@ func TestVerify(t *testing.T) {
 					{Call: "minimize$0", States: map[int]ReturnState{1: {Errno: 3, Flags: 7}, 4: {Errno: 3, Flags: 7}}},
 					{Call: "test$res0", States: map[int]ReturnState{1: {Errno: 2, Flags: 7}, 4: {Errno: 5, Flags: 3}}, Mismatch: true},
 				},
+				Mismatch: true,
 			},
 		}}
 
@@ -86,8 +143,7 @@ func TestVerify(t *testing.T) {
 			if err != nil {
 				t.Fatalf("failed to deserialise test program: %v", err)
 			}
-			stats := emptyTestStats()
-			got := Verify(test.res, prog, stats)
+			got := CompareResults(test.res, prog)
 			if diff := cmp.Diff(test.wantReport, got); diff != "" {
 				t.Errorf("Verify report mismatch (-want +got):\n%s", diff)
 			}
diff --git a/syz-verifier/exectask.go b/syz-verifier/exectask.go
new file mode 100644
index 000000000..052469ed7
--- /dev/null
+++ b/syz-verifier/exectask.go
@@ -0,0 +1,141 @@
+// Copyright 2021 syzkaller project authors. All rights reserved.
+// Use of this source code is governed by Apache 2 LICENSE that can be found in the LICENSE file.
+
+package main
+
+import (
+	"container/heap"
+	"sync"
+	"sync/atomic"
+	"time"
+
+	"github.com/google/syzkaller/pkg/rpctype"
+	"github.com/google/syzkaller/prog"
+)
+
+type EnvDescr int64
+
+const (
+	AnyEnvironment EnvDescr = iota
+	NewEnvironment
+	// TODO: add CleanVMEnvironment support.
+
+	EnvironmentsCount
+)
+
+// ExecTask is the atomic analysis entity. Once executed, it could trigger the
+// pipeline propagation fof the program.
+type ExecTask struct {
+	CreationTime   time.Time
+	Program        *prog.Prog
+	ID             int64
+	ExecResultChan ExecResultChan
+
+	priority int // The priority of the item in the queue.
+	// The index is needed by update and is maintained by the heap.Interface methods.
+	index int // The index of the item in the heap.
+}
+
+func (t *ExecTask) ToRPC() *rpctype.ExecTask {
+	return &rpctype.ExecTask{
+		Prog: t.Program.Serialize(),
+		ID:   t.ID,
+	}
+}
+
+var (
+	ChanMapMutex           = sync.Mutex{}
+	TaskIDToExecResultChan = map[int64]ExecResultChan{}
+	TaskCounter            = int64(-1)
+)
+
+type ExecResultChan chan *ExecResult
+
+func MakeExecTask(prog *prog.Prog) *ExecTask {
+	task := &ExecTask{
+		CreationTime:   time.Now(),
+		Program:        prog,
+		ExecResultChan: make(ExecResultChan),
+		ID:             atomic.AddInt64(&TaskCounter, 1),
+	}
+
+	ChanMapMutex.Lock()
+	defer ChanMapMutex.Unlock()
+	TaskIDToExecResultChan[task.ID] = task.ExecResultChan
+
+	return task
+}
+
+func DeleteExecTask(task *ExecTask) {
+	ChanMapMutex.Lock()
+	defer ChanMapMutex.Unlock()
+	delete(TaskIDToExecResultChan, task.ID)
+}
+
+func GetExecResultChan(taskID int64) ExecResultChan {
+	ChanMapMutex.Lock()
+	defer ChanMapMutex.Unlock()
+
+	return TaskIDToExecResultChan[taskID]
+}
+
+func MakeExecTaskQueue() *ExecTaskQueue {
+	return &ExecTaskQueue{
+		pq: make(ExecTaskPriorityQueue, 0),
+	}
+}
+
+// ExecTaskQueue respects the pq.priority. Internally it is a thread-safe PQ.
+type ExecTaskQueue struct {
+	pq ExecTaskPriorityQueue
+}
+
+// PopTask return false if no tasks are available.
+func (q *ExecTaskQueue) PopTask() (*ExecTask, bool) {
+	if q.pq.Len() == 0 {
+		return nil, false
+	}
+
+	return heap.Pop(&q.pq).(*ExecTask), true
+}
+
+func (q *ExecTaskQueue) PushTask(task *ExecTask) {
+	heap.Push(&q.pq, task)
+}
+
+func (q *ExecTaskQueue) Len() int {
+	return q.pq.Len()
+}
+
+// ExecTaskPriorityQueue reused example from https://pkg.go.dev/container/heap
+type ExecTaskPriorityQueue []*ExecTask
+
+func (pq ExecTaskPriorityQueue) Len() int { return len(pq) }
+
+func (pq ExecTaskPriorityQueue) Less(i, j int) bool {
+	// We want Pop to give us the highest, not lowest, priority so we use greater than here.
+	return pq[i].priority > pq[j].priority
+}
+
+func (pq ExecTaskPriorityQueue) Swap(i, j int) {
+	pq[i], pq[j] = pq[j], pq[i]
+	pq[i].index = i
+	pq[j].index = j
+}
+
+func (pq *ExecTaskPriorityQueue) Push(x interface{}) {
+	n := len(*pq)
+	item := x.(*ExecTask)
+	item.index = n
+	*pq = append(*pq, item)
+}
+
+func (pq *ExecTaskPriorityQueue) Pop() interface{} {
+	old := *pq
+	n := len(old)
+	item := old[n-1]
+	old[n-1] = nil  // avoid memory leak
+	item.index = -1 // for safety
+	*pq = old[0 : n-1]
+	return item
+}
diff --git a/syz-verifier/main.go b/syz-verifier/main.go
index d17d01437..7ecbaa76b 100755
--- a/syz-verifier/main.go
+++ b/syz-verifier/main.go
@@ -8,11 +8,9 @@ package main
 import (
 	"flag"
 	"io"
-	"math/rand"
 	"os"
 	"path/filepath"
 	"strconv"
-	"time"
 
 	"github.com/google/syzkaller/pkg/log"
 	"github.com/google/syzkaller/pkg/mgrconfig"
@@ -35,33 +33,11 @@ type poolInfo struct {
 	cfg      *mgrconfig.Config
 	pool     *vm.Pool
 	Reporter *report.Reporter
-	//  runners keeps track of what programs have been sent to each Runner.
-	//  There is one Runner executing per VM instance.
-	runners map[int]runnerProgs
-	// progs stores the programs that haven't been sent to this kernel yet but
-	// have been sent to at least one other kernel.
-	progs []*progInfo
-	// toRerun stores the programs that still need to be rerun by this kernel.
-	toRerun []*progInfo
 	// checked is set to true when the set of system calls not supported on the
 	// kernel is known.
 	checked bool
 }
 
-type progInfo struct {
-	prog       *prog.Prog
-	idx        int
-	serialized []byte
-	res        [][]*ExecResult
-	// received stores the number of results received for this program.
-	received int
-
-	runIdx int
-	report *ResultReport
-}
-
-type runnerProgs map[int]*progInfo
-
 func main() {
 	var cfgs tool.CfgsFlag
 	flag.Var(&cfgs, "configs", "[MANDATORY] list of at least two kernel-specific comma-sepatated configuration files")
@@ -154,7 +130,6 @@ func main() {
 		if err != nil {
 			log.Fatalf("failed to create reporter for instance-%d: %v", idx, err)
 		}
-		pi.runners = make(map[int]runnerProgs)
 	}
 
 	calls := make(map[*prog.Syscall]bool)
@@ -172,7 +147,6 @@ func main() {
 		target:        target,
 		calls:         calls,
 		reasons:       make(map[*prog.Syscall]string),
-		rnd:           rand.New(rand.NewSource(time.Now().UnixNano() + 1e12)),
 		runnerBin:     runnerBin,
 		executorBin:   execBin,
 		addr:          addr,
@@ -183,15 +157,14 @@ func main() {
 		reruns:        *flagReruns,
 	}
 
-	vrf.srv, err = startRPCServer(vrf)
-	if err != nil {
-		log.Fatalf("failed to initialise RPC server: %v", err)
-	}
+	vrf.Init()
 
+	vrf.StartProgramsAnalysis()
 	vrf.startInstances()
 
 	monitor := MakeMonitor()
 	monitor.SetStatsTracking(vrf.stats)
+
 	// TODO: move binding address to configuration
 	log.Logf(0, "run the Monitor at http://127.0.0.1:8080/")
 	go monitor.ListenAndServe("127.0.0.1:8080")
diff --git a/syz-verifier/main_test.go b/syz-verifier/main_test.go
index 1dfefaa61..197daa285 100644
--- a/syz-verifier/main_test.go
+++ b/syz-verifier/main_test.go
@@ -1,555 +1,3 @@
 // Copyright 2021 syzkaller project authors. All rights reserved.
 // Use of this source code is governed by Apache 2 LICENSE that can be found in the LICENSE file.
 package main
-
-import (
-	"bytes"
-	"os"
-	"path/filepath"
-	"strings"
-	"testing"
-
-	"github.com/google/go-cmp/cmp"
-	"github.com/google/syzkaller/pkg/osutil"
-	"github.com/google/syzkaller/pkg/rpctype"
-	"github.com/google/syzkaller/prog"
-)
-
-func TestNewProgram(t *testing.T) {
-	tests := []struct {
-		name                           string
-		pool, vm, retProgIdx, srvProgs int
-	}{
-		{
-			name:       "doesn't generate new program",
-			pool:       1,
-			vm:         1,
-			retProgIdx: 3,
-			srvProgs:   2,
-		},
-		{
-			name:       "generates new program",
-			pool:       2,
-			vm:         2,
-			retProgIdx: 4,
-			srvProgs:   3,
-		},
-	}
-	for _, test := range tests {
-		t.Run(test.name, func(t *testing.T) {
-			srv := createTestServer(t)
-			srv.pools = map[int]*poolInfo{
-				1: {
-					runners: map[int]runnerProgs{
-						1: {1: {}},
-					},
-					progs: []*progInfo{{idx: 3}},
-				},
-				2: {runners: map[int]runnerProgs{
-					2: {1: {}}},
-					progs: []*progInfo{},
-				},
-			}
-
-			srv.progs = map[int]*progInfo{
-				1: {idx: 1},
-				3: {idx: 3},
-			}
-
-			_, gotProgIdx, _ := srv.newProgram(test.pool, test.vm)
-			if gotProgIdx != test.retProgIdx {
-				t.Errorf("srv.newProgram returned idx: got %d, want %d", gotProgIdx, test.retProgIdx)
-			}
-
-			if got, want := len(srv.progs), test.srvProgs; got != want {
-				t.Errorf("len(srv.progs): got %d, want %d", got, want)
-			}
-		})
-	}
-}
-
-func TestNewResult(t *testing.T) {
-	tests := []struct {
-		name      string
-		idx       int
-		wantReady bool
-	}{
-		{
-			name:      "Results ready for verification",
-			idx:       3,
-			wantReady: true,
-		},
-		{
-			name:      "No results ready for verification",
-			idx:       1,
-			wantReady: false,
-		},
-	}
-	for _, test := range tests {
-		t.Run(test.name, func(t *testing.T) {
-			srv := createTestServer(t)
-			srv.pools = map[int]*poolInfo{0: {}, 1: {}}
-			srv.progs = map[int]*progInfo{
-				1: {idx: 1,
-					res: func() [][]*ExecResult {
-						res := make([][]*ExecResult, 1)
-						res[0] = make([]*ExecResult, 2)
-						return res
-					}(),
-				},
-				3: {idx: 3,
-					res: func() [][]*ExecResult {
-						res := make([][]*ExecResult, 1)
-						res[0] = make([]*ExecResult, 2)
-						res[0][1] = &ExecResult{Pool: 1}
-						return res
-					}(),
-					received: 1,
-				},
-			}
-			gotReady := srv.newResult(&ExecResult{Pool: 0}, srv.progs[test.idx])
-			if test.wantReady != gotReady {
-				t.Errorf("srv.newResult: got %v want %v", gotReady, test.wantReady)
-			}
-		})
-	}
-}
-
-func TestConnect(t *testing.T) {
-	srv := createTestServer(t)
-	srv.pools = map[int]*poolInfo{
-		1: {
-			runners: map[int]runnerProgs{
-				0: {1: {idx: 1}},
-			},
-			progs: []*progInfo{{
-				idx: 3}},
-		}}
-	a := &rpctype.RunnerConnectArgs{
-		Pool: 1,
-		VM:   1,
-	}
-	r := &rpctype.RunnerConnectRes{}
-	if err := srv.Connect(a, r); err != nil {
-		t.Fatalf("srv.Connect failed: %v", err)
-	}
-	if diff := cmp.Diff(&rpctype.RunnerConnectRes{CheckUnsupportedCalls: true}, r); diff != "" {
-		t.Errorf("Connect result mismatch (-want +got):\n%s", diff)
-	}
-	want, got := map[int]runnerProgs{
-		0: {1: {idx: 1}},
-		1: {},
-	}, srv.pools[a.Pool].runners
-	if diff := cmp.Diff(want, got, cmp.AllowUnexported(progInfo{})); diff != "" {
-		t.Errorf("srv.progs[a.Name] mismatch (-want +got):\n%s", diff)
-	}
-}
-
-func TestFinalizeCallSet(t *testing.T) {
-	target, err := prog.GetTarget("test", "64")
-	if err != nil {
-		t.Fatalf("failed to initialise test target: %v", err)
-	}
-
-	vrf := Verifier{
-		target: target,
-		reasons: map[*prog.Syscall]string{
-			target.SyscallMap["test$res0"]:  "foo",
-			target.SyscallMap["minimize$0"]: "bar",
-		},
-		calls: map[*prog.Syscall]bool{
-			target.SyscallMap["minimize$0"]: true,
-			target.SyscallMap["test$res0"]:  true,
-			target.SyscallMap["disabled1"]:  true,
-		},
-		reportReasons: true,
-	}
-
-	out := bytes.Buffer{}
-	vrf.finalizeCallSet(&out)
-	wantLines := []string{
-		"The following calls have been disabled:\n",
-		"\ttest$res0: foo\n",
-		"\tminimize$0: bar\n",
-	}
-	output := out.String()
-	for _, line := range wantLines {
-		if !strings.Contains(output, line) {
-			t.Errorf("finalizeCallSet: %q missing in reported output", line)
-		}
-	}
-
-	wantCalls, gotCalls := map[*prog.Syscall]bool{
-		target.SyscallMap["disabled1"]: true,
-	}, vrf.calls
-	if diff := cmp.Diff(wantCalls, gotCalls); diff != "" {
-		t.Errorf("srv.calls mismatch (-want +got):\n%s", diff)
-	}
-}
-
-func TestUpdateUnsupported(t *testing.T) {
-	target, err := prog.GetTarget("test", "64")
-	if err != nil {
-		t.Fatalf("failed to initialise test target: %v", err)
-	}
-
-	tests := []struct {
-		name           string
-		vrfPools       map[int]*poolInfo
-		wantPools      map[int]*poolInfo
-		wantCalls      map[*prog.Syscall]bool
-		wantNotChecked int
-		nilCT          bool
-	}{
-		{
-			name:           "choice table not generated",
-			vrfPools:       map[int]*poolInfo{0: {}, 1: {}},
-			wantPools:      map[int]*poolInfo{0: {checked: true}, 1: {}},
-			wantNotChecked: 1,
-			wantCalls: map[*prog.Syscall]bool{
-				target.SyscallMap["minimize$0"]:     true,
-				target.SyscallMap["breaks_returns"]: true,
-				target.SyscallMap["test$res0"]:      true,
-				target.SyscallMap["test$union0"]:    true,
-			},
-			nilCT: true,
-		},
-		{
-			name:           "choice table generated",
-			vrfPools:       map[int]*poolInfo{0: {}},
-			wantPools:      map[int]*poolInfo{0: {checked: true}},
-			wantNotChecked: 0,
-			wantCalls: map[*prog.Syscall]bool{
-				target.SyscallMap["minimize$0"]:     true,
-				target.SyscallMap["breaks_returns"]: true,
-			},
-			nilCT: false,
-		},
-	}
-
-	for _, test := range tests {
-		t.Run(test.name, func(t *testing.T) {
-			vrf := Verifier{
-				target:        target,
-				pools:         test.vrfPools,
-				reasons:       make(map[*prog.Syscall]string),
-				reportReasons: true,
-				calls: map[*prog.Syscall]bool{
-					target.SyscallMap["minimize$0"]:     true,
-					target.SyscallMap["breaks_returns"]: true,
-					target.SyscallMap["test$res0"]:      true,
-					target.SyscallMap["test$union0"]:    true,
-				},
-				stats: MakeStats(),
-			}
-			srv, err := startRPCServer(&vrf)
-			if err != nil {
-				t.Fatalf("failed to initialise RPC server: %v", err)
-			}
-
-			a := &rpctype.UpdateUnsupportedArgs{
-				Pool: 0,
-				UnsupportedCalls: []rpctype.SyscallReason{
-					{ID: target.SyscallMap["test$res0"].ID, Reason: "foo"},
-					{ID: target.SyscallMap["csource1"].ID, Reason: "bar"},
-					{ID: target.SyscallMap["test$union0"].ID, Reason: "tar"},
-				}}
-			if err := srv.UpdateUnsupported(a, nil); err != nil {
-				t.Fatalf("srv.UpdateUnsupported failed: %v", err)
-			}
-
-			if diff := cmp.Diff(test.wantPools, srv.pools, cmp.AllowUnexported(poolInfo{})); diff != "" {
-				t.Errorf("srv.pools mismatch (-want +got):\n%s", diff)
-			}
-
-			wantReasons := map[*prog.Syscall]string{
-				target.SyscallMap["test$res0"]:   "foo",
-				target.SyscallMap["test$union0"]: "tar",
-			}
-			if diff := cmp.Diff(wantReasons, vrf.reasons); diff != "" {
-				t.Errorf("srv.reasons mismatch (-want +got):\n%s", diff)
-			}
-
-			if diff := cmp.Diff(test.wantCalls, vrf.calls); diff != "" {
-				t.Errorf("srv.calls mismatch (-want +got):\n%s", diff)
-			}
-
-			if want, got := test.wantNotChecked, srv.notChecked; want != got {
-				t.Errorf("srv.notChecked: got %d want %d", got, want)
-			}
-
-			if want, got := test.nilCT, vrf.choiceTable == nil; want != got {
-				t.Errorf("vrf.choiceTable == nil: want nil, got: %v", srv.vrf.choiceTable)
-			}
-		})
-	}
-}
-
-func TestUpdateUnsupportedNotCalledTwice(t *testing.T) {
-	vrf := Verifier{
-		pools: map[int]*poolInfo{
-			0: {runners: map[int]runnerProgs{0: nil, 1: nil}, checked: false},
-			1: {runners: map[int]runnerProgs{}, checked: false},
-		},
-	}
-	srv, err := startRPCServer(&vrf)
-	if err != nil {
-		t.Fatalf("failed to initialise RPC server: %v", err)
-	}
-	a := &rpctype.UpdateUnsupportedArgs{Pool: 0}
-
-	if err := srv.UpdateUnsupported(a, nil); err != nil {
-		t.Fatalf("srv.UpdateUnsupported failed: %v", err)
-	}
-	if want, got := 1, srv.notChecked; want != got {
-		t.Errorf("srv.notChecked: got %d want %d", got, want)
-	}
-
-	if err := srv.UpdateUnsupported(a, nil); err != nil {
-		t.Fatalf("srv.UpdateUnsupported failed: %v", err)
-	}
-	if want, got := 1, srv.notChecked; want != got {
-		t.Fatalf("srv.UpdateUnsupported called twice")
-	}
-
-	wantPools := map[int]*poolInfo{
-		0: {runners: map[int]runnerProgs{0: nil, 1: nil}, checked: true},
-		1: {runners: map[int]runnerProgs{}, checked: false},
-	}
-	if diff := cmp.Diff(wantPools, srv.pools, cmp.AllowUnexported(poolInfo{}, progInfo{})); diff != "" {
-		t.Errorf("srv.pools mismatch (-want +got):\n%s", diff)
-	}
-}
-
-func TestProcessResults(t *testing.T) {
-	tests := []struct {
-		name      string
-		res       []*ExecResult
-		prog      string
-		wantExist bool
-		wantStats *Stats
-	}{
-		{
-			name: "report written",
-			res: []*ExecResult{
-				makeExecResult(0, []int{1, 3, 2}),
-				makeExecResult(1, []int{1, 3, 5}),
-			},
-			wantExist: true,
-			wantStats: &Stats{
-				TotalMismatches: 1,
-				TotalProgs:      1,
-				Calls: map[string]*CallStats{
-					"breaks_returns": makeCallStats("breaks_returns", 1, 0, map[ReturnState]bool{}),
-					"test$res0":      makeCallStats("test$res0", 1, 1, map[ReturnState]bool{{Errno: 2}: true, {Errno: 5}: true}),
-					"minimize$0":     makeCallStats("minimize$0", 1, 0, map[ReturnState]bool{}),
-				},
-			},
-		},
-		{
-			name: "no report written",
-			res: []*ExecResult{
-				makeExecResult(0, []int{11, 33, 22}),
-				makeExecResult(1, []int{11, 33, 22}),
-			},
-			wantStats: &Stats{
-				TotalProgs: 1,
-				Calls: map[string]*CallStats{
-					"breaks_returns": makeCallStats("breaks_returns", 1, 0, map[ReturnState]bool{}),
-					"minimize$0":     makeCallStats("minimize$0", 1, 0, map[ReturnState]bool{}),
-					"test$res0":      makeCallStats("test$res0", 1, 0, map[ReturnState]bool{}),
-				},
-			},
-		},
-	}
-	for _, test := range tests {
-		t.Run(test.name, func(t *testing.T) {
-			prog := getTestProgram(t)
-			pi := &progInfo{
-				prog: prog,
-				res: func() [][]*ExecResult {
-					res := make([][]*ExecResult, 1)
-					res[0] = test.res
-					return res
-				}()}
-			vrf := Verifier{
-				resultsdir: makeTestResultDirectory(t),
-				stats:      emptyTestStats(),
-			}
-			resultFile := filepath.Join(vrf.resultsdir, "result-0")
-
-			vrf.processResults(pi)
-
-			if diff := cmp.Diff(test.wantStats, vrf.stats); diff != "" {
-				t.Errorf("vrf.stats mismatch (-want +got):\n%s", diff)
-			}
-
-			if got, want := osutil.IsExist(resultFile), test.wantExist; got != want {
-				t.Errorf("osutil.IsExist report file: got %v want %v", got, want)
-			}
-			os.Remove(filepath.Join(vrf.resultsdir, "result-0"))
-		})
-	}
-}
-
-func TestCreateReport(t *testing.T) {
-	rr := ResultReport{
-		Prog: "breaks_returns()\n" +
-			"minimize$0(0x1, 0x1)\n" +
-			"test$res0()\n",
-		Reports: []*CallReport{
-			{Call: "breaks_returns", States: map[int]ReturnState{
-				0: returnState(1, 1),
-				1: returnState(1, 1),
-				2: returnState(1, 1)}},
-			{Call: "minimize$0", States: map[int]ReturnState{
-				0: returnState(3, 3),
-				1: returnState(3, 3),
-				2: returnState(3, 3)}},
-			{Call: "test$res0", States: map[int]ReturnState{
-				0: returnState(2, 7),
-				1: returnState(5, 3),
-				2: returnState(22, 1)},
-				Mismatch: true},
-		},
-	}
-	got := string(createReport(&rr, 3))
-	want := "ERRNO mismatches found for program:\n\n" +
-		"[=] breaks_returns()\n" +
-		"\t↳ Pool: 0, Flags: 1, Errno: 1 (operation not permitted)\n" +
-		"\t↳ Pool: 1, Flags: 1, Errno: 1 (operation not permitted)\n" +
-		"\t↳ Pool: 2, Flags: 1, Errno: 1 (operation not permitted)\n\n" +
-		"[=] minimize$0(0x1, 0x1)\n" +
-		"\t↳ Pool: 0, Flags: 3, Errno: 3 (no such process)\n" +
-		"\t↳ Pool: 1, Flags: 3, Errno: 3 (no such process)\n" +
-		"\t↳ Pool: 2, Flags: 3, Errno: 3 (no such process)\n\n" +
-		"[!] test$res0()\n" +
-		"\t↳ Pool: 0, Flags: 7, Errno: 2 (no such file or directory)\n" +
-		"\t↳ Pool: 1, Flags: 3, Errno: 5 (input/output error)\n" +
-		"\t↳ Pool: 2, Flags: 1, Errno: 22 (invalid argument)\n\n"
-	if diff := cmp.Diff(got, want); diff != "" {
-		t.Errorf("createReport: (-want +got):\n%s", diff)
-	}
-}
-
-func TestCleanup(t *testing.T) {
-	prog := getTestProgram(t)
-	tests := []struct {
-		name       string
-		progs      map[int]*progInfo
-		wantProg   *progInfo
-		wantStats  *Stats
-		progExists bool
-		fileExists bool
-	}{
-		{
-			name: "results not ready for verification",
-			progs: map[int]*progInfo{
-				4: {
-					idx:      4,
-					received: 0,
-					res: func() [][]*ExecResult {
-						res := make([][]*ExecResult, 1)
-						res[0] = make([]*ExecResult, 3)
-						return res
-					}(),
-				}},
-			wantProg: &progInfo{
-				idx:      4,
-				received: 1,
-				res:      [][]*ExecResult{{makeExecResultCrashed(0), nil, nil}},
-			},
-			wantStats:  emptyTestStats(),
-			fileExists: false,
-		},
-		{
-			name: "results sent for verification, no report generated",
-			progs: map[int]*progInfo{
-				4: {
-					idx:      4,
-					prog:     prog,
-					received: 2,
-					res: func() [][]*ExecResult {
-						res := make([][]*ExecResult, 1)
-						res[0] = make([]*ExecResult, 3)
-						res[0][1] = makeExecResultCrashed(1)
-						res[0][2] = makeExecResultCrashed(2)
-						return res
-					}(),
-				}},
-			wantStats: &Stats{
-				TotalProgs: 1,
-				Calls: map[string]*CallStats{
-					"breaks_returns": makeCallStats("breaks_returns", 1, 0, map[ReturnState]bool{}),
-					"minimize$0":     makeCallStats("minimize$0", 1, 0, map[ReturnState]bool{}),
-					"test$res0":      makeCallStats("test$res0", 1, 0, map[ReturnState]bool{}),
-				},
-			},
-			fileExists: false,
-		},
-		{
-			name: "results sent for verification, report generation",
-			progs: map[int]*progInfo{
-				4: {
-					idx:      4,
-					prog:     prog,
-					received: 2,
-					res: func() [][]*ExecResult {
-						res := make([][]*ExecResult, 1)
-						res[0] = make([]*ExecResult, 3)
-						res[0][1] = makeExecResult(1, []int{11, 33, 44})
-						res[0][2] = makeExecResult(2, []int{11, 33, 22})
-						return res
-					}(),
-				}},
-			wantStats: &Stats{
-				TotalMismatches:  3,
-				TotalProgs:       1,
-				MismatchingProgs: 1,
-				Calls: map[string]*CallStats{
-					"breaks_returns": makeCallStats("breaks_returns", 1, 1,
-						map[ReturnState]bool{
-							crashedReturnState(): true,
-							returnState(11):      true}),
-					"minimize$0": makeCallStats("minimize$0", 1, 1,
-						map[ReturnState]bool{
-							crashedReturnState(): true,
-							returnState(33):      true}),
-					"test$res0": makeCallStats("test$res0", 1, 1,
-						map[ReturnState]bool{
-							crashedReturnState(): true,
-							returnState(22):      true,
-							returnState(44):      true}),
-				},
-			},
-			fileExists: true,
-		},
-	}
-	for _, test := range tests {
-		t.Run(test.name, func(t *testing.T) {
-			srv := createTestServer(t)
-			srv.progs = test.progs
-			srv.pools = map[int]*poolInfo{
-				0: {runners: map[int]runnerProgs{
-					0: {4: srv.progs[4]}},
-				}, 1: {}, 2: {}}
-			resultFile := filepath.Join(srv.vrf.resultsdir, "result-0")
-
-			srv.cleanup(0, 0)
-
-			prog := srv.progs[4]
-			if diff := cmp.Diff(test.wantProg, prog, cmp.AllowUnexported(progInfo{})); diff != "" {
-				t.Errorf("srv.progs[4] mismatch (-want +got):\n%s", diff)
-			}
-
-			if diff := cmp.Diff(test.wantStats, srv.vrf.stats); diff != "" {
-				t.Errorf("srv.vrf.stats mismatch (-want +got):\n%s", diff)
-			}
-
-			if got, want := osutil.IsExist(resultFile), test.fileExists; got != want {
-				t.Errorf("osutil.IsExist report file: got %v want %v", got, want)
-			}
-			os.Remove(filepath.Join(srv.vrf.resultsdir, "result-0"))
-		})
-	}
-}
diff --git a/syz-verifier/rpcserver.go b/syz-verifier/rpcserver.go
index e392e1c9e..3726799c1 100644
--- a/syz-verifier/rpcserver.go
+++ b/syz-verifier/rpcserver.go
@@ -4,6 +4,7 @@
 package main
 
 import (
+	"errors"
 	"net"
 	"os"
 	"sync"
@@ -15,25 +16,22 @@ import (
 // RPCServer is a wrapper around the rpc.Server. It communicates with  Runners,
 // generates programs and sends complete Results for verification.
 type RPCServer struct {
-	vrf             *Verifier
-	port            int
-	mu              sync.Mutex
-	cond            *sync.Cond
-	pools           map[int]*poolInfo
-	progs           map[int]*progInfo
-	notChecked      int
-	rerunsAvailable *sync.Cond
+	vrf  *Verifier
+	port int
+
+	// protects next variables
+	mu sync.Mutex
+	// used to count the pools w/o UnsupportedCalls result
+	notChecked int
+	// vmTasks store the per-VM currently assigned tasks Ids
+	vmTasksInProgress map[int]map[int64]bool
 }
 
 func startRPCServer(vrf *Verifier) (*RPCServer, error) {
 	srv := &RPCServer{
 		vrf:        vrf,
-		pools:      vrf.pools,
-		progs:      make(map[int]*progInfo),
 		notChecked: len(vrf.pools),
 	}
-	srv.cond = sync.NewCond(&srv.mu)
-	srv.rerunsAvailable = sync.NewCond(&srv.mu)
 
 	s, err := rpctype.NewRPCServer(vrf.addr, "Verifier", srv)
 	if err != nil {
@@ -49,11 +47,7 @@ func startRPCServer(vrf *Verifier) (*RPCServer, error) {
 
 // Connect notifies the RPCServer that a new Runner was started.
 func (srv *RPCServer) Connect(a *rpctype.RunnerConnectArgs, r *rpctype.RunnerConnectRes) error {
-	srv.mu.Lock()
-	defer srv.mu.Unlock()
-	pool, vm := a.Pool, a.VM
-	srv.pools[pool].runners[vm] = make(runnerProgs)
-	r.CheckUnsupportedCalls = !srv.pools[pool].checked
+	r.CheckUnsupportedCalls = !srv.vrf.pools[a.Pool].checked
 	return nil
 }
 
@@ -66,10 +60,11 @@ func (srv *RPCServer) Connect(a *rpctype.RunnerConnectArgs, r *rpctype.RunnerCon
 func (srv *RPCServer) UpdateUnsupported(a *rpctype.UpdateUnsupportedArgs, r *int) error {
 	srv.mu.Lock()
 	defer srv.mu.Unlock()
-	if srv.pools[a.Pool].checked {
+
+	if srv.vrf.pools[a.Pool].checked {
 		return nil
 	}
-	srv.pools[a.Pool].checked = true
+	srv.vrf.pools[a.Pool].checked = true
 	vrf := srv.vrf
 
 	for _, unsupported := range a.UnsupportedCalls {
@@ -86,7 +81,7 @@ func (srv *RPCServer) UpdateUnsupported(a *rpctype.UpdateUnsupportedArgs, r *int
 		vrf.SetPrintStatAtSIGINT()
 
 		vrf.choiceTable = vrf.target.BuildChoiceTable(nil, vrf.calls)
-		srv.cond.Signal()
+		vrf.progGeneratorInit.Done()
 	}
 	return nil
 }
@@ -94,119 +89,63 @@ func (srv *RPCServer) UpdateUnsupported(a *rpctype.UpdateUnsupportedArgs, r *int
 // NextExchange is called when a Runner requests a new program to execute and,
 // potentially, wants to send a new Result to the RPCServer.
 func (srv *RPCServer) NextExchange(a *rpctype.NextExchangeArgs, r *rpctype.NextExchangeRes) error {
-	srv.mu.Lock()
-	defer srv.mu.Unlock()
-
-	var res *ExecResult
-	var prog *progInfo
 	if a.Info.Calls != nil {
-		res = &ExecResult{
-			Pool:   a.Pool,
-			Hanged: a.Hanged,
-			Info:   a.Info,
-			RunIdx: a.RunIdx,
-		}
-
-		prog = srv.progs[a.ProgIdx]
-		if prog == nil {
-			// This case can happen if both conditions are true:
-			// 1. a Runner calls Verifier.NextExchange, then crashes,
-			// its corresponding Pool being the only one that hasn't
-			// sent results for the program yet
-			// 2.the cleanup call for the crash got the server's mutex before
-			// the NextExchange call.
-			// As the pool was the only one that hasn't sent the result, the
-			// cleanup call has already removed prog from srv.progs by the time
-			// the NextExchange call gets the server's mutex, which is why the
-			// variable is nil. As the results for this program have already
-			// been sent for verification, we discard this one.
-			return nil
-		}
-
-		delete(srv.pools[a.Pool].runners[a.VM], prog.idx)
-		if srv.newResult(res, prog) {
-			if srv.vrf.processResults(prog) {
-				delete(srv.progs, prog.idx)
-			}
-		}
+		srv.stopWaitResult(a.Pool, a.VM, a.ExecTaskID)
+		PutExecResult(&ExecResult{
+			Pool:       a.Pool,
+			Hanged:     a.Hanged,
+			Info:       a.Info,
+			ExecTaskID: a.ExecTaskID,
+		})
 	}
 
-	if srv.notChecked > 0 {
-		// Runner is blocked until the choice table is created.
-		srv.cond.Wait()
-	}
+	// TODO: NewEnvironment is the currently hardcoded logic. Relax it.
+	task := srv.vrf.GetRunnerTask(a.Pool, NewEnvironment)
+	srv.startWaitResult(a.Pool, a.VM, task.ID)
+	r.ExecTask = *task
 
-	newProg, pi, ri := srv.newProgram(a.Pool, a.VM)
-	r.Prog = rpctype.Prog{Bytes: newProg, ProgIdx: pi, RunIdx: ri}
 	return nil
 }
 
-// newResult is called when a Runner sends a new Result. It returns true if all
-// Results from the corresponding programs have been received and they can be
-// sent for verification. Otherwise, it returns false.
-func (srv *RPCServer) newResult(res *ExecResult, prog *progInfo) bool {
-	ri := prog.runIdx
-	if prog.res[ri][res.Pool] != nil {
-		return false
-	}
-	prog.res[ri][res.Pool] = res
-	prog.received++
-	return prog.received == len(srv.pools)
+func vmTasksKey(poolID, vmID int) int {
+	return poolID*1000 + vmID
 }
 
-func (srv *RPCServer) newRun(p *progInfo) {
-	p.runIdx++
-	p.received = 0
-	p.res[p.runIdx] = make([]*ExecResult, len(srv.pools))
-	for _, pool := range srv.pools {
-		pool.toRerun = append(pool.toRerun, p)
-	}
-}
-
-// newProgram returns a new program for the Runner identified by poolIdx and
-// vmIdx and the program's index.
-func (srv *RPCServer) newProgram(poolIdx, vmIdx int) ([]byte, int, int) {
-	pool := srv.pools[poolIdx]
+func (srv *RPCServer) startWaitResult(poolID, vmID int, taskID int64) {
+	srv.mu.Lock()
+	defer srv.mu.Unlock()
 
-	if len(pool.toRerun) != 0 {
-		p := pool.toRerun[0]
-		pool.runners[vmIdx][p.idx] = p
-		pool.toRerun = pool.toRerun[1:]
-		return p.serialized, p.idx, p.runIdx
+	if srv.vmTasksInProgress == nil {
+		srv.vmTasksInProgress = make(map[int]map[int64]bool)
 	}
 
-	if len(pool.progs) == 0 {
-		prog, progIdx := srv.vrf.generate()
-		pi := &progInfo{
-			prog:       prog,
-			idx:        progIdx,
-			serialized: prog.Serialize(),
-			res:        make([][]*ExecResult, srv.vrf.reruns),
-		}
-		pi.res[0] = make([]*ExecResult, len(srv.pools))
-		for _, pool := range srv.pools {
-			pool.progs = append(pool.progs, pi)
-		}
-		srv.progs[progIdx] = pi
+	if srv.vmTasksInProgress[vmTasksKey(poolID, vmID)] == nil {
+		srv.vmTasksInProgress[vmTasksKey(poolID, vmID)] =
+			make(map[int64]bool)
 	}
-	p := pool.progs[0]
-	pool.runners[vmIdx][p.idx] = p
-	pool.progs = pool.progs[1:]
-	return p.serialized, p.idx, p.runIdx
+
+	srv.vmTasksInProgress[vmTasksKey(poolID, vmID)][taskID] = true
+}
+
+func (srv *RPCServer) stopWaitResult(poolID, vmID int, taskID int64) {
+	srv.mu.Lock()
+	defer srv.mu.Unlock()
+	delete(srv.vmTasksInProgress[vmTasksKey(poolID, vmID)], taskID)
 }
 
 // cleanup is called when a vm.Instance crashes.
-func (srv *RPCServer) cleanup(poolIdx, vmIdx int) {
+func (srv *RPCServer) cleanup(poolID, vmID int) {
 	srv.mu.Lock()
 	defer srv.mu.Unlock()
-	progs := srv.pools[poolIdx].runners[vmIdx]
-
-	for _, prog := range progs {
-		if srv.newResult(&ExecResult{Pool: poolIdx, Crashed: true}, prog) {
-			srv.vrf.processResults(prog)
-			delete(srv.progs, prog.idx)
-			delete(srv.pools[poolIdx].runners[vmIdx], prog.idx)
-			continue
-		}
+
+	// Signal error for every VM related task and let upper level logic to process it.
+	for taskID := range srv.vmTasksInProgress[vmTasksKey(poolID, vmID)] {
+		PutExecResult(&ExecResult{
+			Pool:       poolID,
+			ExecTaskID: taskID,
+			Crashed:    true,
+			Error:      errors.New("VM crashed during the task execution"),
+		})
 	}
+	delete(srv.vmTasksInProgress, vmTasksKey(poolID, vmID))
 }
diff --git a/syz-verifier/rpcserver_test.go b/syz-verifier/rpcserver_test.go
new file mode 100644
index 000000000..8d630e8c6
--- /dev/null
+++ b/syz-verifier/rpcserver_test.go
@@ -0,0 +1,32 @@
+// Copyright 2021 syzkaller project authors. All rights reserved.
+// Use of this source code is governed by Apache 2 LICENSE that can be found in the LICENSE file.
+
+package main
+
+import (
+	"testing"
+
+	"github.com/google/go-cmp/cmp"
+	"github.com/google/syzkaller/pkg/rpctype"
+)
+
+func TestConnect(t *testing.T) {
+	vrf := createTestVerifier(t)
+	vrf.pools = make(map[int]*poolInfo)
+	vrf.pools[1] = &poolInfo{}
+
+	a := &rpctype.RunnerConnectArgs{
+		Pool: 1,
+		VM:   1,
+	}
+
+	r := &rpctype.RunnerConnectRes{}
+
+	if err := vrf.srv.Connect(a, r); err != nil {
+		t.Fatalf("srv.Connect failed: %v", err)
+	}
+
+	if diff := cmp.Diff(&rpctype.RunnerConnectRes{CheckUnsupportedCalls: true}, r); diff != "" {
+		t.Errorf("Connect result mismatch (-want +got):\n%s", diff)
+	}
+}
diff --git a/syz-verifier/utils_test.go b/syz-verifier/utils_test.go
index a4affe90a..ffd255894 100644
--- a/syz-verifier/utils_test.go
+++ b/syz-verifier/utils_test.go
@@ -5,35 +5,32 @@ package main
 
 import (
 	"io/ioutil"
-	"math/rand"
 	"os"
 	"testing"
-	"time"
 
 	"github.com/google/syzkaller/pkg/ipc"
 	"github.com/google/syzkaller/pkg/osutil"
 	"github.com/google/syzkaller/prog"
 )
 
-func createTestServer(t *testing.T) *RPCServer {
+func createTestVerifier(t *testing.T) *Verifier {
 	target, err := prog.GetTarget("test", "64")
 	if err != nil {
 		t.Fatalf("failed to initialise test target: %v", err)
 	}
-	vrf := Verifier{
+	vrf := &Verifier{
 		target:      target,
 		choiceTable: target.DefaultChoiceTable(),
-		rnd:         rand.New(rand.NewSource(time.Now().UnixNano())),
 		progIdx:     3,
 		reruns:      1,
 	}
 	vrf.resultsdir = makeTestResultDirectory(t)
 	vrf.stats = emptyTestStats()
-	srv, err := startRPCServer(&vrf)
+	vrf.srv, err = startRPCServer(vrf)
 	if err != nil {
 		t.Fatalf("failed to initialise RPC server: %v", err)
 	}
-	return srv
+	return vrf
 }
 
 func getTestProgram(t *testing.T) *prog.Prog {
diff --git a/syz-verifier/verifier.go b/syz-verifier/verifier.go
index 043ed07d7..1ad9eaab9 100644
--- a/syz-verifier/verifier.go
+++ b/syz-verifier/verifier.go
@@ -12,11 +12,14 @@ import (
 	"os/signal"
 	"path/filepath"
 	"strings"
+	"sync"
+	"sync/atomic"
 	"time"
 
 	"github.com/google/syzkaller/pkg/instance"
 	"github.com/google/syzkaller/pkg/log"
 	"github.com/google/syzkaller/pkg/osutil"
+	"github.com/google/syzkaller/pkg/rpctype"
 	"github.com/google/syzkaller/prog"
 	"github.com/google/syzkaller/vm"
 )
@@ -31,24 +34,172 @@ type Verifier struct {
 	// - <workdir>/corpus.db: corpus with interesting programs
 	// - <workdir>/<OS-Arch>/instance-x: per VM instance temporary files
 	// grouped by OS/Arch
-	workdir       string
-	crashdir      string
-	resultsdir    string
-	target        *prog.Target
-	runnerBin     string
-	executorBin   string
-	choiceTable   *prog.ChoiceTable
-	rnd           *rand.Rand
-	progIdx       int
-	addr          string
-	srv           *RPCServer
-	calls         map[*prog.Syscall]bool
-	reasons       map[*prog.Syscall]string
-	reportReasons bool
-	stats         *Stats
-	statsWrite    io.Writer
-	newEnv        bool
-	reruns        int
+	workdir           string
+	crashdir          string
+	resultsdir        string
+	target            *prog.Target
+	runnerBin         string
+	executorBin       string
+	progGeneratorInit sync.WaitGroup
+	choiceTable       *prog.ChoiceTable
+	progIdx           int
+	addr              string
+	srv               *RPCServer
+	calls             map[*prog.Syscall]bool
+	reasons           map[*prog.Syscall]string
+	reportReasons     bool
+	stats             *Stats
+	statsWrite        io.Writer
+	newEnv            bool
+	reruns            int
+
+	// We use single queue for every kernel environment.
+	tasksMutex     sync.Mutex
+	onTaskAdded    *sync.Cond
+	kernelEnvTasks [][]*ExecTaskQueue
+}
+
+func (vrf *Verifier) Init() {
+	vrf.progGeneratorInit.Add(1)
+
+	vrf.onTaskAdded = sync.NewCond(&vrf.tasksMutex)
+
+	vrf.kernelEnvTasks = make([][]*ExecTaskQueue, len(vrf.pools))
+	for i := range vrf.kernelEnvTasks {
+		vrf.kernelEnvTasks[i] = make([]*ExecTaskQueue, EnvironmentsCount)
+		for j := range vrf.kernelEnvTasks[i] {
+			vrf.kernelEnvTasks[i][j] = MakeExecTaskQueue()
+		}
+	}
+
+	srv, err := startRPCServer(vrf)
+	if err != nil {
+		log.Fatalf("failed to initialise RPC server: %v", err)
+	}
+	vrf.srv = srv
+}
+
+func (vrf *Verifier) StartProgramsAnalysis() {
+	go func() {
+		vrf.progGeneratorInit.Wait()
+
+		type AnalysisResult struct {
+			Diff []*ExecResult
+			Prog *prog.Prog
+		}
+
+		results := make(chan *AnalysisResult)
+		go func() {
+			for result := range results {
+				if result.Diff != nil {
+					vrf.SaveDiffResults(result.Diff, result.Prog)
+				}
+			}
+		}()
+
+		for i := 0; i < 100; i++ {
+			go func() {
+				for {
+					prog := vrf.generate()
+					results <- &AnalysisResult{
+						vrf.TestProgram(prog),
+						prog,
+					}
+				}
+			}()
+		}
+	}()
+}
+
+func (vrf *Verifier) GetRunnerTask(kernel int, existing EnvDescr) *rpctype.ExecTask {
+	vrf.tasksMutex.Lock()
+	defer vrf.tasksMutex.Unlock()
+
+	for {
+		for env := existing; env >= AnyEnvironment; env-- {
+			if task, ok := vrf.kernelEnvTasks[kernel][env].PopTask(); ok {
+				return task.ToRPC()
+			}
+		}
+
+		vrf.onTaskAdded.Wait()
+	}
+}
+
+func PutExecResult(result *ExecResult) {
+	c := GetExecResultChan(result.ExecTaskID)
+	c <- result
+}
+
+// TestProgram return the results slice if some exec diff was found.
+func (vrf *Verifier) TestProgram(prog *prog.Prog) (result []*ExecResult) {
+	steps := []EnvDescr{
+		NewEnvironment,
+		NewEnvironment,
+	}
+
+	defer atomic.AddInt64(&vrf.stats.TotalProgs, 1)
+
+	for i, env := range steps {
+		stepRes, err := vrf.Run(prog, env)
+		if err != nil {
+			return
+		}
+		vrf.AddCallsExecutionStat(stepRes, prog)
+		if stepRes[0].IsEqual(stepRes[1]) {
+			if i != 0 {
+				atomic.AddInt64(&vrf.stats.FlakyProgs, 1)
+			}
+			return
+		}
+		if i == len(steps)-1 {
+			atomic.AddInt64(&vrf.stats.MismatchingProgs, 1)
+			return stepRes
+		}
+	}
+	return
+}
+
+// Run sends the program for verification to execution queues and return
+// result once it's ready.
+// In case of time-out, return (nil, error).
+func (vrf *Verifier) Run(prog *prog.Prog, env EnvDescr) (result []*ExecResult, err error) {
+	totalKernels := len(vrf.kernelEnvTasks)
+	result = make([]*ExecResult, totalKernels)
+
+	wg := sync.WaitGroup{}
+	wg.Add(totalKernels)
+	for i := 0; i < totalKernels; i++ {
+		i := i
+		q := vrf.kernelEnvTasks[i][env]
+
+		go func() {
+			defer wg.Done()
+			task := MakeExecTask(prog)
+			defer DeleteExecTask(task)
+
+			vrf.tasksMutex.Lock()
+			q.PushTask(task)
+			vrf.onTaskAdded.Signal()
+			vrf.tasksMutex.Unlock()
+
+			result[i] = <-task.ExecResultChan
+		}()
+	}
+	wg.Wait()
+
+	for _, item := range result {
+		if item == nil {
+			err = errors.New("something went wrong and we exit w/o results")
+			return nil, err
+		}
+		if item.Error != nil {
+			err = item.Error
+			return nil, err
+		}
+	}
+
+	return result, nil
 }
 
 // SetPrintStatAtSIGINT asks Stats object to report verification
@@ -77,24 +228,24 @@ func (vrf *Verifier) SetPrintStatAtSIGINT() error {
 }
 
 func (vrf *Verifier) startInstances() {
-	for idx, pi := range vrf.pools {
-		go func(pi *poolInfo, idx int) {
+	for poolID, pi := range vrf.pools {
+		go func(pi *poolInfo, poolID int) {
 			for {
 				// TODO: implement support for multiple VMs per Pool.
 
-				vrf.createAndManageInstance(pi, idx)
+				vrf.createAndManageInstance(pi, poolID)
 			}
-		}(pi, idx)
+		}(pi, poolID)
 	}
 }
 
-func (vrf *Verifier) createAndManageInstance(pi *poolInfo, idx int) {
+func (vrf *Verifier) createAndManageInstance(pi *poolInfo, poolID int) {
 	inst, err := pi.pool.Create(0)
 	if err != nil {
 		log.Fatalf("failed to create instance: %v", err)
 	}
 	defer inst.Close()
-	defer vrf.srv.cleanup(idx, 0)
+	defer vrf.srv.cleanup(poolID, 0)
 
 	fwdAddr, err := inst.Forward(vrf.srv.port)
 	if err != nil {
@@ -110,7 +261,7 @@ func (vrf *Verifier) createAndManageInstance(pi *poolInfo, idx int) {
 		log.Fatalf("failed to copy executor binary: %v", err)
 	}
 
-	cmd := instance.RunnerCmd(runnerBin, fwdAddr, vrf.target.OS, vrf.target.Arch, idx, 0, false, vrf.newEnv)
+	cmd := instance.RunnerCmd(runnerBin, fwdAddr, vrf.target.OS, vrf.target.Arch, poolID, 0, false, vrf.newEnv)
 	outc, errc, err := inst.Run(pi.cfg.Timeouts.VMRunningTime, vrf.vmStop, cmd)
 	if err != nil {
 		log.Fatalf("failed to start runner: %v", err)
@@ -118,7 +269,7 @@ func (vrf *Verifier) createAndManageInstance(pi *poolInfo, idx int) {
 
 	inst.MonitorExecution(outc, errc, pi.Reporter, vm.ExitTimeout)
 
-	log.Logf(0, "reboot the VM in pool %d", idx)
+	log.Logf(0, "reboot the VM in pool %d", poolID)
 }
 
 // finalizeCallSet removes the system calls that are not supported from the set
@@ -154,41 +305,16 @@ func (vrf *Verifier) finalizeCallSet(w io.Writer) {
 	}
 }
 
-// processResults will send a set of complete results for verification and, in
-// case differences are found, it will start the rerun process for the program
-// (if reruns are enabled). If every rerun produces the same results, the result
-// report will be printed to persistent storage. Otherwise, the program is
-// discarded as flaky.
-func (vrf *Verifier) processResults(prog *progInfo) bool {
-	// TODO: Simplify this if clause.
-	if prog.runIdx == 0 {
-		vrf.stats.TotalProgs++
-		prog.report = Verify(prog.res[0], prog.prog, vrf.stats)
-		if prog.report == nil {
-			return true
-		}
-	} else {
-		if !VerifyRerun(prog.res[prog.runIdx], prog.report) {
-			vrf.stats.FlakyProgs++
-			log.Logf(0, "flaky results detected: %d", vrf.stats.FlakyProgs)
-			return true
-		}
-	}
-
-	if prog.runIdx < vrf.reruns-1 {
-		vrf.srv.newRun(prog)
-		return false
-	}
-
-	rr := prog.report
-	vrf.stats.MismatchingProgs++
-
+func (vrf *Verifier) AddCallsExecutionStat(results []*ExecResult, program *prog.Prog) {
+	rr := CompareResults(results, program)
 	for _, cr := range rr.Reports {
+		atomic.AddInt64(&vrf.stats.Calls[cr.Call].Occurrences, 1)
+
 		if !cr.Mismatch {
-			break
+			continue
 		}
-		vrf.stats.Calls[cr.Call].Mismatches++
-		vrf.stats.TotalMismatches++
+		atomic.AddInt64(&vrf.stats.Calls[cr.Call].Mismatches, 1)
+		atomic.AddInt64(&vrf.stats.TotalMismatches, 1)
 		for _, state := range cr.States {
 			if state0 := cr.States[0]; state0 != state {
 				vrf.stats.Calls[cr.Call].States[state] = true
@@ -196,6 +322,11 @@ func (vrf *Verifier) processResults(prog *progInfo) bool {
 			}
 		}
 	}
+}
+
+// SaveDiffResults extract diff and save result on the persistent storage.
+func (vrf *Verifier) SaveDiffResults(results []*ExecResult, program *prog.Prog) bool {
+	rr := CompareResults(results, program)
 
 	oldest := 0
 	var oldestTime time.Time
@@ -226,10 +357,12 @@ func (vrf *Verifier) processResults(prog *progInfo) bool {
 	return true
 }
 
-// generate will return a newly generated program and its index.
-func (vrf *Verifier) generate() (*prog.Prog, int) {
-	vrf.progIdx++
-	return vrf.target.Generate(vrf.rnd, prog.RecommendedCalls, vrf.choiceTable), vrf.progIdx
+// generate returns a newly generated program or error.
+func (vrf *Verifier) generate() *prog.Prog {
+	vrf.progGeneratorInit.Wait()
+
+	rnd := rand.New(rand.NewSource(time.Now().UnixNano() + 1e12))
+	return vrf.target.Generate(rnd, prog.RecommendedCalls, vrf.choiceTable)
 }
 
 func createReport(rr *ResultReport, pools int) []byte {
diff --git a/syz-verifier/verifier_test.go b/syz-verifier/verifier_test.go
new file mode 100644
index 000000000..f3068787a
--- /dev/null
+++ b/syz-verifier/verifier_test.go
@@ -0,0 +1,279 @@
+// Copyright 2021 syzkaller project authors. All rights reserved.
+// Use of this source code is governed by Apache 2 LICENSE that can be found in the LICENSE file.
+
+package main
+
+import (
+	"bytes"
+	"os"
+	"path/filepath"
+	"strings"
+	"testing"
+
+	"github.com/google/go-cmp/cmp"
+	"github.com/google/syzkaller/pkg/osutil"
+	"github.com/google/syzkaller/pkg/rpctype"
+	"github.com/google/syzkaller/prog"
+)
+
+func TestFinalizeCallSet(t *testing.T) {
+	target, err := prog.GetTarget("test", "64")
+	if err != nil {
+		t.Fatalf("failed to initialise test target: %v", err)
+	}
+
+	vrf := Verifier{
+		target: target,
+		reasons: map[*prog.Syscall]string{
+			target.SyscallMap["test$res0"]:  "foo",
+			target.SyscallMap["minimize$0"]: "bar",
+		},
+		calls: map[*prog.Syscall]bool{
+			target.SyscallMap["minimize$0"]: true,
+			target.SyscallMap["test$res0"]:  true,
+			target.SyscallMap["disabled1"]:  true,
+		},
+		reportReasons: true,
+	}
+
+	out := bytes.Buffer{}
+	vrf.finalizeCallSet(&out)
+	wantLines := []string{
+		"The following calls have been disabled:\n",
+		"\ttest$res0: foo\n",
+		"\tminimize$0: bar\n",
+	}
+	output := out.String()
+	for _, line := range wantLines {
+		if !strings.Contains(output, line) {
+			t.Errorf("finalizeCallSet: %q missing in reported output", line)
+		}
+	}
+
+	wantCalls, gotCalls := map[*prog.Syscall]bool{
+		target.SyscallMap["disabled1"]: true,
+	}, vrf.calls
+	if diff := cmp.Diff(wantCalls, gotCalls); diff != "" {
+		t.Errorf("srv.calls mismatch (-want +got):\n%s", diff)
+	}
+}
+
+func TestUpdateUnsupported(t *testing.T) {
+	target, err := prog.GetTarget("test", "64")
+	if err != nil {
+		t.Fatalf("failed to initialise test target: %v", err)
+	}
+
+	tests := []struct {
+		name           string
+		vrfPools       map[int]*poolInfo
+		wantPools      map[int]*poolInfo
+		wantCalls      map[*prog.Syscall]bool
+		wantNotChecked int
+		nilCT          bool
+	}{
+		{
+			name:           "choice table not generated",
+			vrfPools:       map[int]*poolInfo{0: {}, 1: {}},
+			wantPools:      map[int]*poolInfo{0: {checked: true}, 1: {}},
+			wantNotChecked: 1,
+			wantCalls: map[*prog.Syscall]bool{
+				target.SyscallMap["minimize$0"]:     true,
+				target.SyscallMap["breaks_returns"]: true,
+				target.SyscallMap["test$res0"]:      true,
+				target.SyscallMap["test$union0"]:    true,
+			},
+			nilCT: true,
+		},
+		{
+			name:           "choice table generated",
+			vrfPools:       map[int]*poolInfo{0: {}},
+			wantPools:      map[int]*poolInfo{0: {checked: true}},
+			wantNotChecked: 0,
+			wantCalls: map[*prog.Syscall]bool{
+				target.SyscallMap["minimize$0"]:     true,
+				target.SyscallMap["breaks_returns"]: true,
+			},
+			nilCT: false,
+		},
+	}
+
+	for _, test := range tests {
+		t.Run(test.name, func(t *testing.T) {
+			vrf := Verifier{
+				target:        target,
+				pools:         test.vrfPools,
+				reasons:       make(map[*prog.Syscall]string),
+				reportReasons: true,
+				calls: map[*prog.Syscall]bool{
+					target.SyscallMap["minimize$0"]:     true,
+					target.SyscallMap["breaks_returns"]: true,
+					target.SyscallMap["test$res0"]:      true,
+					target.SyscallMap["test$union0"]:    true,
+				},
+				stats: MakeStats(),
+			}
+			vrf.Init()
+
+			a := &rpctype.UpdateUnsupportedArgs{
+				Pool: 0,
+				UnsupportedCalls: []rpctype.SyscallReason{
+					{ID: 142, Reason: "foo"},
+					{ID: 2, Reason: "bar"},
+					{ID: 156, Reason: "tar"},
+				}}
+			if err := vrf.srv.UpdateUnsupported(a, nil); err != nil {
+				t.Fatalf("srv.UpdateUnsupported failed: %v", err)
+			}
+
+			if diff := cmp.Diff(test.wantPools, vrf.pools, cmp.AllowUnexported(poolInfo{})); diff != "" {
+				t.Errorf("srv.pools mismatch (-want +got):\n%s", diff)
+			}
+
+			wantReasons := map[*prog.Syscall]string{
+				target.SyscallMap["test$res0"]:   "foo",
+				target.SyscallMap["test$union0"]: "tar",
+			}
+			if diff := cmp.Diff(wantReasons, vrf.reasons); diff != "" {
+				t.Errorf("srv.reasons mismatch (-want +got):\n%s", diff)
+			}
+
+			if diff := cmp.Diff(test.wantCalls, vrf.calls); diff != "" {
+				t.Errorf("srv.calls mismatch (-want +got):\n%s", diff)
+			}
+
+			if want, got := test.wantNotChecked, vrf.srv.notChecked; want != got {
+				t.Errorf("srv.notChecked: got %d want %d", got, want)
+			}
+
+			if want, got := test.nilCT, vrf.choiceTable == nil; want != got {
+				t.Errorf("vrf.choiceTable == nil: want nil, got: %v", vrf.choiceTable)
+			}
+		})
+	}
+}
+
+func TestUpdateUnsupportedNotCalledTwice(t *testing.T) {
+	vrf := Verifier{
+		pools: map[int]*poolInfo{
+			0: {checked: false},
+			1: {checked: false},
+		},
+	}
+	srv, err := startRPCServer(&vrf)
+	if err != nil {
+		t.Fatalf("failed to initialise RPC server: %v", err)
+	}
+	a := &rpctype.UpdateUnsupportedArgs{Pool: 0}
+
+	if err := srv.UpdateUnsupported(a, nil); err != nil {
+		t.Fatalf("srv.UpdateUnsupported failed: %v", err)
+	}
+	if want, got := 1, srv.notChecked; want != got {
+		t.Errorf("srv.notChecked: got %d want %d", got, want)
+	}
+
+	if err := srv.UpdateUnsupported(a, nil); err != nil {
+		t.Fatalf("srv.UpdateUnsupported failed: %v", err)
+	}
+	if want, got := 1, srv.notChecked; want != got {
+		t.Fatalf("srv.UpdateUnsupported called twice")
+	}
+
+	wantPools := map[int]*poolInfo{
+		0: {checked: true},
+		1: {checked: false},
+	}
+	if diff := cmp.Diff(wantPools, vrf.pools, cmp.AllowUnexported(poolInfo{})); diff != "" {
+		t.Errorf("srv.pools mismatch (-want +got):\n%s", diff)
+	}
+}
+
+func TestSaveDiffResults(t *testing.T) {
+	tests := []struct {
+		name      string
+		res       []*ExecResult
+		prog      string
+		wantExist bool
+		wantStats *Stats
+	}{
+		{
+			name: "report written",
+			res: []*ExecResult{
+				makeExecResult(0, []int{1, 3, 2}),
+				makeExecResult(1, []int{1, 3, 5}),
+			},
+			wantExist: true,
+			wantStats: &Stats{
+				TotalMismatches: 1,
+				Calls: map[string]*CallStats{
+					"breaks_returns": makeCallStats("breaks_returns", 1, 0, map[ReturnState]bool{}),
+					"test$res0":      makeCallStats("test$res0", 1, 1, map[ReturnState]bool{{Errno: 2}: true, {Errno: 5}: true}),
+					"minimize$0":     makeCallStats("minimize$0", 1, 0, map[ReturnState]bool{}),
+				},
+			},
+		},
+	}
+	for _, test := range tests {
+		t.Run(test.name, func(t *testing.T) {
+			prog := getTestProgram(t)
+			vrf := Verifier{
+				resultsdir: makeTestResultDirectory(t),
+				stats:      emptyTestStats(),
+			}
+			resultFile := filepath.Join(vrf.resultsdir, "result-0")
+
+			vrf.AddCallsExecutionStat(test.res, prog)
+			vrf.SaveDiffResults(test.res, prog)
+
+			if diff := cmp.Diff(test.wantStats, vrf.stats); diff != "" {
+				t.Errorf("vrf.stats mismatch (-want +got):\n%s", diff)
+			}
+
+			if got, want := osutil.IsExist(resultFile), test.wantExist; got != want {
+				t.Errorf("osutil.IsExist report file: got %v want %v", got, want)
+			}
+			os.Remove(filepath.Join(vrf.resultsdir, "result-0"))
+		})
+	}
+}
+
+func TestCreateReport(t *testing.T) {
+	rr := ResultReport{
+		Prog: "breaks_returns()\n" +
+			"minimize$0(0x1, 0x1)\n" +
+			"test$res0()\n",
+		Reports: []*CallReport{
+			{Call: "breaks_returns", States: map[int]ReturnState{
+				0: returnState(1, 1),
+				1: returnState(1, 1),
+				2: returnState(1, 1)}},
+			{Call: "minimize$0", States: map[int]ReturnState{
+				0: returnState(3, 3),
+				1: returnState(3, 3),
+				2: returnState(3, 3)}},
+			{Call: "test$res0", States: map[int]ReturnState{
+				0: returnState(2, 7),
+				1: returnState(5, 3),
+				2: returnState(22, 1)},
+				Mismatch: true},
+		},
+	}
+	got := string(createReport(&rr, 3))
+	want := "ERRNO mismatches found for program:\n\n" +
+		"[=] breaks_returns()\n" +
+		"\t↳ Pool: 0, Flags: 1, Errno: 1 (operation not permitted)\n" +
+		"\t↳ Pool: 1, Flags: 1, Errno: 1 (operation not permitted)\n" +
+		"\t↳ Pool: 2, Flags: 1, Errno: 1 (operation not permitted)\n\n" +
+		"[=] minimize$0(0x1, 0x1)\n" +
+		"\t↳ Pool: 0, Flags: 3, Errno: 3 (no such process)\n" +
+		"\t↳ Pool: 1, Flags: 3, Errno: 3 (no such process)\n" +
+		"\t↳ Pool: 2, Flags: 3, Errno: 3 (no such process)\n\n" +
+		"[!] test$res0()\n" +
+		"\t↳ Pool: 0, Flags: 7, Errno: 2 (no such file or directory)\n" +
+		"\t↳ Pool: 1, Flags: 3, Errno: 5 (input/output error)\n" +
+		"\t↳ Pool: 2, Flags: 1, Errno: 22 (invalid argument)\n\n"
+	if diff := cmp.Diff(got, want); diff != "" {
+		t.Errorf("createReport: (-want +got):\n%s", diff)
+	}
+}