>
> I see you changed the "Race if ..." condition in MSMProp1 from "LS={}"
> to "LS={} and #SS > 1", yes?
>
Yep. That's sort of obvious. There is no race in exclusive state.
>
> 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
>
There are several primary "synchronization events":
semaphore post-waits
condition variable signal-wait when the waiter blocks or the while-wait
loop is annotated
thread creation/joinage
and various possible secondary (defined via primary) events:
message queue (aka PCQ), defined through semaphore.
barrier, defined through condition variable
> * 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
>
I could not express it better! I'll borrow this description for the wiki :)
It also helps to see what this machine can not do.
Good examples are test38 and test40 which differ only by calls to sleep().
test38 is not handled by this machine, while test40 works fine.
--kcc
-------------------------------------------------------------------------
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
