MMgc thread safety annotations: Difference between revisions

m
(heh - this applies to Requires too)
 
Line 103: Line 103:
For the last two conditions, entering or leaving any kind of lock at those state transitions is enough.
For the last two conditions, entering or leaving any kind of lock at those state transitions is enough.


(Elementary stuff, maybe, but I'm not used to thinking this way, so it's a big deal to me.)
(Elementary stuff, maybe, but I'm not used to thinking this way, so it's a big deal to me.)  (I'd like to make a stronger statement, allowing the timing of the flushes to be a little fuzzier, but can't pin it down right now.)


Note that <code>Requires(X)</code> is the same as <code>ReadWrite(X, X)</code>.  In that case, at least, the above conjecture simplifies to something obviously (heh) true.
Note that <code>Requires(X)</code> is the same as <code>ReadWrite(X, X)</code>.  In that case, at least, the above conjecture simplifies to something obviously (heh) true.
638

edits