From: Brian Norris <banorris@uci.edu>
Date: Mon, 19 Nov 2012 21:10:07 +0000 (-0800)
Subject: model: optimize get_last_conflict() search
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=77319560c9921c0d814ed30e55c07ead41836cbe;p=cdsspec-compiler.git

model: optimize get_last_conflict() search

Relaxed operations should never require backtracking, so don't even
bother with searching the list in such cases. I ran some simple
benchmarking tests with linuxrwlocks (timing results below). Also, perf
shows a significant decrease in % time spent in
ModelAction::could_synchronize_with.

------------
Before:
------------

$ time ./run.sh test/linuxrwlocks.o -f 10 -m 10
Number of complete, bug-free executions: 7110
Number of redundant executions: 29
Number of buggy executions: 0
Number of infeasible executions: 43578
Total executions: 50717
Total nodes created: 63463

real	0m7.274s
user	0m6.596s
sys	0m0.652s

2.10%  linuxrwlocks.o  libmodel.so          [.] ModelAction::could_synchronize_with(ModelAction const*) const

------------
After:
------------

$ time ./run.sh test/linuxrwlocks.o -f 10 -m 10
Number of complete, bug-free executions: 7110
Number of redundant executions: 29
Number of buggy executions: 0
Number of infeasible executions: 43578
Total executions: 50717
Total nodes created: 63463

real	0m6.690s
user	0m6.000s
sys	0m0.664s

0.73%  linuxrwlocks.o  libmodel.so          [.] ModelAction::could_synchronize_with(ModelAction const*) const
---

diff --git a/model.cc b/model.cc
index df06760..8aef67d 100644
--- a/model.cc
+++ b/model.cc
@@ -494,6 +494,9 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
 	case ATOMIC_READ:
 	case ATOMIC_WRITE:
 	case ATOMIC_RMW: {
+		/* Optimization: relaxed operations don't need backtracking */
+		if (act->is_relaxed())
+			return NULL;
 		/* linear search: from most recent to oldest */
 		action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
 		action_list_t::reverse_iterator rit;