theory memory_manage_sys
imports rg_cond func_cor_other func_cor_mempoolfree func_cor_mempoolalloc "../../picore/PiCore_ext"
begin
section ‹Formal specification of Zephyr memory management›
context event_hoare begin
definition mk_react_sys :: "(('a, 'b, 's, 'prog) esys, 's) PiCore_Validity.rgformula set ⇒ ('a, 'b, 's, 'prog) esys" where
‹mk_react_sys rgfs ≡ react_sys (map rgformula.Com (list_of_set rgfs))›
end
lemma event_hoareI: "event_hoare ptranI None prog_validityI rghoare_pI"
apply(rule event_hoare.intro)
apply(rule event_validity.intro)
apply(rule event_compI)
apply(rule event_validity_axioms.intro)
apply(erule prog_validity_defI)
apply(rule event_hoare_axioms.intro)
using rgsound_pI by blast
consts
all_ref :: "mempool_ref set"
max_sz :: nat
max_timeout :: int
all_blocks :: "Mem_block set"
all_threads :: "Thread set"
axiomatization where
all_ref_finite: ‹finite all_ref› and
all_blocks_finite: ‹finite all_blocks› and
all_threads_finite: ‹finite all_threads› and
all_threads_nonempty: ‹all_threads ≠ {}› and
all_ref_nonempty: ‹all_ref ≠ {}› and
max_timeout_nonneg: ‹max_timeout ≥ 0›
definition Thread_RGF :: "Thread ⇒ ((EL × Parameter list × Core, 'a, State, State com option) esys, State) PiCore_Validity.rgformula"
where "Thread_RGF t ≡
⦇ rgformula.Com = mk_react_sys ((⋃p∈all_ref. ⋃sz≤max_sz. ⋃timeout∈{(-1)..max_timeout}. {Mem_pool_alloc_RGCond t p sz timeout}) ∪
(⋃b∈all_blocks. {Mem_pool_free_RGCond t b})),
Pre = (Mem_pool_free_pre t ∩ Mem_pool_alloc_pre t),
Rely = (Mem_pool_free_rely t ∩ Mem_pool_alloc_rely t),
Guar = (Mem_pool_free_guar t ∪ Mem_pool_alloc_guar t),
Post = (Mem_pool_free_post t ∪ (⋃p∈all_ref. ⋃sz≤max_sz. ⋃timeout∈{(-1)..max_timeout}. Mem_pool_alloc_post t p sz timeout)) ⦈"
definition Scheduler_RGF
where "Scheduler_RGF ≡
⦇ rgformula.Com = mk_react_sys (⋃t∈all_threads. {Schedule_RGCond t}),
Pre = {s. inv s}, Rely = Schedule_rely, Guar = Schedule_guar, Post = {s. inv s} ⦈"
definition Timer_RGF
where "Timer_RGF ≡
⦇ rgformula.Com = mk_react_sys {Tick_RGCond},
Pre = ⦃True⦄, Rely = Tick_rely, Guar = Tick_guar, Post = ⦃True⦄ ⦈"
definition Memory_manage_system_Spec
where "Memory_manage_system_Spec k ≡
case k of (𝒯 t) ⇒ Thread_RGF t
| 𝒮 ⇒ Scheduler_RGF
| Timer ⇒ Timer_RGF"
section ‹ functional correctness of the whole specification›
definition "sys_rely ≡ {}"
definition "sys_guar ≡ Tick_guar ∪ Schedule_guar ∪ (⋃t. (Mem_pool_free_guar t ∪ Mem_pool_alloc_guar t))"
lemma scheduler_esys_sat: "Evt_sat_RG Γ (Memory_manage_system_Spec 𝒮)"
apply(simp add: Evt_sat_RG_def Memory_manage_system_Spec_def mk_react_sys_def Scheduler_RGF_def)
apply(rule event_hoare.Evt_react_set)
apply(fact event_hoareI)
apply auto[1]
using Schedule_satRG apply(simp add:Schedule_RGCond_def Evt_sat_RG_def Schedule_def) apply fast
apply(simp add: Schedule_RGCond_def)
apply(simp add: Schedule_RGCond_def)
apply(simp add: Schedule_RGCond_def)
apply(simp add: Schedule_RGCond_def)
apply(simp add: Schedule_RGCond_def)
apply(fact all_threads_nonempty)
using all_threads_finite apply simp
using stable_inv_sched_rely apply(simp add: PiCore_Hoare.stable_def)
apply(simp add: Schedule_guar_def)
done
lemma stable_int2_r: ‹stable p r ⟹ stable p (r ∩ s)› by (simp add: stable_def)
thm event_hoare.Evt_react_set
lemma thread_esys_sat: "Evt_sat_RG Γ (Memory_manage_system_Spec (𝒯 t))"
apply(simp add: Evt_sat_RG_def Memory_manage_system_Spec_def mk_react_sys_def Thread_RGF_def)
apply(rule event_hoare.Evt_react_set')
apply(fact event_hoareI)
apply auto[1]
using Mempool_alloc_satRG apply(simp add: Evt_sat_RG_def Mem_pool_alloc_RGCond_def)
apply force
apply(simp add: Mem_pool_alloc_RGCond_def)
apply(simp add: Mem_pool_alloc_RGCond_def)
apply(simp add: Mem_pool_alloc_RGCond_def)
apply(simp add: Mem_pool_alloc_RGCond_def Mem_pool_alloc_post_def)
apply(simp add: Mem_pool_alloc_RGCond_def Mem_pool_alloc_post_def)
apply(simp add: Mem_pool_alloc_RGCond_def Mem_pool_alloc_post_def)
using Mempool_alloc_satRG apply(simp add: Evt_sat_RG_def Mem_pool_alloc_RGCond_def Mem_pool_free_RGCond_def)
apply (smt Collect_cong Evt_sat_RG_def Mem_pool_free_RGCond_def Mempool_free_satRG rgformula.select_convs(1) rgformula.select_convs(2) rgformula.select_convs(3) rgformula.select_convs(4) rgformula.select_convs(5))
apply(simp add: Mem_pool_free_RGCond_def)
apply(simp add: Mem_pool_free_RGCond_def)
apply(simp add: Mem_pool_free_RGCond_def)
apply(simp add: Mem_pool_free_RGCond_def Mem_pool_free_post_def)
apply(simp add: Mem_pool_free_RGCond_def Mem_pool_free_post_def)
apply(simp add: Mem_pool_free_RGCond_def Mem_pool_free_post_def)
apply auto[1]
using all_ref_nonempty apply blast
using max_timeout_nonneg apply fastforce
using all_ref_finite all_blocks_finite apply simp
apply(subst stable_equiv)
using mem_pool_free_pre_stb stable_int2_r apply blast
apply(simp add: Mem_pool_free_guar_def)
using Mem_pool_free_post_def by auto
lemma timer_esys_sat: "Evt_sat_RG Γ (Memory_manage_system_Spec Timer)"
apply(simp add: Memory_manage_system_Spec_def Evt_sat_RG_def Timer_RGF_def mk_react_sys_def)
apply(rule event_hoare.Evt_react_set)
apply(rule event_hoare.intro)
apply(rule event_validity.intro)
apply(rule event_compI)
apply(rule event_validity_axioms.intro)
apply(erule prog_validity_defI)
apply(rule event_hoare_axioms.intro)
using rgsound_pI apply blast
apply auto[1]
using Tick_satRG apply(simp add:Tick_RGCond_def Evt_sat_RG_def Tick_def)
apply fast
apply(simp add:Tick_RGCond_def)+
apply(simp add: PiCore_Hoare.stable_def)
apply(simp add: Tick_guar_def)
done
lemma esys_sat: "Evt_sat_RG Γ (Memory_manage_system_Spec k)"
apply(induct k)
using scheduler_esys_sat apply fast
using thread_esys_sat apply fast
using timer_esys_sat apply fast
done
lemma s0_esys_pre: "{s0} ⊆ rgformula.Pre (Memory_manage_system_Spec k)"
apply(induct k)
apply(simp add:Memory_manage_system_Spec_def Scheduler_RGF_def)
using s0_inv apply fast
apply(simp add:Memory_manage_system_Spec_def Thread_RGF_def)
using s0_inv s0a4 s0a10 apply auto[1]
apply(simp add:Memory_manage_system_Spec_def Timer_RGF_def)
done
lemma alloc_free_eq_guar: "Mem_pool_free_guar x = Mem_pool_alloc_guar x"
by(simp add:Mem_pool_free_guar_def Mem_pool_alloc_guar_def)
lemma alloc_free_eq_rely: "Mem_pool_free_rely x = Mem_pool_alloc_rely x"
by(simp add:Mem_pool_free_rely_def Mem_pool_alloc_rely_def)
lemma esys_guar_in_other:
"jj ≠ k ⟶ rgformula.Guar (Memory_manage_system_Spec jj) ⊆ rgformula.Rely (Memory_manage_system_Spec k)"
apply auto
apply(induct jj)
apply(induct k)
apply simp
apply(simp add: Memory_manage_system_Spec_def Scheduler_RGF_def Thread_RGF_def)
using schedguar_in_allocrely apply(simp add:Mem_pool_free_rely_def Mem_pool_alloc_rely_def) apply auto[1]
apply(simp add: Memory_manage_system_Spec_def Scheduler_RGF_def Timer_RGF_def)
using schedguar_in_tickrely apply auto[1]
apply(induct k)
apply(simp add: Memory_manage_system_Spec_def Scheduler_RGF_def Thread_RGF_def)
apply auto[1]
using allocguar_in_schedrely alloc_free_eq_guar apply fast
using allocguar_in_schedrely apply fast
apply(simp add: Memory_manage_system_Spec_def Thread_RGF_def)
apply auto[1]
using allocguar_in_allocrely alloc_free_eq_guar alloc_free_eq_rely apply fast+
apply(simp add: Memory_manage_system_Spec_def Timer_RGF_def Thread_RGF_def)
apply auto[1]
using allocguar_in_tickrely alloc_free_eq_guar alloc_free_eq_rely apply fast+
apply(induct k)
apply(simp add: Memory_manage_system_Spec_def Scheduler_RGF_def Timer_RGF_def)
using tickguar_in_schedrely apply fast
apply(simp add: Memory_manage_system_Spec_def Thread_RGF_def Timer_RGF_def)
apply auto[1]
using tickguar_in_allocrely alloc_free_eq_guar alloc_free_eq_rely apply fast+
done
lemma esys_guar_in_sys: "rgformula.Guar (Memory_manage_system_Spec k) ⊆ sys_guar"
apply(induct k)
apply(simp add: Memory_manage_system_Spec_def Scheduler_RGF_def sys_guar_def) apply auto[1]
apply(simp add: Memory_manage_system_Spec_def Thread_RGF_def sys_guar_def) apply auto[1]
apply(simp add: Memory_manage_system_Spec_def Timer_RGF_def sys_guar_def) apply auto[1]
done
lemma mem_sys_sat: "rghoare_pes Γ Memory_manage_system_Spec {s0} sys_rely sys_guar UNIV"
apply(rule Par[of Γ Memory_manage_system_Spec "{s0}" sys_rely sys_guar UNIV])
apply clarify using esys_sat
using Evt_sat_RG_def apply fastforce
using s0_esys_pre apply fast
apply(simp add:sys_rely_def)
using esys_guar_in_other apply fast
using esys_guar_in_sys apply fast
apply simp
done
end