Here are some conventions [Update: typos fix, Friday]

  • We are concerned with state machines and sequences of events. The prefixes of a sequence include the empty sequence “null” and the sequence itself.
  • Relative state: If “w” is the sequence of events that have driven a system of state machines from their initial to their current state then
    • |M is the output of state machine “M” in the current state (reached by following input sequence “w” from the initial state of M)
    • a|M is the output of M in the state reached from the current state by an “a” event.
    • z|M is the output of M in the state reached from the current state by the sequence of events “z” (if it is not clear from the context whether “z” is an event or a sequence, then we can just say which it is.)
  • Absolute state where the sequence parameter is made explicit. This is mostly useful fordefining the initial output and for when we construct composite state machines.
    • w:M is the output of state machine “M” in the state reached by following input sequence “w” from the initial state of M.
    • wa:M is the output of M in the state reached by following the sequence wa (obtained by appending event a to sequence w) from the initial state of M.
    • wz:M is the output of M n the state reached by following the sequence wz (obtained by appending event sequence z to sequence w) from the initial state of M (if it is not clear from the context whether “z” is an event or a sequence, then we can just say which it is.)
    • null:M is the output of M in its initial state.

Specific state machines

  • |Time is the current real-time.
  • |Running(p) =1 if p is executing and 0 otherwise
  • |Runnable(p) =1 if p wants to be scheduled, 0 otherwise.
  • |RequestWakeup(p,e)=1 if p is requesting a wakeup on event e, 0 otherwise
  • If |Runnable(p)=0 then a|Running(p) ≤ |Running(p) (if p is not runnable it can stop running, but not start running.)
  • If a|Runnable(p) > |Runnable(p) then there is at least one e so that a|RequestWakeup(p,e)< |RequestWakeup(p,e) (a process can only become runnable if some wakeup event happens and is cleared.)
  • If a|RequestWakeup(p,e) < |RequestWakeup(p,e) then a|Running(p)=1 (a request is only cleared if the process is actually made runnable)
  • If |RequestWake(p,e) then there is a t so that whenever z|Time ≥ |Time +t then Sum(prefixes u of z; u|Runable(p)) > 0 (if a process has requested a wakeup, it will become runnable in some bounded time – This liveness criteria is not strictly necessary)
  • Define |Safe(p) by null:Safe(p)=1 and
    • a|Safe(p)=

      • 0 if a|Running(p)=0 and a|Runnable(p)=0 and there is no e so that a|RequestWakeup(p,e) (real trouble requires that we are not runnable so can never start running unless we become runnable and cannot become runnable because we have no requests outstanding).
      • |Safe(p) otherwise (|Safe(p) does not change otherwise)
  • So what we want is to ensure that |Safe(p)=1. If a process requests a wakeup, then deschedules, and then gets a wakeup, everything is fine. The ordering is critical. If the wakeup happens before the process deschedules, but it is committed to descheduling then the process gets in trouble. If the code looks like Request e; sleep; then a wakeup event in-between the two operations is trouble. Note that Request e; if requeststill pending then sleep; is not safe unless the test and the sleep are atomic in some sense. Define |RequestOrder(p) by null:RequestOrder(p)=idle and
    • a|RequestOrder(p) =
      • requesting if |RequestOrder(p) = idle and a|RequestWakeup(p,e)>|RequestWakeup(p,e) for some e.
      • idle if a|Runnable(p) < |Runnable(p) and |RequestOrder(p)=requesting
      • error if a|Runnable(p) < |Runnable(p) and |RequestOrder(p) != requesting
      • |RequestOrder(p) otherwise.
  • |RequestOrder(p) != error does not ensure |Safe(p).
  • One solution is a lock. Suppose (Property L) If |locked(p)>0 then a|Running(p) = Running(p) and a|RequestWakeup(p,e) >= |RequestWakeup(p,e). That is, the lock prevents a running process from not running and prevents events from clearing requests -but we can make a process not-runnable while it holds the lock. Redefine RequestOrder to watch the lock.
    • a|RequestOrder(p) =
    • errror

      • if a|Locked(p) <|Locked(p) and RequestOrder(p) != (Ready or Idle)
      • or if a|Runnable(p) <|Runnable(p) and RequestOrder(p) != ready
    • locked otherwise if |RequestOrder(p) = idle and a|Locked(p) > |Locked(p) .
    • requesting otherwise if |RequestOrder(p)=locked and a|RequestWakeup(p,e)>|RequestWakeup(p,e) for some e
    • ready otherwise if a|Runnable(p) < |Runnable(p) and |RequestOrder(p)=requesting
    • idle otherwise if a|Locked(p) < |Locked(p) and |RequestOrder(p)=ready
    • |RequestOrder(p) otherwise.
  • Given Property L, |RequestOrder(p) != errror does assure |Safe(p).
more on missed wakeup