• Home
  • History
  • Annotate
  • only in /external/valgrind/main/helgrind/
NameDateSize

..02-Jul-20154 KiB

docs/02-Jul-20154 KiB

helgrind.h02-Jul-201533 KiB

hg_addrdescr.c02-Jul-20153.2 KiB

hg_addrdescr.h02-Jul-20153.1 KiB

hg_basics.c02-Jul-20152.7 KiB

hg_basics.h02-Jul-20155.4 KiB

hg_errors.c02-Jul-201545.7 KiB

hg_errors.h02-Jul-20153.8 KiB

hg_intercepts.c02-Jul-201572.9 KiB

hg_lock_n_thread.c02-Jul-20153.8 KiB

hg_lock_n_thread.h02-Jul-20156.9 KiB

hg_main.c02-Jul-2015186.6 KiB

hg_wordset.c02-Jul-201527.9 KiB

hg_wordset.h02-Jul-20155.1 KiB

libhb.h02-Jul-20157.2 KiB

libhb_core.c02-Jul-2015215 KiB

Makefile.am02-Jul-20154.3 KiB

Makefile.in02-Jul-201582.9 KiB

README_MSMProp2.txt02-Jul-20155.4 KiB

README_YARD.txt02-Jul-20151.3 KiB

tests/02-Jul-201512 KiB

README_MSMProp2.txt

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

README_YARD.txt

1
2YARD, Yet Another Race Detector, built on the Helgrind framework
3~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
4
5Julian Seward, OpenWorks Ltd, 19 August 2008
6~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
7
8The YARD race detector lives in svn://svn.valgrind.org/branches/YARD.
9
10It uses a new and relatively simple race detection engine, based on
11the idea of shadowing each memory location with two vector timestamps,
12indicating respectively the "earliest safe read point" and "earliest
13safe write point".  As far as I know this is a novel approach.  Some
14features 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
31To use, build as usual and run as "--tool=helgrind".
32
33You can disable lock order checking with --track-lockorders=no, as it
34sometimes produces an annoying amount of output.
35