mirror of
https://github.com/ioacademy-jikim/debugging
synced 2025-06-24 08:16:27 +00:00
157 lines
5.4 KiB
Plaintext
157 lines
5.4 KiB
Plaintext
|
|
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.
|
|
|