## 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 | Alt-Ergo 2.3.0 | CVC4 1.5 | CVC4 1.7 | Z3 4.5.0 | Z3 4.8.6 | ||

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

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

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

VC for bzero | --- | 0.01 | --- | --- | --- | --- | ||

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

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

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

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

split_goal_right | ||||||||

assertion | --- | --- | --- | --- | --- | --- | ||

split_goal_right | ||||||||

VC for increment | 0.01 | --- | --- | --- | --- | --- | ||

VC for increment | 0.01 | --- | --- | --- | --- | --- | ||

VC for increment | 0.00 | --- | --- | --- | --- | --- | ||

VC for increment | --- | --- | 0.18 | --- | --- | --- | ||

VC for increment | 0.00 | --- | --- | --- | --- | --- | ||

VC for increment | 0.13 | --- | --- | --- | --- | --- | ||

VC for increment | 0.00 | --- | --- | --- | --- | --- | ||

precondition | 0.01 | --- | --- | --- | --- | --- | ||

precondition | --- | --- | 0.05 | --- | --- | --- | ||

postcondition | 0.00 | --- | --- | --- | --- | --- | ||

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

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

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

split_goal_right | ||||||||

array creation size | 0.01 | --- | --- | --- | --- | --- | ||

postcondition | 0.01 | --- | --- | --- | --- | --- | ||

precondition | 0.01 | --- | --- | --- | --- | --- | ||

array creation size | 0.01 | --- | --- | --- | --- | --- | ||

array creation size | 0.01 | --- | --- | --- | --- | --- | ||

loop invariant init | 0.01 | --- | --- | --- | --- | --- | ||

loop invariant init | 0.01 | --- | --- | --- | --- | --- | ||

precondition | 0.01 | --- | --- | --- | --- | --- | ||

index in array bounds | 0.01 | --- | --- | --- | --- | --- | ||

index in array bounds | 0.02 | --- | --- | --- | --- | --- | ||

loop invariant preservation | 0.16 | --- | --- | --- | --- | --- | ||

loop invariant preservation | 0.01 | --- | --- | --- | --- | --- | ||

loop invariant init | 0.01 | --- | --- | --- | --- | --- | ||

index in array bounds | 0.01 | --- | --- | --- | --- | --- | ||

loop invariant preservation | 0.02 | --- | --- | --- | --- | --- | ||

index in array bounds | 0.01 | --- | --- | --- | --- | --- | ||

loop invariant init | 0.01 | --- | --- | --- | --- | --- | ||

loop invariant init | 0.01 | --- | --- | --- | --- | --- | ||

loop invariant init | 0.02 | --- | --- | --- | --- | --- | ||

loop invariant init | 0.02 | --- | --- | --- | --- | --- | ||

loop invariant init | 0.04 | --- | --- | --- | --- | --- | ||

loop invariant init | 0.01 | --- | --- | --- | --- | --- | ||

loop invariant init | 0.06 | --- | --- | --- | --- | --- | ||

loop invariant init | 0.00 | --- | --- | --- | --- | --- | ||

loop invariant init | 0.01 | --- | --- | --- | --- | --- | ||

index in array bounds | 0.03 | --- | --- | --- | --- | --- | ||

index in array bounds | 0.02 | --- | --- | --- | --- | --- | ||

index in array bounds | 0.02 | --- | --- | --- | --- | --- | ||

loop invariant preservation | 0.02 | --- | --- | --- | --- | --- | ||

loop invariant preservation | --- | --- | --- | --- | --- | 0.07 | ||

loop invariant preservation | 0.01 | --- | --- | --- | --- | --- | ||

loop invariant preservation | --- | --- | 0.09 | --- | --- | --- | ||

loop invariant preservation | --- | --- | 0.12 | --- | --- | --- | ||

loop invariant preservation | --- | --- | 0.10 | --- | --- | --- | ||

loop invariant preservation | --- | --- | 0.11 | --- | --- | --- | ||

loop invariant preservation | --- | --- | 0.12 | --- | --- | --- | ||

loop invariant preservation | --- | --- | --- | --- | --- | 0.40 | ||

loop invariant preservation | 0.01 | --- | --- | --- | --- | --- | ||

loop invariant preservation | 0.09 | --- | --- | --- | --- | --- | ||

loop invariant preservation | 0.01 | --- | --- | --- | --- | --- | ||

loop invariant preservation | 0.03 | --- | --- | --- | --- | --- | ||

loop invariant preservation | --- | --- | 0.12 | --- | --- | --- | ||

loop invariant preservation | 0.02 | --- | --- | --- | --- | --- | ||

loop invariant preservation | 0.02 | --- | --- | --- | --- | --- | ||

loop invariant preservation | 0.03 | --- | --- | --- | --- | --- | ||

loop invariant preservation | 0.80 | --- | --- | --- | --- | --- | ||

index in array bounds | 0.01 | --- | --- | --- | --- | --- | ||

index in array bounds | 0.03 | --- | --- | --- | --- | --- | ||

loop invariant preservation | 0.34 | --- | --- | --- | --- | --- | ||

loop invariant preservation | --- | --- | --- | --- | --- | 0.08 | ||

loop invariant preservation | 0.01 | --- | --- | --- | --- | --- | ||

loop invariant preservation | --- | --- | 0.13 | --- | --- | --- | ||

loop invariant preservation | --- | --- | 0.08 | --- | --- | --- | ||

loop invariant preservation | --- | --- | --- | --- | 0.15 | --- | ||

loop invariant preservation | --- | --- | 0.21 | --- | --- | --- | ||

loop invariant preservation | --- | --- | --- | --- | 0.11 | --- | ||

loop invariant preservation | --- | --- | --- | --- | --- | 0.16 | ||

loop invariant preservation | 0.01 | --- | --- | --- | --- | --- | ||

loop invariant preservation | --- | --- | --- | --- | 0.04 | --- | ||

loop invariant preservation | 0.01 | --- | --- | --- | --- | --- | ||

loop invariant preservation | 0.02 | --- | --- | --- | --- | --- | ||

loop invariant preservation | --- | --- | 0.13 | --- | --- | --- | ||

loop invariant preservation | 0.02 | --- | --- | --- | --- | --- | ||

loop invariant preservation | --- | --- | --- | --- | --- | --- | ||

split_goal_right | ||||||||

loop invariant preservation | --- | --- | 0.21 | --- | --- | --- | ||

loop invariant preservation | --- | --- | 0.10 | --- | --- | --- | ||

loop invariant preservation | 0.02 | --- | --- | --- | --- | --- | ||

loop invariant preservation | --- | --- | --- | --- | --- | --- | ||

split_goal_right | ||||||||

loop invariant preservation | --- | --- | --- | --- | 0.06 | --- | ||

loop invariant preservation | 0.16 | --- | --- | --- | --- | --- | ||

loop invariant preservation | 0.19 | --- | --- | --- | --- | --- | ||

loop invariant preservation | 0.15 | --- | --- | --- | --- | --- | ||

index in array bounds | 0.01 | --- | --- | --- | --- | --- | ||

index in array bounds | 0.02 | --- | --- | --- | --- | --- | ||

loop invariant preservation | 0.87 | --- | --- | --- | --- | --- | ||

loop invariant preservation | --- | --- | --- | --- | 0.06 | --- | ||

loop invariant preservation | 0.01 | --- | --- | --- | --- | --- | ||

loop invariant preservation | --- | --- | 0.11 | --- | --- | --- | ||

loop invariant preservation | --- | --- | --- | 0.16 | --- | --- | ||

loop invariant preservation | --- | --- | --- | --- | --- | 0.14 | ||

loop invariant preservation | --- | --- | --- | --- | --- | 0.32 | ||

loop invariant preservation | --- | --- | --- | 0.20 | --- | --- | ||

loop invariant preservation | --- | --- | --- | --- | --- | 0.20 | ||

index in array bounds | 0.01 | --- | --- | --- | --- | --- | ||

index in array bounds | 0.02 | --- | --- | --- | --- | --- | ||

index in array bounds | 0.01 | --- | --- | --- | --- | --- | ||

index in array bounds | 0.01 | --- | --- | --- | --- | --- | ||

index in array bounds | 0.02 | --- | --- | --- | --- | --- | ||

index in array bounds | 0.02 | --- | --- | --- | --- | --- | ||

loop invariant preservation | 0.04 | --- | --- | --- | --- | --- | ||

loop invariant preservation | --- | --- | --- | --- | --- | 0.06 | ||

loop invariant preservation | 0.94 | --- | --- | --- | --- | --- | ||

loop invariant preservation | --- | --- | 0.12 | --- | --- | --- | ||

loop invariant preservation | --- | --- | 0.14 | --- | --- | --- | ||

loop invariant preservation | --- | --- | 0.26 | --- | --- | --- | ||

loop invariant preservation | --- | --- | 0.28 | --- | --- | --- | ||

loop invariant preservation | --- | --- | 0.24 | --- | --- | --- | ||

loop invariant preservation | --- | --- | --- | --- | 0.06 | --- | ||

unreachable point | --- | --- | 0.13 | --- | --- | --- | ||

loop invariant preservation | 0.01 | --- | --- | --- | --- | --- | ||

loop invariant preservation | --- | --- | --- | --- | --- | --- | ||

split_goal_right | ||||||||

loop invariant preservation | 0.08 | --- | --- | --- | --- | --- | ||

loop invariant preservation | --- | --- | --- | --- | 0.06 | --- | ||

loop invariant preservation | 0.08 | --- | --- | --- | --- | --- | ||

loop invariant preservation | 0.06 | --- | --- | --- | --- | --- | ||

loop invariant preservation | 0.01 | --- | --- | --- | --- | --- | ||

loop invariant preservation | 0.01 | --- | --- | --- | --- | --- | ||

loop invariant preservation | --- | --- | 0.12 | --- | --- | --- | ||

loop invariant preservation | 0.02 | --- | --- | --- | --- | --- | ||

loop invariant preservation | 0.02 | --- | --- | --- | --- | --- | ||

loop invariant preservation | 0.02 | --- | --- | --- | --- | --- | ||

loop invariant preservation | 0.68 | --- | --- | --- | --- | --- | ||

out of loop bounds | 0.03 | --- | --- | --- | --- | --- | ||

out of loop bounds | 0.03 | --- | --- | --- | --- | --- |