Alloy spec for Snapshot Isolation

snapshot_isolation.als

// Alloy spec for Snapshot Isolation
// https://dl.acm.org/doi/10.1145/3360591
// Author of this spec: Ranadeep Biswas & John Wickerson

pred reflexive[r : univ -> univ, s : set univ] { (s <: iden) in r }

pred symmetric[r : univ -> univ] { r in ~r }

pred transitive[r : univ -> univ] { r.r in r }

pred irreflexive[r : univ -> univ] { no (iden & r) }

pred acyclic[r: univ->univ] { irreflexive[^r] }

pred equivalence[r : univ -> univ, s : set univ] {
  reflexive[r,s]
  symmetric[r]
  transitive[r]
}

pred strict_partial_order[r : univ -> univ ] {
  transitive[r]
  acyclic[r]
}

// cartesian product of a set with itself
fun sq[s : set univ] : univ -> univ { s -> s }

pred strict_total[r : univ -> univ, d : univ -> univ] { (d - iden) in (r + ~r) }

fun restrict[r : univ -> univ, s : set univ] : univ -> univ { r & (s -> s) }

//////////////////////////////////////

sig E {
  po : set E, // program order within transaction
  so : set E, // session order between transactions
  rf : set E, // reads-from
  sloc : set E// same-location 
}

sig W extends E {} // writes
sig R extends E {} // reads

fun w : E -> E { W <: iden }
fun r : E -> E { R <: iden }

fact {
  E in W + R // every event is a write or a read
}

// same-transaction
fun stxn : E -> E { *po + *~po }

// same-session
fun sses : E -> E { *(po+so) + *~(po+so) }

fact {
  strict_partial_order[po]
  ~po . po in stxn // no "forks" in po
  po . ~po in stxn // no "joins" in po
  no (po & (W -> R)) // two-phase transactions
  no (po & sloc & (W -> W)) // no two writes on the same location in the same transaction
  no (po & sloc & (R -> R)) // no two reads on the same location in the same transaction
}

fact {
  equivalence[sloc, E]
}

fact {
  strict_partial_order[so]
  ~so . so in sses // no "forks" in so
  so . ~so in sses // no "joins" in so
  stxn . so . stxn in so // so links every event in first transaction to every event in second transaction
  no (po & so) // po and so are disjoint
}

fact {
  rf . ~rf in iden // no "joins" in rf
  rf in W -> R // reads connect writes to reads
  rf in sloc
}

pred prefix_consistency[co : E->E] {
  w . ((*co . (so + rf)) & sloc) . r in *co . rf
  po + rf + so in co
  strict_partial_order[co]
  strict_total[co, E->E]
}

pred conflict[co : E->E] {
  w . ((*co . w . (co & sloc) . w . stxn) & sloc) . r in *co . rf
}

pred snapshot_isolation[co : E->E] {
  conflict[co]
  prefix_consistency[co]
}

pred PC_but_not_SI {

  not (some co : E->E | snapshot_isolation[co])

  some co : E->E | prefix_consistency[co]
}

run PC_but_not_SI for 2 E // expect no solution
run PC_but_not_SI for 3 E // expect no solution
run PC_but_not_SI for 4 E