> I think it is possible to describe a pure happens-before detector in
> the same framework (almost).
Like this:
Generate segments as currently. Also, generate segments for each
lock/unlock operation.
Shadow information for each address A is now a pair:
"w-owner" (thread segment)
"r-owners" (set of thread segments)
no locksets are tracked
w-owner(A) is the segment that most recently wrote A.
r-owners(A) are the segment(s) that most recently read A. As per
comment in previous message, r-owners is potentially redundant; we
only need to store the maximum-frontier subset of r-owners. (*)
For segments S1, S2,
define S1 >= S2 to mean "S1 == S2 or S1 happens-after S2"
Then the update rules are:
for a write in seg S:
valid if S >= w-owner and S >= all elements in r-owners
if (!valid) report race
w-owner := S
r-owners := {}
// intuition: a valid write must happen-after the previous
// write, or happen in the same segment. Also, a valid write
// must happen-after all reads, or be in the same segment
for a read in seg S:
valid if S >= w-owner
r-owners := union(r-owners, {S})
// intuition: a valid read must happen-after the previous write.
// but that's all; it can happen in parallel with other reads.
// we merely need to record that it happened, in order that we
// can check that a later write happens-after all reads
(*) follows trivially from definition of max(a segment set). The
only comparison against r-owners is
"S >= all elements in r-owners"
which is equivalent to
"S >= all elements in max(r-owners)"
J
-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2008.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
_______________________________________________
Valgrind-developers mailing list
Valgrind-developers@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/valgrind-developers
