Wiki Agenda Contact Version française

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

ObligationsAlt-Ergo 2.0.0Alt-Ergo 2.3.3CVC4 1.8
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.40---
assertion---0.40---
postcondition------5.88
mod_diff---------
split_vc
mod_diff.0---0.02---
mod_diff.1---0.02---
mod_diff.2---0.02---
mod_diff.30.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.00.000.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------1.01
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.02---
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---
VC for main---0.04---
VC for main---0.04---
VC for main---1.17---
VC for main---0.04---
VC for main---0.04---
VC for main---0.08---
VC for main---0.51---
VC for main---0.04---
VC for main---0.13---
VC for main---0.04---
VC for main---0.05---
VC for main---0.54---
VC for main---0.04---
VC for main---0.05---
VC for main---0.02---
VC for main---0.35---
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---
VC for main---0.06---
VC for main---0.06---
VC for main---0.15---
VC for main---0.16---
assertion---------
split_vc
assertion---0.16---
VC for main---------
rewrite H
VC for main---------
apply consecutive_last_push
apply premises---0.03---
apply premises---0.05---
assertion---0.24---
assertion---0.08---
assertion---0.20---
safety---1.08---
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)---0.78---
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---1.25---
loop invariant preservation------0.52
loop invariant preservation---------
split_all_full
VC for main---0.86---
VC for main------0.89
VC for main------0.92
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.34
loop invariant preservation---0.04---
loop invariant preservation---0.06---
loop invariant preservation---------
split_vc
loop invariant preservation---1.56---
loop invariant preservation---1.78---
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---
VC for main---0.05---
VC for main---0.04---
VC for main---0.23---
assertion---------
split_vc
assertion---0.06---
VC for main---0.03---
VC for main---1.32---
VC for main---0.04---
VC for main---0.25---
VC for main---0.10---
VC for main---0.12---
VC for main---0.08---
VC for main---0.30---
VC for main---0.03---
assertion---------
split_vc
assertion---0.03---
assertion---0.03---
assertion---0.04---
VC for main---0.03---
VC for main---0.04---
VC for main---0.28---
VC for main---0.04---
VC for main---0.05---
assertion---0.78---
assertion---------
split_vc
assertion------0.24
VC for main---0.04---
assertion---0.11---
assertion---0.96---
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.22
loop invariant preservation---0.12---
loop invariant preservation---0.12---
loop invariant preservation---0.70---
loop invariant preservation------0.77
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.50---
loop invariant preservation---0.24---
loop invariant preservation---0.06---
loop invariant preservation---0.85---
loop invariant preservation---0.03---
loop invariant preservation---0.64---
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.46---
loop invariant preservation---0.25---
loop invariant preservation---0.05---
loop invariant preservation---0.89---
loop invariant preservation---0.03---
loop invariant preservation---0.57---
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---1.81---
loop invariant preservation---0.10---
loop invariant preservation---0.07---
loop invariant preservation---0.07---
loop invariant preservation---0.84---
loop invariant preservation---0.33---
loop invariant preservation---0.06---
loop invariant preservation---0.38---
loop invariant preservation---0.02---
loop invariant preservation---1.36---
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.09---
VC for main---0.03---
VC for main---0.06---
VC for main---0.03---
VC for main---0.03---
assertion---1.85---
assertion---------
split_vc
VC for main---------
replace memo[th']' memo1[th']' in H
VC for main---0.19---
equality hypothesis---0.05---
VC for main---------
assert (memo1[th]' <> memo1[th']')
asserted formula---1.00---
VC for main---0.05---
VC for main---0.20---
VC for main---0.03---
safety---4.36---
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---1.85---
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.66---
loop invariant preservation---------
case (th=th1)
true case (loop invariant preservation)---0.12---
false case (loop invariant preservation)---4.46---
loop invariant preservation---------
split_vc
loop invariant preservation---0.88---
loop invariant preservation---0.30---
loop invariant preservation---2.23---
loop invariant preservation---0.23---
loop invariant preservation---0.57---
loop invariant preservation---0.03---
loop invariant preservation---4.90---
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---