Library mcertikos.mm.MContainerIntroCode
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import MemWithData.
Require Import EventsX.
Require Import Globalenvs.
Require Import Locations.
Require Import LAsm.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import ZArith.Zwf.
Require Import LoopProof.
Require Import VCGen.
Require Import RealParams.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CommonTactic.
Require Import TacticsForTesting.
Require Import MContainerIntroCSource.
Require Import MContainerIntro.
Require Import ContainerGenSpec.
Require Import CalMCSLock.
Require Import AbstractDataType.
Require Import DeviceStateDataType.
Require Import XOmega.
Module MCONTAINERINTROCODE.
Lemma container_double_update_eq :
∀ d ac1 ac2, d {AC : ac1} {AC : ac2} = d {AC: ac2}.
Proof.
clearAll.
intros; unfold update_AC; simpl; auto.
Qed.
Section WithPrimitives.
Context `{real_params: RealParams}.
Context `{oracle_prop: MultiOracleProp}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Context `{wait_time: WaitTime}.
Let mem := mwd (cdata RData).
Context `{Hstencil: Stencil}.
Context `{make_program_ops: !MakeProgramOps Clight.function type Clight.fundef type}.
Context `{Hmake_program: !MakeProgram Clight.function type Clight.fundef type}.
Local Open Scope Z_scope.
Section CONTAINERSPLIT.
Let L: compatlayer (cdata RData) :=
container_get_nchildren ↦ gensem container_get_nchildren_intro_spec
⊕ container_get_usage ↦ gensem container_get_usage_intro_spec
⊕ container_node_init ↦ gensem container_node_init_spec
⊕ container_set_usage ↦ gensem container_set_usage_spec
⊕ container_set_nchildren ↦ gensem container_set_nchildren_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section CONTAINERSPLITBODY.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import MemWithData.
Require Import EventsX.
Require Import Globalenvs.
Require Import Locations.
Require Import LAsm.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import ZArith.Zwf.
Require Import LoopProof.
Require Import VCGen.
Require Import RealParams.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CommonTactic.
Require Import TacticsForTesting.
Require Import MContainerIntroCSource.
Require Import MContainerIntro.
Require Import ContainerGenSpec.
Require Import CalMCSLock.
Require Import AbstractDataType.
Require Import DeviceStateDataType.
Require Import XOmega.
Module MCONTAINERINTROCODE.
Lemma container_double_update_eq :
∀ d ac1 ac2, d {AC : ac1} {AC : ac2} = d {AC: ac2}.
Proof.
clearAll.
intros; unfold update_AC; simpl; auto.
Qed.
Section WithPrimitives.
Context `{real_params: RealParams}.
Context `{oracle_prop: MultiOracleProp}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Context `{wait_time: WaitTime}.
Let mem := mwd (cdata RData).
Context `{Hstencil: Stencil}.
Context `{make_program_ops: !MakeProgramOps Clight.function type Clight.fundef type}.
Context `{Hmake_program: !MakeProgram Clight.function type Clight.fundef type}.
Local Open Scope Z_scope.
Section CONTAINERSPLIT.
Let L: compatlayer (cdata RData) :=
container_get_nchildren ↦ gensem container_get_nchildren_intro_spec
⊕ container_get_usage ↦ gensem container_get_usage_intro_spec
⊕ container_node_init ↦ gensem container_node_init_spec
⊕ container_set_usage ↦ gensem container_set_usage_spec
⊕ container_set_nchildren ↦ gensem container_set_nchildren_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section CONTAINERSPLITBODY.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
container_get_nchildren
Variable bcontainer_get_nchildren: block.
Hypothesis hcontainer_get_nchildren1 : Genv.find_symbol ge container_get_nchildren = Some bcontainer_get_nchildren.
Hypothesis hcontainer_get_nchildren2 :
Genv.find_funct_ptr ge bcontainer_get_nchildren =
Some (External (EF_external container_get_nchildren
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
Hypothesis hcontainer_get_nchildren1 : Genv.find_symbol ge container_get_nchildren = Some bcontainer_get_nchildren.
Hypothesis hcontainer_get_nchildren2 :
Genv.find_funct_ptr ge bcontainer_get_nchildren =
Some (External (EF_external container_get_nchildren
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
container_get_usage
Variable bcontainer_get_usage: block.
Hypothesis hcontainer_get_usage1 : Genv.find_symbol ge container_get_usage = Some bcontainer_get_usage.
Hypothesis hcontainer_get_usage2 :
Genv.find_funct_ptr ge bcontainer_get_usage =
Some (External (EF_external container_get_usage
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
Hypothesis hcontainer_get_usage1 : Genv.find_symbol ge container_get_usage = Some bcontainer_get_usage.
Hypothesis hcontainer_get_usage2 :
Genv.find_funct_ptr ge bcontainer_get_usage =
Some (External (EF_external container_get_usage
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
container_node_init
Variable bcontainer_node_init: block.
Hypothesis hcontainer_node_init1 : Genv.find_symbol ge container_node_init = Some bcontainer_node_init.
Hypothesis hcontainer_node_init2 :
Genv.find_funct_ptr ge bcontainer_node_init =
Some (External (EF_external container_node_init
(signature_of_type (Tcons tint (Tcons tint (Tcons tint Tnil))) Tvoid cc_default))
(Tcons tint (Tcons tint (Tcons tint Tnil))) Tvoid cc_default).
Hypothesis hcontainer_node_init1 : Genv.find_symbol ge container_node_init = Some bcontainer_node_init.
Hypothesis hcontainer_node_init2 :
Genv.find_funct_ptr ge bcontainer_node_init =
Some (External (EF_external container_node_init
(signature_of_type (Tcons tint (Tcons tint (Tcons tint Tnil))) Tvoid cc_default))
(Tcons tint (Tcons tint (Tcons tint Tnil))) Tvoid cc_default).
container_set_usage
Variable bcontainer_set_usage: block.
Hypothesis hcontainer_set_usage1 : Genv.find_symbol ge container_set_usage = Some bcontainer_set_usage.
Hypothesis hcontainer_set_usage2 :
Genv.find_funct_ptr ge bcontainer_set_usage =
Some (External (EF_external container_set_usage
(signature_of_type (Tcons tint (Tcons tint Tnil)) Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
Hypothesis hcontainer_set_usage1 : Genv.find_symbol ge container_set_usage = Some bcontainer_set_usage.
Hypothesis hcontainer_set_usage2 :
Genv.find_funct_ptr ge bcontainer_set_usage =
Some (External (EF_external container_set_usage
(signature_of_type (Tcons tint (Tcons tint Tnil)) Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
container_set_nchildren
Variable bcontainer_set_nchildren: block.
Hypothesis hcontainer_set_nchildren1 : Genv.find_symbol ge container_set_nchildren = Some bcontainer_set_nchildren.
Hypothesis hcontainer_set_nchildren2 :
Genv.find_funct_ptr ge bcontainer_set_nchildren =
Some (External (EF_external container_set_nchildren
(signature_of_type (Tcons tint (Tcons tint Tnil)) Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
Lemma container_split_body_correct:
∀ m d d´ env le id quota res,
env = PTree.empty _ →
le ! _id = Some (Vint id) → le ! _quota = Some (Vint quota) →
kernel_mode d →
high_level_invariant d →
container_split_low_spec (Int.unsigned id) (Int.unsigned quota) d = Some (d´, Int.unsigned res) →
∃ le´,
exec_stmt ge env le ((m, d): mem) container_split_body E0 le´ (m, d´)
(Out_return (Some (Vint res, tint))).
Proof.
intros.
generalize max_unsigned_val; intros muval.
functional inversion H4; subst.
assert (quota_range: 0 ≤ Int.unsigned quota ≤ Int.max_unsigned).
{ clear H8 H9 H10.
fold c in _x0, _x1.
rewrite muval in _x0.
rewrite muval.
assert (0 ≤ cquota c) by omega.
revert H _x1.
revert _x0.
revert _x4.
clearAll.
intros.
omega. }
assert (cusge_range : 0 ≤ cusage c ≤ Int.max_unsigned).
{ rewrite muval.
unfold c; omega. }
assert (id_disjoint: Int.unsigned id ≠ (Int.unsigned id × 8 + 1 + Z.of_nat (length (cchildren c)))).
{ omega. }
assert (cusage_quota_range: 0 ≤ cusage (ZMap.get (Int.unsigned id) (AC d)) + Int.unsigned quota ≤
cquota (ZMap.get (Int.unsigned id) (AC d))).
{ fold c.
clear H8 H9 H10.
fold c in _x0, _x1.
rewrite muval in _x0.
assert (0 ≤ cquota c) by omega.
revert H _x1.
revert _x0.
revert _x4.
clearAll.
intros.
omega. }
unfold container_split_body; simpl; subst.
unfold child; unfold cur.
rewrite <- H6 in H4.
unfold exec_stmt.
change E0 with (E0 ** E0).
esplit.
econstructor.
{ repeat vcgen.
unfold container_get_nchildren_intro_spec.
fold c.
rewrite H14, H15, H16.
rewrite zle_lt_true; eauto.
instantiate (1:= Int.repr (Z.of_nat (length (cchildren c)))).
rewrite Int.unsigned_repr.
auto.
omega. }
change E0 with (E0 ** E0).
econstructor.
{ repeat vcgen.
unfold container_get_usage_intro_spec.
rewrite zle_lt_true; eauto.
fold c; rewrite H14, H15, H16.
unfold c.
instantiate (1 := Int.repr (cusage (ZMap.get (Int.unsigned id) (AC d)))).
rewrite Int.unsigned_repr; eauto; try omega. }
change E0 with (E0 ** E0).
econstructor.
{ repeat vcgen. }
change E0 with (E0 ** E0).
econstructor.
{ repeat vcgen.
unfold container_set_usage_spec; simpl.
rewrite zle_lt_true; auto.
rewrite zle_le_true; try omega.
rewrite H15, H16, H17; simpl.
fold c.
rewrite H14.
eauto. }
change E0 with (E0 ** E0).
econstructor.
{ repeat vcgen.
unfold container_set_nchildren_spec.
simpl.
rewrite zle_lt_true; auto.
rewrite ZMap.gss; auto.
simpl.
rewrite zlt_true; auto.
rewrite H15, H16, H17.
auto. }
change E0 with (E0 ** E0).
econstructor.
{ repeat vcgen.
unfold container_node_init_spec.
simpl.
rewrite zle_lt_true.
rewrite zle_le_true; auto.
rewrite zle_lt_true; auto.
rewrite H15, H16, H17.
eauto.
omega. }
rewrite ZMap.set2.
rewrite H14.
rewrite container_double_update_eq.
rewrite container_double_update_eq.
rewrite H6.
rewrite Int.repr_unsigned.
repeat vcgen.
Qed.
End CONTAINERSPLITBODY.
Theorem container_split_code_correct:
spec_le (container_split ↦ container_split_spec_low) (〚container_split ↦ f_container_split 〛L).
Proof.
set (L´ := L) in ×.
unfold L in ×.
fbigstep_pre L´.
assert (0 ≤ c ≤ Int.max_unsigned).
{ functional inversion H; subst.
omega. }
Require Import TacticsForTesting.
fbigsteptest (container_split_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp
b3 Hb3fs Hb3fp b4 Hb4fs Hb4fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_container_split)
(Vint i::Vint n::nil)
(create_undef_temps (fn_temps f_container_split)))) muval.
reflexivity.
omega.
omega.
intros.
destruct H3 as (le´, Hstmt).
repeat fbigstep_post.
Qed.
End CONTAINERSPLIT.
Section CONTAINERINIT.
Let L: compatlayer (cdata RData) :=
ticket_lock_init ↦ gensem ticket_lock_init0_spec
⊕ container_node_init ↦ gensem container_node_init_spec
⊕ container_set_nchildren ↦ gensem container_set_nchildren_spec
⊕ container_set_usage ↦ gensem container_set_usage_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section MCSWAITLOCKBODY.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Hypothesis hcontainer_set_nchildren1 : Genv.find_symbol ge container_set_nchildren = Some bcontainer_set_nchildren.
Hypothesis hcontainer_set_nchildren2 :
Genv.find_funct_ptr ge bcontainer_set_nchildren =
Some (External (EF_external container_set_nchildren
(signature_of_type (Tcons tint (Tcons tint Tnil)) Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
Lemma container_split_body_correct:
∀ m d d´ env le id quota res,
env = PTree.empty _ →
le ! _id = Some (Vint id) → le ! _quota = Some (Vint quota) →
kernel_mode d →
high_level_invariant d →
container_split_low_spec (Int.unsigned id) (Int.unsigned quota) d = Some (d´, Int.unsigned res) →
∃ le´,
exec_stmt ge env le ((m, d): mem) container_split_body E0 le´ (m, d´)
(Out_return (Some (Vint res, tint))).
Proof.
intros.
generalize max_unsigned_val; intros muval.
functional inversion H4; subst.
assert (quota_range: 0 ≤ Int.unsigned quota ≤ Int.max_unsigned).
{ clear H8 H9 H10.
fold c in _x0, _x1.
rewrite muval in _x0.
rewrite muval.
assert (0 ≤ cquota c) by omega.
revert H _x1.
revert _x0.
revert _x4.
clearAll.
intros.
omega. }
assert (cusge_range : 0 ≤ cusage c ≤ Int.max_unsigned).
{ rewrite muval.
unfold c; omega. }
assert (id_disjoint: Int.unsigned id ≠ (Int.unsigned id × 8 + 1 + Z.of_nat (length (cchildren c)))).
{ omega. }
assert (cusage_quota_range: 0 ≤ cusage (ZMap.get (Int.unsigned id) (AC d)) + Int.unsigned quota ≤
cquota (ZMap.get (Int.unsigned id) (AC d))).
{ fold c.
clear H8 H9 H10.
fold c in _x0, _x1.
rewrite muval in _x0.
assert (0 ≤ cquota c) by omega.
revert H _x1.
revert _x0.
revert _x4.
clearAll.
intros.
omega. }
unfold container_split_body; simpl; subst.
unfold child; unfold cur.
rewrite <- H6 in H4.
unfold exec_stmt.
change E0 with (E0 ** E0).
esplit.
econstructor.
{ repeat vcgen.
unfold container_get_nchildren_intro_spec.
fold c.
rewrite H14, H15, H16.
rewrite zle_lt_true; eauto.
instantiate (1:= Int.repr (Z.of_nat (length (cchildren c)))).
rewrite Int.unsigned_repr.
auto.
omega. }
change E0 with (E0 ** E0).
econstructor.
{ repeat vcgen.
unfold container_get_usage_intro_spec.
rewrite zle_lt_true; eauto.
fold c; rewrite H14, H15, H16.
unfold c.
instantiate (1 := Int.repr (cusage (ZMap.get (Int.unsigned id) (AC d)))).
rewrite Int.unsigned_repr; eauto; try omega. }
change E0 with (E0 ** E0).
econstructor.
{ repeat vcgen. }
change E0 with (E0 ** E0).
econstructor.
{ repeat vcgen.
unfold container_set_usage_spec; simpl.
rewrite zle_lt_true; auto.
rewrite zle_le_true; try omega.
rewrite H15, H16, H17; simpl.
fold c.
rewrite H14.
eauto. }
change E0 with (E0 ** E0).
econstructor.
{ repeat vcgen.
unfold container_set_nchildren_spec.
simpl.
rewrite zle_lt_true; auto.
rewrite ZMap.gss; auto.
simpl.
rewrite zlt_true; auto.
rewrite H15, H16, H17.
auto. }
change E0 with (E0 ** E0).
econstructor.
{ repeat vcgen.
unfold container_node_init_spec.
simpl.
rewrite zle_lt_true.
rewrite zle_le_true; auto.
rewrite zle_lt_true; auto.
rewrite H15, H16, H17.
eauto.
omega. }
rewrite ZMap.set2.
rewrite H14.
rewrite container_double_update_eq.
rewrite container_double_update_eq.
rewrite H6.
rewrite Int.repr_unsigned.
repeat vcgen.
Qed.
End CONTAINERSPLITBODY.
Theorem container_split_code_correct:
spec_le (container_split ↦ container_split_spec_low) (〚container_split ↦ f_container_split 〛L).
Proof.
set (L´ := L) in ×.
unfold L in ×.
fbigstep_pre L´.
assert (0 ≤ c ≤ Int.max_unsigned).
{ functional inversion H; subst.
omega. }
Require Import TacticsForTesting.
fbigsteptest (container_split_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp
b3 Hb3fs Hb3fp b4 Hb4fs Hb4fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_container_split)
(Vint i::Vint n::nil)
(create_undef_temps (fn_temps f_container_split)))) muval.
reflexivity.
omega.
omega.
intros.
destruct H3 as (le´, Hstmt).
repeat fbigstep_post.
Qed.
End CONTAINERSPLIT.
Section CONTAINERINIT.
Let L: compatlayer (cdata RData) :=
ticket_lock_init ↦ gensem ticket_lock_init0_spec
⊕ container_node_init ↦ gensem container_node_init_spec
⊕ container_set_nchildren ↦ gensem container_set_nchildren_spec
⊕ container_set_usage ↦ gensem container_set_usage_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section MCSWAITLOCKBODY.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
ticket_lock_init
Variable bticket_lock_init: block.
Hypothesis hticket_lock_init1 : Genv.find_symbol ge ticket_lock_init = Some bticket_lock_init.
Hypothesis hticket_lock_init2 :
Genv.find_funct_ptr ge bticket_lock_init =
Some (External (EF_external ticket_lock_init
(signature_of_type (Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
Hypothesis hticket_lock_init1 : Genv.find_symbol ge ticket_lock_init = Some bticket_lock_init.
Hypothesis hticket_lock_init2 :
Genv.find_funct_ptr ge bticket_lock_init =
Some (External (EF_external ticket_lock_init
(signature_of_type (Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
container_node_init
Variable bcontainer_node_init: block.
Hypothesis hcontainer_node_init1 : Genv.find_symbol ge container_node_init = Some bcontainer_node_init.
Hypothesis hcontainer_node_init2 :
Genv.find_funct_ptr ge bcontainer_node_init =
Some (External (EF_external container_node_init
(signature_of_type (Tcons tint (Tcons tint (Tcons tint Tnil))) Tvoid cc_default))
(Tcons tint (Tcons tint (Tcons tint Tnil))) Tvoid cc_default).
Hypothesis hcontainer_node_init1 : Genv.find_symbol ge container_node_init = Some bcontainer_node_init.
Hypothesis hcontainer_node_init2 :
Genv.find_funct_ptr ge bcontainer_node_init =
Some (External (EF_external container_node_init
(signature_of_type (Tcons tint (Tcons tint (Tcons tint Tnil))) Tvoid cc_default))
(Tcons tint (Tcons tint (Tcons tint Tnil))) Tvoid cc_default).
container_set_nchildren
Variable bcontainer_set_nchildren: block.
Hypothesis hcontainer_set_nchildren1 : Genv.find_symbol ge container_set_nchildren = Some bcontainer_set_nchildren.
Hypothesis hcontainer_set_nchildren2 :
Genv.find_funct_ptr ge bcontainer_set_nchildren =
Some (External (EF_external container_set_nchildren
(signature_of_type (Tcons tint (Tcons tint Tnil)) Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
Hypothesis hcontainer_set_nchildren1 : Genv.find_symbol ge container_set_nchildren = Some bcontainer_set_nchildren.
Hypothesis hcontainer_set_nchildren2 :
Genv.find_funct_ptr ge bcontainer_set_nchildren =
Some (External (EF_external container_set_nchildren
(signature_of_type (Tcons tint (Tcons tint Tnil)) Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
container_set_usage
Variable bcontainer_set_usage: block.
Hypothesis hcontainer_set_usage1 : Genv.find_symbol ge container_set_usage = Some bcontainer_set_usage.
Hypothesis hcontainer_set_usage2 :
Genv.find_funct_ptr ge bcontainer_set_usage =
Some (External (EF_external container_set_usage
(signature_of_type (Tcons tint (Tcons tint Tnil)) Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
Lemma container_init_state_eq:
∀ d´ multi_val lock_val AC_val,
(((d´ {init : true}) {multi_log : multi_val}) {lock : lock_val}) {AC : AC_val} =
(((d´ {AC: AC_val}) {init : true}) {multi_log : multi_val}) {lock :lock_val}.
Proof.
clearAll.
simpl; intros.
eauto.
Qed.
Lemma container_init_body_correct:
∀ m d d´ env le mbi_addr,
env = PTree.empty _ →
PTree.get _mbi_addr le = Some (Vint mbi_addr) →
kernel_mode d →
high_level_invariant d →
container_init_spec (Int.unsigned mbi_addr) d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) container_init_body E0 le´ (m, d´) Out_normal.
Proof.
intros.
generalize max_unsigned_val; intros muval.
functional inversion H3; subst.
unfold container_init_body.
esplit.
Opaque CalTicketLock.real_lock IoApicMaxIntr CalTicketLock.real_multi_log real_vmxinfo ioapic_init_aux
LapicMaxLvt real_vmxinfo.
unfold exec_stmt.
replace E0 with (E0 ** E0); auto.
econstructor.
-
instantiate (1:= (m, ((((((((d { ioapic / s : ioapic_init_aux (s (ioapic d))
(Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1))})
{ lapic : (((mkLApicData {| LapicEsr := 0;
LapicEoi := NoIntr;
LapicMaxLvt := LapicMaxLvt (s (lapic d));
LapicEnable := true;
LapicSpurious := 39;
LapicLint0Mask := true;
LapicLint1Mask := true;
LapicPcIntMask := true;
LapicLdr := 0;
LapicErrorIrq := 50;
LapicEsrClrPen := false;
LapicTpr := 0 |})
{ l1 : l1 (lapic d)}) { l2 : l2 (lapic d)}) { l3 : l3 (lapic d)}})
{ ioapic : ((ioapic d) { s : ioapic_init_aux
(s (ioapic d))
(Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1))})
{ s : (ioapic_init_aux (s (ioapic d))
(Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1)))
{ CurrentIrq : None}}}) {MM : real_mm}) {MMSize : real_size})
{vmxinfo : real_vmxinfo}) {init : true})
{multi_log : CalTicketLock.real_multi_log (multi_log d)})
{lock : CalTicketLock.real_lock (lock d)})).
econstructor.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
econstructor.
vcgen.
unfold ticket_lock_init0_spec.
rewrite H5, H6, H7, H8, H9, H10, H11.
simpl.
reflexivity.
- assert (init_container_inv : AC d = ZMap.init Container_unused).
{ inv H2.
eapply init_false_empty_container; eauto. }
repeat vcgen.
{
unfold container_node_init_spec.
rewrite zle_lt_true; try omega.
rewrite muval.
rewrite zle_lt_true; try omega.
rewrite zle_le_true; try omega.
simpl.
rewrite H7, H8.
reflexivity. }
{ unfold container_set_usage_spec.
simpl.
rewrite ZMap.gss.
simpl.
rewrite H7, H8.
rewrite container_double_update_eq.
rewrite ZMap.set2.
eauto. }
{ unfold container_set_nchildren_spec.
simpl.
rewrite ZMap.gss.
simpl.
rewrite H7, H8.
rewrite container_double_update_eq.
rewrite ZMap.set2.
eauto. }
{ unfold container_set_nchildren_spec.
simpl.
rewrite ZMap.gss.
simpl.
rewrite H7, H8.
rewrite container_double_update_eq.
rewrite ZMap.set2.
eauto. }
{ unfold container_set_nchildren_spec.
simpl.
rewrite ZMap.gss.
simpl.
rewrite H7, H8.
rewrite container_double_update_eq.
rewrite ZMap.set2.
eauto. }
{ unfold container_set_nchildren_spec.
simpl.
rewrite ZMap.gss.
simpl.
rewrite H7, H8.
rewrite container_double_update_eq.
rewrite ZMap.set2.
eauto. }
{ unfold container_set_nchildren_spec.
simpl.
rewrite ZMap.gss.
simpl.
rewrite H7, H8.
rewrite container_double_update_eq.
rewrite ZMap.set2.
eauto. }
{ unfold container_set_nchildren_spec.
simpl.
rewrite ZMap.gss.
simpl.
rewrite H7, H8.
rewrite container_double_update_eq.
rewrite ZMap.set2.
eauto. }
{ unfold container_set_nchildren_spec.
simpl.
rewrite ZMap.gss.
simpl.
rewrite H7, H8.
rewrite container_double_update_eq.
rewrite ZMap.set2.
eauto. }
{ unfold container_set_nchildren_spec.
simpl.
rewrite ZMap.gss.
simpl.
rewrite H7, H8.
rewrite container_double_update_eq.
rewrite ZMap.set2.
eauto. }
{
unfold container_node_init_spec.
rewrite zle_lt_true; try omega.
rewrite muval.
rewrite zle_lt_true; try omega.
rewrite zle_le_true; try omega.
simpl.
rewrite H7, H8.
reflexivity.
clearAll.
xomega. }
{
rewrite container_double_update_eq.
repeat vcgen.
unfold container_node_init_spec.
rewrite zle_lt_true; try omega.
rewrite muval.
rewrite zle_lt_true; try omega.
rewrite zle_le_true; try omega.
simpl.
rewrite H7, H8.
reflexivity.
clearAll.
xomega. }
{
rewrite container_double_update_eq.
repeat vcgen.
unfold container_node_init_spec.
rewrite zle_lt_true; try omega.
rewrite muval.
rewrite zle_lt_true; try omega.
rewrite zle_le_true; try omega.
simpl.
rewrite H7, H8.
reflexivity.
clearAll.
xomega. }
{
rewrite container_double_update_eq.
repeat vcgen.
unfold container_node_init_spec.
rewrite zle_lt_true; try omega.
rewrite muval.
rewrite zle_lt_true; try omega.
rewrite zle_le_true; try omega.
simpl.
rewrite H7, H8.
reflexivity.
clearAll.
xomega. }
{
rewrite container_double_update_eq.
repeat vcgen.
unfold container_node_init_spec.
rewrite zle_lt_true; try omega.
rewrite muval.
rewrite zle_lt_true; try omega.
rewrite zle_le_true; try omega.
simpl.
rewrite H7, H8.
reflexivity.
clearAll.
xomega. }
{
rewrite container_double_update_eq.
repeat vcgen.
unfold container_node_init_spec.
rewrite zle_lt_true; try omega.
rewrite muval.
rewrite zle_lt_true; try omega.
rewrite zle_le_true; try omega.
simpl.
rewrite H7, H8.
reflexivity.
clearAll.
xomega. }
{
rewrite container_double_update_eq.
repeat vcgen.
unfold container_node_init_spec.
rewrite zle_lt_true; try omega.
rewrite muval.
rewrite zle_lt_true; try omega.
rewrite zle_le_true; try omega.
simpl.
rewrite H7, H8.
reflexivity.
clearAll.
xomega. }
{
rewrite container_double_update_eq.
repeat vcgen.
unfold container_node_init_spec.
rewrite zle_lt_true; try omega.
rewrite muval.
rewrite zle_lt_true; try omega.
rewrite zle_le_true; try omega.
simpl.
rewrite H7, H8.
unfold AC_init.
unfold init_real_container.
unfold init_container_children; simpl.
rewrite init_container_inv.
rewrite container_double_update_eq.
fold init_container.
set (d´ := ((((((d { ioapic / s : ioapic_init_aux (s (ioapic d))
(Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1))})
{ lapic : (((mkLApicData {| LapicEsr := 0;
LapicEoi := NoIntr;
LapicMaxLvt := LapicMaxLvt (s (lapic d));
LapicEnable := true;
LapicSpurious := 39;
LapicLint0Mask := true;
LapicLint1Mask := true;
LapicPcIntMask := true;
LapicLdr := 0;
LapicErrorIrq := 50;
LapicEsrClrPen := false;
LapicTpr := 0 |})
{ l1 : l1 (lapic d)}) { l2 : l2 (lapic d)}) { l3 : l3 (lapic d)}})
{ ioapic : ((ioapic d) { s : ioapic_init_aux
(s (ioapic d))
(Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1))})
{ s : (ioapic_init_aux (s (ioapic d))
(Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1)))
{ CurrentIrq : None}}}) {MM : real_mm}) {MMSize : real_size})
{vmxinfo : real_vmxinfo})).
rewrite container_init_state_eq.
reflexivity.
clearAll.
xomega. }
Qed.
End MCSWAITLOCKBODY.
Theorem container_init_code_correct:
spec_le (container_init ↦ container_init_spec_low) (〚container_init ↦ f_container_init 〛L).
Proof.
set (L´ := L) in ×.
unfold L in ×.
fbigstep_pre L´.
fbigstep (container_init_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp
b3 Hb3fs Hb3fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_container_init)
(Vint mbi_adr::nil)
(create_undef_temps (fn_temps f_container_init)))) muval.
Qed.
End CONTAINERINIT.
End WithPrimitives.
End MCONTAINERINTROCODE.
Hypothesis hcontainer_set_usage1 : Genv.find_symbol ge container_set_usage = Some bcontainer_set_usage.
Hypothesis hcontainer_set_usage2 :
Genv.find_funct_ptr ge bcontainer_set_usage =
Some (External (EF_external container_set_usage
(signature_of_type (Tcons tint (Tcons tint Tnil)) Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
Lemma container_init_state_eq:
∀ d´ multi_val lock_val AC_val,
(((d´ {init : true}) {multi_log : multi_val}) {lock : lock_val}) {AC : AC_val} =
(((d´ {AC: AC_val}) {init : true}) {multi_log : multi_val}) {lock :lock_val}.
Proof.
clearAll.
simpl; intros.
eauto.
Qed.
Lemma container_init_body_correct:
∀ m d d´ env le mbi_addr,
env = PTree.empty _ →
PTree.get _mbi_addr le = Some (Vint mbi_addr) →
kernel_mode d →
high_level_invariant d →
container_init_spec (Int.unsigned mbi_addr) d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) container_init_body E0 le´ (m, d´) Out_normal.
Proof.
intros.
generalize max_unsigned_val; intros muval.
functional inversion H3; subst.
unfold container_init_body.
esplit.
Opaque CalTicketLock.real_lock IoApicMaxIntr CalTicketLock.real_multi_log real_vmxinfo ioapic_init_aux
LapicMaxLvt real_vmxinfo.
unfold exec_stmt.
replace E0 with (E0 ** E0); auto.
econstructor.
-
instantiate (1:= (m, ((((((((d { ioapic / s : ioapic_init_aux (s (ioapic d))
(Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1))})
{ lapic : (((mkLApicData {| LapicEsr := 0;
LapicEoi := NoIntr;
LapicMaxLvt := LapicMaxLvt (s (lapic d));
LapicEnable := true;
LapicSpurious := 39;
LapicLint0Mask := true;
LapicLint1Mask := true;
LapicPcIntMask := true;
LapicLdr := 0;
LapicErrorIrq := 50;
LapicEsrClrPen := false;
LapicTpr := 0 |})
{ l1 : l1 (lapic d)}) { l2 : l2 (lapic d)}) { l3 : l3 (lapic d)}})
{ ioapic : ((ioapic d) { s : ioapic_init_aux
(s (ioapic d))
(Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1))})
{ s : (ioapic_init_aux (s (ioapic d))
(Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1)))
{ CurrentIrq : None}}}) {MM : real_mm}) {MMSize : real_size})
{vmxinfo : real_vmxinfo}) {init : true})
{multi_log : CalTicketLock.real_multi_log (multi_log d)})
{lock : CalTicketLock.real_lock (lock d)})).
econstructor.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
econstructor.
vcgen.
unfold ticket_lock_init0_spec.
rewrite H5, H6, H7, H8, H9, H10, H11.
simpl.
reflexivity.
- assert (init_container_inv : AC d = ZMap.init Container_unused).
{ inv H2.
eapply init_false_empty_container; eauto. }
repeat vcgen.
{
unfold container_node_init_spec.
rewrite zle_lt_true; try omega.
rewrite muval.
rewrite zle_lt_true; try omega.
rewrite zle_le_true; try omega.
simpl.
rewrite H7, H8.
reflexivity. }
{ unfold container_set_usage_spec.
simpl.
rewrite ZMap.gss.
simpl.
rewrite H7, H8.
rewrite container_double_update_eq.
rewrite ZMap.set2.
eauto. }
{ unfold container_set_nchildren_spec.
simpl.
rewrite ZMap.gss.
simpl.
rewrite H7, H8.
rewrite container_double_update_eq.
rewrite ZMap.set2.
eauto. }
{ unfold container_set_nchildren_spec.
simpl.
rewrite ZMap.gss.
simpl.
rewrite H7, H8.
rewrite container_double_update_eq.
rewrite ZMap.set2.
eauto. }
{ unfold container_set_nchildren_spec.
simpl.
rewrite ZMap.gss.
simpl.
rewrite H7, H8.
rewrite container_double_update_eq.
rewrite ZMap.set2.
eauto. }
{ unfold container_set_nchildren_spec.
simpl.
rewrite ZMap.gss.
simpl.
rewrite H7, H8.
rewrite container_double_update_eq.
rewrite ZMap.set2.
eauto. }
{ unfold container_set_nchildren_spec.
simpl.
rewrite ZMap.gss.
simpl.
rewrite H7, H8.
rewrite container_double_update_eq.
rewrite ZMap.set2.
eauto. }
{ unfold container_set_nchildren_spec.
simpl.
rewrite ZMap.gss.
simpl.
rewrite H7, H8.
rewrite container_double_update_eq.
rewrite ZMap.set2.
eauto. }
{ unfold container_set_nchildren_spec.
simpl.
rewrite ZMap.gss.
simpl.
rewrite H7, H8.
rewrite container_double_update_eq.
rewrite ZMap.set2.
eauto. }
{ unfold container_set_nchildren_spec.
simpl.
rewrite ZMap.gss.
simpl.
rewrite H7, H8.
rewrite container_double_update_eq.
rewrite ZMap.set2.
eauto. }
{
unfold container_node_init_spec.
rewrite zle_lt_true; try omega.
rewrite muval.
rewrite zle_lt_true; try omega.
rewrite zle_le_true; try omega.
simpl.
rewrite H7, H8.
reflexivity.
clearAll.
xomega. }
{
rewrite container_double_update_eq.
repeat vcgen.
unfold container_node_init_spec.
rewrite zle_lt_true; try omega.
rewrite muval.
rewrite zle_lt_true; try omega.
rewrite zle_le_true; try omega.
simpl.
rewrite H7, H8.
reflexivity.
clearAll.
xomega. }
{
rewrite container_double_update_eq.
repeat vcgen.
unfold container_node_init_spec.
rewrite zle_lt_true; try omega.
rewrite muval.
rewrite zle_lt_true; try omega.
rewrite zle_le_true; try omega.
simpl.
rewrite H7, H8.
reflexivity.
clearAll.
xomega. }
{
rewrite container_double_update_eq.
repeat vcgen.
unfold container_node_init_spec.
rewrite zle_lt_true; try omega.
rewrite muval.
rewrite zle_lt_true; try omega.
rewrite zle_le_true; try omega.
simpl.
rewrite H7, H8.
reflexivity.
clearAll.
xomega. }
{
rewrite container_double_update_eq.
repeat vcgen.
unfold container_node_init_spec.
rewrite zle_lt_true; try omega.
rewrite muval.
rewrite zle_lt_true; try omega.
rewrite zle_le_true; try omega.
simpl.
rewrite H7, H8.
reflexivity.
clearAll.
xomega. }
{
rewrite container_double_update_eq.
repeat vcgen.
unfold container_node_init_spec.
rewrite zle_lt_true; try omega.
rewrite muval.
rewrite zle_lt_true; try omega.
rewrite zle_le_true; try omega.
simpl.
rewrite H7, H8.
reflexivity.
clearAll.
xomega. }
{
rewrite container_double_update_eq.
repeat vcgen.
unfold container_node_init_spec.
rewrite zle_lt_true; try omega.
rewrite muval.
rewrite zle_lt_true; try omega.
rewrite zle_le_true; try omega.
simpl.
rewrite H7, H8.
reflexivity.
clearAll.
xomega. }
{
rewrite container_double_update_eq.
repeat vcgen.
unfold container_node_init_spec.
rewrite zle_lt_true; try omega.
rewrite muval.
rewrite zle_lt_true; try omega.
rewrite zle_le_true; try omega.
simpl.
rewrite H7, H8.
unfold AC_init.
unfold init_real_container.
unfold init_container_children; simpl.
rewrite init_container_inv.
rewrite container_double_update_eq.
fold init_container.
set (d´ := ((((((d { ioapic / s : ioapic_init_aux (s (ioapic d))
(Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1))})
{ lapic : (((mkLApicData {| LapicEsr := 0;
LapicEoi := NoIntr;
LapicMaxLvt := LapicMaxLvt (s (lapic d));
LapicEnable := true;
LapicSpurious := 39;
LapicLint0Mask := true;
LapicLint1Mask := true;
LapicPcIntMask := true;
LapicLdr := 0;
LapicErrorIrq := 50;
LapicEsrClrPen := false;
LapicTpr := 0 |})
{ l1 : l1 (lapic d)}) { l2 : l2 (lapic d)}) { l3 : l3 (lapic d)}})
{ ioapic : ((ioapic d) { s : ioapic_init_aux
(s (ioapic d))
(Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1))})
{ s : (ioapic_init_aux (s (ioapic d))
(Z.to_nat (IoApicMaxIntr (s (ioapic d)) + 1 - 1)))
{ CurrentIrq : None}}}) {MM : real_mm}) {MMSize : real_size})
{vmxinfo : real_vmxinfo})).
rewrite container_init_state_eq.
reflexivity.
clearAll.
xomega. }
Qed.
End MCSWAITLOCKBODY.
Theorem container_init_code_correct:
spec_le (container_init ↦ container_init_spec_low) (〚container_init ↦ f_container_init 〛L).
Proof.
set (L´ := L) in ×.
unfold L in ×.
fbigstep_pre L´.
fbigstep (container_init_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp
b3 Hb3fs Hb3fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_container_init)
(Vint mbi_adr::nil)
(create_undef_temps (fn_temps f_container_init)))) muval.
Qed.
End CONTAINERINIT.
End WithPrimitives.
End MCONTAINERINTROCODE.