(** {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