|
From: <sv...@va...> - 2007-10-05 10:07:36
|
Author: sewardj
Date: 2007-10-05 11:07:38 +0100 (Fri, 05 Oct 2007)
New Revision: 6956
Log:
Don't search for a whole bunch of individual lock-to-lock paths in the
lock acquisition order graph (almost all of which searches fail and
are expensive). Instead search from one lock to any in a set of
locks. This makes the laog check mechanism a whole lot cheaper.
Modified:
branches/THRCHECK/thrcheck/tc_main.c
Modified: branches/THRCHECK/thrcheck/tc_main.c
===================================================================
--- branches/THRCHECK/thrcheck/tc_main.c 2007-10-05 07:24:18 UTC (rev 6955)
+++ branches/THRCHECK/thrcheck/tc_main.c 2007-10-05 10:07:38 UTC (rev 6956)
@@ -4086,7 +4086,10 @@
tl_assert(0);
}
-static Bool laog__do_dfs_from_to ( Lock* src, Lock* dst )
+/* Return True iff there is a path in laog from 'src' to any of the
+ elements in 'dst'. */
+static
+Bool laog__do_dfs_from_to ( Lock* src, WordSetID dsts /* univ_lsets */ )
{
Bool ret;
Word i, ssz;
@@ -4097,6 +4100,12 @@
Word succs_size;
Word* succs_words;
//laog__sanity_check();
+
+ /* If the destination set is empty, we can never get there from
+ 'src' :-), so don't bother to try */
+ if (TC_(isEmptyWS)( univ_lsets, dsts ))
+ return False;
+
stack = VG_(newXA)( tc_zalloc, tc_free, sizeof(Lock*) );
visited = TC_(newFM)( tc_zalloc, tc_free, NULL/*unboxedcmp*/ );
@@ -4111,7 +4120,7 @@
here = *(Lock**) VG_(indexXA)( stack, ssz-1 );
VG_(dropTailXA)( stack, 1 );
- if (here == dst) { ret = True; break; }
+ if (TC_(elemWS)( univ_lsets, dsts, (Word)here )) { ret = True; break; }
if (TC_(lookupFM)( visited, NULL, NULL, (Word)here ))
continue;
@@ -4141,7 +4150,6 @@
{
Word* ls_words;
Word ls_size, i;
- Bool complain;
/* It may be that 'thr' already holds 'lk' and is recursively
relocking in. In this case we just ignore the call. */
@@ -4152,18 +4160,13 @@
if (!laog)
laog = TC_(newFM)( tc_zalloc, tc_free, NULL/*unboxedcmp*/ );
- /* First, the check. Complain if there is any path in laog
- from lk to old for each old <- locks already held by thr.
+ /* First, the check. Complain if there is any path in laog from lk
+ to any of the locks already held by thr, since if any such path
+ existed, it would mean that previously lk was acquired before
+ (rather than after, as we are doing here) at least one of those
+ locks.
*/
- complain = False;
- TC_(getPayloadWS)( &ls_words, &ls_size, univ_lsets, thr->locksetA );
- for (i = 0; i < ls_size; i++) {
- if (laog__do_dfs_from_to( lk, (Lock*)ls_words[i] )) {
- complain = True;
- break;
- }
- }
- if (complain) {
+ if (laog__do_dfs_from_to(lk, thr->locksetA)) {
record_error_Misc( thr, "Lock acquisition order is inconsistent "
"with previously observed ordering" );
}
@@ -4171,6 +4174,7 @@
/* Second, add to laog the pairs
(old, lk) | old <- locks already held by thr
*/
+ TC_(getPayloadWS)( &ls_words, &ls_size, univ_lsets, thr->locksetA );
for (i = 0; i < ls_size; i++)
laog__add_edge( (Lock*)ls_words[i], lk );
}
@@ -5678,6 +5682,8 @@
VG_(printf)("\n");
TC_(ppWSUstats)( univ_lsets, "univ_lsets" );
VG_(printf)("\n");
+ TC_(ppWSUstats)( univ_laog, "univ_laog" );
+ VG_(printf)("\n");
}
}
|