Readers-writers monitor.

R. Clayton (rclayton@monmouth.edu)
(no date)

• Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
• Next message: R. Clayton: "C# concurrency."
• Previous message: R. Clayton: "More on threading."

I was working over my solution to the readers-writers monitor problem and I
began to mutate it under the influence of yesterday's lecture. It ended up
looking nothing like my original solution - which, compared to this solution,
is dumb, dumb, dumb - but it's pretty slick none-the-less (if I do say so
myself). You might want to make a copy and delete all the comments to get an
idea of the actual code size.

--
// monitor invariants
//
//   I1: writers working = 0 or readers working = 0
//
//     If writers working is not zero, then readers working is zero, and vice
//     versa.
//
//   I2: writers waiting = 0 or readers working + writers working > 0
//
//     If there are writers waiters, there workers available to release them.
//
//   I3: readers waiting = 0 or writers waiting + writers working > 0
//
//     If there are readers waiting, then there are writers available to
//     release them.
// Assuming the invariants are true whenever a thread enters the monitor, then
// I1 provides mutual-exclusion safety:  there is no state in which readers and
// writers are in the database at the same time.
// The combination of I2 and I3 provides waiter progress: there is no state in
// which there are waiting threads but no working threads to release them.
// Suppose such a state existed; that is, suppose there exists a state in which
// readers waiting + writers waiting > 0 and readers working + writers working
// = 0.  There are two cases based on which of readers waiting or writers
// waiting are positive:
//
//   Case 1 - If writers waiting is positive, then, by the second part of I2,
//   readers working + writers working > 0, which contradicts our claim that
//   there are no workers; writers waiting must be zero.  
// 
//   Case 2 - If readers waiting is positive, now I3 lies in ambush:  if
//   readers waiting is positive, then writers waiting + writers working > 0
//   must be true.  There are two further cases to consider:
//
//     Case 2a - If writers waiting is zero, then writers working is
//     positive, another contradiction to our no workers claim.
//    
//     Case 2b - Writers waiting is positive.  Case 1 already took care of this
//     case.
// 
// Because it is impossible to derive the hypothesized state from the
// invariants, such a state can't exist when the monitor is empty, and all
// waiters eventually get to execute.
// These arguments are incomplete - for example, there's no argument that a
// worker will release a waiter when the worker exits the database (which can
// be established by inspection) - and there are missing invariants - for
// example, I1, I2, and I3 can't establish the absence of overtaking (which can
// also be established by inspection), but the additions will follow the
// general outline shown here.
// These initializations establish I1 and I2 and I3.
readers waiting = 0
writers waiting = 0
readers working = 0
writers working = 0
condvar writers  // condition: writers working + readers working = 0
condvar readers  // condition: writers working = 0
reader enter
  // I1 and I2 and I3 on entry
  if writers waiting + writers working > 0
    // Increasing readers waiting by one makes the first part if I3 (readers
    // waiting = 0) false, which means the second part (writers waiting +
    // writers working > 0) has to be true to preserve I3.  The second part of
    // I3 is the guard of the if statement, and so I3 is true.  I1 and I2 are
    // untouched and remain true.
    readers waiting++
    // I1 and I2 and I3 on exit
    readers.wait()
    // I1 and I2 and I3 and writers working = 0 on entry.  Because readers
    // waiting is positive, decreasing it by one maintains I3.
    readers waiting--
  // Increasing readers working by one makes the second part (readers working =
  // 0) of I1 false, which means that the first part of I1 (writers working =
  // 0) has to be true to preserve I1.  Control can reach this point by passing
  // through the if statement or going around it.  Passing through the if
  // statement establishes writers working = 0.  To go around the if statement,
  // the guard must be false; that is, writers waiting + writer working = 0.
  // Because both values are non-negative, it must be that writers working = 0.
  // In either case, I1 remains true when readers working is increased by one.
  // Increasing readers working by one makes readers working + writers
  // working > 0 true, and I2 is true.
  // I3 is untouched and remains true.
  readers working++
  // I1 and I2 and I3 on exit
writer enter
  // I1 and I2 and I3 on entry
  if reader waiting + writer working + reader working > 0
    // Increasing writers waiting by one makes the second part of I3 (writers
    // waiting + writers working > 0) true, and I3 remains true.
    // Increasing writers waiting by one makes the first part of I2 (writers
    // waiting = 0) false, which means the second part of I2 (readers working +
    // writers working > 0) has to be true.  Unfortunately, the if guard is
    // weaker than the second part of I2 (because when reader waiting is
    // positive, writer working + reader working can be zero), so we can't
    // conclude that the second part of I2 is true because the guard is.
    // However, I3 comes to the rescue.  If readers waiting is positive, then
    // the second half of I3 (writer waiting + reader working > 0) must be
    // true.  Either writer waiting is zero or it's positive.  If it's zero,
    // then writers working must be positive by the second half of I3, which
    // makes the second half of I2 true.  If writer waiting is positive, then
    // the second half of I2 must be true.  If reader waiting is zero, then the
    // guard reduces to writer working + reader working > 0.  In all cases, the
    // second half of I2 is true and adding one to writers waiting doesn't
    // change I2.
    writers waiting++
    // I1 and I2 and I3 on exit.
    writers.waiting()
    // I1 and I2 and I3 and writers working + readers working = 0 on entry.
    // Because writes waiting is positive, decreasing it by one maintains I2.
    writers waiting--
  // No matter how control gets here - through the if or around it - writers
  // working + readers working is zero, and adding one to writers working
  // maintains I1.  I2 and I3 are true too. 
  writers working = 1
  // I1 and I2 and I3 on exit.
reader exit
  // I1 and I2 and I3 on entry
  if --readers working == 0
    // On entry readers working was positive, which meant that writers working
    // is zero (by I1).  Readers working is now zero too, which leaves I1 true
    // and enables the condition on writers.  I2 and I3, being unmodified,
    // remain true.
    writers.notify()
  // I1 and I2 and I3 on exit.
writer exit
  // I1 and I2 and I3 on entry.
  // writers working is positive on entry, which means that readers working is
  // zero by I1.  Setting writers working to 0 leaves I1 true and establishes
  // the condition for waiting readers.  I2 and I3 are unchanged and remain
  // true.
  writer working = 0
  if readers waiting > 0
    // There are waiting readers.  Let them go.
    readers.notifyAll()
  else
    // There are no waiting readers and the condition for waiting writers is
    // satisfied.  Let a waiting writer go, if there's one available.
    writer.notify()
  // I1 and I2 and I3 on exit.

• Next message: R. Clayton: "C# concurrency."
• Previous message: R. Clayton: "More on threading."

This archive was generated by hypermail 2.0b3 on Tue Aug 20 2002 - 12:45:05 EDT