Few observations regarding MSMProp1:
When in exclusive state (i.e. state is Read or Write and #SS == 1) and we
access the memory from the same thread, HB(SS,currS) is always true.
This means that each access that leaves us in the same thread rewrites the
shadow value with SS={currS}; LS=currLS.
In other words, while in exclusive state we do not track the history, but
only store information about the last access.
This helps us to avoid false positives on tests like test{37,43,44,45},
while still reporting a (true) race on test10.
Both MSMProp1 and MSMHelgrind have false negative on test46:
//
// First: Second:
// 1. write
// 2. MU.Lock()
// 3. write
// 4. MU.Unlock() (sleep)
// a. MU.Lock()
// b. write
// c. MU.Unlock();
With MSMProp1 we no longer need to scan all memory at thread_join.
We, however, still have this scan-all-memory in shadow_mem_make_NoAccess.
The comment says:
7. Modify all shadow words, by removing ToDelete from the lockset
of all ShM and ShR states. Note this involves a complete scan
over map_shmem, which is very expensive...
Do we really need this?
If we don't do that and if a new lock gets allocated at the same memory
location we may miss some very weird race.
Any other reason for doing this?
Thanks,
--kcc
On Jan 24, 2008 12:49 PM, Konstantin Serebryany <
[EMAIL PROTECTED]> wrote:
>
>
> 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
