Merge Helgrind from branches/YARD into the trunk. Also includes some
minor changes to make stack unwinding on amd64-linux approximately
twice as fast as it was before.
git-svn-id: svn://svn.valgrind.org/valgrind/trunk@8707 a5019735-40e9-0310-863c-91ae7b9d1cf9
diff --git a/helgrind/README_MSMProp2.txt b/helgrind/README_MSMProp2.txt
new file mode 100644
index 0000000..6b4ac5f
--- /dev/null
+++ b/helgrind/README_MSMProp2.txt
@@ -0,0 +1,156 @@
+
+MSMProp2, a simplified but functionally equivalent version of MSMProp1
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Julian Seward, OpenWorks Ltd, 19 August 2008
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Note that this file does NOT describe the state machine used in the
+svn://svn.valgrind.org/branches/YARD version of Helgrind. That state
+machine is different again from any previously described machine.
+
+See the file README_YARD.txt for more details on YARD.
+
+ ----------------------
+
+In early 2008 Konstantin Serebryany proposed "MSMProp1", a memory
+state machine for data race detection. It is described at
+http://code.google.com/p/data-race-test/wiki/MSMProp1
+
+Implementation experiences show MSMProp1 is useful, but difficult to
+implement efficiently. In particular keeping the memory usage under
+control is complex and difficult.
+
+This note points out a key simplification of MSMProp1, which makes it
+easier to implement without changing the functionality.
+
+
+The idea
+~~~~~~~~
+
+The core of the idea pertains to the "Condition" entry for MSMProp1
+state machine rules E5 and E6(r). These are, respectively:
+
+ HB(SS, currS) and its negation
+ ! HB(SS, currS).
+
+Here, SS is a set of segments, and currS is a single segment. Each
+segment contains a vector timestamp. The expression "HB(SS, currS)"
+is intended to denote
+
+ for each segment S in SS . happens_before(S,currS)
+
+where happens_before(S,T) means that S's vector timestamp is ordered
+before-or-equal to T's vector timestamp.
+
+In words, the expression
+
+ for each segment S in SS . happens_before(S,currS)
+
+is equivalent to saying that currS has a timestamp which is
+greater-than-equal to the timestamps of all the segments in SS.
+
+The key observation is that this is equivalent to
+
+ happens_before( JOIN(SS), currS )
+
+where JOIN is the lattice-theoretic "max" or "least upper bound"
+operation on vector clocks. Given the definition of HB,
+happens_before and (binary) JOIN, this is easy to prove.
+
+
+The consequences
+~~~~~~~~~~~~~~~~
+
+With that observation in place, it is a short step to observe that
+storing segment sets in MSMProp1 is unnecessary. Instead of
+storing a segment set in each shadow value, just store and
+update a single vector timestamp. The following two equivalences
+hold:
+
+ MSMProp1 MSMProp2
+
+ adding a segment S join-ing S's vector timestamp
+ to the segment-set to the current vector timestamp
+
+ HB(SS,currS) happens_before(
+ currS's timestamp,
+ current vector timestamp )
+
+Once it is no longer necessary to represent segment sets, it then
+also becomes unnecessary to represent segments. This constitutes
+a significant simplication to the implementation.
+
+
+The resulting state machine, MSMProp2
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+MSMProp2 is isomorphic to MSMProp1, with the following changes:
+
+States are New, Read(VTS,LS), Write(VTS,LS)
+
+where LS is a lockset (as before) and VTS is a vector timestamp.
+
+For a thread T with current lockset 'currLS' and current VTS 'currVTS'
+making a memory access, the new rules are
+
+Name Old-State Op Guard New-State Race-If
+
+E1 New rd True Read(currVTS,currLS) False
+
+E2 New wr True Write(currVTS,currLS) False
+
+E3 Read(oldVTS,oldLS) rd True Read(newVTS,newLS) False
+
+E4 Read(oldVTS,oldLS) wr True Write(newVTS,newLS) #newLS == 0
+ && !hb(oldVTS,currVTS)
+
+E5 Write(oldVTS,oldLS) rd hb(oldVTS, Read(currVTS,currLS) False
+ currVTS)
+
+E6r Write(oldVTS,oldLS) rd !hb(oldVTS, Write(newVTS,newLS) #newLS == 0
+ currVTS) && !hb(oldVTS,currVTS)
+
+E6w Write(oldVTS,oldLS) wr True Write(newVTS,newLS) #newLS == 0
+ && !hb(oldVTS,currVTS)
+
+ where newVTS = join2(oldVTS,currVTS)
+
+ newLS = if hb(oldVTS,currVTS)
+ then currLS
+ else intersect(oldLS,currLS)
+
+ hb(vts1, vts2) = vts1 happens before or is equal to vts2
+
+
+Interpretation of the states
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+I always found the state names in MSMProp1 confusing. Both MSMProp1
+and MSMProp2 are easier to understand if the states Read and Write are
+renamed, like this:
+
+ old name new name
+
+ Read WriteConstraint
+ Write AllConstraint
+
+The effect of a state Read(VTS,LS) is to constrain all later-observed
+writes so that either (1) the writing thread holds at least one lock
+in common with LS, or (2) those writes must happen-after VTS. If
+neither of those two conditions hold, a race is reported.
+
+Hence a Read state places a constraint on writes.
+
+The effect of a state Write(VTS,LS) is similar, but it applies to all
+later-observed accesses: either (1) the accessing thread holds at
+least one lock in common with LS, or (2) those accesses must
+happen-after VTS. If neither of those two conditions hold, a race is
+reported.
+
+Hence a Write state places a constraint on all accesses.
+
+If we ignore the LS component of these states, the intuitive
+interpretation of the VTS component is that it states the earliest
+vector-time that the next write / access may safely happen.
+