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 list.List
use list.HdTl
use list.Append
clone list.Sorted with type t = tick, predicate le = lt, lemma Transitive.Trans

inductive consecutive (l:list tick) =
  | 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:list tick) : option tick
= match l with
  | Nil -> None
  | Cons x Nil -> Some x
  | Cons _ l -> last l
  end

let rec lemma last_push (l: list tick) (x:tick)
  ensures { last (l ++ (Cons x Nil)) = Some x }
  variant { l }
= match l with
  | Nil -> ()
  | Cons _ l -> last_push l x
  end

let rec lemma consecutive_last_push (l: list 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 Nil)) }
  variant  { l }
= match l with
  | Nil -> ()
  | Cons _ l -> consecutive_last_push l x
  end

lemma hd_push: forall l,x:tick. hd l = None \/ hd (l ++ (Cons x Nil)) = hd l

let rec lemma consecutive_implies_sorted (l:list tick)
  requires { consecutive l }
  ensures  { sorted l }
  variant  { l }
= match l with
  | Nil -> ()
  | Cons _ t -> consecutive_implies_sorted t
  end

(*
  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 list.NumOcc
use list.Mem

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.elts ->
                       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.elts
                                        \/ !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.elts end }
    invariant { consecutive waiting_list.elts } (* also implies unicity *)
    invariant { length waiting_list = numof pcs A2 0 n }
    invariant { forall tick. mem tick waiting_list.elts ->
                       !next.v - length waiting_list <= tick.v < !next.v }
    invariant { match last waiting_list.elts with
                      | None -> true
                      | Some t -> t.v = !next.v - 1 end}
    invariant { match hd waiting_list.elts with
                      | None -> true
                      | Some t -> t.v = !next.v - length waiting_list end }
    invariant { match !active_tick with
                      | None -> !lock_holder = -1
                      | Some tick ->
                          (match hd waiting_list.elts with
                             | None -> !next.v = tick.v + 1
                             | Some t -> t.v = tick.v + 1 end)
                          /\ tick.v = !next.v - length waiting_list - 1
                          /\ 0 <= !lock_holder < n
                          /\ memo[!lock_holder] = Some tick end }
    invariant { 0 <= 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... *)
                 ((match waiting_list.elts with
                   | Nil -> false
                   | Cons tick _ -> pass[tick.b] = true end)
                 (* ...or someone has a ticket to the critical section... *)
              \/ (exists th. 0 <= th < n /\ memo[th] = None
                                         /\ pass[!next.b] = true)
                                         /\ waiting_list.elts = Nil)
                 (* ...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 length waiting_list <= n < 2*n - 1 <= k*n - 1
                   so ((forall tick'. mem tick' waiting_list.elts
                                    -> (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.elts
                                       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.elts ->
                          tick'.b <> tick.b /\ owners[tick'.b] <> Some th };
          assert { forall tick'. mem tick' waiting_list.elts ->
                          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.elts
                   by waiting_list.elts
                      = waiting_list.elts at Step ++ (Cons tick Nil) };
          assert { match !active_tick with
                      | None -> !lock_holder = -1
                      | Some tick' ->
                          (match hd waiting_list.elts with
                             | None -> false
                             | Some t ->
                               t.v = tick'.v + 1
                               by match hd waiting_list.elts 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.elts = Some t end
                           end)
                   end };
           assert { !lock_holder = -1 ->
                     match waiting_list.elts with
                      | Nil -> false
                      | Cons t1 _ ->
                         pass[t1.b]
                         by
                         match waiting_list.elts at Step with
                         | Nil -> pass[t1.b]
                                  by (t1 = tick /\
                                  pass[tick.b] by pass[!next.b at Step])
                         | Cons t _ -> pass[t1.b] by t=t1 so pass[t.b] end
                     end };
           assert { match hd waiting_list.elts with
                    | None -> true
                    | Some t ->
                        if t = tick
                        then t.v = !next.v - length waiting_list
                             by waiting_list.elts at Step = Nil
                             so length waiting_list = 1
                        else t.v = !next.v - length waiting_list
                             by hd waiting_list.elts at Step = Some t
                             so t.v = !next.v - 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.elts at Step
                        so mem tick' waiting_list.elts at Step };
               assert { not mem tick waiting_list.elts
                        by waiting_list.elts at Step
                           = Cons tick waiting_list.elts
                        so consecutive waiting_list.elts at Step
                        so (forall t. mem t waiting_list.elts -> tick.v < t.v)
                        so consecutive waiting_list.elts
                        so match waiting_list.elts with
                           | Nil -> not mem tick waiting_list.elts
                           | Cons x l -> not mem tick waiting_list.elts
                                         by tick.v < x.v
                                         so (forall t. mem t l -> x.v < t.v)
                                          end };
              assert { forall tick1 tick2. mem tick1 waiting_list.elts at Step
                                        -> mem tick2 waiting_list.elts at Step
                                        -> tick1.v < tick2.v
                                        -> tick1.b <> tick2.b
                       by 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.elts ->
                          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.elts ->
                       !next.v - length waiting_list <= t.v
                       by mem t waiting_list.elts at Step
                       so t <> tick
                       so waiting_list.elts at Step
                          = Cons tick waiting_list.elts
                       so !next.v - length waiting_list at Step = tick.v
                       so !next.v - length waiting_list at Step < t.v };
              assert { match waiting_list.elts with
                       | Nil -> true
                       | Cons t l ->
                         hd waiting_list.elts = Some t
                         /\ t.v = !next.v - waiting_list.length
                         by waiting_list.elts at Step
                            = Cons tick (Cons t l)
                         so consecutive waiting_list.elts at Step
                         so t.v = tick.v + 1 end };
               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 { match waiting_list.elts with
                         | Nil -> pass[!next.b] = true
                                  by !next.v = tick.v + 1
                                  so !next.b = nt
                                  /\
                                  exists th. memo[th] = None
                         | Cons x _ -> pass[x.b]
                                       by x.v = tick.v + 1
                                       so x.b = nt
                         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.0CVC4 1.4Eprover 1.9.1-001Z3 4.5.0
VC n---------0.02
VC k0.00---------
VC tick---------0.01
VC fetch_and_add------------
split_vc
VC fetch_and_add.0------------
split_vc
VC fetch_and_add.0.0------------
subst a
VC fetch_and_add.0.0.0------------
apply Div_mod
VC fetch_and_add.0.0.0.0---------0.02
VC fetch_and_add.0.1---------0.01
VC fetch_and_add.0.2---------0.02
VC fetch_and_add.0.30.00---------
VC fetch_and_add.0.4---------0.02
VC fetch_and_add.1---------0.01
VC fetch_and_add.2---------0.02
VC fetch_and_add.3---------0.01
VC fetch_and_add.4---------0.01
Sorted.Transitive.Trans---------0.03
VC last_push------------
split_vc
VC last_push.0---------0.03
VC last_push.1---0.33------
VC consecutive_last_push------------
split_vc
VC consecutive_last_push.0---------0.03
VC consecutive_last_push.10.02---------
VC consecutive_last_push.20.23---------
VC consecutive_last_push.3---------0.47
hd_push---------0.17
VC consecutive_implies_sorted------------
split_vc
VC consecutive_implies_sorted.0---------0.04
VC consecutive_implies_sorted.10.02---------
VC consecutive_implies_sorted.20.02---------
VC numof_equiv---------0.35
VC numof_add------------
split_vc
VC numof_add.00.07---------
VC numof_add.10.15---------
VC numof_add.20.08---------
VC numof_add.3---------0.44
mod_diff------------
split_vc
mod_diff.0---------0.03
mod_diff.1---------0.02
mod_diff.2---------0.15
mod_diff.30.02---------
mod_diff.4---------0.02
mod_diff.5---------0.02
VC main------------
split_vc
VC main.0---------0.20
VC main.1---------0.18
VC main.2---------0.45
VC main.3---------0.03
VC main.40.01---------
VC main.5---------0.05
VC main.60.02---------
VC main.70.01---------
VC main.8---------0.02
VC main.9---------0.04
VC main.10---------0.01
VC main.110.23---------
VC main.12---------0.01
VC main.130.03---------
VC main.14------------
split_vc
VC main.14.00.02---------
VC main.14.10.02---------
VC main.150.01---------
VC main.16---------0.04
VC main.170.01---------
VC main.180.12---------
VC main.190.16---------
VC main.200.02---------
VC main.21---------0.02
VC main.22---------0.04
VC main.23---------0.01
VC main.24---------0.04
VC main.25------------
right
VC main.25.0------------
split_vc
VC main.25.0.0------------
exists 0
VC main.25.0.0.00.01---------
VC main.25.0.1---------0.02
VC main.26---------0.03
VC main.27---------0.02
VC main.280.08---------
VC main.290.02---------
VC main.30---------0.05
VC main.310.04---------
VC main.320.50---------
VC main.330.05---------
VC main.340.13---------
VC main.350.04---------
VC main.360.23---------
VC main.37------------
split_all_full
VC main.37.00.03---------
VC main.37.10.46---------
VC main.37.20.12---------
VC main.38---------0.05
VC main.39---0.26------
VC main.400.03---------
VC main.410.06---------
VC main.42------------
split_vc
VC main.42.00.03---------
VC main.42.10.03---------
VC main.43---------0.02
VC main.44------------
split_all_full
VC main.44.00.03---------
VC main.45---------0.04
VC main.460.13---------
VC main.47---------0.04
VC main.48------------
split_vc
VC main.48.0---------0.02
VC main.48.1---------0.02
VC main.48.20.01---------
VC main.48.3---------0.02
VC main.48.4---------0.02
VC main.48.50.05---------
VC main.48.60.22---------
VC main.48.70.02---------
VC main.48.8---------0.01
VC main.48.9---------0.03
VC main.48.10---------0.02
VC main.48.110.37---------
VC main.48.12---------0.04
VC main.48.13---------0.03
VC main.48.140.20---------
VC main.48.150.27---------
VC main.48.16---------1.66
VC main.48.17---------0.01
VC main.48.180.01---------
VC main.490.04---------
VC main.50---------0.03
VC main.51---------0.02
VC main.52---------0.02
VC main.53---------0.03
VC main.54---------0.03
VC main.55------------
split_vc
VC main.55.0---------0.04
VC main.55.10.54---------
VC main.56------------
split_vc
VC main.56.00.04---------
VC main.56.1---------0.03
VC main.56.20.03---------
VC main.56.30.01---------
VC main.56.40.08---------
VC main.56.50.07---------
VC main.57------------
split_vc
VC main.57.0---------0.02
VC main.57.1------------
rewrite H
VC main.57.1.0------------
apply consecutive_last_push
VC main.57.1.0.0---------0.04
VC main.57.1.0.1---------0.02
VC main.58------------
split_vc
VC main.58.0---------0.03
VC main.58.10.57---------
VC main.58.20.28---------
VC main.58.30.12---------
VC main.58.4---------0.05
VC main.58.5---------0.05
VC main.58.6---------0.03
VC main.58.70.08---------
VC main.59------------
split_vc
VC main.59.0---------0.04
VC main.59.1---------0.02
VC main.59.20.12---------
VC main.59.30.03---------
VC main.59.4---------0.03
VC main.59.5---------0.01
VC main.59.6------0.03---
VC main.59.70.04---------
VC main.59.8------0.04---
VC main.60------------
split_vc
VC main.60.0---------0.12
VC main.60.10.68---------
VC main.60.20.04---------
VC main.60.30.03---------
VC main.60.40.04---------
VC main.60.50.04---------
VC main.610.53---------
VC main.62---------0.01
VC main.63------------
case (b = tick.b1)
VC main.63.00.25---------
VC main.63.1------------
replace owners[b] owners1[b]
VC main.63.1.0------------
split_vc
VC main.63.1.0.0---------0.07
VC main.63.1.0.1---------0.04
VC main.63.1.0.20.24---------
VC main.63.1.0.3------------
assert ( x1 <> th )
VC main.63.1.0.3.0---------0.08
VC main.63.1.0.3.1------------
replace memo[x1] memo1[x1] in H
VC main.63.1.0.3.1.0---------0.06
VC main.63.1.0.3.1.10.05---------
VC main.63.1.10.04---------
VC main.640.46---------
VC main.650.86---------
VC main.66---------0.03
VC main.670.18---------
VC main.68------------
split_all_full
VC main.68.00.90---------
VC main.69------------
case (th=th1)
VC main.69.00.04---------
VC main.69.10.55---------
VC main.70------------
split_all_full
VC main.70.00.83---------
VC main.70.11.06---------
VC main.70.21.27---------
VC main.71------------
case th=th1
VC main.71.00.06---------
VC main.71.1------------
replace memo[th] memo1[th]
VC main.71.1.0---------0.08
VC main.71.1.10.03---------
VC main.72------2.06---
VC main.730.11---------
VC main.740.06---------
VC main.751.87---------
VC main.760.03---------
VC main.77------------
split_vc
VC main.77.0------------
assert (elts waiting_list <> Nil)
VC main.77.0.00.06---------
VC main.77.0.10.03---------
VC main.78------------
split_vc
VC main.78.0---------0.03
VC main.78.1------------
split_all_full
VC main.78.1.00.08---------
VC main.78.2------------
split_all_full
VC main.78.2.00.05---------
VC main.78.3------------
split_all_full
VC main.78.3.00.04---------
VC main.78.4---------0.04
VC main.78.5---------0.01
VC main.78.60.06---------
VC main.790.19---0.23---
VC main.80---------0.03
VC main.81---------0.02
VC main.820.05---------
VC main.83---------0.03
VC main.84---------0.02
VC main.85---------0.02
VC main.86---------0.03
VC main.871.01---------
VC main.88------------
split_vc
VC main.88.0---------0.05
VC main.88.1---------0.04
VC main.88.20.12---------
VC main.88.30.34---------
VC main.89------------
split_vc
VC main.89.0---------0.04
VC main.89.10.10---------
VC main.89.21.97---------
VC main.89.30.12---------
VC main.89.4---------0.08
VC main.89.50.03---------
VC main.89.63.77---------
VC main.89.7---------0.04
VC main.89.80.07---------
VC main.90------------
split_vc
VC main.90.0---------0.01
VC main.90.1---------0.04
VC main.90.20.02---------
VC main.90.3---------0.03
VC main.90.4---------0.05
VC main.90.50.05---------
VC main.90.60.11---------
VC main.90.70.02---------
VC main.91------------
split_vc
VC main.91.00.44---------
VC main.91.1---------0.03
VC main.91.2------------
case (t.v < x1.v)
VC main.91.2.0------------
apply H3
VC main.91.2.0.0---------0.02
VC main.91.2.0.1---------0.04
VC main.91.2.0.20.34---------
VC main.91.2.1------------
cut (not b x1 = b t)
VC main.91.2.1.0---------0.04
VC main.91.2.1.1------------
apply H3
VC main.91.2.1.1.0------------
split_all_full
VC main.91.2.1.1.0.00.62---------
VC main.91.2.1.1.10.31---------
VC main.91.2.1.1.2---------0.04
VC main.91.3---------0.04
VC main.91.40.02---------
VC main.91.50.19---------
VC main.91.61.16---------
VC main.92------------
split_vc
VC main.92.00.33---------
VC main.92.10.10---------
VC main.93------------
split_vc
VC main.93.00.26---------
VC main.93.1---------0.04
VC main.93.2---------0.06
VC main.93.3------------
split_all_full
VC main.93.3.00.20---------
VC main.93.40.31---------
VC main.93.50.04---------
VC main.94------------
split_vc
VC main.94.0---------0.05
VC main.94.1---------0.01
VC main.94.23.82---------
VC main.94.3---------0.04
VC main.94.40.14---------
VC main.950.22---------
VC main.96---------0.02
VC main.970.63---------
VC main.980.34---------
VC main.990.09---------
VC main.100---------0.03
VC main.1010.03---------
VC main.1020.05---------
VC main.1030.56---------
VC main.1040.12---------
VC main.1054.64---------
VC main.1060.41---------
VC main.1070.26---------
VC main.1080.58---------
VC main.109------------
split_vc
VC main.109.00.03---------
VC main.109.10.98---------
VC main.1100.93---------
VC main.111------0.06---
VC main.112------------
split_vc
VC main.112.0---------0.04
VC main.112.1------0.08---
split_all_full
VC main.112.1.02.18---------
VC main.112.2------------
split_all_full
VC main.112.2.05.06---------
VC main.112.32.10---------
VC main.112.40.05---------
VC main.112.5---------0.01
VC main.112.60.07---------
VC main.113---------0.04
VC main.1140.05---------
VC main.1150.04---------
VC main.116---------0.01
VC main.117---------0.04
VC main.1180.04---------
VC main.1190.05---------
VC main.120---------0.04
VC main.1210.02---------
VC main.122------------
split_all_full
VC main.122.00.05---------
VC main.1230.03---------
VC main.124------------
split_all_full
VC main.124.00.03---------
VC main.124.10.10---------
VC main.124.20.09---------
VC main.1250.05---0.090.03
VC main.1260.16---------
VC main.1270.02---------
VC main.128------------
split_all_full
VC main.128.00.04---------
VC main.129---------0.02
VC main.1300.04---------
VC main.131---------0.01
VC main.132------------
split_vc
VC main.132.0---------0.03
VC main.132.10.04---------
VC main.132.20.06---------
VC main.132.30.05---------
VC main.132.40.04---------
VC main.132.5---------0.01
VC main.132.60.08---------
VC main.1330.12---------
VC main.134------------
revert H41
VC main.134.0------------
split_goal_full
VC main.134.0.0------0.040.02
VC main.134.0.1------0.010.01
VC main.134.0.2------0.040.02
VC main.134.0.3------0.040.02
VC main.134.0.4------0.020.01
VC main.134.0.5------0.020.01
VC main.134.0.6------0.020.01
VC main.134.0.7------0.020.01
VC main.134.0.80.04---------
VC main.134.0.9---------0.04
VC main.134.0.100.03---------
VC main.134.0.110.04---------
VC main.134.0.12------0.040.04
VC main.134.0.13------0.020.02
VC main.134.0.14------0.050.03
VC main.134.0.15------0.060.03
VC main.134.0.16------0.060.03
VC main.134.0.17------0.030.02
VC main.134.0.18------0.040.03
VC main.134.0.19------0.060.03
VC main.134.0.20------0.040.03
VC main.134.0.21------0.020.02
VC main.134.0.22------0.040.03
VC main.134.0.23------0.040.03
VC main.135---------0.02
VC main.1360.15---------
VC main.137---------0.02
VC main.138---------0.04
VC main.1390.04---------
VC main.1400.42---------
VC main.1410.08---------
VC main.1420.06---------
VC main.1430.06---------
VC main.1441.28---------
VC main.1450.31---------
VC main.1460.38---------
VC main.1472.41---------
VC main.1480.10---------
VC main.1490.10---------
VC main.1500.03---------
VC main.1510.05---------
VC main.152---------0.01
VC main.153------------
split_vc
VC main.153.0---------0.05
VC main.153.10.05---------
VC main.153.20.05---------
VC main.153.30.04---------
VC main.153.4---------0.03
VC main.153.5---------0.01
VC main.153.6---------0.03
VC main.1540.02---------
VC main.155------------
split_all_full
VC main.155.00.05---------
VC main.155.1---------0.01
VC main.155.2---------0.01
VC main.155.3---------0.02
VC main.156---------0.02
VC main.1570.20---------
VC main.158---------0.01
VC main.159---------0.07
VC main.1600.05---------
VC main.1610.55---------
VC main.162---------0.04
VC main.1630.12---------
VC main.164------------
split_all_full
VC main.164.00.10---------
VC main.1651.10---------
VC main.166------------
split_vc
VC main.166.0---------0.05
VC main.166.10.73---------
VC main.166.20.08---------
VC main.1670.26---------
VC main.168------1.720.93
VC main.1690.02---------
VC main.1700.03---------
VC main.171------------
split_vc
VC main.171.00.04---------
VC main.171.10.04---------
VC main.1720.03---------
VC main.173---------0.01
VC main.174------------
split_all_full
VC main.174.0---------0.04
VC main.174.10.05---------
VC main.174.2---------0.01
VC main.174.3---------0.01
VC main.174.4---------0.04
VC main.174.5---------0.03
VC main.174.60.08---------
VC main.1750.10---------
VC main.1760.14---------
VC main.177---------0.03
VC main.178---------0.01
VC main.179------------
apply H22
VC main.179.00.15---------
VC main.179.1---------0.04
VC main.179.2---------0.02
VC main.180---------0.02
VC main.181---------0.02
VC main.1820.36---------
VC main.183---------0.02
VC main.1840.69---------
VC main.1850.02---------
VC main.1862.22---------
VC main.1870.47---------
VC main.1880.11---------
VC main.189------------
split_all_full
VC main.189.00.04---------
VC main.1901.48---------
VC main.191------------
split_all_full
VC main.191.00.04---------
VC main.191.11.17---------
VC main.191.20.62---------
VC main.1920.19---------
VC main.193---0.28------
VC main.1940.02---------
VC main.1950.07---------
VC main.1960.04---------
VC main.197---------0.02
VC main.198---------0.02
VC main.199------------
split_all_full
VC main.199.0---------0.02
VC main.199.1---------0.01
VC main.199.2---------0.01
VC main.199.3---------0.01
VC main.199.4---------0.01
VC main.199.5---------0.01
VC main.199.60.10---------
VC main.2000.05---------
VC main.201---------0.02
VC main.202---------0.03
VC main.203---------0.02
VC main.204---------0.01
VC main.205------------
split_vc
VC main.205.0---------0.04
VC main.205.1---------0.04
VC main.2060.06---------
VC main.2070.85---------
VC main.208---------0.02
VC main.209---------0.04
VC main.210---------0.03
VC main.211---------0.03
VC main.212------------
split_vc
VC main.212.00.03---------
VC main.212.10.02---------
VC main.212.20.03---------
VC main.212.3---------0.01
VC main.212.40.04---------
VC main.213------------
split_vc
VC main.213.00.37---------
VC main.213.11.91---------
VC main.213.20.04---------
VC main.213.30.33---------
VC main.213.40.03---------
VC main.213.50.04---------
VC main.213.60.03---------
VC main.2141.13---------
VC main.215---------0.02
VC main.216------------
case b=x.b1
VC main.216.00.04---------
VC main.216.1------------
replace owners[b] owners1[b]
VC main.216.1.0------------
split_vc
VC main.216.1.0.00.70------0.04
VC main.216.1.0.10.92------0.04
VC main.216.1.0.2------------
split_all_full
VC main.216.1.0.2.08.54---------
VC main.216.1.0.3------------
assert ( x1 <> th )
VC main.216.1.0.3.00.04------0.09
VC main.216.1.0.3.1------------
replace memo[x1] memo1[x1] in H
VC main.216.1.0.3.1.0---------0.05
VC main.216.1.0.3.1.10.04---------
VC main.216.1.10.05---------
VC main.2170.04---------
VC main.2180.08---------
VC main.219---------0.04
VC main.2200.14---------
VC main.221------------
split_all_full
VC main.221.02.65---------
VC main.222------1.78---
VC main.223------------
split_all_full
VC main.223.02.22---------
VC main.223.11.13---------
VC main.223.27.49---------
VC main.224------------
case th=th1
VC main.224.00.05---------
VC main.224.1------------
replace memo[th] memo1[th]
VC main.224.1.0---------0.07
VC main.224.1.10.03---------
VC main.2250.29---------
VC main.2260.11---------
VC main.2270.15---------
VC main.228------------
split_all_full
VC main.228.00.03---------
VC main.228.10.02---------
VC main.229---------0.01
VC main.230------------
split_vc
VC main.230.0------------
assert (elts waiting_list <> Nil)
VC main.230.0.00.57---------
VC main.230.0.10.04---------
VC main.231------------
split_vc
VC main.231.0---------0.02
VC main.231.10.10---------
VC main.231.20.11---------
VC main.231.30.10---------
VC main.231.40.05---0.06---
VC main.231.5---------0.01
VC main.231.60.10---------
VC main.2320.13---------
VC main.233------------
split_all_full
VC main.233.00.53---------
VC main.233.1---------0.01
VC main.233.20.12---------
VC main.233.30.02---------