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.0Alt-Ergo 2.2.0CVC4 1.4CVC4 1.6Eprover 1.9.1-001Z3 4.5.0
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.18---------
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.03
VC main.1---------------0.18
VC main.2---------------0.30
VC main.3---------------0.02
VC main.4---------------0.05
VC main.50.01---------------
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.10---------------
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.05---------------
VC main.29---------------0.02
VC main.300.32---------------
VC main.310.02---------------
VC main.320.33---------------
VC main.330.04---------------
VC main.340.06---------------
VC main.35------------------
split_all_full
VC main.35.00.10---------------
VC main.360.15---------------
VC main.37------------------
split_all_full
VC main.37.00.02---------------
VC main.37.10.33---------------
VC main.37.20.07---------------
VC main.38---------0.18------
VC main.39------------------
split_all_full
VC main.39.0---------0.16------
VC main.39.1---------0.53------
VC main.400.02---------------
VC main.410.06---------------
VC main.420.03---------------
VC main.43---------------0.01
VC main.44---------------0.01
VC main.45---------------0.04
VC main.460.13---------------
VC main.47------------------
revert H41
VC main.47.0------------------
split_goal_full
VC main.47.0.00.04---------------
VC main.47.0.1---------------0.04
VC main.47.0.20.03---------------
VC main.47.0.30.04---------------
VC main.48------------------
split_vc
VC main.48.00.02---------------
VC main.48.10.02---------------
VC main.48.20.01---------------
VC main.48.30.05---------------
VC main.48.40.02---------------
VC main.48.50.07---------------
VC main.48.60.13---------------
VC main.48.70.03---------------
VC main.48.80.06---------------
VC main.48.9---------------0.03
VC main.48.100.03---------------
VC main.48.110.29---------------
VC main.48.120.02---------------
VC main.48.130.02---------------
VC main.48.140.10---------------
VC main.48.150.17---------------
VC main.48.160.02---------------
VC main.48.170.01---------------
VC main.48.180.02---------------
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.00.04---------------
VC main.55.10.39---------------
VC main.56------------------
split_vc
VC main.56.00.03---------------
VC main.56.10.08---------------
VC main.56.20.04---------------
VC main.56.30.07---------------
VC main.56.40.10---------------
VC main.56.50.11---------------
VC main.57------------------
split_vc
VC main.57.0---------------0.01
VC main.57.1------------------
rewrite H
VC main.57.1.0------------------
apply consecutive_last_push
VC main.57.1.0.0---------------0.03
VC main.57.1.0.1---------------0.01
VC main.58------------------
split_vc
VC main.58.00.08---------------
VC main.58.10.41---------------
VC main.58.20.19---------------
VC main.58.30.03---------------
VC main.58.40.12---------------
VC main.58.50.02---------------
VC main.58.60.03---------------
VC main.58.70.08---------------
VC main.59------------------
split_vc
VC main.59.00.12---------------
VC main.59.10.03---------------
VC main.59.20.08---------------
VC main.59.30.03---------------
VC main.59.40.04---------------
VC main.59.5------------0.03---
VC main.59.60.10---------------
VC main.59.70.02---------------
VC main.59.8------------0.04---
VC main.60------------------
split_vc
VC main.60.0---------------0.08
VC main.60.10.60---------------
VC main.60.20.03---------------
VC main.60.30.04---------------
VC main.60.40.03---------------
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.680.87---------------
VC main.690.88---------------
VC main.70------------------
split_vc
VC main.70.00.73---------------
VC main.70.11.41---------------
VC main.70.21.15---------------
VC main.71------------------
case th=th1
VC main.71.00.08---------------
VC main.71.1------------------
replace memo[th] memo1[th]
VC main.71.1.0---------------0.08
VC main.71.1.10.04---------------
VC main.72------------1.63---
split_all_full
VC main.72.0---------0.18------
VC main.72.1------------------
introduce_premises
VC main.72.1.0---11.81------------
VC main.730.11---------------
VC main.740.07---------------
VC main.751.45---------------
VC main.760.03---------------
VC main.77------------------
split_vc
VC main.77.0------------------
assert (elts waiting_list <> Nil)
VC main.77.0.00.05---------------
VC main.77.0.10.04---------------
VC main.78------------------
split_all_full
VC main.78.0---------------0.04
VC main.78.10.05---------------
VC main.78.2---------------0.01
VC main.78.3---------------0.01
VC main.78.4---------------0.04
VC main.78.5---------------0.03
VC main.78.60.08---------------
VC main.790.13---------------
VC main.800.05---------------
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.04
VC main.88.1---------------0.05
VC main.88.20.12---------------
VC main.88.30.33---------------
VC main.89------------------
split_vc
VC main.89.00.48---------------
VC main.89.10.10---------------
VC main.89.21.63---------------
VC main.89.30.07---------------
VC main.89.4---------------0.04
VC main.89.50.04---------------
VC main.89.6---------------0.08
VC main.89.70.03---------------
VC main.89.80.02---------------
VC main.90------------------
split_vc
VC main.90.00.02---------------
VC main.90.10.05---------------
VC main.90.20.02---------------
VC main.90.30.02---------------
VC main.90.40.11---------------
VC main.90.50.05---------------
VC main.90.60.13---------------
VC main.90.70.03---------------
VC main.91------------------
split_vc
VC main.91.00.39---------------
VC main.91.10.02---------------
VC main.91.22.55---------------
VC main.91.30.60---------------
VC main.91.40.02---------------
VC main.91.50.16---------------
VC main.91.60.72---------------
VC main.92------------------
split_vc
VC main.92.00.23---------------
VC main.92.10.09---------------
VC main.93------------------
split_vc
VC main.93.00.16---------------
VC main.93.10.02---------------
VC main.93.20.98---------------
VC main.93.30.04---------------
VC main.93.40.19---------------
VC main.93.50.03---------------
VC main.94------------------
split_vc
VC main.94.03.20---------------
VC main.94.10.02---------------
VC main.94.22.64---------------
VC main.94.30.03---------------
VC main.94.40.11---------------
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.102------------------
split_all_full
VC main.102.00.06---------------
VC main.1030.39---------------
VC main.104------------------
split_all_full
VC main.104.00.03---------------
VC main.104.10.10---------------
VC main.104.20.09---------------
VC main.1053.60---------0.093.78
VC main.1060.36---------------
VC main.1070.19---------------
VC main.1080.60---------------
VC main.109------------------
split_vc
VC main.109.00.03---------------
VC main.109.10.96---------------
VC main.110---0.71------------
VC main.111------------------
split_vc
VC main.111.0------------------
assert (elts waiting_list <> Nil)
VC main.111.0.00.06---------------
VC main.111.0.11.76---------------
VC main.112------------------
split_vc
VC main.112.0---------0.11------
VC main.112.1---0.83------------
VC main.112.2---0.72------------
VC main.112.3---0.73------------
VC main.112.4---------0.11------
VC main.112.5---------0.06------
VC main.112.6---------0.10------
VC main.1130.10---------------
VC main.114------------------
split_all_full
VC main.114.00.05---------------
VC main.114.1---------------0.01
VC main.114.2---------------0.01
VC main.114.3---------------0.02
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.1240.14---------------
VC main.125---------------0.05
VC main.1260.16---------------
VC main.1270.10---------------
VC main.1280.02---------------
VC main.129------------------
split_vc
VC main.129.00.03---------------
VC main.129.10.03---------------
VC main.1300.02---------------
VC main.131------------0.06---
VC main.132------------------
split_vc
VC main.132.00.10---------------
VC main.132.10.04---------------
VC main.132.20.05---------------
VC main.132.30.05---------------
VC main.132.40.10---------------
VC main.132.50.11---------------
VC main.132.60.10---------------
VC main.133---------------0.04
VC main.134---------------0.04
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.12---------------
VC main.143------------------
split_all_full
VC main.143.00.04---------------
VC main.144------------------
case (th=th1)
VC main.144.00.04---------------
VC main.144.10.55---------------
VC main.145------------------
split_all_full
VC main.145.00.02---------------
VC main.145.10.80---------------
VC main.145.20.26---------------
VC main.146---------0.20------
VC main.1471.88---------------
VC main.1480.11---------------
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.00.05---------------
VC main.153.1---------------0.05
VC main.153.2---------------0.01
VC main.153.3---------------0.03
VC main.153.40.04---------------
VC main.153.50.05---------------
VC main.153.6---------------0.03
VC main.1540.02---------0.02---
VC main.155------------------
split_all_full
VC main.155.00.03---------------
VC main.155.1---------------0.01
VC main.155.20.12---------------
VC main.155.30.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.34---------------
VC main.162---------------0.04
VC main.1630.13---------------
VC main.164------------------
split_all_full
VC main.164.00.04---------------
VC main.165------------1.50---
VC main.166------------------
split_all_full
VC main.166.00.04---------------
VC main.166.10.57---------------
VC main.166.20.14---------------
VC main.1670.21---------------
VC main.168------------1.640.93
VC main.1690.02---------------
VC main.170------------------
split_all_full
VC main.170.00.04---------------
VC main.171---------------0.02
VC main.1720.04---------------
VC main.173---------------0.01
VC main.174------------------
split_vc
VC main.174.00.04---------------
VC main.174.1---------------0.03
VC main.174.2---------------0.01
VC main.174.30.04---------------
VC main.174.40.05---------------
VC main.174.50.06---------------
VC main.174.60.08---------------
VC main.1750.05---------------
VC main.176---------------0.03
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.03
VC main.181---------------0.02
VC main.1820.20---------------
VC main.1830.02---------------
VC main.184---------------0.05
VC main.1850.04---------------
VC main.1862.12---------------
VC main.1870.29---------------
VC main.1880.11---------------
VC main.1890.06---------------
VC main.1901.36---------------
VC main.1910.28---------------
VC main.1920.19---------------
VC main.193------0.11---------
VC main.1940.02---------------
VC main.1950.15---------------
VC main.196------------------
split_all_full
VC main.196.00.03---------------
VC main.196.10.02---------------
VC main.197---------------0.02
VC main.198------------------
split_all_full
VC main.198.00.03---------------
VC main.199------------------
split_vc
VC main.199.0------------------
split_all_full
VC main.199.0.00.08---------------
VC main.199.1---------------0.03
VC main.199.2---------------0.01
VC main.199.3---------------0.04
VC main.199.4------------------
split_all_full
VC main.199.4.00.04---------------
VC main.199.5------------------
split_all_full
VC main.199.5.00.05---------------
VC main.199.60.06---------------
VC main.2000.12---------------
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.62---------------
VC main.208---------------0.02
VC main.209---------------0.04
VC main.210---------------0.02
VC main.211---------------0.03
VC main.212------------------
split_vc
VC main.212.00.03---------------
VC main.212.10.02---------------
VC main.212.20.04---------------
VC main.212.30.03---------------
VC main.212.40.03---------------
VC main.213------------------
split_vc
VC main.213.00.22---------------
VC main.213.10.98---------------
VC main.213.20.03---------------
VC main.213.30.21---------------
VC main.213.40.03---------------
VC main.213.50.03---------------
VC main.213.60.03---------------
VC main.2140.76---------------
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.43------------0.04
VC main.216.1.0.10.44------------0.04
VC main.216.1.0.2------------------
split_all_full
VC main.216.1.0.2.04.38---------------
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.2212.61---------------
VC main.2222.66---------------
VC main.223------------------
split_all_full
VC main.223.01.81---------------
VC main.223.11.10---------------
VC main.223.2---2.14------------
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.05
VC main.224.1.10.04---------------
VC main.225------------0.15---
VC main.2260.02---------------
VC main.2270.03---------------
VC main.228------------------
split_vc
VC main.228.00.04---------------
VC main.228.10.04---------------
VC main.2290.03---------------
VC main.230---------------0.02
VC main.231------------------
split_vc
VC main.231.00.02---------------
VC main.231.10.05---------------
VC main.231.20.06---------------
VC main.231.30.05---------------
VC main.231.40.03---------------
VC main.231.50.02---------------
VC main.231.60.07---------------
VC main.2320.13---------------
VC main.2330.66---------------