Consistency models

// findOrder looks for one total order of all ops in which each read returns the latest write on
// its key (0 if none), and op a comes before op b whenever mustPrecede(a, b). It tries every op
// whose predecessors are already placed, applies it to the registers, and backtracks on a read
// that does not match. Dead ends are remembered by (ops placed, register values).
func findOrder(h History, mustPrecede func(a, b Op) bool) ([]int, bool) {
  n := len(h.Ops)
  placed := make([]bool, n)
  order := make([]int, 0, n)
  regs := map[string]int{}
  dead := map[string]bool{}

  var place func() bool
  place = func() bool {
    if len(order) == n {
      return true
    }
    memo := stateKey(placed, regs)
    if dead[memo] {
      return false
    }
    for i, o := range h.Ops {
      if placed[i] || !ready(h, placed, o, mustPrecede) {
        continue
      }
      if o.Kind == Read && regs[o.Key] != o.Value {
        continue // this read cannot come next: the register holds another value
      }
      prev, had := regs[o.Key]
      if o.Kind == Write {
        regs[o.Key] = o.Value
      }
      placed[i] = true
      order = append(order, i)
      if place() {
        return true
      }
      order = order[:len(order)-1]
      placed[i] = false
      if o.Kind == Write {
        if had {
          regs[o.Key] = prev
        } else {
          delete(regs, o.Key)
        }
      }
    }
    dead[memo] = true
    return false
  }
  if !place() {
    return nil, false
  }
  return order, true
}

// ready reports whether every op that must precede o is already placed.
func ready(h History, placed []bool, o Op, mustPrecede func(a, b Op) bool) bool {
  for j, p := range h.Ops {
    if !placed[j] && j != o.ID && mustPrecede(p, o) {
      return false
    }
  }
  return true
}

// Causal checks causal consistency: no read returns a value that its own causal past has
// overwritten. Concurrent writes may appear in any order, and different clients may disagree.
func Causal(h History) Verdict {
  if r := h.thinAir(); r >= 0 {
    return Verdict{Bad: []int{r}, Rule: RuleThinAir}
  }
  c := newCausalOrder(h)
  for _, a := range h.Ops {
    if c.before[a.ID][a.ID] {
      return Verdict{Bad: []int{a.ID}, Rule: RuleCycle}
    }
  }
  for _, r := range h.Ops {
    if r.Kind != Read {
      continue
    }
    for _, w := range h.Ops {
      // A newer write on the same key happens before the read, and the read returned
      // something older: the initial value, or a write that happens before w.
      if w.Kind != Write || w.Key != r.Key || !c.before[w.ID][r.ID] || !c.older(c.src[r.ID], w.ID) {
        continue
      }
      if c.src[r.ID] < 0 {
        return Verdict{Bad: []int{w.ID, r.ID}, Path: c.path(w.ID, r.ID), Rule: RuleInitRead}
      }
      return Verdict{Bad: []int{c.src[r.ID], w.ID, r.ID}, Path: c.path(w.ID, r.ID), Rule: RuleOverwritten}
    }
  }
  return Verdict{OK: true}
}

// ReadYourWrites: after a client writes a key, its reads of that key never return anything older.
func ReadYourWrites(h History) Verdict {
  if r := h.thinAir(); r >= 0 {
    return Verdict{Bad: []int{r}, Rule: RuleThinAir}
  }
  c := newCausalOrder(h)
  for _, w := range h.Ops {
    for _, r := range h.Ops {
      if w.Kind == Write && r.Kind == Read && r.Key == w.Key && programBefore(w, r) && c.older(c.src[r.ID], w.ID) {
        return Verdict{Bad: []int{w.ID, r.ID}, Path: []int{w.ID, r.ID}, Rule: RuleRYW}
      }
    }
  }
  return Verdict{OK: true}
}

// MonotonicReads: once a client has read a value, its later reads of that key never return
// anything older.
func MonotonicReads(h History) Verdict {
  if r := h.thinAir(); r >= 0 {
    return Verdict{Bad: []int{r}, Rule: RuleThinAir}
  }
  c := newCausalOrder(h)
  for _, r1 := range h.Ops {
    for _, r2 := range h.Ops {
      if r1.Kind == Read && r2.Kind == Read && r1.Key == r2.Key && programBefore(r1, r2) &&
        c.src[r1.ID] >= 0 && c.older(c.src[r2.ID], c.src[r1.ID]) {
        return Verdict{Bad: []int{r1.ID, r2.ID}, Path: []int{c.src[r1.ID], r1.ID, r2.ID}, Rule: RuleMR}
      }
    }
  }
  return Verdict{OK: true}
}

// MonotonicWrites: a client that sees a client's second write also sees its first.
func MonotonicWrites(h History) Verdict {
  if r := h.thinAir(); r >= 0 {
    return Verdict{Bad: []int{r}, Rule: RuleThinAir}
  }
  c := newCausalOrder(h)
  for _, w1 := range h.Ops {
    for _, w2 := range h.Ops {
      if w1.Kind != Write || w2.Kind != Write || !programBefore(w1, w2) {
        continue
      }
      if v, ok := sawThenMissed(h, c, w2.ID, w1); ok {
        return Verdict{Bad: append([]int{w1.ID}, v...), Path: append([]int{w1.ID}, v...), Rule: RuleMW}
      }
    }
  }
  return Verdict{OK: true}
}

// WritesFollowReads: a client's write comes after everything the client had read, directly or
// through earlier reads. A client that sees the write also sees those values.
func WritesFollowReads(h History) Verdict {
  if r := h.thinAir(); r >= 0 {
    return Verdict{Bad: []int{r}, Rule: RuleThinAir}
  }
  c := newCausalOrder(h)
  for _, w1 := range h.Ops {
    for _, w2 := range h.Ops {
      // w1 is another client's write that w2's writer had seen before writing w2.
      if w1.Kind != Write || w2.Kind != Write || w1.Proc == w2.Proc || !c.before[w1.ID][w2.ID] {
        continue
      }
      if v, ok := sawThenMissed(h, c, w2.ID, w1); ok {
        p := append(c.path(w1.ID, w2.ID), v[1:]...)
        return Verdict{Bad: append([]int{w1.ID}, v...), Path: p, Rule: RuleWFR}
      }
    }
  }
  return Verdict{OK: true}
}

// sawThenMissed finds a client that reads write w2 and later reads w1's key and gets something
// older than w1. It returns [w2, that read, the later read].
func sawThenMissed(h History, c causalOrder, w2 int, w1 Op) ([]int, bool) {
  for _, r := range h.Ops {
    if r.Kind != Read || c.src[r.ID] != w2 {
      continue
    }
    for _, r2 := range h.Ops {
      if r2.Kind == Read && r2.Key == w1.Key && programBefore(r, r2) && c.older(c.src[r2.ID], w1.ID) {
        return []int{w2, r.ID, r2.ID}, true
      }
    }
  }
  return nil, false
}