verifythis_2018_array_based_queuing_lock_1.mlw 6.56 KB
Newer Older
1 2 3 4 5 6 7 8
(**

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

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

9 10
use int.Int
use int.ComputerDivision
11
use import seq.Seq as S
12 13
use array.Array
use ref.Ref
14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188

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