On Thursday 24 January 2008 17:07, Konstantin Serebryany wrote:
> I've made first (quick-and-dirty) implementation.
> The machine works as expected, at least on my set of tests.
Sounds good.
I see you changed the "Race if ..." condition in MSMProp1 from "LS={}"
to "LS={} and #SS > 1", yes?
I tried to summarise the MSMProp1 state machine, so as to get a
clearer idea of what behaviour it allows and does not allow. But
really I am guessing. Can you fix/refine this summary? You must
have some intuition of what the state machine allows/disallows.
J
* define a "synchronization event" as any of the following:
semaphore post-waits
condition variable signal-wait when the waiter blocks
thread creation
thread joinage
a barrier
* synchronisation events partition the execution of a threaded program
into a set of segments which have a partial ordering, called the
the "happens-before" ordering.
* a location may be read by a segment S, without a protecting lock,
only if all writes to it happened-before S
* a location may be written by a segment S, without a protecting
lock, only if all reads and all writes to it happened-before S
* a location may be read by a segment S, using a protecting lock, only
if all writes to it which are concurrent (not-happens-before) use
the same protecting lock
* a location may be read by a segment S, using a protecting lock,
only if all reads and all writes to it which are concurrent
(not happens-before) use the same protecting lock
-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2008.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
_______________________________________________
Valgrind-developers mailing list
Valgrind-developers@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/valgrind-developers
