Wiki Agenda Contact Version française

VerifyThis 2018: Array-based queuing lock

solution to VerifyThis 2018 challenge 3


Authors: Martin Clochard

Topics: Array Data Structure

Tools: Why3

References: VerifyThis @ ETAPS 2018

see also the index (by topic, by tool, by reference, by year)


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


download ZIP archive

Why3 Proof Results for Project "verifythis_2018_array_based_queuing_lock_1"

Theory "verifythis_2018_array_based_queuing_lock_1.Top": fully verified

ObligationsAlt-Ergo 2.0.0CVC4 1.5Z3 4.4.1
VC k0.00------
VC n0.00------
VC bounded_int0.00------
VC bzero0.00------
VC bounded_int20.00------
VC ticket0.01------
VC zero0.00------
VC increment---------
split_goal_right
VC increment.0---------
split_goal_right
VC increment.0.00.01------
VC increment.0.10.01------
VC increment.0.20.00------
VC increment.0.3---0.18---
VC increment.0.40.00------
VC increment.0.50.13------
VC increment.0.60.00------
VC increment.10.01------
VC increment.2---0.05---
VC increment.30.00------
VC modn0.00------
VC tinc0.02------
VC main---------
split_goal_right
VC main.00.01------
VC main.10.01------
VC main.20.01------
VC main.30.01------
VC main.40.01------
VC main.50.01------
VC main.60.01------
VC main.70.01------
VC main.80.02------
VC main.90.01------
VC main.100.16------
VC main.110.01------
VC main.120.01------
VC main.130.01------
VC main.140.02------
VC main.150.01------
VC main.160.01------
VC main.170.01------
VC main.180.02------
VC main.190.02------
VC main.200.04------
VC main.210.01------
VC main.220.00------
VC main.230.06------
VC main.240.01------
VC main.250.02------
VC main.260.02------
VC main.270.01------
VC main.280.11------
VC main.29---------
split_goal_right
VC main.29.01.37------
VC main.29.11.02------
VC main.29.21.80------
VC main.29.31.81------
VC main.300.01------
VC main.31---0.09---
VC main.32---0.12---
VC main.330.41------
VC main.340.63------
VC main.35---0.11---
VC main.36---------
split_goal_right
VC main.36.0------0.04
VC main.36.10.05------
VC main.36.20.09------
VC main.36.30.05------
VC main.370.02------
VC main.380.09------
VC main.390.01------
VC main.400.02------
VC main.410.02------
VC main.420.02------
VC main.430.02------
VC main.440.02------
VC main.450.60------
VC main.460.01------
VC main.470.02------
VC main.480.16------
VC main.49---------
split_goal_right
VC main.49.0------0.06
VC main.49.1------0.07
VC main.49.2------0.06
VC main.49.30.06------
VC main.500.01------
VC main.51---0.11---
VC main.52---0.13---
VC main.530.48------
VC main.54---------
split_goal_right
VC main.54.00.07------
VC main.54.10.19------
VC main.55---------
split_goal_right
VC main.55.0---0.21---
VC main.55.1---0.23---
VC main.56---------
split_goal_right
VC main.56.00.15------
VC main.56.10.19------
VC main.56.20.16------
VC main.56.33.30---0.10
VC main.570.01------
VC main.580.08------
VC main.590.01------
VC main.600.03------
VC main.61---0.20---
VC main.620.02------
VC main.630.02------
VC main.640.01------
VC main.65---------
split_goal_right
VC main.65.00.08------
VC main.65.10.11------
VC main.65.20.10------
VC main.65.30.12------
VC main.660.01------
VC main.670.01------
VC main.680.63------
VC main.69---------
split_goal_right
VC main.69.01.46------
VC main.69.11.59------
VC main.69.21.88------
VC main.69.33.98------
VC main.700.01------
VC main.71---0.13---
VC main.72---0.12---
VC main.73---------
split_goal_right
VC main.73.0------0.07
VC main.73.1------0.08
VC main.74------0.10
VC main.75---0.21---
VC main.76---------
split_goal_right
VC main.76.01.40------
VC main.76.10.15------
VC main.76.20.14------
VC main.76.30.20------
VC main.770.02------
VC main.780.03------
VC main.790.02------
VC main.800.03------
VC main.810.02------
VC main.820.01------
VC main.830.04------
VC main.84---------
split_goal_right
VC main.84.0------0.04
VC main.84.11.05------
VC main.84.2------0.04
VC main.84.3------0.04
VC main.85---------
split_goal_right
VC main.85.00.36------
VC main.85.10.26------
VC main.86---0.12---
VC main.87---0.14---
VC main.88---0.26---
VC main.89---0.24---
VC main.90---0.28---
VC main.91---------
split_goal_right
VC main.91.0------0.07
VC main.91.10.26------
VC main.91.20.33------
VC main.91.3------0.06
VC main.92---0.13---
VC main.930.01------
VC main.940.11------
VC main.950.01------
VC main.960.01------
VC main.97---0.12---
VC main.980.02------
VC main.990.03------
VC main.1000.02------
VC main.1010.68------
VC main.1020.03------
VC main.1030.03------