## VerifyThis 2018: Array-based queuing lock (alt)

solution to VerifyThis 2018 challenge 3

**Authors:** Raphaël Rieu-Helft

**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: Raphaël Rieu-Helft (LRI, Université Paris Sud)

module ABQL use array.Array use int.Int use ref.Refint use int.EuclideanDivision use option.Option val constant n : int axiom N_val: 2 <= n val constant k : int axiom K_val: 2 <= k type tick = { b : int; (* ticket number *) ghost v : int; (* unbounded ticket number *) } invariant { 0 <= v /\ 0 <= b < k*n /\ b = mod v (k*n) } by { b = 0; v = 0 } let fetch_and_add (r:ref tick) ensures { !r.v = old !r.v + 1 } ensures { result = old !r } = let res = !r in assert { mod (res.b + 1) (k*n) = mod (res.v + 1) (k*n) by let a = div res.v (k*n) in res.v = (k*n) * a + mod res.v (k*n) so mod res.v (k*n) = res.b so mod (res.v+1) (k*n) = mod ((k*n) * a + (res.b + 1)) (k*n) = mod (res.b+1) (k*n) }; r := { v = res.v + 1; b = mod (res.b + 1) (k*n) }; res predicate lt (tick1 tick2: tick) = tick1.v < tick2.v use import seq.Seq as S use seq.Mem use seq.FreeMonoid predicate sorted (s: seq tick) = forall i j. 0 <= i < j < length s -> lt s[i] s[j] predicate consecutive (l: seq tick) = forall i. 0 < i < length l -> l[i].v = l[i-1].v + 1 (* | Consecutive_Nil : consecutive Nil | Consecutive_One : forall t. consecutive (Cons t Nil) | Consecutive_Two : forall t1 t2 l. t2.v = t1.v + 1 -> consecutive (Cons t2 l) -> consecutive (Cons t1 (Cons t2 l)) *) function last (l: seq tick) : option tick = if length l = 0 then None else Some l[length l - 1] (* = match l with | Nil -> None | Cons x Nil -> Some x | Cons _ l -> last l end *) let lemma last_push (l: seq tick) (x:tick) ensures { last (l ++ (cons x empty)) = Some x } = () let lemma consecutive_last_push (l: seq tick) (x:tick) requires { consecutive l } requires { match last l with | None -> true | Some y -> x.v = y.v + 1 end } ensures { consecutive (l ++ (cons x empty)) } = () function hd (l: seq tick) : option tick = if length l = 0 then None else Some l[0] lemma hd_push: forall l,x:tick. hd l = None \/ hd (l ++ (cons x empty)) = hd l let rec lemma consecutive_implies_sorted (l: seq tick) (i j: int) requires { consecutive l } requires { 0 <= i < j < length l } ensures { lt l[i] l[j] } variant { j - i } = if i+1 < j then consecutive_implies_sorted l (i+1) j (* we associate a program counter to each thread I: idle function acquire A1: var my_ticket = fetch_and_add (next,1) A2: while not pass[my_ticket] do () done; A3: return my_ticket W: working (with lock) function release(my_ticket) R1: pass[my_ticket] = false R2: pass[my_ticket+1 mod N] = true *) type pc = A1 | A2 | A3 | R1 | R2 | I | W predicate has_ticket (pc:pc) = match pc with | A1 | I -> false | _ -> true end predicate has_lock (pc:pc) = match pc with | A3 | W | R1 | R2 -> true | _ -> false end type nondet_source type rng = abstract { mutable source : nondet_source } val random : rng val scheduler () : int ensures { 0 <= result < n } writes { random } use array.NumOfEq use queue.Queue use array.Array let lemma numof_equiv (a1 a2: array 'a) (v:'a) (l u: int) requires { forall i. l <= i < u -> a1[i]=v <-> a2[i]=v } ensures { numof a1 v l u = numof a2 v l u } = () let lemma numof_add (a: array 'a) (v:'a) (l u: int) (i:int) requires { l <= i < u } requires { a[i] <> v } ensures { numof a[i <- v] v l u = numof a v l u + 1 } = assert { numof a[i<-v] v l i = numof a v l i }; assert { numof a[i<-v] v i (i+1) = 1 + numof a v i (i+1) }; assert { numof a[i<-v] v (i+1) u = numof a v (i+1) u } lemma mod_diff: forall a b c:int. c > 0 -> mod a c = mod b c -> mod (a-b) c = 0 by a = c * (div a c) + mod a c so b = c * (div b c) + mod b c so a - b = c * (div a c - div b c) + 0 so mod (a-b) c = mod 0 c = 0 let main () : unit diverges = let pass = Array.make (k*n) false in pass[0] <- true; let next = ref { v = 0; b = 0 } in let pcs = Array.make n I in let memo : array (option tick) = Array.make n None in (* value of my_ticket if set *) let owners : array (option int) = Array.make (k*n) None in (* who owns which ticket *) let ghost lock_holder : ref int = ref (-1) in let ghost waiting_list = Queue.create () in let ghost active_tick = ref None in while true do invariant { [@expl:safety] forall th. 0 <= th < n -> th <> !lock_holder -> not has_lock (pcs[th]) } invariant { -1 <= !lock_holder < n } invariant { forall b. 0 <= b < k*n -> match owners[b] with | None -> true | Some th -> 0 <= th < n /\ match memo[th] with | None -> false | Some tick -> tick.b = b end end } invariant { forall tick. pass[tick.b] -> match owners[tick.b] with | None -> !lock_holder = -1 | Some th -> !lock_holder = -1 \/ !lock_holder = th end } invariant { 0 <= !lock_holder < n -> match pcs[!lock_holder] with | A3 | W | R1 -> match memo[!lock_holder] with | None -> false | Some tick -> pass[tick.b] end | R2 -> forall b. 0 <= b < k * n -> not pass[b] | _ -> false end } invariant { forall b1 b2. 0 <= b1 < k*n -> 0 <= b2 < k*n -> pass[b1] = true /\ pass[b2] = true -> b1 = b2 } invariant { 0 <= !lock_holder < n -> has_lock (pcs[!lock_holder]) /\ match memo[!lock_holder] with | None -> false | Some tick -> !active_tick = Some tick end } invariant { forall th. 0 <= th < n -> match memo[th] with | Some tick -> owners[tick.b] = Some th | None -> true end } invariant { forall th. 0 <= th < n -> (memo[th] <> None <-> has_ticket (pcs[th])) } invariant { forall tick. mem tick waiting_list -> match owners[tick.b] with | None -> false | Some th -> pcs[th] = A2 /\ memo[th] = Some tick end } invariant { forall th. 0 <= th < n -> match memo[th] with | Some tick -> mem tick waiting_list \/ !active_tick = Some tick | None -> true end } invariant { forall th. 0 <= th < n -> not has_lock pcs[th] -> match memo[th] with | None -> pcs[th] <> A2 | Some tick -> mem tick waiting_list end } invariant { consecutive waiting_list } (* also implies unicity *) invariant { S.length waiting_list = numof pcs A2 0 n } invariant { forall tick. mem tick waiting_list -> !next.v - S.length waiting_list <= tick.v < !next.v } invariant { match last waiting_list with | None -> true | Some t -> t.v = !next.v - 1 end} invariant { match hd waiting_list with | None -> true | Some t -> t.v = !next.v - S.length waiting_list end } invariant { match !active_tick with | None -> !lock_holder = -1 | Some tick -> (match hd waiting_list with | None -> !next.v = tick.v + 1 | Some t -> t.v = tick.v + 1 end) /\ tick.v = !next.v - S.length waiting_list - 1 /\ 0 <= !lock_holder < n /\ memo[!lock_holder] = Some tick end } invariant { 0 <= S.length waiting_list <= n } (* invariant { length waiting_list = n \/ owners[!next.b] = None } *) invariant { [@expl:liveness] !lock_holder = - 1 -> (* someone is in the critical section... *) ((if S.length waiting_list = 0 then false else let tick = S.get waiting_list 0 in pass[tick.b] = true) (* ...or someone has a ticket to the critical section... *) \/ (exists th. 0 <= th < n /\ memo[th] = None /\ pass[!next.b] = true) /\ waiting_list = empty) (* ...or someone can take one *) } let th = scheduler () in (*choose a thread*) (* make it progress by 1 step *) label Step in match pcs[th] with | I -> pcs[th] <- A1 | A1 -> let tick = fetch_and_add next in assert { is_none owners[tick.b] by S.length waiting_list <= n < 2*n - 1 <= k*n - 1 so ((forall tick'. mem tick' waiting_list -> (tick'.b <> tick.b) by 0 < tick.v - tick'.v < k*n so mod (tick.v - tick'.v) (k*n) <> 0 so mod tick.v (k*n) <> mod tick'.v (k*n))) so forall th'. owners[tick.b] = Some th' -> false by match memo[th'] with | None -> false | Some tick' -> false by tick'.b = tick.b so not mem tick' waiting_list so !active_tick = Some tick' so 0 < tick.v - tick'.v < k*n so mod (tick.v - tick'.v) (k*n) <> 0 so mod tick.v (k*n) <> mod tick'.v (k*n) end }; assert { forall th. 0 <= th < n -> memo[th] <> Some tick }; owners[tick.b] <- Some th; memo[th] <- Some tick; pcs[th] <- A2; assert { numof pcs A2 0 n = numof pcs A2 0 n at Step + 1 }; assert { !lock_holder = !lock_holder at Step <> th }; assert { forall tick'. mem tick' waiting_list -> tick'.b <> tick.b /\ owners[tick'.b] <> Some th }; assert { forall tick'. mem tick' waiting_list -> match owners[tick'.b] with | None -> false | Some th' -> pcs[th'] = A2 /\ memo[th'] = Some tick' by th <> th' so pcs[th'] = pcs[th'] at Step so memo[th'] = memo[th'] at Step end }; push tick waiting_list; assert { consecutive waiting_list by waiting_list = waiting_list at Step ++ (cons tick empty) }; assert { match !active_tick with | None -> !lock_holder = -1 | Some tick' -> (match hd waiting_list with | None -> false | Some t -> t.v = tick'.v + 1 by match hd waiting_list at Step with | None -> t = tick so tick.v = !next.v at Step = tick'.v + 1 | Some t -> t.v = tick'.v + 1 /\ hd waiting_list = Some t end end) end }; assert { !lock_holder = -1 -> if S.length waiting_list = 0 then false else let t1 = S.get waiting_list 0 in pass[t1.b] by if S.length (waiting_list at Step) = 0 then pass[t1.b] by (t1 = tick /\ pass[tick.b] by pass[!next.b at Step]) else let t = S.get (waiting_list at Step) 0 in pass[t1.b] by t=t1 so pass[t.b] }; assert { match hd waiting_list with | None -> true | Some t -> if t = tick then t.v = !next.v - S.length waiting_list by waiting_list at Step = empty so S.length waiting_list = 1 else t.v = !next.v - S.length waiting_list by hd waiting_list at Step = Some t so t.v = !next.v - S.length waiting_list at Step end }; | A2 -> match memo[th] with | None -> absurd | Some tick -> if pass[tick.b] then begin active_tick := Some tick; assert { !lock_holder = - 1 }; lock_holder := th; pcs[th] <- A3; (* progress only with lock *) let ghost tick' = safe_pop waiting_list in assert { pass[tick'.b] }; assert { [@expl:fairness] tick=tick' by tick.b = tick'.b so mem tick waiting_list at Step so mem tick' waiting_list at Step }; assert { not mem tick waiting_list by waiting_list at Step = cons tick waiting_list so consecutive waiting_list at Step so consecutive waiting_list so if S.length waiting_list = 0 then not mem tick waiting_list else let x = S.get waiting_list 0 in let l = waiting_list[1 .. ] in not mem tick waiting_list by tick.v < x.v so (forall t. mem t l -> lt x t by forall i. 0 <= i < S.length l -> t = S.([]) l i -> (lt x t by t = S.([]) waiting_list (i+1))) }; assert { forall tick1 tick2. mem tick1 waiting_list at Step -> mem tick2 waiting_list at Step -> tick1.v < tick2.v -> tick1.b <> tick2.b by S.length waiting_list at Step <= n < 2*n - 1 <= k*n - 1 so 0 < tick2.v - tick1.v < k*n so mod (tick2.v - tick1.v) (k*n) <> 0 so mod tick1.v (k*n) <> mod tick2.v (k*n) }; assert { forall t. mem t waiting_list -> match owners[t.b] with | None -> false | Some n -> (pcs[n] = A2 /\ memo[n] = Some t) by t <> tick so t.b <> tick.b so th <> n so pcs[n] = pcs[n] at Step so memo[n] = memo[n] at Step end }; assert { numof pcs A2 0 n at Step = numof pcs A2 0 n + 1 by numof pcs A2 0 n at Step = numof pcs[th <- A2] A2 0 n }; assert { forall t. mem t waiting_list -> !next.v - S.length waiting_list <= t.v by mem t waiting_list at Step so t <> tick so waiting_list at Step = cons tick waiting_list so !next.v - S.length waiting_list at Step = tick.v so !next.v - S.length waiting_list at Step < t.v }; assert { if S.length waiting_list = 0 then true else let t = S.get waiting_list 0 in let l = waiting_list[1 .. ] in hd waiting_list = Some t /\ t.v = !next.v - S.length waiting_list by waiting_list at Step = cons tick (cons t l) so consecutive waiting_list at Step so t.v = tick.v + 1 }; end end | A3 -> pcs[th] <- W | W -> pcs[th] <- R1 (* move to release *) | R1 -> match memo[th] with | None -> absurd | Some tick -> assert { forall b'. 0 <= b' < k*n -> pass[b'] -> b' = tick.b }; pass[tick.b] <- false; pcs[th] <- R2 end | R2 -> match memo[th] with | None -> absurd | Some tick -> let nt = mod (tick.b + 1) (k*n) in assert { forall b. 0 <= b < k*n -> not pass[b] by !active_tick = Some tick }; lock_holder := -1; pass[nt] <- true; assert { forall b. 0 <= b < k*n -> pass[b] -> b = nt }; memo[th] <- None; assert { owners[tick.b] = Some th }; owners[tick.b] <- None; active_tick := None; pcs[th] <- I; assert { nt = mod (tick.v + 1) (k*n) by let d = div tick.v (k*n) in tick.v = (k*n) * d + tick.b so mod (tick.v + 1) (k*n) = mod ((k*n) * d + (tick.b + 1)) (k*n) = mod (tick.b + 1) (k*n) = nt }; assert { if S.length waiting_list = 0 then pass[!next.b] = true by !next.v = tick.v + 1 so !next.b = nt /\ exists th. memo[th] = None else let x = S.get waiting_list 0 in pass[x.b] by x.v = tick.v + 1 so x.b = nt }; assert { forall th'. 0 <= th' < n -> th <> th' -> match memo[th'] with | None -> true | Some tick1 -> mem tick1 waiting_list by waiting_list = waiting_list at Step so (mem tick1 waiting_list at Step \/ !active_tick at Step = Some tick1) so tick <> tick1 so !active_tick at Step <> Some tick1 end }; end end done end

download ZIP archive

# Why3 Proof Results for Project "verifythis_2018_array_based_queuing_lock_2"

## Theory "verifythis_2018_array_based_queuing_lock_2.ABQL": fully verified

Obligations | Alt-Ergo 2.0.0 | Alt-Ergo 2.3.3 | CVC5 1.0.5 | ||||||

VC for tick | --- | 0.00 | --- | ||||||

VC for fetch_and_add | --- | --- | --- | ||||||

split_vc | |||||||||

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

split_vc | |||||||||

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

subst a | |||||||||

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

apply Div_mod | |||||||||

apply premises | --- | 0.00 | --- | ||||||

VC for fetch_and_add | --- | 0.01 | --- | ||||||

VC for fetch_and_add | --- | 0.00 | --- | ||||||

VC for fetch_and_add | --- | 0.01 | --- | ||||||

VC for fetch_and_add | --- | 0.00 | --- | ||||||

precondition | --- | 0.00 | --- | ||||||

precondition | --- | 0.03 | --- | ||||||

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

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

VC for last_push | --- | 0.02 | --- | ||||||

VC for consecutive_last_push | --- | 0.10 | --- | ||||||

hd_push | --- | 0.02 | --- | ||||||

VC for consecutive_implies_sorted | --- | 0.03 | --- | ||||||

VC for numof_equiv | --- | 0.38 | --- | ||||||

VC for numof_add | --- | --- | --- | ||||||

split_vc | |||||||||

assertion | --- | 0.15 | --- | ||||||

assertion | --- | 3.49 | --- | ||||||

assertion | --- | 0.40 | --- | ||||||

postcondition | --- | --- | 3.70 | ||||||

mod_diff | --- | --- | --- | ||||||

split_vc | |||||||||

mod_diff.0 | --- | 0.02 | --- | ||||||

mod_diff.1 | --- | 0.02 | --- | ||||||

mod_diff.2 | --- | 0.02 | --- | ||||||

mod_diff.3 | 0.02 | --- | --- | ||||||

remove zero1,one1,(-),(>),(<=),(>=),abs,get1,set1,([]''),([<-]''),(!),is_none,([]'),numof,([]),singleton,cons,snoc,(++),mem,lt,sorted,consecutive,last,hd,has_ticket,has_lock,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Div_mod,Mod_bound,Div_unique,Div_bound,Mod_1,Div_1,Div_inf,Div_inf_neg,Mod_0,Div_1_left,Div_minus1_left,Mod_1_left,Mod_minus1_left,Div_mult,numof'def,Numof_bounds,Numof_append,Numof_left_no_add,Numof_left_add,Empty,Full,numof_increasing,numof_strictly_increasing,numof_change_any,numof_change_some,numof_change_equiv,is_none'spec,array'invariant,([<-])'spec,make_spec,length_nonnegative,(==)'spec,create'spec,empty'def,set'spec,set'def,([<-])'def,singleton'spec,cons'spec,snoc'spec,([..])'spec,([..])'def,([_..])'def,([.._])'def,(++)'spec,associative,left_neutral,right_neutral,cons_def,snoc_def,double_sub_sequence,cons_back,snoc_back,cat_back,cons_dec,snoc_dec,cat_dec,empty_dec,singleton_dec,mem_append,mem_tail,N_val,K_val,tick'invariant,last_push,consecutive_last_push,hd_push,consecutive_implies_sorted,zero'def,one'def,numof_equiv,numof_add,H3,H2,H1 | |||||||||

mod_diff.3.0 | 0.00 | 0.00 | --- | ||||||

mod_diff.4 | --- | 0.03 | --- | ||||||

mod_diff.5 | --- | 0.02 | --- | ||||||

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

split_vc | |||||||||

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

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

precondition | --- | 0.02 | --- | ||||||

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

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

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

safety | --- | 0.02 | --- | ||||||

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

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

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

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

loop invariant init | --- | 0.03 | --- | ||||||

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

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

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

loop invariant init | --- | 0.03 | --- | ||||||

loop invariant init | --- | 0.03 | --- | ||||||

loop invariant init | --- | 0.03 | --- | ||||||

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

loop invariant init | --- | 0.44 | --- | ||||||

loop invariant init | --- | 0.03 | --- | ||||||

loop invariant init | --- | 0.03 | --- | ||||||

loop invariant init | --- | 0.03 | --- | ||||||

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

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

liveness | --- | --- | --- | ||||||

split_all_full | |||||||||

liveness | --- | --- | 2.21 | ||||||

liveness | --- | 0.02 | --- | ||||||

liveness | --- | 0.02 | --- | ||||||

liveness | --- | 0.02 | --- | ||||||

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

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

safety | --- | 0.19 | --- | ||||||

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

liveness | --- | 0.07 | --- | ||||||

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

split_vc | |||||||||

assertion | --- | 0.03 | --- | ||||||

assertion | --- | 0.02 | --- | ||||||

assertion | --- | 0.03 | --- | ||||||

assertion | --- | 0.04 | --- | ||||||

assertion | --- | 0.04 | --- | ||||||

assertion | --- | 1.17 | --- | ||||||

assertion | --- | 0.04 | --- | ||||||

assertion | --- | 0.04 | --- | ||||||

assertion | --- | 0.13 | --- | ||||||

assertion | --- | 0.50 | --- | ||||||

assertion | --- | 0.04 | --- | ||||||

assertion | --- | 0.08 | --- | ||||||

assertion | --- | 0.04 | --- | ||||||

assertion | --- | 0.05 | --- | ||||||

assertion | --- | 0.50 | --- | ||||||

assertion | --- | 0.04 | --- | ||||||

assertion | --- | 0.05 | --- | ||||||

assertion | --- | 0.02 | --- | ||||||

assertion | --- | 0.36 | --- | ||||||

assertion | --- | 0.10 | --- | ||||||

index in array bounds | --- | 0.04 | --- | ||||||

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

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

assertion | --- | 0.05 | --- | ||||||

assertion | --- | 0.03 | --- | ||||||

assertion | --- | 0.44 | --- | ||||||

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

split_vc | |||||||||

assertion | --- | 0.14 | --- | ||||||

assertion | --- | 0.06 | --- | ||||||

assertion | --- | 0.16 | --- | ||||||

assertion | --- | 0.15 | --- | ||||||

assertion | --- | 0.17 | --- | ||||||

assertion | --- | 0.19 | --- | ||||||

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

split_vc | |||||||||

assertion | --- | 0.16 | --- | ||||||

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

rewrite H | |||||||||

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

apply consecutive_last_push | |||||||||

apply premises | --- | 0.03 | --- | ||||||

apply premises | --- | 0.05 | --- | ||||||

assertion | --- | 0.24 | --- | ||||||

assertion | --- | 0.08 | --- | ||||||

assertion | --- | 0.20 | --- | ||||||

safety | --- | 1.85 | --- | ||||||

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

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

case (b = tick.b1) | |||||||||

true case (loop invariant preservation) | --- | 0.25 | --- | ||||||

false case (loop invariant preservation) | --- | --- | --- | ||||||

replace owners[b]' owners1[b]' | |||||||||

false case (loop invariant preservation) | --- | 1.39 | --- | ||||||

equality hypothesis | --- | 0.06 | --- | ||||||

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

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

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

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

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

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

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

split_all_full | |||||||||

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

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

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

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

case (th=th1) | |||||||||

true case (loop invariant preservation) | --- | 0.18 | --- | ||||||

false case (loop invariant preservation) | --- | --- | --- | ||||||

replace memo[th]' memo1[th]' | |||||||||

false case (loop invariant preservation) | --- | 0.18 | --- | ||||||

equality hypothesis | --- | 0.07 | --- | ||||||

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

split_all_full | |||||||||

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

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

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

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

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

split_vc | |||||||||

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

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

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

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

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

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

liveness | --- | 0.04 | --- | ||||||

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

unreachable point | --- | 0.04 | --- | ||||||

index in array bounds | --- | 0.04 | --- | ||||||

assertion | --- | 0.16 | --- | ||||||

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

precondition | --- | 0.06 | --- | ||||||

assertion | --- | 0.06 | --- | ||||||

fairness | --- | --- | --- | ||||||

split_vc | |||||||||

fairness | --- | 0.04 | --- | ||||||

fairness | --- | 0.06 | --- | ||||||

fairness | --- | 0.04 | --- | ||||||

fairness | --- | 0.27 | --- | ||||||

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

split_vc | |||||||||

assertion | --- | 0.06 | --- | ||||||

assertion | --- | 0.03 | --- | ||||||

assertion | --- | 1.36 | --- | ||||||

assertion | --- | 0.08 | --- | ||||||

assertion | --- | 0.28 | --- | ||||||

assertion | --- | 0.10 | --- | ||||||

assertion | --- | 0.12 | --- | ||||||

assertion | --- | 0.04 | --- | ||||||

assertion | --- | 0.30 | --- | ||||||

assertion | --- | 0.03 | --- | ||||||

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

split_vc | |||||||||

assertion | --- | 0.03 | --- | ||||||

assertion | --- | 0.03 | --- | ||||||

assertion | --- | 0.04 | --- | ||||||

assertion | --- | 0.05 | --- | ||||||

assertion | --- | 0.04 | --- | ||||||

assertion | --- | 0.28 | --- | ||||||

assertion | --- | 0.04 | --- | ||||||

assertion | --- | 0.03 | --- | ||||||

assertion | --- | 0.97 | --- | ||||||

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

split_vc | |||||||||

assertion | --- | --- | 0.43 | ||||||

assertion | --- | 0.04 | --- | ||||||

assertion | --- | 0.11 | --- | ||||||

assertion | --- | 1.30 | --- | ||||||

safety | --- | 0.42 | --- | ||||||

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

liveness | --- | 0.04 | --- | ||||||

safety | --- | 0.03 | --- | ||||||

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

liveness | --- | 0.06 | --- | ||||||

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

safety | --- | 0.17 | --- | ||||||

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

liveness | --- | 0.06 | --- | ||||||

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

safety | --- | 0.21 | --- | ||||||

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

liveness | --- | 0.07 | --- | ||||||

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

unreachable point | --- | 0.06 | --- | ||||||

assertion | --- | 0.09 | --- | ||||||

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

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

safety | --- | 0.26 | --- | ||||||

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

liveness | --- | 0.08 | --- | ||||||

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

unreachable point | --- | 0.06 | --- | ||||||

precondition | --- | 0.02 | --- | ||||||

assertion | --- | 0.06 | --- | ||||||

index in array bounds | --- | 0.13 | --- | ||||||

assertion | --- | 0.47 | --- | ||||||

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

assertion | --- | 0.09 | --- | ||||||

index in array bounds | --- | 0.04 | --- | ||||||

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

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

split_vc | |||||||||

assertion | --- | 0.21 | --- | ||||||

assertion | --- | 0.03 | --- | ||||||

assertion | --- | 0.03 | --- | ||||||

assertion | --- | 0.03 | --- | ||||||

assertion | --- | 0.06 | --- | ||||||

assertion | --- | 1.85 | --- | ||||||

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

split_vc | |||||||||

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

assert (memo1[th]' <> memo1[th']') | |||||||||

asserted formula | --- | 1.21 | --- | ||||||

assertion | --- | 0.19 | --- | ||||||

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

replace memo[th']' memo1[th']' in H | |||||||||

assertion | --- | 4.39 | --- | ||||||

equality hypothesis | --- | 0.05 | --- | ||||||

assertion | --- | 0.20 | --- | ||||||

assertion | --- | 0.03 | --- | ||||||

safety | --- | 4.92 | --- | ||||||

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

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

case (b = x.b1) | |||||||||

true case (loop invariant preservation) | --- | 0.05 | --- | ||||||

false case (loop invariant preservation) | --- | --- | --- | ||||||

replace owners[b]' owners1[b]' | |||||||||

false case (loop invariant preservation) | --- | --- | --- | ||||||

split_vc | |||||||||

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

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

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

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

assert (x1 <> th) | |||||||||

asserted formula | --- | 0.06 | --- | ||||||

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

replace memo[x1]' memo1[x1]' in H | |||||||||

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

equality hypothesis | --- | 0.05 | --- | ||||||

equality hypothesis | --- | 0.06 | --- | ||||||

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

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

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

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

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

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

case (th=th1) | |||||||||

true case (loop invariant preservation) | --- | 0.12 | --- | ||||||

false case (loop invariant preservation) | --- | 5.02 | --- | ||||||

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

split_vc | |||||||||

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

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

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

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

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

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

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

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

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

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

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

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

liveness | --- | 0.13 | --- |