Home | History | Annotate | only in /external/valgrind/main/helgrind
Up to higher level directory
NameDateSize
docs/10-Jul-2012
helgrind.h10-Jul-201232.9K
hg_basics.c10-Jul-20122.7K
hg_basics.h10-Jul-20125.4K
hg_errors.c10-Jul-201248.9K
hg_errors.h10-Jul-20124.2K
hg_intercepts.c10-Jul-201273.6K
hg_lock_n_thread.c10-Jul-20123.8K
hg_lock_n_thread.h10-Jul-20126.9K
hg_main.c10-Jul-2012175.1K
hg_wordset.c10-Jul-201227.9K
hg_wordset.h10-Jul-20125.1K
libhb.h10-Jul-20127.2K
libhb_core.c10-Jul-2012218.1K
Makefile.am10-Jul-20124.3K
README_MSMProp2.txt10-Jul-20125.4K
README_YARD.txt10-Jul-20121.3K
tests/10-Jul-2012

README_MSMProp2.txt

      1 
      2 MSMProp2, a simplified but functionally equivalent version of MSMProp1
      3 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
      4 
      5 Julian Seward, OpenWorks Ltd, 19 August 2008
      6 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
      7 
      8 Note that this file does NOT describe the state machine used in the
      9 svn://svn.valgrind.org/branches/YARD version of Helgrind.  That state
     10 machine is different again from any previously described machine.
     11 
     12 See the file README_YARD.txt for more details on YARD.
     13 
     14                      ----------------------
     15 
     16 In early 2008 Konstantin Serebryany proposed "MSMProp1", a memory
     17 state machine for data race detection.  It is described at
     18 http://code.google.com/p/data-race-test/wiki/MSMProp1
     19 
     20 Implementation experiences show MSMProp1 is useful, but difficult to
     21 implement efficiently.  In particular keeping the memory usage under
     22 control is complex and difficult.
     23 
     24 This note points out a key simplification of MSMProp1, which makes it
     25 easier to implement without changing the functionality.
     26 
     27 
     28 The idea
     29 ~~~~~~~~
     30 
     31 The core of the idea pertains to the "Condition" entry for MSMProp1
     32 state machine rules E5 and E6(r).  These are, respectively:
     33 
     34     HB(SS, currS)  and its negation
     35     ! HB(SS, currS).
     36 
     37 Here, SS is a set of segments, and currS is a single segment.  Each
     38 segment contains a vector timestamp.  The expression "HB(SS, currS)"
     39 is intended to denote
     40 
     41    for each segment S in SS  .  happens_before(S,currS)
     42 
     43 where happens_before(S,T) means that S's vector timestamp is ordered
     44 before-or-equal to T's vector timestamp.
     45 
     46 In words, the expression
     47 
     48    for each segment S in SS  .  happens_before(S,currS)
     49 
     50 is equivalent to saying that currS has a timestamp which is
     51 greater-than-equal to the timestamps of all the segments in SS.
     52 
     53 The key observation is that this is equivalent to
     54 
     55    happens_before( JOIN(SS), currS )
     56 
     57 where JOIN is the lattice-theoretic "max" or "least upper bound"
     58 operation on vector clocks.  Given the definition of HB,
     59 happens_before and (binary) JOIN, this is easy to prove.
     60 
     61 
     62 The consequences
     63 ~~~~~~~~~~~~~~~~
     64 
     65 With that observation in place, it is a short step to observe that
     66 storing segment sets in MSMProp1 is unnecessary.  Instead of
     67 storing a segment set in each shadow value, just store and
     68 update a single vector timestamp.  The following two equivalences
     69 hold:
     70 
     71    MSMProp1                        MSMProp2
     72 
     73    adding a segment S              join-ing S's vector timestamp
     74    to the segment-set              to the current vector timestamp
     75 
     76    HB(SS,currS)                    happens_before(
     77                                       currS's timestamp,
     78                                       current vector timestamp )
     79 
     80 Once it is no longer necessary to represent segment sets, it then
     81 also becomes unnecessary to represent segments.  This constitutes
     82 a significant simplication to the implementation.
     83 
     84 
     85 The resulting state machine, MSMProp2
     86 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
     87 
     88 MSMProp2 is isomorphic to MSMProp1, with the following changes:
     89 
     90 States are    New,   Read(VTS,LS),   Write(VTS,LS)
     91 
     92 where LS is a lockset (as before) and VTS is a vector timestamp.
     93 
     94 For a thread T with current lockset 'currLS' and current VTS 'currVTS'
     95 making a memory access, the new rules are
     96 
     97 Name  Old-State         Op  Guard         New-State              Race-If
     98 
     99 E1  New                 rd  True          Read(currVTS,currLS)   False
    100 
    101 E2  New                 wr  True          Write(currVTS,currLS)  False
    102 
    103 E3  Read(oldVTS,oldLS)  rd  True          Read(newVTS,newLS)     False
    104 
    105 E4  Read(oldVTS,oldLS)  wr  True          Write(newVTS,newLS)    #newLS == 0 
    106                                                                  && !hb(oldVTS,currVTS)
    107 
    108 E5  Write(oldVTS,oldLS) rd  hb(oldVTS,    Read(currVTS,currLS)   False
    109                                currVTS)
    110 
    111 E6r Write(oldVTS,oldLS) rd  !hb(oldVTS,   Write(newVTS,newLS)    #newLS == 0 
    112                                 currVTS)                         && !hb(oldVTS,currVTS)
    113 
    114 E6w Write(oldVTS,oldLS) wr  True          Write(newVTS,newLS)    #newLS == 0 
    115                                                                  && !hb(oldVTS,currVTS)
    116 
    117    where newVTS = join2(oldVTS,currVTS)
    118 
    119          newLS  = if   hb(oldVTS,currVTS)
    120                   then currLS
    121                   else intersect(oldLS,currLS)
    122 
    123          hb(vts1, vts2) =  vts1 happens before or is equal to vts2
    124 
    125 
    126 Interpretation of the states
    127 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    128 
    129 I always found the state names in MSMProp1 confusing.  Both MSMProp1
    130 and MSMProp2 are easier to understand if the states Read and Write are
    131 renamed, like this:
    132 
    133    old name           new name
    134 
    135    Read               WriteConstraint
    136    Write              AllConstraint
    137 
    138 The effect of a state Read(VTS,LS) is to constrain all later-observed
    139 writes so that either (1) the writing thread holds at least one lock
    140 in common with LS, or (2) those writes must happen-after VTS.  If
    141 neither of those two conditions hold, a race is reported.
    142 
    143 Hence a Read state places a constraint on writes.
    144 
    145 The effect of a state Write(VTS,LS) is similar, but it applies to all
    146 later-observed accesses: either (1) the accessing thread holds at
    147 least one lock in common with LS, or (2) those accesses must
    148 happen-after VTS.  If neither of those two conditions hold, a race is
    149 reported.
    150 
    151 Hence a Write state places a constraint on all accesses.
    152 
    153 If we ignore the LS component of these states, the intuitive
    154 interpretation of the VTS component is that it states the earliest
    155 vector-time that the next write / access may safely happen.
    156 
    157

README_YARD.txt

      1 
      2 YARD, Yet Another Race Detector, built on the Helgrind framework
      3 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
      4 
      5 Julian Seward, OpenWorks Ltd, 19 August 2008
      6 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
      7 
      8 The YARD race detector lives in svn://svn.valgrind.org/branches/YARD.
      9 
     10 It uses a new and relatively simple race detection engine, based on
     11 the idea of shadowing each memory location with two vector timestamps,
     12 indicating respectively the "earliest safe read point" and "earliest
     13 safe write point".  As far as I know this is a novel approach.  Some
     14 features of the implementation:
     15 
     16 * Modularity.  The entire race detection engine is placed in a
     17   standalone library (libhb_core.c) with a simple interface (libhb.h).
     18   This makes it easier to debug and verify the engine; indeed it can
     19   be built as a standalone executable with test harness using "make -f
     20   Makefile_sa".
     21 
     22 * Simplified and scalable storage management, so that large programs,
     23   with many synchronisation events, can be handled.
     24 
     25 * Ability to report both call stacks involved in a race, without
     26   excessive time or space overhead.
     27 
     28 * Pure happens before operation, so as not to give any false
     29   positives.
     30 
     31 To use, build as usual and run as "--tool=helgrind".
     32 
     33 You can disable lock order checking with --track-lockorders=no, as it
     34 sometimes produces an annoying amount of output.
     35