On Jan 24, 2008 11:22 PM, Konstantin Serebryany <
[EMAIL PROTECTED]> wrote:
> 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.
Ehmm.
The last bullet should probably be 'a location may be *written* by a segment
S'
And actually it is not correct. For test38 this bullet is true, but we still
have a false positive.
Same for reads and test28.
--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
[email protected]
https://lists.sourceforge.net/lists/listinfo/valgrind-developers
