> I've described the proposed memory state machine at
> http://code.google.com/p/data-race-test/wiki/MSMProp1.
That's good. It will be useful to have some results from
alternative state machines -- essentially, to see if we can
find a better compromise between scheduling-sensitivity and
false error rates.
Some comments (without really understanding all the consequences
of your proposal):
* I did not understand what the red/green boxes ("R:", "W:")
signify. Maybe it would be simpler to remove them? At least
for MSMHelgrind the names "ShR" and "ShM", by themselves,
carry enough meaning for me.
* In MSMProp1, isn't "Read" state similar to "ShR" and "Write"
similar to "ShM" ?
* I like that MSMProp1 removes E9/10/11/12 from MSMHelgrind.
Those scanned all of memory and were potentially very expensive.
* So it is kind-of like MSMHelgrind, except that
- The Excl is merged back into ShR / ShR
- Segment-sets are tracked, not thread-sets
- transition E6 allows transfer of ownership at any read event
which happens-after all previous accesses - MSMHelgrind only
allows such transfers of memory in Excl state
* A general comment when you are dealing with segment sets rather
than thread sets. There is a possible redundancy which you may
need to remove in the implementation:
HB(seg,segSet) is equivalent to HB(seg,max(segSet))
and max(segSet) is always same size or smaller than segSet.
Intuitively, max(segSet) == segSet except that it only has the
most recent seg for each thread:
max(segSet) = { seg1 | seg1 <- segSet,
not (exists seg2 <- segSet
such that seg1 < seg2) }
if that makes any sense. (Standard lattice-theory stuff).
> I will try to implement it in helgrind and see if it really works.
Good.
> Regrading size of SVal: I will prefer 64-bit over 48 bit. These extra 16
> bits will give us some room for experiments with 'heavy' state machines.
48- or 64-bits is more or less unavoidable. Not sure 48-bit is practical
- it might give fewer cache misses than 64-bit, but is likely to involve
more instructions to pack/unpack the values where needed.
------------
I like the idea of describing these state machines in a relatively
uniform notation.
I think it is possible to describe a pure happens-before detector in
the same framework (almost). This would give a lower bound on the false
error rate and so would be a useful reference point.
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
