638
edits
(heh - this applies to Requires too) |
m (→Basic idea) |
||
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. |
edits