L18: Lab 3 discussion and Lab 4 preview

Lab 3
questions?
abstraction relation
  diskSize is an invariant
  some people had disk(ptr_a) = block0 or block1
    need this if absR refers only to block1
  \/ vs /\
proving put_ok
  tip: don't unfold abstraction relation, use lemmas
  especially for large number of crash cases
  helps notice symmetries and re-use proofs
  benefit more from automation (esp eauto)

Lab 4

replicated disk
  base API: two disks with read/write/size
  twist: either disk can fail at any time
  goal: implement single disk
  failures should not be visible
  if computer crashes, atomic

two challenges:
  concurrency from disk failures
  need recovery from crashes

how do we handle concurrency?
  concurrency means some things are changing in background
  illustrate problem with read specification
    read(i, a)
    pre: true
    post(r, state, state'):
      disk_failure(state, state') /\
      match disk_i state' with
      | Some d -> r = Working (diskGet d a)
      | None   -> r = Failed
    all proofs have to carry information from state to state'
    especially about disk_\bar{i} (other disk)

  what can we rely on over disk_failure?
    if a disk doesn't fail, it stays the same
    if a disk has failed, it stays failed
  we address preserving facts about other disk with maybe_holds and a "frame"
  framed spec
    read(i, a)
    pre: disk_i state ?|= eq d /\
         disk_\bar{i} state ?|= F
    post(r, state, state'):
      match r with
      | Working b -> b = diskGet d a /\
                      disk_i state' ?|= eq d /\
                      disk_\bar{i} state' ?|= F
      | Failed    -> disk_i state' ?|= missing /\
                      disk_\bar{i} state' ?|= F

how do we implement this plan in Coq?
  need ghost variables to express this spec
  ghost variables are parameters to a function that only appear in its spec
  need to provide them in the proof to chain from one function to the next

also in this lab: recovery
recovery as part of refinement diagram
every function + crash + recovery is another transition of the system
  spec: pre + recovered of a top-level method
  code: impl with crash + recovery
  same diagram, but what is code transition?
    combination of a crash case for code and recovery procedure
    what does running recovery do? want to include crashes during recovery
      repeatedly run recovery with crashes
      finally recovery runs to completion
      intuition: recovery should be safe to re-run on crash
                 recovery with some crashes should be same as just running it
                 once (idempotence)
      theorem: if recovery satisifes a specification, and specification is idempotent,
               recovery satisfies the same specification even when re-run after every crash

what does replicated disk recovery do?
  disks can become out-of-sync on crash during write
  why is this a problem?
    disk starts out all zero
    write 1, crash in the middle
    now read returns 1
    first disk fails
    read now returns 0 -> not possible with single disk
  solution: on crash, copy from first disk to second
            only need to copy one sector
  maintain invariant even on crash that at most one sector is out-of-sync
  recovery fixes addresses one by one