## 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

Obligations | Alt-Ergo 2.0.0 | CVC4 1.5 | Z3 4.4.1 | ||

VC k | 0.00 | --- | --- | ||

VC n | 0.00 | --- | --- | ||

VC bounded_int | 0.00 | --- | --- | ||

VC bzero | 0.00 | --- | --- | ||

VC bounded_int2 | 0.00 | --- | --- | ||

VC ticket | 0.01 | --- | --- | ||

VC zero | 0.00 | --- | --- | ||

VC increment | --- | --- | --- | ||

split_goal_right | |||||

VC increment.0 | --- | --- | --- | ||

split_goal_right | |||||

VC increment.0.0 | 0.01 | --- | --- | ||

VC increment.0.1 | 0.01 | --- | --- | ||

VC increment.0.2 | 0.00 | --- | --- | ||

VC increment.0.3 | --- | 0.18 | --- | ||

VC increment.0.4 | 0.00 | --- | --- | ||

VC increment.0.5 | 0.13 | --- | --- | ||

VC increment.0.6 | 0.00 | --- | --- | ||

VC increment.1 | 0.01 | --- | --- | ||

VC increment.2 | --- | 0.05 | --- | ||

VC increment.3 | 0.00 | --- | --- | ||

VC modn | 0.00 | --- | --- | ||

VC tinc | 0.02 | --- | --- | ||

VC main | --- | --- | --- | ||

split_goal_right | |||||

VC main.0 | 0.01 | --- | --- | ||

VC main.1 | 0.01 | --- | --- | ||

VC main.2 | 0.01 | --- | --- | ||

VC main.3 | 0.01 | --- | --- | ||

VC main.4 | 0.01 | --- | --- | ||

VC main.5 | 0.01 | --- | --- | ||

VC main.6 | 0.01 | --- | --- | ||

VC main.7 | 0.01 | --- | --- | ||

VC main.8 | 0.02 | --- | --- | ||

VC main.9 | 0.01 | --- | --- | ||

VC main.10 | 0.16 | --- | --- | ||

VC main.11 | 0.01 | --- | --- | ||

VC main.12 | 0.01 | --- | --- | ||

VC main.13 | 0.01 | --- | --- | ||

VC main.14 | 0.02 | --- | --- | ||

VC main.15 | 0.01 | --- | --- | ||

VC main.16 | 0.01 | --- | --- | ||

VC main.17 | 0.01 | --- | --- | ||

VC main.18 | 0.02 | --- | --- | ||

VC main.19 | 0.02 | --- | --- | ||

VC main.20 | 0.04 | --- | --- | ||

VC main.21 | 0.01 | --- | --- | ||

VC main.22 | 0.00 | --- | --- | ||

VC main.23 | 0.06 | --- | --- | ||

VC main.24 | 0.01 | --- | --- | ||

VC main.25 | 0.02 | --- | --- | ||

VC main.26 | 0.02 | --- | --- | ||

VC main.27 | 0.01 | --- | --- | ||

VC main.28 | 0.11 | --- | --- | ||

VC main.29 | --- | --- | --- | ||

split_goal_right | |||||

VC main.29.0 | 1.37 | --- | --- | ||

VC main.29.1 | 1.02 | --- | --- | ||

VC main.29.2 | 1.80 | --- | --- | ||

VC main.29.3 | 1.81 | --- | --- | ||

VC main.30 | 0.01 | --- | --- | ||

VC main.31 | --- | 0.09 | --- | ||

VC main.32 | --- | 0.12 | --- | ||

VC main.33 | 0.41 | --- | --- | ||

VC main.34 | 0.63 | --- | --- | ||

VC main.35 | --- | 0.11 | --- | ||

VC main.36 | --- | --- | --- | ||

split_goal_right | |||||

VC main.36.0 | --- | --- | 0.04 | ||

VC main.36.1 | 0.05 | --- | --- | ||

VC main.36.2 | 0.09 | --- | --- | ||

VC main.36.3 | 0.05 | --- | --- | ||

VC main.37 | 0.02 | --- | --- | ||

VC main.38 | 0.09 | --- | --- | ||

VC main.39 | 0.01 | --- | --- | ||

VC main.40 | 0.02 | --- | --- | ||

VC main.41 | 0.02 | --- | --- | ||

VC main.42 | 0.02 | --- | --- | ||

VC main.43 | 0.02 | --- | --- | ||

VC main.44 | 0.02 | --- | --- | ||

VC main.45 | 0.60 | --- | --- | ||

VC main.46 | 0.01 | --- | --- | ||

VC main.47 | 0.02 | --- | --- | ||

VC main.48 | 0.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.3 | 0.06 | --- | --- | ||

VC main.50 | 0.01 | --- | --- | ||

VC main.51 | --- | 0.11 | --- | ||

VC main.52 | --- | 0.13 | --- | ||

VC main.53 | 0.48 | --- | --- | ||

VC main.54 | --- | --- | --- | ||

split_goal_right | |||||

VC main.54.0 | 0.07 | --- | --- | ||

VC main.54.1 | 0.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.0 | 0.15 | --- | --- | ||

VC main.56.1 | 0.19 | --- | --- | ||

VC main.56.2 | 0.16 | --- | --- | ||

VC main.56.3 | 3.30 | --- | 0.10 | ||

VC main.57 | 0.01 | --- | --- | ||

VC main.58 | 0.08 | --- | --- | ||

VC main.59 | 0.01 | --- | --- | ||

VC main.60 | 0.03 | --- | --- | ||

VC main.61 | --- | 0.20 | --- | ||

VC main.62 | 0.02 | --- | --- | ||

VC main.63 | 0.02 | --- | --- | ||

VC main.64 | 0.01 | --- | --- | ||

VC main.65 | --- | --- | --- | ||

split_goal_right | |||||

VC main.65.0 | 0.08 | --- | --- | ||

VC main.65.1 | 0.11 | --- | --- | ||

VC main.65.2 | 0.10 | --- | --- | ||

VC main.65.3 | 0.12 | --- | --- | ||

VC main.66 | 0.01 | --- | --- | ||

VC main.67 | 0.01 | --- | --- | ||

VC main.68 | 0.63 | --- | --- | ||

VC main.69 | --- | --- | --- | ||

split_goal_right | |||||

VC main.69.0 | 1.46 | --- | --- | ||

VC main.69.1 | 1.59 | --- | --- | ||

VC main.69.2 | 1.88 | --- | --- | ||

VC main.69.3 | 3.98 | --- | --- | ||

VC main.70 | 0.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.0 | 1.40 | --- | --- | ||

VC main.76.1 | 0.15 | --- | --- | ||

VC main.76.2 | 0.14 | --- | --- | ||

VC main.76.3 | 0.20 | --- | --- | ||

VC main.77 | 0.02 | --- | --- | ||

VC main.78 | 0.03 | --- | --- | ||

VC main.79 | 0.02 | --- | --- | ||

VC main.80 | 0.03 | --- | --- | ||

VC main.81 | 0.02 | --- | --- | ||

VC main.82 | 0.01 | --- | --- | ||

VC main.83 | 0.04 | --- | --- | ||

VC main.84 | --- | --- | --- | ||

split_goal_right | |||||

VC main.84.0 | --- | --- | 0.04 | ||

VC main.84.1 | 1.05 | --- | --- | ||

VC main.84.2 | --- | --- | 0.04 | ||

VC main.84.3 | --- | --- | 0.04 | ||

VC main.85 | --- | --- | --- | ||

split_goal_right | |||||

VC main.85.0 | 0.36 | --- | --- | ||

VC main.85.1 | 0.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.1 | 0.26 | --- | --- | ||

VC main.91.2 | 0.33 | --- | --- | ||

VC main.91.3 | --- | --- | 0.06 | ||

VC main.92 | --- | 0.13 | --- | ||

VC main.93 | 0.01 | --- | --- | ||

VC main.94 | 0.11 | --- | --- | ||

VC main.95 | 0.01 | --- | --- | ||

VC main.96 | 0.01 | --- | --- | ||

VC main.97 | --- | 0.12 | --- | ||

VC main.98 | 0.02 | --- | --- | ||

VC main.99 | 0.03 | --- | --- | ||

VC main.100 | 0.02 | --- | --- | ||

VC main.101 | 0.68 | --- | --- | ||

VC main.102 | 0.03 | --- | --- | ||

VC main.103 | 0.03 | --- | --- |