Perennial
=========

Why this paper?
  Iris: a different approach to concurrency
  tackles concurrency and crash safety
  takes refinement and crash safety and scales up to complex programs
    with separation logic and concurrency

Three parts to lecture
  separation logic
  key ideas in Iris
  extending Iris in Perennial

preview: contrast between CSPEC and ownership-style reasoning
  recall: delivery proof reasoned that operations on temp files could
    move after other threads
  Iris: delivery finds a free file and then retains exclusive access
  recall: reading messages moves left
  Iris: ownership of directory contents cannot be invalidated by other
    threads (for delete, protect that ownership with a lock)

separation logic
  what is an assertion? example: boolean algebra over 0-1 variables
    variables x, y
    operations x /\ y, x \/ y, !x
    ex: {x: true, y: false} satisfies x \/ y as well as x /\ !y

  assertions/predicates are about _heaplets_
    heap: a map from locations to values
      on machine, the heap is from addresses to bytes
      in C, heap is from pointers to a sequence of values
    heaplet: a part of the heap
    simplest example of a predicate: a |-> v is true for a heaplet with
      only one mapping, from a to v

  what can we do with predicates?
    most interesting operation: p * q ("p and separately q") is a
      predicate that says the heap can be split into disjoint
      components, one satisfying p and the other q

    example: a1 |-> v * a2 |-> v says that the heap has exactly two
      mappings, and both point to v; if this holds, then a1 != a2
    example: a |-> v * a |-> v never holds in any heap
    assertion language also has logical operators like exists and forall

  separation logic is a program logic: think Hoare logic where we use
    these predicates to describe states
  example: {x |-> 5} x := 3 {x |-> 3}
  example: list(l, vs) := match vs with
                          | [] => x == null
                          | v::vs => exists tl,
                            l |-> (v, tl) * list(tl, vs)
                          end
           {list(l, vs)} insert(l, v) {r. list(r, v::vs)}

  read the triple {P} C {Q} as "if C is given a heaplet satisfying P, it
    will run without errors and will deliver a heaplet satisfying Q"

  using a triple: frame rule
         {P} C {Q}
    -----------------
    {P * F} C {Q * F}
    read this clockwise from bottom left: starting with a heap with a
      part satisfying P and separately F, prove that C can start with P
      and deliver Q, which produces Q and doesn't touch the F part
    alternately: if we know C only needs P, then if we give it extra
      resources it won't touch them

  why has separation logic been successful?
    corresponds to programmer intuition about memory
    more generally applies to resources
    amenable to automated techniques (esp Facebook's Infer)

Iris
  use separation logic for concurrency
  re-interpret assertions as ownership
    eg, a |-> v now means owning address a (and knowing it stores v)
    eg, emp means owning no resources
  key idea: threads own disjoint regions
    embodied in spawn rule (again, read clockwise)
       {R} C {True}
    ------------------
    {R} spawn(C) {emp}

    due to frame rule, spawn(C) means parent decides what to give child
  generalize from heaps to any resources
    previously, only resource was an address
  generalize splitting resources
    previously, heaps with disjoint domains
    now, any definition of separation
    resources should not be affected by other threads
    example: read-only pointers
  figure: Perennial figure 7
  invariants are a way to share resources
    inv I (in figures, box around I) is a shared invariant
    resources in invariant can only be used for one atomic step
    knowledge of invariant is freely shareable
    figure: Perennial figure 8
  lock invariants are a way to share resources for more than one step
    {I} new_lock() {l. is_lock(l, I)}
    {is_lock(l, I)} lock(l) {I}
    {I * is_lock(l, I)} unlock(l) {emp}
    is_lock is shareable
    is_lock can be defined using invariants and the above rules are
      theorems
  refinement reasoning as a resource
    introduce _specification resources_
      j |=> op means spec thread issued op
      source(σ) means abstract state is σ
    note: this is not quite how the labs work, because we don't need the
      spec operation resource
    implementation note: these together represent a forward simulation
      proof up till now
    what can we do with spec resources?
      forward simulation!
      j |=> Write(a, v) * source(σ) ==> j |=> ret r * source(σ')
      if σ ~~> σ' and returns r under Write(a, v) in spec
    if operations can maintain source(σ) as an invariant and transform
      spec operations into returns, then there is a forward simulation
  example of using these features: replicated disk, without crash safety
    d1[a] |-> v means disk 1 has block v at address a, if it has not
      failed (somewhat similar to =?= from labs)
    AbsR       := star(LockInv(a) for a in 0..disk.size()) * source(σ)
    LockInv(a) := is_lock(m[a], exists v. σ[a] = v *
                                          d1[a] |-> v *
                                          d2[a] |-> v)

Perennial
  motivation: concurrency and crash safety are difficult together
  example: observing write before a crash should imply it is durable
  example: without recovery, after crash completed write could go away
  need a specification: concurrent recovery refinement
    this is refinement + recovery (as seen in labs) + concurrency
  proof strategy:
  - refinement using standard Iris implementation
  - developer identifies a crash invariant
  - prove recovery goes from crash invariant to abstraction relation

  three techniques to make this work:
  - memory versioning: add version number to volatile resources,
    invalidate them by incrementing the current version (on crash)
  - recovery leases: lease on a durable resource can be locked to
    prevent other threads from accessing it, but recovery gets access
    even without lease
  - recovery helping: recovery can commit a pre-crash operation stored
    in the crash invariant

  memory versioning solves the problem that invariants hold at each
  intermediate point, but we need them to hold after a crash;
  incrementing the version number lets us express the global crash

  recovery leases solve the problem that threads need to lock durable
  resources, but they can't be in both a lock invariant and the crash
  invariant; separate lease and master copy, so lease can be locked to
  prevent concurrent access, but recovery gets master copy

  recovery helping solve the problem of justifying recovery simulating a
  crashed thread, by making the simulation persistent across a crash and
  giving recovery the same power to commit operations as any other
  thread

  example: extending replicated disk proof to crash safety
    AbsR       := star(LockInv(a) for a in 0..|d|) * CrashInv
    LockInv(a) := is_lock(m[a], exists v. σ[a] = v *
                                          lease(d1[a], v) * lease(d2[a], v)
    CrashInv   := source(σ) * star(DurInv(a) for a in 0..|d|)
    DurInv(a)  := exists v1 v2.
                    σ[a] = v2 *
                    d1[a] |-> v1 * d2[a] |-> v2 *
                    (v1 != v2 ==> exists j. j |=> Write(a, v1))

    idea: most of the abstraction relation holds on crash, except for
      case where disks differ, where we put a spec resource for the
      writing thread; lock invariant now protects leases rather than
      durable resources

Goose
  different strategy for running code: import system into a model in Coq
  model is kept simple by importing only stylized Go
  (demo of mailboat Go and Coq model)