model: optimize get_last_conflict() search
authorBrian Norris <banorris@uci.edu>
Mon, 19 Nov 2012 21:10:07 +0000 (13:10 -0800)
committerBrian Norris <banorris@uci.edu>
Mon, 19 Nov 2012 21:16:36 +0000 (13:16 -0800)
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

model.cc

index df06760893018d5bc1756cd89df263c6ed117cc6..8aef67d8b911b70b94f8cd7d47f703f7b27bb677 100644 (file)
--- 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;