The basic model-checking algorithm is trying to enumerate all possible global system states. There are, however, many irrelevant states that can be skipped while ensuring that we learn all relevant states. For example, any two independent events are worth exploring in one order only. DPOR is reducing the state-space by capturing the dependencies between different threads/processes during the runtime. The main weakness of DPOR thus lies in the “dependent events” definition. If all events depend on each other, DPOR will not be able to reduce the search space. Thus, our goal is to create a simple application which will have a lot of dependencies and (because we want to beat DPOR) these dependencies can be removed by domain-specific knowledge. One such example might be an application which is performing different tasks in parallel and it is accessing global statistics.

main() {
	read_all_tasks();
	for i = 1 to n {
		new thread(process(i))
	}
	join_threads()
	print(counter + “ tasks processed successfully”)
}

process(i) {
	run(tasks[i])
	if (!error) {
		lock(counter); counter = counter + 1; unlock(counter)
	}
}

DPOR will find dependencies between all tasks in our example. Thus the technique won’t be able to reduce the search space even if the running of the tasks itself is independent. This result of DPOR can be easily beaten by simple domain knowledge: additions are commutative and thus there is no point in checking different orderings of increments. But this is only ``enhancement’’ of DPOR technique. To really show another POR technique let us remove the “print” line from the main algorithm and do complex operations with the counter:

lock(counter); counter= counter*counter + i; unlock(counter)

If the calculation of the new value does not create any branches in the code and the resulting value is never used, we may argue that the value of the counter is irrelevant. Thus, even if there are many dependencies between accesses to this counter, it would be enough to explore only one ordering. My POR technique is thus “if the manipulations to the shared object cannot affect the execution (no branching) and the value is never stored to other variables/objects, it is sufficient to explore any one ordering of these accesses”.