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.

YARD, Yet Another Race Detector, built on the Helgrind framework
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Julian Seward, OpenWorks Ltd, 19 August 2008
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

The YARD race detector lives in svn://svn.valgrind.org/branches/YARD.

It uses a new and relatively simple race detection engine, based on
the idea of shadowing each memory location with two vector timestamps,
indicating respectively the "earliest safe read point" and "earliest
safe write point".  As far as I know this is a novel approach.  Some
features of the implementation:

* Modularity.  The entire race detection engine is placed in a
  standalone library (libhb_core.c) with a simple interface (libhb.h).
  This makes it easier to debug and verify the engine; indeed it can
  be built as a standalone executable with test harness using "make -f
  Makefile_sa".

* Simplified and scalable storage management, so that large programs,
  with many synchronisation events, can be handled.

* Ability to report both call stacks involved in a race, without
  excessive time or space overhead.

* Pure happens before operation, so as not to give any false
  positives.

To use, build as usual and run as "--tool=helgrind".

You can disable lock order checking with --track-lockorders=no, as it
sometimes produces an annoying amount of output.