// A port of the proof of Peterson's Algorithm from:
// http://homes.cs.washington.edu/~jrw12/SharedMem.html
//
// Look ma, no proofs!
//
// James R. Wilcox
// January 9, 2017

// There are six possible PCs for each thread, each corresponding to
// the beginning of one atomic step.
datatype PC = SetFlag | SetVictim | CheckFlag | CheckVictim | Crit | ResetFlag

method Peterson()
decreases *
{
  // Thread ids will be ints 0 or 1.
  // Below, we will use 1-t to get the "other" tid from a tid t.

  // We store some variables in arrays so that we can write the code
  // for both threads at once, indexed by the thread id.
  var flag := new bool[2];
  flag[0] := false;
  flag[1] := false;

  // The algorithm is correct regardless of the initial value of
  // victim, so we initialize it nondeterministically.
  var victim;
  if * {
    victim := 0;
  } else {
    victim := 1;
  }

  var pc := new PC[2];
  pc[0] := SetFlag;
  pc[1] := SetFlag;


  while true
    // Invariant 1: whenever t's flag is false, its PC is at SetFlag.
    //
    // Comment this out to see that it is required by Invariant 2.
    invariant forall t :: 0 <= t < 2 && !flag[t] ==> pc[t] == SetFlag

    // Invariant 2: If t holds the lock and 1-t is trying to get it,
    //              then victim == 1-t. (victim != t works too!).
    //
    // Comment this out to see that it is required by the mutual
    // exclusion invariant below!
    //
    // Writing the invariant like this, using t' to represent the
    // other thread, avoids a trigger matching loop.
    invariant forall t, t' :: 0 <= t < 2 ==> t' == 1-t ==>
        (pc[t] == Crit || pc[t] == ResetFlag) ==>
        (pc[t'] == CheckVictim || pc[t'] == CheckFlag ||
         pc[t'] == Crit || pc[t'] == ResetFlag) ==>
        victim != t

     // This is mutual exclusion: It is never the case that both
     // threads are in the critical section.
     //
     // This is directly implied by Invariant 2, since if both PCs are
     // Crit, then the victim cannot be equal to either thread.
     //
     // Dafny is clever enough to infer an additional loop invariant,
     // namely 0 <= victim < 2, which is required to complete the proof.
    invariant !(pc[0] == Crit && pc[1] == Crit)

    decreases *
  {
    // Each iteration of the loop simulates one atomic step of execution.

    // First, nondeterministically select the thread that gets to step.
    var t;
    if * {
      t := 0;
    } else {
      t := 1;
    }

    // Now, branch on the selected thread's current PC and execute the
    // corresponding atomic step.
    //
    // Note that each step only reads or writes one shared variable.
    match pc[t] {
      case SetFlag     => flag[t] := true; pc[t] := SetVictim;
      case SetVictim   => victim := t; pc[t] := CheckFlag;
      case CheckFlag   => pc[t] := if flag[1-t] then CheckVictim else Crit;
      case CheckVictim => pc[t] := if victim == t then CheckFlag else Crit;
      case Crit        => pc[t] := ResetFlag;
      case ResetFlag   => flag[t] := false; pc[t] := SetFlag;
    }
  }
}