Require Export Memory. Require Export Memory_hypotheses. Require Export Op. Require Export Maps. Require Cmconstr. Load param. Notation color_mask := extra_mask (only parsing). Notation Color_header := Extra_header (only parsing). Definition COLOR_WHITE := zero. Definition COLOR_GRAY := repr (Z_of_bits wordsize (fun z => (zeq (Z_of_nat wordsize - 2) z))). Definition COLOR_BLACK := color_mask. Definition construct_val_is_pointer_or_dumb_weak (v : val) := match v with | Vint i => if eq i zero then Some None else None | Vptr b i => Some (Some (b, i)) | _ => None end. Lemma construct_val_is_pointer_or_dumb_weak_some : forall v o, construct_val_is_pointer_or_dumb_weak v = Some o -> val_is_pointer_or_dumb v o. Proof. destruct v; simpl; try (intros; discriminate). case_eq (eq i zero); try (intros; discriminate). intro Heq_zero. generalize (eq_bool_eq_prop Heq_zero). intro; subst. injection 1; intro; subst; auto. injection 1; intro; subst; auto. Qed. Lemma val_is_pointer_or_dumb_constructs_some : forall v o, val_is_pointer_or_dumb v o -> construct_val_is_pointer_or_dumb_weak v = Some o. Proof. inversion 1; subst; auto. Qed. Module Type Marksweep_parameters. Parameter GRAY_CACHE_SIZE : int. Axiom four_divides_gray_cache_size : four_divides GRAY_CACHE_SIZE. Axiom gray_cache_well_bounded : cmp Cle zero GRAY_CACHE_SIZE = true. Hint Resolve four_divides_gray_cache_size gray_cache_well_bounded. End Marksweep_parameters. Module Type Marksweep_variables. Parameters gray_cache gray_cache_offset gray_cache_overflow : ident. Parameters mb_b mb_header mb_cache : ident. Axiom mb_b_header_indep : mb_b <> mb_header. Axiom mb_b_cache_indep : mb_b <> mb_cache. Axiom mb_header_cache_indep : mb_header <> mb_cache. Parameters gm_root gm_numroots gm_p gm_cache gm_b gm_header gm_firstfield gm_n : ident. Axiom gm_root_numroots_indep : gm_root <> gm_numroots. Axiom gm_root_p_indep : gm_root <> gm_p. Axiom gm_root_cache_indep : gm_root <> gm_cache. Axiom gm_root_b_indep : gm_root <> gm_b. Axiom gm_root_header_indep : gm_root <> gm_header. Axiom gm_root_firstfield_indep : gm_root <> gm_firstfield. Axiom gm_root_n_indep : gm_root <> gm_n. Axiom gm_p_cache_indep : gm_p <> gm_cache. Axiom gm_p_b_indep : gm_p <> gm_b. Axiom gm_p_header_indep : gm_p <> gm_header. Axiom gm_p_firstfield_indep : gm_p <> gm_firstfield. Axiom gm_p_n_indep : gm_p <> gm_n. Axiom gm_cache_b_indep : gm_cache <> gm_b. Axiom gm_cache_header_indep : gm_cache <> gm_header. Axiom gm_cache_firstfield_indep : gm_cache <> gm_firstfield. Axiom gm_cache_n_indep : gm_cache <> gm_n. Axiom gm_b_header_indep : gm_b <> gm_header. Axiom gm_b_firstfield_indep : gm_b <> gm_firstfield. Axiom gm_b_n_indep : gm_b <> gm_n. Axiom gm_header_firstfield_indep : gm_header <> gm_firstfield. Axiom gm_header_n_indep : gm_header <> gm_n. Axiom gm_firstfield_n_indep : gm_firstfield <> gm_n. Hint Resolve mb_b_header_indep mb_b_cache_indep mb_header_cache_indep gm_root_numroots_indep gm_root_p_indep gm_root_cache_indep gm_root_b_indep gm_root_header_indep gm_root_firstfield_indep gm_root_n_indep gm_p_cache_indep gm_p_b_indep gm_p_header_indep gm_p_firstfield_indep gm_p_n_indep gm_cache_b_indep gm_cache_header_indep gm_cache_firstfield_indep gm_cache_n_indep gm_b_header_indep gm_b_firstfield_indep gm_b_n_indep gm_header_firstfield_indep gm_header_n_indep gm_firstfield_n_indep. Parameter gm_mark_block : ident. End Marksweep_variables. Module Marksweep_programs (MP : Marksweep_parameters) (CV : Common_variables) (MV : Marksweep_variables). Export MP. Export CV. Export MV. Definition mark_block_cminor_prog := Sseq (Cmconstr.ifthenelse (Cmconstr.cmp Ceq (Evar mb_b) (Eop (Ointconst zero) Enil)) (Sreturn None) Sskip) (Sseq (Sassign mb_header (Eload Mint32 (Aindexed (neg four)) (Econs (Evar mb_b) Enil))) (Sseq (Cmconstr.ifthenelse (Cmconstr.cmp Cne (Cmconstr.and (Evar mb_header) (Eop (Ointconst color_mask) Enil)) (Eop (Ointconst COLOR_WHITE) Enil)) (Sreturn None) Sskip) (Cmconstr.ifthenelse (Cmconstr.cmp Ceq (Cmconstr.and (Evar mb_header) (Eop (Ointconst kind_mask) Enil)) (Eop (Ointconst KIND_RAWDATA) Enil)) (Sexpr (Estore Mint32 (Aindexed (neg four)) (Econs (Evar mb_b) Enil) (Cmconstr.or (Evar mb_header) (Eop (Ointconst COLOR_BLACK) Enil)))) (Sseq (Sexpr (Estore Mint32 (Aindexed (neg four)) (Econs (Evar mb_b) Enil) (Cmconstr.or (Evar mb_header) (Eop (Ointconst COLOR_GRAY) Enil)))) (Sseq (Sassign mb_cache (Eload Mint32 (Aglobal gray_cache_offset zero) Enil)) (Cmconstr.ifthenelse (Cmconstr.cmp Ceq (Evar mb_cache) (Eop (Ointconst GRAY_CACHE_SIZE) Enil)) (Sexpr (Estore Mint32 (Aglobal gray_cache_overflow zero) Enil (Eop (Ointconst one) Enil))) (Sseq (Sexpr (Estore Mint32 (Abased gray_cache zero) (Econs (Evar mb_cache) Enil) (Evar mb_b))) (Sexpr (Estore Mint32 (Aglobal gray_cache_offset zero) Enil (Cmconstr.addimm four (Evar mb_cache)))) ) ) ) ) ) ) ) . Definition mark_block_cminor_function := Internal ( mkfunction (mksignature (Tint :: nil) None) (mb_b :: nil) (mb_header :: mb_cache :: nil) 0 mark_block_cminor_prog ). Definition mark_root_list_body_cminor := Sseq (Cmconstr.ifthenelse (Cmconstr.cmp Ceq (Evar gm_numroots) (Eop (Ointconst zero) Enil)) (Sexit O) (Sskip)) (Sseq (Sexpr (Ecall (funsig mark_block_cminor_function) (Eop (Oaddrsymbol gm_mark_block zero) Enil) (Econs (Eload Mint32 (Aindexed zero) (Econs (Evar gm_p) Enil)) Enil)) ) (Sseq (Sassign gm_p (Cmconstr.addimm four (Evar gm_p))) (Sassign gm_numroots (Cmconstr.addimm (neg one) (Evar gm_numroots))) ) ) . Definition mark_root_list_loop_cminor := Sloop mark_root_list_body_cminor. Definition mark_all_roots_body_cminor := Sseq (Cmconstr.ifthenelse (Cmconstr.cmp Ceq (Evar gm_root) (Eop (Ointconst zero) Enil)) (Sexit O) (Sskip)) (Sseq (Sassign gm_numroots (Eload Mint32 (Aindexed four) (Econs (Evar gm_root) Enil))) (Sseq (Sassign gm_p (Eload Mint32 (Aindexed (add four four)) (Econs (Evar gm_root) Enil))) (Sseq (Sblock mark_root_list_loop_cminor) (Sassign gm_root (Eload Mint32 (Aindexed zero) (Econs (Evar gm_root) Enil))) ) ) ). End Marksweep_programs. Module Type Marksweep_hypotheses. Declare Module CH : Common_hypotheses. Export CH. Declare Module MV : Marksweep_variables. Export MV. Parameters gray_cache_block gray_cache_offset_block gray_cache_overflow_block : block. Axiom gray_cache_offset_heap_start_indep : gray_cache_offset_block <> heap_start_block. Axiom gray_cache_offset_heap_end_indep : gray_cache_offset_block <> heap_end_block. Axiom gray_cache_offset_freelist_head_indep : gray_cache_offset_block <> freelist_head_block. Axiom gray_cache_overflow_heap_start_indep : gray_cache_overflow_block <> heap_start_block. Axiom gray_cache_overflow_heap_end_indep : gray_cache_overflow_block <> heap_end_block. Axiom gray_cache_overflow_freelist_head_indep : gray_cache_overflow_block <> freelist_head_block. Axiom gray_cache_offset_gray_cache_overflow_indep : gray_cache_offset_block <> gray_cache_overflow_block. Axiom gray_cache_heap_start_indep : gray_cache_block <> heap_start_block. Axiom gray_cache_heap_end_indep : gray_cache_block <> heap_end_block. Axiom gray_cache_freelist_head_indep : gray_cache_block <> freelist_head_block. Axiom gray_cache_gray_cache_offset_indep : gray_cache_block <> gray_cache_offset_block. Axiom gray_cache_gray_cache_overflow_indep : gray_cache_block <> gray_cache_overflow_block. Hint Resolve gray_cache_offset_heap_start_indep gray_cache_offset_heap_end_indep gray_cache_offset_freelist_head_indep gray_cache_overflow_heap_start_indep gray_cache_overflow_heap_end_indep gray_cache_overflow_freelist_head_indep gray_cache_offset_gray_cache_overflow_indep gray_cache_heap_start_indep gray_cache_heap_end_indep gray_cache_freelist_head_indep gray_cache_gray_cache_offset_indep gray_cache_gray_cache_overflow_indep. Axiom genv_gray_cache : Genv.find_symbol genv gray_cache = Some gray_cache_block. Axiom genv_gray_cache_offset : Genv.find_symbol genv gray_cache_offset = Some gray_cache_offset_block. Axiom genv_gray_cache_overflow : Genv.find_symbol genv gray_cache_overflow = Some gray_cache_overflow_block. End Marksweep_hypotheses. Module Marksweep_algorithms (MP : Marksweep_parameters) (MH : Marksweep_hypotheses). Export MP. Export MH. Definition mark_block_body m bi := match bi with | None => Some m | Some (b, i) => match load Mint32 m b (signed (sub i four)) with | Some (Vint header) => if (negb (eq (Color_header header) COLOR_WHITE)) then Some m else if eq (Kind_header header) KIND_RAWDATA then store Mint32 m b (signed (sub i four)) (Vint (or header COLOR_BLACK)) else match store Mint32 m b (signed (sub i four)) (Vint (or header COLOR_GRAY)) with | None => None | Some m1 => match load Mint32 m1 gray_cache_offset_block 0 with | Some (Vint cache) => if eq cache GRAY_CACHE_SIZE then store Mint32 m1 gray_cache_overflow_block 0 (Vint one) else match store Mint32 m1 gray_cache_block (signed cache) (Vptr b i) with | Some m2 => store Mint32 m2 gray_cache_offset_block 0 (Vint (add cache four)) | None => None end | _ => None end end | _ => None end end. Definition mark_block m bi := let (m0, sp) := alloc m 0 0 in match mark_block_body m0 bi with | Some m' => Some (free m' sp) | None => None end. Record mark_root_list_param : Set := make_mark_root_list_param { mark_root_list_mem : mem; mark_root_list_numroots : int; mark_root_list_block : block; mark_root_list_offset : int }. Definition mark_root_list_body p0 := match p0 with | None => (true, None) (* infinite loop if indefinite state *) | Some p => let m := mark_root_list_mem p in if eq (mark_root_list_numroots p) zero then (false, Some p) else (true, match load Mint32 m (mark_root_list_block p) (signed (mark_root_list_offset p)) with | Some v => match construct_val_is_pointer_or_dumb_weak v with | Some v0 => match mark_block m v0 with | None => None | Some m' => Some (make_mark_root_list_param m' (sub (mark_root_list_numroots p) one) (mark_root_list_block p) (add (mark_root_list_offset p) four)) end | _ => None end | _ => None (* loop forever if value not defined *) end ) end. Lemma mark_root_list_none_nonterm : forall p, Loop.loop_term mark_root_list_body p -> p = None -> False. Proof. induction 1. intro ; subst. discriminate. intro ; subst. injection H. congruence. Qed. Lemma mark_root_list_res_some : forall p q, Loop.loop_prop mark_root_list_body p q -> q = None -> False. Proof. induction 1. intro ; subst. generalize H. unfold mark_root_list_body. destruct a; try (intros; discriminate). destruct (eq (mark_root_list_numroots m) zero); try (intros; discriminate). assumption. Qed. Record mark_all_roots_param : Set := make_mark_all_roots_param { mark_all_roots_root : val; mark_all_roots_mem : mem }. Definition mark_all_roots_body_before p := let m := mark_all_roots_mem p in match mark_all_roots_root p with | Vint z => if eq z zero then (false, (Some p, None)) else (true, (None, None)) | Vptr r d => (true, match load Mint32 m r (signed (add d four)) with | Some (Vint numroots) => (Some (make_mark_all_roots_param (mark_all_roots_root p) m), Some (make_mark_root_list_param m numroots r (add (add d four) four))) | _ => (None, None) end ) | _ => (true, (None, None)) end . Definition mark_all_roots_body_after p := match mark_all_roots_root p with | Vptr r d => let m' := (mark_all_roots_mem p) in match (load Mint32 m' r (signed d)) with | None => None | Some v => Some (make_mark_all_roots_param v m' ) end | _ => None end . Inductive mark_all_roots_body : mark_all_roots_param -> bool -> mark_all_roots_param -> Prop := | mark_all_roots_body_end : forall p p' j, (false, (Some p', j)) = mark_all_roots_body_before p -> mark_all_roots_body p false p' | mark_all_roots_body_cont : forall p p' rp', (true, (Some p', Some rp')) = mark_all_roots_body_before p -> forall rp''0, Loop.loop_prop mark_root_list_body (Some rp') (Some rp''0) -> forall p'', Some p'' = mark_all_roots_body_after (make_mark_all_roots_param (mark_all_roots_root p') (mark_root_list_mem rp''0) ) -> mark_all_roots_body p true p'' . Theorem mark_all_roots_body_func_bool : forall p b1 p1, mark_all_roots_body p b1 p1 -> forall b2 p2, mark_all_roots_body p b2 p2 -> b1 = b2. induction 1; inversion 1; congruence. Qed. Theorem mark_all_roots_body_func_A : forall p b1 p1, mark_all_roots_body p b1 p1 -> forall b2 p2, mark_all_roots_body p b2 p2 -> p1 = p2. induction 1; inversion 1; try congruence. subst. replace p'0 with p' in *; [ | congruence]. replace rp'0 with rp' in *; [ |congruence]. cut (Some rp''0 = Some rp''1). congruence. eapply Loop.loop_functional. eassumption. assumption. Qed. Theorem mark_all_roots_body_dec : forall p, (exists b, exists p1, mark_all_roots_body p b p1) -> {b : _ & {p1 : _ | mark_all_roots_body p b p1}}. Proof. intros p Hp. case_eq (mark_all_roots_body_before p). destruct b. destruct p0. intro Hm. destruct o0. destruct (@Loop.loop _ mark_root_list_body (Some m)). inversion Hp as [b [p1 Hp1]]. inversion Hp1. subst. rewrite Hm in H. discriminate. subst. rewrite Hm in H. injection H. intros; subst. eapply Loop.loop_terminates. eassumption. destruct x. destruct o. case_eq (mark_all_roots_body_after (make_mark_all_roots_param (mark_all_roots_root m1) (mark_root_list_mem m0) )). intros m2 Hm2. exists true. exists m2. eapply mark_all_roots_body_cont. eauto. eauto. auto. intro Habs. apply False_rect. inversion Hp as [b [p1 Hp1]]. inversion Hp1. subst. rewrite Hm in H. discriminate. subst. rewrite Hm in H. injection H; intros; subst. generalize (Loop.loop_functional l H0). injection 1; intros; subst; congruence. apply False_rect. inversion Hp as [b [p1 Hp1]]. inversion Hp1. subst. rewrite Hm in H. discriminate. subst. rewrite Hm in H. discriminate. apply False_rect. inversion Hp as [b [p1 Hp1]]. inversion Hp1. subst. rewrite Hm in H. discriminate. subst. rewrite Hm in H. injection H; intros; subst. generalize (Loop.loop_functional l H0). discriminate 1. apply False_rect. inversion Hp as [b [p1 Hp1]]. inversion Hp1. subst. rewrite Hm in H. discriminate. subst. rewrite Hm in H. discriminate. destruct p0. destruct o. intro Hm. exists false. exists m. eapply mark_all_roots_body_end. eauto. intro Habs. apply False_rect. inversion Hp as [b [p1 Hp1]]. inversion Hp1. subst. rewrite Habs in H. discriminate. subst. rewrite Habs in H. discriminate. Defined. Theorem all_roots_loop : forall p, Loop.genloop_term mark_all_roots_body p -> {p' | Loop.genloop_prop mark_all_roots_body p p'}. Proof. intros. eapply Loop.genloop. exact mark_all_roots_body_func_bool. exact mark_all_roots_body_func_A. exact mark_all_roots_body_dec. assumption. Defined. Section Find_first_gray_block. Variable m : mem. Variable heap : block. Variable he : int. Record find_first_gray_block_param : Set := make_find_first_gray_block_param { find_first_gray_block_scan : int; find_first_gray_block_result : val }. Definition find_first_gray_block_body p0 := match p0 with | Some p => let i := (find_first_gray_block_scan p) in if eq i he then (false, Some (make_find_first_gray_block_param i (Vint zero))) else match load Mint32 m heap (signed (find_first_gray_block_scan p)) with | Some (Vint v) => if eq (Color_header v) COLOR_GRAY then (false, Some (make_find_first_gray_block_param i (Vptr heap (add i four)))) else (true, Some (make_find_first_gray_block_param (add (add i (Size_header v)) four) (find_first_gray_block_result p))) | _ => (true, None) end | _ => (true, None) end . Lemma find_first_gray_block_loop_arg_none : forall p0 q0, Loop.loop_prop find_first_gray_block_body p0 q0 -> p0 = None -> False. Proof. induction 1; intros; subst. discriminate. injection H. congruence. Qed. Corollary find_first_gray_block_loop_term_arg_none : Loop.loop_term find_first_gray_block_body None -> False. Proof. intro Habs. destruct (Loop.loop Habs). eapply find_first_gray_block_loop_arg_none; eauto. Qed. Lemma find_first_gray_block_loop_res_some : forall p0 q0, Loop.loop_prop find_first_gray_block_body p0 q0 -> q0 = None -> False. Proof. induction 1; intros; subst. generalize H. unfold find_first_gray_block_body. destruct a; try (intros; discriminate). destruct (eq (find_first_gray_block_scan f)); try (intros; discriminate). destruct (load Mint32 m heap (signed (find_first_gray_block_scan f))); try (intros; discriminate). destruct v; try (intros; discriminate). destruct (eq (Color_header i) COLOR_GRAY); try (intros; discriminate). congruence. Qed. Corollary find_first_gray_block_loop_term : forall p, Loop.loop_term find_first_gray_block_body (Some p) -> {q | Loop.loop_prop find_first_gray_block_body (Some p) (Some q)}. Proof. intros p Hp. destruct (Loop.loop Hp) as [q0 Hq0]. destruct q0. esplit; eauto. apply False_rect. eapply find_first_gray_block_loop_res_some. eassumption. trivial. Defined. Lemma find_first_gray_block_loop_func_strong : forall p0 q0, Loop.loop_prop find_first_gray_block_body p0 q0 -> forall p, Some p = p0 -> forall q, Some q = q0 -> forall p10 q10, Loop.loop_prop find_first_gray_block_body p10 q10 -> forall p1, Some p1 = p10 -> forall q1, Some q1 = q10 -> find_first_gray_block_scan p = find_first_gray_block_scan p1 -> find_first_gray_block_result q = find_first_gray_block_result q1. Proof. induction 1. intros until 2. subst. inversion 1. intros; subst. generalize H H1. unfold find_first_gray_block_body. rewrite H6. destruct (eq (find_first_gray_block_scan p1) he). congruence. destruct (load Mint32 m heap (signed (find_first_gray_block_scan p1))); try (intros; discriminate). destruct v; try (intros; discriminate). destruct (eq (Color_header i) COLOR_GRAY); try (intros; discriminate). congruence. intros; subst. generalize H H1. unfold find_first_gray_block_body. rewrite H7. destruct (eq (find_first_gray_block_scan p1) he); try (intros; discriminate). destruct (load Mint32 m heap (signed (find_first_gray_block_scan p1))); try (intros; discriminate). destruct v; try (intros; discriminate). destruct (eq (Color_header i) COLOR_GRAY); try (intros; discriminate). intros until 2. subst. inversion 1. intros; subst. generalize H H2. unfold find_first_gray_block_body. rewrite H7. destruct (eq (find_first_gray_block_scan p1) he); try (intros; discriminate). destruct (load Mint32 m heap (signed (find_first_gray_block_scan p1))); try (intros; discriminate). destruct v; try (intros; discriminate). destruct (eq (Color_header i) COLOR_GRAY); try (intros; discriminate). intros; subst. generalize H H2. unfold find_first_gray_block_body. rewrite H8. destruct (eq (find_first_gray_block_scan p1) he); try (intros; discriminate). destruct (load Mint32 m heap (signed (find_first_gray_block_scan p1))); try (intros; discriminate). destruct v; try (intros; discriminate). injection 1; intros; subst; destruct (find_first_gray_block_loop_arg_none H0 (refl_equal _)). destruct (eq (Color_header i) COLOR_GRAY); try (intros; discriminate). injection 1; injection 2; intros; subst. eapply IHloop_prop. reflexivity. trivial. eexact H3. reflexivity. trivial. simpl. trivial. injection 1; intros; subst; destruct (find_first_gray_block_loop_arg_none H0 (refl_equal _)). injection 1; intros; subst; destruct (find_first_gray_block_loop_arg_none H0 (refl_equal _)). injection 1; intros; subst; destruct (find_first_gray_block_loop_arg_none H0 (refl_equal _)). Qed. Lemma find_first_gray_block_loop_term_strong_1 : forall p0, Loop.loop_term find_first_gray_block_body p0 -> forall p, Some p = p0 -> forall p2, find_first_gray_block_scan p2 = find_first_gray_block_scan p -> Loop.loop_term find_first_gray_block_body (Some p2). Proof. induction 1. intros; subst. generalize H. unfold find_first_gray_block_body. case_eq (eq (find_first_gray_block_scan p) he). injection 2 ; intros; subst. eapply Loop.loop_term_interrupt. rewrite H1. rewrite H0. reflexivity. intro. case_eq (load Mint32 m heap (signed (find_first_gray_block_scan p))); try (intros; discriminate). destruct v; try (intros; discriminate). case_eq (eq (Color_header i) COLOR_GRAY); try (intros; discriminate). injection 2; intros; subst. eapply Loop.loop_term_interrupt. rewrite H1. rewrite H0. rewrite H4. rewrite H2. reflexivity. intros; subst. generalize H. unfold find_first_gray_block_body. case_eq (eq (find_first_gray_block_scan p) he); try (intros; discriminate). case_eq (load Mint32 m heap (signed (find_first_gray_block_scan p))). destruct v. injection 3; intros; subst;destruct (find_first_gray_block_loop_term_arg_none H0). case_eq (eq (Color_header i) COLOR_GRAY); try (intros; discriminate). injection 4; intros; subst. eapply Loop.loop_term_continue. rewrite H2. rewrite H4. rewrite H3. rewrite H1. reflexivity. eapply IHloop_term. reflexivity. trivial. injection 3; intros; subst;destruct (find_first_gray_block_loop_term_arg_none H0). injection 3; intros; subst;destruct (find_first_gray_block_loop_term_arg_none H0). injection 3; intros; subst;destruct (find_first_gray_block_loop_term_arg_none H0). Qed. Corollary find_first_gray_block_loop_term_strong_0 : forall s p, (exists p, find_first_gray_block_scan p = s /\ Loop.loop_term find_first_gray_block_body (Some p)) -> find_first_gray_block_scan p = s -> {p' | Loop.loop_prop find_first_gray_block_body (Some p) (Some p')}. Proof. intros. cut ({p0' | Loop.loop_prop find_first_gray_block_body (Some p) p0'}). inversion 1. destruct x. esplit; eauto. apply False_rect. eapply find_first_gray_block_loop_res_some. eassumption. trivial. apply Loop.loop. invall. eapply find_first_gray_block_loop_term_strong_1. eassumption. reflexivity. congruence. Defined. Lemma find_first_gray_block_loop_some_in_heap : forall p0 q0, Loop.loop_prop find_first_gray_block_body p0 q0 -> forall p, Some p = p0 -> forall q, Some q = q0 -> forall b i, find_first_gray_block_result q = Vptr b i -> b = heap. Proof. induction 1. intros; subst. generalize H. unfold find_first_gray_block_body. destruct (eq (find_first_gray_block_scan p) he). injection 1; intros; subst; discriminate. destruct (load Mint32 m heap (signed (find_first_gray_block_scan p))); try (intros; discriminate). destruct v; try (intros; discriminate). destruct (eq (Color_header i0) COLOR_GRAY); try (intros; discriminate). injection 1; intros; subst. simpl in H2. congruence. intros; subst. generalize H. unfold find_first_gray_block_body. destruct (eq (find_first_gray_block_scan p) he); try (intros; discriminate). destruct (load Mint32 m heap (signed (find_first_gray_block_scan p))). destruct v. injection 1; intros; subst. destruct (find_first_gray_block_loop_arg_none H0 (refl_equal _)). destruct (eq (Color_header i0) COLOR_GRAY); try (intros; discriminate). injection 1; intros; subst. eauto. injection 1; intros; subst. destruct (find_first_gray_block_loop_arg_none H0 (refl_equal _)). injection 1; intros; subst. destruct (find_first_gray_block_loop_arg_none H0 (refl_equal _)). injection 1; intros; subst. destruct (find_first_gray_block_loop_arg_none H0 (refl_equal _)). Qed. Lemma find_first_gray_block_loop_some_pointer_or_dumb : forall p0 q0, Loop.loop_prop find_first_gray_block_body p0 q0 -> forall p, Some p = p0 -> forall q, Some q = q0 -> val_is_pointer_or_dumb_desc (find_first_gray_block_result q). Proof. induction 1. intros; subst. generalize H. unfold find_first_gray_block_body. destruct (eq (find_first_gray_block_scan p) he). injection 1; intros; subst; auto. destruct (load Mint32 m heap (signed (find_first_gray_block_scan p))); try (intros; discriminate). destruct v; try (intros; discriminate). destruct (eq (Color_header i) COLOR_GRAY); try (intros; discriminate). injection 1; intros; subst. simpl; auto. intros; subst. generalize H. unfold find_first_gray_block_body. destruct (eq (find_first_gray_block_scan p) he); try (intros; discriminate). destruct (load Mint32 m heap (signed (find_first_gray_block_scan p))). destruct v. injection 1; intros; subst. destruct (find_first_gray_block_loop_arg_none H0 (refl_equal _)). destruct (eq (Color_header i) COLOR_GRAY); try (intros; discriminate). injection 1; intros; subst. eauto. injection 1; intros; subst. destruct (find_first_gray_block_loop_arg_none H0 (refl_equal _)). injection 1; intros; subst. destruct (find_first_gray_block_loop_arg_none H0 (refl_equal _)). injection 1; intros; subst. destruct (find_first_gray_block_loop_arg_none H0 (refl_equal _)). Qed. End Find_first_gray_block. Section Mark_gray. Record mark_children_body_param : Set := make_mark_children_body_param { mark_children_body_mem : mem; mark_children_body_n : int }. Definition mark_children_body heap b firstfield p0 := match p0 with | Some p => if eq (mark_children_body_n p) firstfield then (false, Some p) else (true, let n := sub (mark_children_body_n p) four in match match load Mint32 (mark_children_body_mem p) heap (signed (add b n)) with | Some (Vint zero) => mark_block (mark_children_body_mem p) None | Some (Vptr bl of) => mark_block (mark_children_body_mem p) (Some (bl, of)) | _ => None end with | Some m' => Some (make_mark_children_body_param m' n) | _ => None end ) | _ => (true, None) end. Section Mark_gray_body_middle. Variable hi : val. Definition mark_gray_body_middle m m' : Prop := match hi with | Vptr heap i => match load Mint32 m heap (signed (sub i four)) with | Some (Vint header) => match store Mint32 m heap (signed (sub i four)) (Vint (or header COLOR_BLACK)) with | Some m1 => exists n, Loop.loop_prop (mark_children_body heap i (if eq (Kind_header header) KIND_CLOSURE then four else zero)) (Some (make_mark_children_body_param m1 (Size_header header))) (Some (make_mark_children_body_param m' n)) | _ => False end | _ => False end | _ => False end. Lemma mark_gray_body_middle_dec m : (exists m', mark_gray_body_middle m m') -> {m' | mark_gray_body_middle m m'}. Proof. unfold mark_gray_body_middle. introvars. destruct hi; try (intros; apply False_rect; invall; auto ; fail). case_eq (load Mint32 m b (signed (sub i four))); try (intros; apply False_rect; invall; auto ; fail). destruct v ; try (intros; apply False_rect; invall; auto ; fail). case_eq (store Mint32 m b (signed (sub i four)) (Vint (or i0 COLOR_BLACK))); try (intros; apply False_rect; invall; auto ; fail). intros m1 Hm1 Hi0. intro Hloop. assert ( Loop.loop_term (mark_children_body b i (if eq (Kind_header i0) KIND_CLOSURE then four else zero)) (Some (make_mark_children_body_param m1 (Size_header i0)))). invall. eapply Loop.loop_terminates. eassumption. destruct (Loop.loop H) as [p Hp]. destruct p. destruct m0. clear Hloop. exists mark_children_body_mem0. exists mark_children_body_n0. assumption. apply False_rect. invall. generalize (Loop.loop_functional Hp H1). discriminate 1. Defined. Lemma mark_gray_body_middle_func m : forall m'1, mark_gray_body_middle m m'1 -> forall m'2, mark_gray_body_middle m m'2 -> m'1 = m'2. Proof. unfold mark_gray_body_middle. introvars. destruct hi; try (intros; contradiction). destruct (load Mint32 m b (signed (sub i four))); try (intros; contradiction). destruct v; try (intros; contradiction). destruct (store Mint32 m b (signed (sub i four)) (Vint (or i0 COLOR_BLACK))); try (intros; contradiction). intros. invall. generalize (Loop.loop_functional H1 H0). congruence. Qed. End Mark_gray_body_middle. Section Mark_gray_body. Variable heap : block. Variables hs he : int. Definition mark_gray_body m b m' := match load Mint32 m gray_cache_offset_block 0 with | Some (Vint cache) => if eq cache zero then match load Mint32 m gray_cache_overflow_block 0 with | Some (Vint overflow) => if eq overflow one then exists v, exists i', exists bi, Loop.loop_prop (find_first_gray_block_body m heap he) (Some (make_find_first_gray_block_param hs v)) (Some (make_find_first_gray_block_param i' bi)) /\ match bi with | Vint z => if eq z zero then (b = false /\ m' = m) else (b = true /\ mark_gray_body_middle (Vint z) m m') | blof => (b = true /\ mark_gray_body_middle blof m m') end else (b = false /\ m' = m) | _ => False end else let cache' := sub cache four in match load Mint32 m gray_cache_block (signed cache') with | Some blof => match store Mint32 m gray_cache_offset_block 0 (Vint cache') with | Some m1 => b = true /\ mark_gray_body_middle blof m1 m' | _ => False end | _ => False end | _ => False end. Lemma mark_gray_body_func_bool m b m' : mark_gray_body m b m' -> forall b2 m'2 , mark_gray_body m b2 m'2 -> b = b2. Proof. unfold mark_gray_body. introvars. destruct (load Mint32 m gray_cache_offset_block 0 ); try (intros; contradiction). destruct v; try (intros; contradiction). destruct (eq i zero). destruct (load Mint32 m gray_cache_overflow_block 0 ); try (intros; contradiction). destruct v; try (intros; contradiction). destruct(eq i0 one). intros. invall. generalize (find_first_gray_block_loop_func_strong H0 (refl_equal _) (refl_equal _) H (refl_equal _) (refl_equal _) (refl_equal _)). simpl. intros; subst. destruct x4; invall; try congruence. destruct (eq i1 zero); invall; try congruence. intros; invall; congruence. destruct (load Mint32 m gray_cache_block (signed (sub i four))); try (intros; contradiction). destruct (store Mint32 m gray_cache_offset_block 0 (Vint (sub i four))); intros; try contradiction; invall; congruence. Qed. Lemma mark_gray_body_func_A m b m' : mark_gray_body m b m' -> forall b2 m'2 , mark_gray_body m b2 m'2 -> m' = m'2. Proof. unfold mark_gray_body. introvars. destruct (load Mint32 m gray_cache_offset_block 0 ); try (intros; contradiction). destruct v; try (intros; contradiction). destruct (eq i zero). destruct (load Mint32 m gray_cache_overflow_block 0 ); try (intros; contradiction). destruct v; try (intros; contradiction). destruct(eq i0 one). intros. invall. generalize (find_first_gray_block_loop_func_strong H0 (refl_equal _) (refl_equal _) H (refl_equal _) (refl_equal _) (refl_equal _)). simpl. intros; subst. destruct x4; invall. eapply mark_gray_body_middle_func ; eauto. destruct (eq i1 zero); invall. congruence. eapply mark_gray_body_middle_func ; eauto. eapply mark_gray_body_middle_func ; eauto. eapply mark_gray_body_middle_func ; eauto. intros; invall; congruence. destruct (load Mint32 m gray_cache_block (signed (sub i four))); try (intros; contradiction). destruct (store Mint32 m gray_cache_offset_block 0 (Vint (sub i four))); intros; try contradiction; invall. eapply mark_gray_body_middle_func; eauto. Qed. Lemma mark_gray_body_dec m : (exists b, exists m', mark_gray_body m b m') -> {b : _ & {m' : _ | mark_gray_body m b m'}}. Proof. unfold mark_gray_body. intros. destruct (load Mint32 m gray_cache_offset_block 0); try (apply False_rect; invall; contradiction; fail). destruct v; try (apply False_rect; invall; contradiction; fail). destruct (eq i zero). destruct (load Mint32 m gray_cache_overflow_block 0); try (apply False_rect; invall; contradiction; fail). destruct v; try (apply False_rect; invall; contradiction; fail). destruct (eq i0 one). destruct (@find_first_gray_block_loop_term_strong_0 m heap he hs (make_find_first_gray_block_param hs Vundef)). invall. esplit. esplit. 2 : eapply Loop.loop_terminates; eauto. trivial. trivial. destruct x. destruct find_first_gray_block_result0. apply False_rect. invall. generalize (find_first_gray_block_loop_func_strong l (refl_equal _) (refl_equal _) H (refl_equal _) (refl_equal _) (refl_equal _)). simpl. intros; subst. invall. inversion H2. case_eq (eq i1 zero). intro Hzero. exists false. exists m. repeat esplit; eauto. simpl. rewrite Hzero. auto. intro Hnz. apply False_rect. invall. generalize (find_first_gray_block_loop_func_strong l (refl_equal _) (refl_equal _) H (refl_equal _) (refl_equal _) (refl_equal _)). simpl. intros; subst. rewrite Hnz in H1. invall. inversion H2. apply False_rect. invall. generalize (find_first_gray_block_loop_func_strong l (refl_equal _) (refl_equal _) H (refl_equal _) (refl_equal _) (refl_equal _)). simpl. intros; subst. invall. inversion H2. assert (exists m', mark_gray_body_middle (Vptr b i1) m m'). invall. generalize (find_first_gray_block_loop_func_strong l (refl_equal _) (refl_equal _) H (refl_equal _) (refl_equal _) (refl_equal _)). intro Hx4. simpl in Hx4. subst. invall. subst. esplit; eauto. generalize (mark_gray_body_middle_dec H0). intros [m' Hm']. exists true. exists m'. invall. generalize (find_first_gray_block_loop_func_strong l (refl_equal _) (refl_equal _) H (refl_equal _) (refl_equal _) (refl_equal _)). simpl. intros; subst. invall. subst. exists Vundef. exists find_first_gray_block_scan0. exists (Vptr b i1). split; auto. repeat esplit; reflexivity. destruct (load Mint32 m gray_cache_block (signed (sub i four))); try ( apply False_rect; invall; contradiction; fail). destruct (store Mint32 m gray_cache_offset_block 0 (Vint (sub i four))); try ( apply False_rect; invall; contradiction; fail). exists true. cut {m' | mark_gray_body_middle v m0 m'}. inversion 1. repeat esplit; eauto. apply mark_gray_body_middle_dec. invall; esplit; eauto. Defined. Lemma mark_gray_loop_term : forall m, Loop.genloop_term (mark_gray_body ) m -> {m' | Loop.genloop_prop (mark_gray_body ) m m'}. Proof. intros. apply Loop.genloop. apply mark_gray_body_func_bool. apply mark_gray_body_func_A. apply mark_gray_body_dec. assumption. Defined. Definition cache_pop m r m' := match load Mint32 m gray_cache_offset_block 0 with | Some (Vint cache) => if eq cache zero then m' = m /\ match load Mint32 m gray_cache_overflow_block 0 with | Some (Vint overflow) => if eq overflow one then exists v, exists i', exists bi, Loop.loop_prop (find_first_gray_block_body m heap he) (Some (make_find_first_gray_block_param hs v)) (Some (make_find_first_gray_block_param i' bi)) /\ match bi with | Vint z => if eq z zero then r = None else r = Some bi | _ => r = Some bi end else r = None | _ => False end else let cache' := sub cache four in match load Mint32 m gray_cache_block (signed cache') with | Some blof => match store Mint32 m gray_cache_offset_block 0 (Vint cache') with | Some m1 => r = Some blof /\ m' = m1 | _ => False end | _ => False end | _ => False end. Definition mark_gray_body_2 m b m' := exists m1, exists r, cache_pop m r m1 /\ match r with | None => (b = false /\ m' = m1) | Some blof => (b = true /\ mark_gray_body_middle blof m1 m') end . Lemma mark_gray_body_is_body_2 : forall m b m', mark_gray_body m b m' -> mark_gray_body_2 m b m'. Proof. unfold mark_gray_body. unfold mark_gray_body_2. unfold cache_pop. introvars. destruct (load Mint32 m gray_cache_offset_block 0); try (intro; contradiction). destruct v; try (intro; contradiction). destruct (eq i zero). destruct (load Mint32 m gray_cache_overflow_block 0); try (intro; contradiction). destruct v; try (intro; contradiction). destruct (eq i0 one). intros. invall. exists m. destruct x1; invall. exists (Some Vundef). split. split. auto. repeat eapply ex_intro. split. eassumption. simpl; auto. auto. case_eq (eq i1 zero). intro Hzero. rewrite Hzero in *; invall. exists (@None val). split. split. trivial. repeat eapply ex_intro. split. eassumption. simpl. rewrite Hzero. trivial. auto. intro Hnz. rewrite Hnz in *. exists (Some (Vint i1)). split. split. trivial. repeat eapply ex_intro. split. eassumption. simpl. rewrite Hnz. trivial. auto. exists (Some (Vfloat f)). split. split. trivial. repeat eapply ex_intro. split. eassumption. simpl. trivial. auto. exists (Some (Vptr b0 i1)). split. split. auto. repeat eapply ex_intro. split. eassumption. simpl. trivial. auto. intros; invall. exists m. exists (@None val). auto. destruct (load Mint32 m gray_cache_block (signed (sub i four))); try (intros; contradiction). destruct (store Mint32 m gray_cache_offset_block 0 (Vint (sub i four))); try (intros; contradiction). intros; invall. exists m0. exists (Some v). auto. Qed. Lemma mark_gray_body_2_is_body : forall m b m', mark_gray_body_2 m b m' -> mark_gray_body m b m'. Proof. unfold mark_gray_body_2, mark_gray_body, cache_pop. introvars. intro H. invall. destruct (load Mint32 m gray_cache_offset_block 0); try contradiction. destruct v; try contradiction. destruct (eq i zero). invall. subst. destruct (load Mint32 m gray_cache_overflow_block 0); try contradiction. destruct v; try contradiction. destruct (eq i0 one). invall. repeat eapply ex_intro. split. eassumption. destruct x2; subst; try assumption. destruct (eq i1 zero) ; subst; assumption. subst; assumption. destruct (load Mint32 m gray_cache_block (signed (sub i four))); try contradiction. destruct (store Mint32 m gray_cache_offset_block 0 (Vint (sub i four))); try contradiction. invall; subst; assumption. Qed. End Mark_gray_body. End Mark_gray. Section Gc_mark. Variable heap : block. Variables hs he : int. Definition gc_mark_body m r m' := exists ap', Loop.genloop_prop mark_all_roots_body (make_mark_all_roots_param r m) ap' /\ Loop.genloop_prop (mark_gray_body heap hs he) (mark_all_roots_mem ap') m'. Lemma gc_mark_body_func m r m'1 m'2 : gc_mark_body m r m'1 -> gc_mark_body m r m'2 -> m'1 = m'2. Proof. inversion 1. invall. inversion 1. invall. subst. replace x with x0 in *. eapply (@Loop.genloop_functional _ (mark_gray_body heap hs he)). apply mark_gray_body_func_bool. apply mark_gray_body_func_A. eassumption. assumption. eapply (@Loop.genloop_functional _ mark_all_roots_body). apply mark_all_roots_body_func_bool. apply mark_all_roots_body_func_A. eassumption. assumption. Qed. Lemma gc_mark_body_dec : forall m r, (exists m', gc_mark_body m r m') -> {m' | gc_mark_body m r m'}. Proof. intros. assert (Loop.genloop_term mark_all_roots_body (make_mark_all_roots_param r m)). inversion H. inversion H0. invall. subst. destruct x0. simpl in *. eapply Loop.genloop_terminates. eauto. generalize (all_roots_loop H0). intros [p' Hp']. assert (Loop.genloop_term (mark_gray_body heap hs he) (mark_all_roots_mem p')). inversion H. inversion H1. invall. subst. simpl in *. replace x0 with p' in *. eapply Loop.genloop_terminates. eassumption. eapply (@Loop.genloop_functional _ mark_all_roots_body). apply mark_all_roots_body_func_bool. apply mark_all_roots_body_func_A. eassumption. assumption. generalize (mark_gray_loop_term H1). intros [m' Hm']. exists m'. unfold gc_mark_body. exists p'. split. assumption. assumption. Defined. Definition gc_mark m r m' := exists m1, Some m1 = store Mint32 m gray_cache_offset_block 0 (Vint zero) /\ exists m2, Some m2 = store Mint32 m1 gray_cache_overflow_block 0 (Vint zero) /\ gc_mark_body m2 r m'. Lemma gc_mark_func m r m'1 m'2 : gc_mark m r m'1 -> gc_mark m r m'2 -> m'1 = m'2. Proof. inversion 1. invall. inversion 1. invall. replace x with x1 in *. replace x0 with x2 in *. eapply gc_mark_body_func. eassumption. eassumption. congruence. congruence. Qed. Lemma gc_mark_dec : forall m r, (exists m', gc_mark m r m') -> {m' | gc_mark m r m'}. Proof. intros. case_eq (store Mint32 m gray_cache_offset_block 0 (Vint zero)). intros. case_eq (store Mint32 m0 gray_cache_overflow_block 0 (Vint zero)). intros. assert (exists m', gc_mark_body m1 r m'). inversion H. inversion H2. invall. exists x. congruence. generalize (gc_mark_body_dec H2). intros [m' Hm']. exists m'. unfold gc_mark. exists m0. split. auto. exists m1. split. auto. assumption. intro Habs. apply False_rect. inversion H. inversion H1. invall. congruence. intros. apply False_rect. inversion H. inversion H1. invall. congruence. Defined. End Gc_mark. Section Sweep. Variable heap : block. Variable he : int. Record sweep_loop_body_param : Set := make_sweep_loop_body_param { sweep_mem : mem; sweep_last_nonempty_block : block; sweep_last_nonempty_offset : int; sweep_last_offset : int; sweep_last_is_empty : bool; sweep_prev_is_free : bool; sweep_scan_ptr_offset : int }. Definition sweep_loop_body p0 := match p0 with | None => (true, None) | Some p => if eq (sweep_scan_ptr_offset p) he then (false, Some p) else (true, match load Mint32 (sweep_mem p) heap (signed (sweep_scan_ptr_offset p)) with | Some (Vint v) => if eq (Color_header v) COLOR_WHITE then if (sweep_prev_is_free p) then match load Mint32 (sweep_mem p) heap (signed (sub (sweep_last_offset p) four)) with | Some (Vint v') => match store Mint32 (sweep_mem p) heap (signed (sub (sweep_last_offset p) four)) (Vint (add v' (add (Size_header v) four))) with | Some m1 => if (sweep_last_is_empty p) then match store Mint32 m1 (sweep_last_nonempty_block p) (signed (sweep_last_nonempty_offset p)) (Vptr heap (sweep_last_offset p)) with | Some m' => Some (make_sweep_loop_body_param m' heap (sweep_last_offset p) (sweep_last_offset p) false true (add (sweep_scan_ptr_offset p) (add (Size_header v) four)) ) | _ => None end else Some (make_sweep_loop_body_param m1 (sweep_last_nonempty_block p) (sweep_last_nonempty_offset p) (sweep_last_offset p) (sweep_last_is_empty p) true (add (sweep_scan_ptr_offset p) (add (Size_header v) four)) ) | _ => None end | _ => None end else if (eq (Size_header v) zero) then Some (make_sweep_loop_body_param (sweep_mem p) (sweep_last_nonempty_block p) (sweep_last_nonempty_offset p) (sweep_scan_ptr_offset p) true true (add (sweep_scan_ptr_offset p) four) ) else match store Mint32 (sweep_mem p) (sweep_last_nonempty_block p) (signed (sweep_last_nonempty_offset p)) (Vptr heap (sweep_scan_ptr_offset p)) with | Some m' => Some (make_sweep_loop_body_param m' heap (sweep_scan_ptr_offset p) (sweep_scan_ptr_offset p) false true (add (sweep_scan_ptr_offset p) (add (Size_header v) four)) ) | _ => None end else match store Mint32 (sweep_mem p) heap (signed (sweep_scan_ptr_offset p)) (Vint (and v (not COLOR_BLACK))) with | Some m' => Some (make_sweep_loop_body_param m' (sweep_last_nonempty_block p) (sweep_last_nonempty_offset p) (sweep_last_offset p) (sweep_last_is_empty p) false (add (sweep_scan_ptr_offset p) (add (Size_header v) four)) ) | _ => None end | _ => None end ) end. End Sweep. End Marksweep_algorithms.