|
From: Julian S. <js...@ac...> - 2008-01-24 19:52:45
|
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
|