Here, in excruciating detail, is an argument that the code
nr++ r_go.signal()
maintains the invariant
nr cs readers
First, rewrite the invariant to the equivalent
{ nr = number of readers in the database }
The invariant is true initially because there are no computations in the
database and nr = 0. Adding one to each side of the equality preserves
the invariant.
{ nr + 1 = number of readers in the database + 1 }
What is this? It's just the predicate
{ nr = number of readers in the database + 1 }
with all occurrences of nr replaced by nr + 1; in other words
{ nr = number of readers in the database + 1 }[ nr <- nr + 1 ]
By the Assignment Rule, we can conclude the triple
{ nr = number of readers in the database + 1 }[ nr <- nr + 1 ]nr = nr + 1{ nr = number of readers in the database + 1 }
is valid. What kind of post-condition is that? It's just the predicate
{ nr = number of readers in the database }
with all occurrences of number of readers in the database replaced by
number of readers in the database + 1, or (with suitable abbreviations)
{ nr = noritdb }[ noritdb <- noritdb + 1 ]
Before applying the Assignment Rule, we should probably squint at
r_go.signal()
to figure out what it does. By signaling r_go, it releases a waiting
reader, which will then go on to (eventually) enter the database (we know that
such a waiting reader exists because this code is only executed when dr >
0 . The statement does indeed increase the number of readers in the database
by one, and the Assignment Rule lets us conclude that the triple
{ nr = noritdb }[ noritdb <- noritdb + 1 ]
r_go.signal()
{ nr = number of readers in the database }
is valid. We now have the original invariant back, and it's still true.
In summary, here're the steps with brief justification:
{ nr = number of readers in the database }, assumed true.
{ nr + 1 = number of readers in the database + 1 }, arithmetic.
{ nr = number of readers in the database + 1 }[ nr <- nr + 1 ]
nr = nr + 1
{ nr = number of readers in the database + 1 }, the Assignment Rule
{ nr = noritdb }[ noritdb <- noritdb + 1 ]
r_go.signal()
{ nr = number of readers in the database }, the Assignment Rule
A similar argument establishes a similar result for nw and the number of
writers in the database.
This page last modified on 26 June 2003.