>
>
> * 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.
That's just a visual sugar. :)
I wanted to create a machine with states were we store separate segment sets
for R and W. Such states would have two boxes: one red and one green.
But I've abandoned it for now as it seems to complex (and useless :))
Anyway, I agree they are redundant here.
>
>
> * In MSMProp1, isn't "Read" state similar to "ShR" and "Write"
> similar to "ShM" ?
Similar, but not the same. Hence the different name to avoid phrases like
'ShR from MSMHelgrind is different from ShR from MSMProp1 ... '
Also Sh in ShR/ShM means 'shared' while Read/Write are not necessary shared.
> * I like that MSMProp1 removes E9/10/11/12 from MSMHelgrind.
> Those scanned all of memory and were potentially very expensive.
We move this cost to handle_read/write, at least partially. But yes, I like
it too.
>
>
> * 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
Yes, except that E4/E5/E7 also transfer ownership.
These edges change segment sets using happens-before (see SS_update).
And if HB(oldSS, currS) these edges take the current locks instead of
intersecting with old lock set (see LS_update).
For example, if we are looking at the first access after a barrier, we will
have HB(oldSS, currS)==True.
Not sure how to express it graphically in a more clear way...
>
>
> * 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).
>
Cool!
>
>
> > 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.
By 'pure happens-before detector' you understand the one which creates
happens-before relation after lock/unlock?
--kcc
-------------------------------------------------------------------------
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
