why3/examples/verifythis_2018_array_based_queuing_lock_1.mlw

(**

{1 VerifyThis @ ETAPS 2018 competition
   Challenge 3: Array-Based Queuing Lock}

Author: Martin Clochard (LRI, Université Paris Sud)
*)

use int.Int
use int.ComputerDivision
use import seq.Seq as S
use array.Array
use ref.Ref

val constant k : int ensures { result > 0 }
val constant n : int ensures { result > 0 }

(* Model of bounded arithmetic.
   Note: bincrement only model the incrementation behind fetch_and_add,
   not the atomic operation itself. *)
type bounded_int = private { ghost bmodel : int }
invariant { 0 <= bmodel < k * n } by { bmodel = 0 }
val constant bzero : bounded_int
  ensures { result.bmodel = 0 }
val bincrement (b:bounded_int) : bounded_int
  ensures { let v = b.bmodel + 1 in
    result.bmodel = if v = k * n then 0 else v }
val bmodn (b:bounded_int) : int
  ensures { result = mod b.bmodel n }

(* Minor ghost wrapping of the model to get rid of k from the model,
   while keeping the same operational meaning. *)
type bounded_int2 = {
  value : bounded_int;
  ghost model : int;
} invariant { 0 <= model < n }
invariant { model = mod value.bmodel n }
by { value = bzero; model = 0 }
type ticket = { tvalue : int } invariant { 0 <= tvalue < n }

let zero () : bounded_int2
  ensures { result.model = 0 }
= { value = bzero; model = 0 }
let increment (b:bounded_int2) : bounded_int2
  ensures { let v = b.model + 1 in
    result.model = if v = n then 0 else v }
= let ghost v0 = b.model in
  let ghost v1 = if v0+1 = n then 0 else v0 + 1 in
  let ghost v2 = b.value.bmodel in
  assert { mod (v2+1) n = v1 by exists q.
    v2 = n * q + v0 so q >= 0 so v2 + 1 = n * q + (v0+1)
    so if v0+1 < n then v0+1 = mod (v2+1) n else
      v2+1 = n * (q+1) + 0 so 0 = mod (v2+1) n };
  { value = bincrement b.value; model = v1 }
let modn (b:bounded_int2) : ticket
  ensures { result.tvalue = b.model }
= { tvalue = bmodn b.value }
let tinc (t:ticket) : ticket
  ensures { let v = t.tvalue + 1 in result.tvalue = if v = n then 0 else v }
= { tvalue = mod (t.tvalue + 1) n }

(* Break down the thread state between each operation that affect or
   read the global state *)
type thread_state =
  | AcqFetched ticket (* Corresponds to control point right after the fetch. *)
  | Granted ticket (* Corresponds to observation that pass was true.
    If it was false, there may be intermediate steps, but they do not
    rely on global state --> state equivalent to lock granted. *)
  | RelSet ticket (* Corresponds to the pass = false operation. *)
  | Released ticket (* Corresponds to a released state.
    for technical reasons, we keep the last ticket used here
    (which is defaulted to the thread id at the beginning *)

function ticket (s:thread_state) : int = match s with
  | AcqFetched t | Granted t | RelSet t | Released t -> t.tvalue
  end

predicate released (s:thread_state) = match s with
  | Released _ -> true | _ -> false
  end

(* For verification of task 2: log of request/acquire events
   identified by thread id. *)
type event =
  | Request int
  | Acquire int

type hidden = private mutable {}
val hidden : hidden

(* scheduler. *)
val schedule () : int
  writes { hidden }
  ensures { 0 <= result < n }

(* if a thread is in a granted or released state,
   check whether it begins an acquire or release. Otherwise,
   the state stays the same. *)
val acqrel (id: int) : bool
  writes { hidden }

(* Model execution of concurrent program. *)
let main () : unit
  diverges
= (* Model of the pass buffer. The begin-end block with post-condition
     hide the fact that the array was technically initialized. *)
  let pass = begin ensures { result.length = n } make n false end in
  (* Model of the next variable. *)
  let next = ref (zero ()) in
  (* Thread state. *)
  let state = make n (Released { tvalue = 0 }) in
  (* Additional reciprocal map for the cyclically allocated tickets. *)
  let tmap = make n 0 in
  for i = 0 to n - 1 do
    invariant { forall j. 0 <= j < i -> match state[j] with
      | Released t -> t.tvalue = j
      | _ -> false end }
    invariant { forall j. 0 <= j < i -> tmap[j] = j }
    state[i] <- Released { tvalue = i };
    tmap[i] <- i
  done;
  (* Extra variable for verification: index of the currently held ticket. *)
  let current = ref (modn (zero ())) in
  (* Event log (for second task). *)
  (* let log = ref empty in *)
  (* Initialisation, done before the threads are executed. *)
  for i = 1 to n - 1 do
    invariant { forall j. 1 <= j < i -> not pass[j] }
    pass[i] <- false;
  done;
  pass[0] <- true;
  while true do
    invariant { forall i. 0 <= i < n /\ pass[i] -> i = !current.tvalue }
    invariant { forall i. 0 <= i < n -> match state[i] with
      | Granted t -> t.tvalue = !current.tvalue /\ pass[t.tvalue]
      | RelSet t -> t.tvalue = !current.tvalue /\ not pass[t.tvalue]
      | _ -> true
      end
    }
    invariant { forall i. 0 <= i < n -> 0 <= tmap[i] < n }
    invariant { forall i. 0 <= i < n -> ticket state[tmap[i]] = i }
    invariant { forall i. 0 <= i < n -> tmap[ticket state[i]] = i }
    invariant { !next.model < !current.tvalue ->
      (forall i. 0 <= i < !next.model \/ !current.tvalue <= i < n ->
        not released state[tmap[i]])
      /\ (forall i. !next.model <= i < !current.tvalue ->
        released state[tmap[i]]) }
    invariant { !next.model > !current.tvalue ->
      (forall i. !current.tvalue <= i < !next.model ->
        not released state[tmap[i]])
      /\ (forall i. 0 <= i < !current.tvalue \/ !next.model <= i < n ->
        released state[tmap[i]]) }
    invariant { !next.model = !current.tvalue ->
      forall i j. 0 <= i < j < n ->
        released state[tmap[i]] <-> released state[tmap[j]] }
    (* Invariant corresponding to Task 1, slightly strengthened. *)
    invariant { forall i j. 0 <= i < j < n ->
      match state[i], state[j] with
      | (Granted _ | RelSet _), (Granted _ | RelSet _) -> false
      | _ -> true end
    }
    let id = schedule () in
    match state[id] with
    | AcqFetched ticket ->
      if pass[ticket.tvalue] then state[id] <- Granted ticket
    | Granted ticket -> if acqrel id then begin
        state[id] <- RelSet ticket;
        pass[ticket.tvalue] <- false;
      end
    | RelSet ticket ->
        state[id] <- Released ticket;
        pass[(tinc ticket).tvalue] <- true;
        current := tinc !current;
    | Released told -> if acqrel id then begin
        let ticket = modn !next in
        let id2 = tmap[ticket.tvalue] in
        match state[id2] with
        | Released _ -> state[id2] <- Released told;
          tmap[ticket.tvalue] <- id;
          tmap[told.tvalue] <- id2
        | _ -> absurd
        end;
        state[id] <- AcqFetched ticket;
        next := increment !next
      end
    end
  done