Library mcertikos.mcslock.MMCSLockIntroCode
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 MMCSLockIntroCSource.
Require Import MMCSLockIntro.
Require Import MCSLockAbsIntroGenSpec.
Require Import CalMCSLock.
Require Import AbstractDataType.
Lemma multi_log_double_update:
∀ d ml1 ml2,
(d {multi_log: ml1}) {multi_log: ml2} = d {multi_log: ml2}.
Proof.
intros.
unfold update_multi_log; simpl.
reflexivity.
Qed.
Lemma ikern_remain :
∀ d ml, ikern d = ikern (d {multi_log: ml}).
Proof. intros; simpl; auto. Qed.
Lemma ihost_remain:
∀ d ml, ihost d = ihost (d {multi_log: ml}).
Proof. intros; simpl; auto. Qed.
Module MMCSLOCKINTROCODE.
Section WithPrimitives.
Context `{real_params: RealParams}.
Context `{mcs_oracle_prop: MCSOracleProp}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
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 MCSGETNEXT.
Let L: compatlayer (cdata RData) :=
mcs_log ↦ gensem mcs_log_spec
⊕ mcs_GET_NEXT ↦ gensem mcs_GET_NEXT_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section MCSGETNEXTBODY.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable bmcs_GET_NEXT: block.
Hypothesis hmcs_GET_NEXT1 : Genv.find_symbol ge mcs_GET_NEXT = Some bmcs_GET_NEXT.
Hypothesis hmcs_GET_NEXT2 : Genv.find_funct_ptr ge bmcs_GET_NEXT =
Some (External (EF_external mcs_GET_NEXT
(signature_of_type (Tcons tint (Tcons tint Tnil))
tint cc_default))
(Tcons tint (Tcons tint Tnil)) tint cc_default).
Variable bmcs_log: block.
Hypothesis hmcs_log1 : Genv.find_symbol ge mcs_log = Some bmcs_log.
Hypothesis hmcs_log2 : Genv.find_funct_ptr ge bmcs_log =
Some (External (EF_external mcs_log
(signature_of_type (Tcons tint (Tcons tint Tnil))
Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
Lemma mcs_get_next_body_correct: ∀ m d d´ env le lock_index cpuid next,
env = PTree.empty _ →
PTree.get _lock_index le = Some (Vint lock_index) →
PTree.get _cpuid le = Some (Vint cpuid) →
mcs_get_next_spec (Int.unsigned lock_index) (Int.unsigned cpuid) d = Some (d´, (Int.unsigned next)) →
kernel_mode d →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_mcs_get_next_body E0 le´ (m, d´)
(Out_return (Some (Vint next, tint))).
Proof.
intros.
functional inversion H2; subst.
unfold f_mcs_get_next_body; subst.
esplit; repeat vcgen.
- unfold mcs_log_spec.
rewrite H7, H8, H9, H10, H11.
unfold l´ in H12.
unfold l1 in H12.
unfold to in H12.
Transparent CalMCSLock.
simpl in H12.
subdestruct ; try (inv H12; fail).
reflexivity.
- unfold mcs_GET_NEXT_spec; repeat vcgen.
rewrite <- ikern_remain.
rewrite <- ihost_remain.
rewrite H7, H8, H9, H10.
simpl; rewrite ZMap.gss.
unfold l´ in H12.
unfold l1 in H12.
unfold to in H12.
Transparent CalMCSLock.
simpl in H12.
subdestruct ; try (inv H12; fail).
inv H12.
rewrite H13.
destruct (ZMap.get (Int.unsigned cpuid) node_pool).
inversion H13; subst.
rewrite multi_log_double_update.
rewrite ZMap.set2.
repeat vcgen.
Qed.
End MCSGETNEXTBODY.
Theorem mcs_get_next_code_correct:
spec_le (mcs_get_next ↦ mcs_get_next_spec_low) (〚mcs_get_next ↦ f_mcs_get_next 〛L).
Proof.
fbigstep_pre L.
fbigstep (mcs_get_next_body_correct s (Genv.globalenv p) makeglobalenv
b1 Hb1fs Hb1fp
b0 Hb0fs Hb0fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_mcs_get_next)
(Vint lock_index::Vint cpuid::nil)
(create_undef_temps (fn_temps f_mcs_get_next)))) muval.
Qed.
End MCSGETNEXT.
Section MCSSETNEXT.
Let L: compatlayer (cdata RData) :=
mcs_log ↦ gensem mcs_log_spec
⊕ mcs_SET_NEXT ↦ gensem mcs_SET_NEXT_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section MCSSETNEXTBODY.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable bmcs_SET_NEXT: block.
Hypothesis hmcs_SET_NEXT1 : Genv.find_symbol ge mcs_SET_NEXT = Some bmcs_SET_NEXT.
Hypothesis hmcs_SET_NEXT2 : Genv.find_funct_ptr ge bmcs_SET_NEXT =
Some (External (EF_external mcs_SET_NEXT
(signature_of_type
(Tcons tint (Tcons tint (Tcons tint Tnil)))
Tvoid cc_default))
(Tcons tint (Tcons tint (Tcons tint Tnil))) Tvoid cc_default).
Variable bmcs_log: block.
Hypothesis hmcs_log1 : Genv.find_symbol ge mcs_log = Some bmcs_log.
Hypothesis hmcs_log2 : Genv.find_funct_ptr ge bmcs_log =
Some (External (EF_external mcs_log
(signature_of_type (Tcons tint (Tcons tint Tnil))
Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
Lemma mcs_set_next_body_correct: ∀ m d d´ env le lock_index cpuid prev_id,
env = PTree.empty _ →
PTree.get _lock_index le = Some (Vint lock_index) →
PTree.get _cpuid le = Some (Vint cpuid) →
PTree.get _prev_id le = Some (Vint prev_id) →
mcs_set_next_spec (Int.unsigned lock_index) (Int.unsigned cpuid) (Int.unsigned prev_id) d
= Some d´ →
kernel_mode d →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_mcs_set_next_body E0 le´ (m, d´) Out_normal.
Proof.
intros.
functional inversion H3; subst.
unfold f_mcs_set_next_body; subst.
esplit; repeat vcgen.
- unfold mcs_log_spec.
rewrite H7, H8, H9, H10, H12.
unfold l1 in H13.
unfold to in H13.
rewrite H13.
reflexivity.
- unfold mcs_SET_NEXT_spec; repeat vcgen.
rewrite <- ikern_remain.
rewrite <- ihost_remain.
rewrite H7, H8, H9, H10, H11.
simpl; rewrite ZMap.gss.
rewrite multi_log_double_update.
simpl; rewrite ZMap.set2.
unfold l´; unfold l1; unfold to.
reflexivity.
Qed.
End MCSSETNEXTBODY.
Theorem mcs_set_next_code_correct:
spec_le (mcs_set_next ↦ mcs_set_next_spec_low) (〚mcs_set_next ↦ f_mcs_set_next 〛L).
Proof.
fbigstep_pre L.
fbigstep (mcs_set_next_body_correct s (Genv.globalenv p) makeglobalenv
b1 Hb1fs Hb1fp
b0 Hb0fs Hb0fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_mcs_set_next)
(Vint lock_index::Vint cpuid::Vint prev_id::nil)
(create_undef_temps (fn_temps f_mcs_set_next)))) muval.
Qed.
End MCSSETNEXT.
Section MCSGETBUSY.
Let L: compatlayer (cdata RData) :=
mcs_log ↦ gensem mcs_log_spec
⊕ mcs_GET_BUSY ↦ gensem mcs_GET_BUSY_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section MCSGETBUSYBODY.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable bmcs_GET_BUSY: block.
Hypothesis hmcs_GET_BUSY1 : Genv.find_symbol ge mcs_GET_BUSY = Some bmcs_GET_BUSY.
Hypothesis hmcs_GET_BUSY2 : Genv.find_funct_ptr ge bmcs_GET_BUSY =
Some (External (EF_external mcs_GET_BUSY
(signature_of_type (Tcons tint (Tcons tint Tnil))
tint cc_default))
(Tcons tint (Tcons tint Tnil)) tint cc_default).
Variable bmcs_log: block.
Hypothesis hmcs_log1 : Genv.find_symbol ge mcs_log = Some bmcs_log.
Hypothesis hmcs_log2 : Genv.find_funct_ptr ge bmcs_log =
Some (External (EF_external mcs_log
(signature_of_type (Tcons tint (Tcons tint Tnil))
Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
Lemma mcs_get_busy_body_correct: ∀ m d d´ env le lock_index cpuid busy,
env = PTree.empty _ →
PTree.get _lock_index le = Some (Vint lock_index) →
PTree.get _cpuid le = Some (Vint cpuid) →
mcs_get_busy_spec (Int.unsigned lock_index) (Int.unsigned cpuid) d = Some (d´, (Int.unsigned busy)) →
kernel_mode d →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_mcs_get_busy_body E0 le´ (m, d´)
(Out_return (Some (Vint busy, tint))).
Proof.
intros.
functional inversion H2; subst.
- unfold f_mcs_get_busy_body; subst.
esplit; repeat vcgen.
+ unfold mcs_log_spec.
rewrite H7, H8, H9, H10, H11.
unfold l´ in H12.
unfold l1 in H12.
unfold to in H12.
rewrite H12.
reflexivity.
+ unfold mcs_GET_BUSY_spec; repeat vcgen.
rewrite <- ikern_remain.
rewrite <- ihost_remain.
rewrite H7, H8, H9, H10.
simpl; rewrite ZMap.gss.
unfold l´ in H12.
unfold l1 in H12.
unfold to in H12.
rewrite H12.
rewrite H13.
destruct (ZMap.get (Int.unsigned cpuid) node_pool).
inversion H13; subst.
rewrite multi_log_double_update.
rewrite ZMap.set2.
rewrite <- H6.
reflexivity.
- unfold f_mcs_get_busy_body; subst.
esplit; repeat vcgen.
+ unfold mcs_log_spec.
rewrite H7, H8, H9, H10, H11.
unfold l´ in H12.
unfold l1 in H12.
unfold to in H12.
rewrite H12.
reflexivity.
+ unfold mcs_GET_BUSY_spec; repeat vcgen.
rewrite <- ikern_remain.
rewrite <- ihost_remain.
rewrite H7, H8, H9, H10.
simpl; rewrite ZMap.gss.
unfold l´ in H12.
unfold l1 in H12.
unfold to in H12.
rewrite H12.
rewrite H13.
destruct (ZMap.get (Int.unsigned cpuid) node_pool).
inv H13.
rewrite multi_log_double_update.
rewrite ZMap.set2.
rewrite <- H6.
unfold l´; unfold l1; unfold to.
reflexivity.
Qed.
End MCSGETBUSYBODY.
Theorem mcs_get_busy_code_correct:
spec_le (mcs_get_busy ↦ mcs_get_busy_spec_low) (〚mcs_get_busy ↦ f_mcs_get_busy 〛L).
Proof.
fbigstep_pre L.
fbigstep (mcs_get_busy_body_correct s (Genv.globalenv p) makeglobalenv
b1 Hb1fs Hb1fp
b0 Hb0fs Hb0fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_mcs_get_busy)
(Vint lock_index::Vint cpuid::nil)
(create_undef_temps (fn_temps f_mcs_get_busy)))) muval.
Qed.
End MCSGETBUSY.
Section MCSSETBUSY.
Let L: compatlayer (cdata RData) :=
mcs_log ↦ gensem mcs_log_spec
⊕ mcs_SET_BUSY ↦ gensem mcs_SET_BUSY_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section MCSSETBUSYBODY.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable bmcs_SET_BUSY: block.
Hypothesis hmcs_SET_BUSY1 : Genv.find_symbol ge mcs_SET_BUSY = Some bmcs_SET_BUSY.
Hypothesis hmcs_SET_BUSY2 : Genv.find_funct_ptr ge bmcs_SET_BUSY =
Some (External (EF_external mcs_SET_BUSY
(signature_of_type
(Tcons tint (Tcons tint Tnil))
Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
Variable bmcs_log: block.
Hypothesis hmcs_log1 : Genv.find_symbol ge mcs_log = Some bmcs_log.
Hypothesis hmcs_log2 : Genv.find_funct_ptr ge bmcs_log =
Some (External (EF_external mcs_log
(signature_of_type (Tcons tint (Tcons tint Tnil))
Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
Lemma mcs_set_busy_body_correct: ∀ m d d´ env le lock_index cpuid,
env = PTree.empty _ →
PTree.get _lock_index le = Some (Vint lock_index) →
PTree.get _cpuid le = Some (Vint cpuid) →
mcs_set_busy_spec (Int.unsigned lock_index) (Int.unsigned cpuid) d = Some d´ →
kernel_mode d →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_mcs_set_busy_body E0 le´ (m, d´) Out_normal.
Proof.
intros.
functional inversion H2; subst.
unfold f_mcs_set_busy_body; subst.
esplit; repeat vcgen.
- unfold mcs_log_spec.
rewrite H6, H7, H8, H9, H10.
unfold l1 in H11.
unfold to in H11.
rewrite H11.
reflexivity.
- unfold mcs_SET_BUSY_spec; repeat vcgen.
rewrite <- ikern_remain.
rewrite <- ihost_remain.
rewrite H6, H7, H8, H9.
simpl; rewrite ZMap.gss.
rewrite multi_log_double_update.
simpl; rewrite ZMap.set2.
unfold l1 in H11; unfold to in H11.
rewrite H11; unfold l´; unfold l1; unfold to.
rewrite H12.
rewrite zle_lt_true; try omega.
reflexivity.
Qed.
End MCSSETBUSYBODY.
Theorem mcs_set_busy_code_correct:
spec_le (mcs_set_busy ↦ mcs_set_busy_spec_low) (〚mcs_set_busy ↦ f_mcs_set_busy 〛L).
Proof.
fbigstep_pre L.
fbigstep (mcs_set_busy_body_correct s (Genv.globalenv p) makeglobalenv
b1 Hb1fs Hb1fp
b0 Hb0fs Hb0fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_mcs_set_busy)
(Vint lock_index::Vint cpuid::nil)
(create_undef_temps (fn_temps f_mcs_set_busy)))) muval.
Qed.
End MCSSETBUSY.
Section MCSSWAPTAIL.
Let L: compatlayer (cdata RData) :=
mcs_log ↦ gensem mcs_log_spec
⊕ mcs_SWAP_TAIL ↦ gensem mcs_SWAP_TAIL_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section MCSSWAPTAILBODY.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable bmcs_SWAP_TAIL: block.
Hypothesis hmcs_SWAP_TAIL1 : Genv.find_symbol ge mcs_SWAP_TAIL = Some bmcs_SWAP_TAIL.
Hypothesis hmcs_SWAP_TAIL2 : Genv.find_funct_ptr ge bmcs_SWAP_TAIL =
Some (External (EF_external mcs_SWAP_TAIL
(signature_of_type (Tcons tint (Tcons tint (Tcons tint Tnil)))
tint cc_default))
(Tcons tint (Tcons tint (Tcons tint Tnil))) tint cc_default).
Variable bmcs_log: block.
Hypothesis hmcs_log1 : Genv.find_symbol ge mcs_log = Some bmcs_log.
Hypothesis hmcs_log2 : Genv.find_funct_ptr ge bmcs_log =
Some (External (EF_external mcs_log
(signature_of_type (Tcons tint (Tcons tint Tnil))
Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
Lemma mcs_swap_tail_body_correct: ∀ m d d´ env le bound lock_index cpuid old_tail,
env = PTree.empty _ →
PTree.get _bound le = Some (Vint bound) →
PTree.get _lock_index le = Some (Vint lock_index) →
PTree.get _cpuid le = Some (Vint cpuid) →
mcs_swap_tail_spec (Int.unsigned bound) (Int.unsigned lock_index) (Int.unsigned cpuid) d
= Some (d´, (Int.unsigned old_tail)) →
kernel_mode d →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_mcs_swap_tail_body E0 le´ (m, d´)
(Out_return (Some (Vint old_tail, tint))).
Proof.
intros.
functional inversion H3; subst.
- unfold f_mcs_swap_tail_body; subst.
esplit; repeat vcgen.
× unfold mcs_log_spec.
rewrite H8, H9, H10, H11, H12.
unfold l1 in H13.
unfold to in H13.
rewrite H13.
reflexivity.
× unfold mcs_SWAP_TAIL_spec; repeat vcgen.
rewrite <- ikern_remain.
rewrite <- ihost_remain.
rewrite H8, H9, H10, H11.
simpl; rewrite ZMap.gss.
unfold l1 in H13.
unfold to in H13.
rewrite H13.
rewrite multi_log_double_update.
rewrite ZMap.set2.
unfold l´; simpl.
rewrite zle_le_true; try omega.
rewrite _x4.
unfold NULL.
rewrite zeq_true; try omega.
repeat vcgen.
- unfold f_mcs_swap_tail_body; subst.
esplit; repeat vcgen.
× unfold mcs_log_spec.
rewrite H8, H9, H10, H11, H12.
unfold l1 in H13.
unfold to in H13.
rewrite H13.
reflexivity.
× unfold mcs_SWAP_TAIL_spec; repeat vcgen.
rewrite <- ikern_remain.
rewrite <- ihost_remain.
rewrite H8, H9, H10, H11.
simpl; rewrite ZMap.gss.
unfold l1 in H13.
unfold to in H13.
rewrite H13.
rewrite zeq_false; try omega.
rewrite multi_log_double_update.
rewrite ZMap.set2.
unfold l´; simpl.
rewrite zle_le_true; try omega.
repeat vcgen.
Qed.
End MCSSWAPTAILBODY.
Theorem mcs_swap_tail_code_correct:
spec_le (mcs_swap_tail ↦ mcs_swap_tail_spec_low) (〚mcs_swap_tail ↦ f_mcs_swap_tail 〛L).
Proof.
fbigstep_pre L.
fbigstep (mcs_swap_tail_body_correct s (Genv.globalenv p) makeglobalenv
b1 Hb1fs Hb1fp
b0 Hb0fs Hb0fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_mcs_swap_tail)
(Vint bound::Vint lock_index::Vint cpuid::nil)
(create_undef_temps (fn_temps f_mcs_swap_tail)))) muval.
Qed.
End MCSSWAPTAIL.
Section MCSCASTAIL.
Let L: compatlayer (cdata RData) :=
mcs_log ↦ gensem mcs_log_spec
⊕ mcs_CAS_TAIL ↦ gensem mcs_CAS_TAIL_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section MCSCASTAILBODY.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable bmcs_CAS_TAIL: block.
Hypothesis hmcs_CAS_TAIL1 : Genv.find_symbol ge mcs_CAS_TAIL = Some bmcs_CAS_TAIL.
Hypothesis hmcs_CAS_TAIL2 : Genv.find_funct_ptr ge bmcs_CAS_TAIL =
Some (External (EF_external mcs_CAS_TAIL
(signature_of_type (Tcons tint (Tcons tint Tnil))
tint cc_default))
(Tcons tint (Tcons tint Tnil)) tint cc_default).
Variable bmcs_log: block.
Hypothesis hmcs_log1 : Genv.find_symbol ge mcs_log = Some bmcs_log.
Hypothesis hmcs_log2 : Genv.find_funct_ptr ge bmcs_log =
Some (External (EF_external mcs_log
(signature_of_type (Tcons tint (Tcons tint Tnil))
Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
Lemma mcs_cas_tail_body_correct: ∀ m d d´ env le lock_index cpuid success,
env = PTree.empty _ →
PTree.get _lock_index le = Some (Vint lock_index) →
PTree.get _cpuid le = Some (Vint cpuid) →
mcs_cas_tail_spec (Int.unsigned lock_index) (Int.unsigned cpuid) d = Some (d´, (Int.unsigned success)) →
kernel_mode d →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_mcs_cas_tail_body E0 le´ (m, d´)
(Out_return (Some (Vint success, tint))).
Proof.
intros.
functional inversion H2; subst.
- unfold f_mcs_cas_tail_body; subst.
esplit; repeat vcgen.
+ unfold mcs_log_spec.
rewrite H7, H8, H9, H10, H11.
unfold l1 in H12.
unfold to in H12.
rewrite H12.
reflexivity.
+ unfold mcs_CAS_TAIL_spec; repeat vcgen.
rewrite <- ikern_remain.
rewrite <- ihost_remain.
rewrite H7, H8, H9, H10.
rewrite <- H6.
simpl; rewrite ZMap.gss.
unfold l1 in H12.
unfold to in H12.
rewrite H12, H13.
rewrite multi_log_double_update.
rewrite ZMap.set2.
unfold l1; unfold to.
repeat vcgen.
- unfold f_mcs_cas_tail_body; subst.
esplit; repeat vcgen.
+ unfold mcs_log_spec.
rewrite H7, H8, H9, H10, H11.
unfold l1 in H12.
unfold to in H12.
rewrite H12.
reflexivity.
+ unfold mcs_CAS_TAIL_spec; repeat vcgen.
rewrite <- ikern_remain.
rewrite <- ihost_remain.
rewrite H7, H8, H9, H10.
rewrite <- H6.
simpl; rewrite ZMap.gss.
unfold l1 in H12.
unfold to in H12.
rewrite H12, H13.
rewrite multi_log_double_update.
rewrite ZMap.set2.
unfold l1; unfold to.
repeat vcgen.
Qed.
End MCSCASTAILBODY.
Theorem mcs_cas_tail_code_correct:
spec_le (mcs_cas_tail ↦ mcs_cas_tail_spec_low) (〚mcs_cas_tail ↦ f_mcs_cas_tail 〛L).
Proof.
fbigstep_pre L.
fbigstep (mcs_cas_tail_body_correct s (Genv.globalenv p) makeglobalenv
b1 Hb1fs Hb1fp
b0 Hb0fs Hb0fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_mcs_cas_tail)
(Vint lock_index::Vint cpuid::nil)
(create_undef_temps (fn_temps f_mcs_cas_tail)))) muval.
Qed.
End MCSCASTAIL.
Section MCSLOCKGETINDEX.
Lemma lock_AT_start_val: lock_AT_start = 0.
Proof. reflexivity. Qed.
Lemma ID_AT_range_val: ID_AT_range = 1.
Proof. unfold ID_AT_range; reflexivity. Qed.
Lemma lock_TCB_start_val : lock_TCB_start = 1.
Proof. unfold lock_TCB_start; reflexivity. Qed.
Lemma num_chan_val: num_chan = num_chan.
Proof. reflexivity. Qed.
Lemma ID_TCB_range_val: ID_TCB_range = num_chan.
Proof. unfold ID_TCB_range; reflexivity. Qed.
Lemma lock_TCB_range_val: lock_TCB_range = num_chan + 1.
Proof. unfold lock_TCB_range; simpl; reflexivity. Qed.
Lemma lock_SC_start_val: lock_SC_start = num_chan + 1.
Proof. unfold lock_SC_start. rewrite lock_TCB_range_val. reflexivity. Qed.
Lemma lock_range_val: lock_range = num_chan + num_chan + 1.
Proof. unfold lock_range; simpl; reflexivity. Qed.
Let L: compatlayer (cdata RData) := ∅.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section MCSLOCKGETINDEXBODY.
Context `{Hwb: WritableBlockOps}.
Variables (ge: genv).
Lemma mcs_lock_get_index_body_correct:
∀ m d d´ env le lock_id offset lock_index,
env = PTree.empty _ →
PTree.get _lock_id le = Some (Vint lock_id) →
PTree.get _offset le = Some (Vint offset) →
mcs_lock_get_index_spec (Int.unsigned lock_id) (Int.unsigned offset) d
= Some (d´, (Int.unsigned lock_index)) →
kernel_mode d →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_mcs_lock_get_index_body E0 le´ (m, d´)
(Out_return (Some (Vint lock_index, tint))).
Proof.
intros.
functional inversion H2; subst.
assert (lock_id_val: (Int.unsigned lock_id) = ID_AT ∨
(Int.unsigned lock_id) = ID_TCB ∨
(Int.unsigned lock_id) = ID_SC).
{ clearAllExceptOne H7.
unfold index2Z in H7.
unfold index_range in ×.
destruct (Int.unsigned lock_id); try tauto; try (inversion H7; fail).
destruct p; try tauto; try (inversion H7; fail).
destruct p; try tauto; try (inversion H7). }
Opaque Z.add Z.mul.
assert (offset_range1: (Int.unsigned lock_id) = ID_AT →
0 ≤ (Int.unsigned offset) < ID_AT_range).
{ intros.
destruct lock_id_val as [lock_id_val | [lock_id_val | lock_id_val]].
- unfold index2Z in H7.
rewrite H in H7.
simpl in H7.
destruct (zle_lt 0 (Int.unsigned offset) ID_AT_range).
× assumption.
× inversion H7.
- rewrite lock_id_val in H.
inversion H.
- rewrite lock_id_val in H.
inversion H. }
assert (offset_range2: (Int.unsigned lock_id) = ID_TCB →
0 ≤ (Int.unsigned offset) < ID_TCB_range).
{ intros.
destruct lock_id_val as [lock_id_val | [lock_id_val | lock_id_val]].
- rewrite lock_id_val in H.
inversion H.
- unfold index2Z in H7.
rewrite H in H7.
simpl in H7.
destruct (zle_lt 0 (Int.unsigned offset) ID_TCB_range).
× assumption.
× inversion H7.
- rewrite lock_id_val in H.
inversion H. }
assert (offset_range3: (Int.unsigned lock_id) = ID_SC →
0 ≤ (Int.unsigned offset) < ID_SC_range).
{ intros.
destruct lock_id_val as [lock_id_val | [lock_id_val | lock_id_val]].
- rewrite lock_id_val in H.
inversion H.
- rewrite lock_id_val in H.
inversion H.
- unfold index2Z in H7.
rewrite H in H7.
simpl in H7.
destruct (zle_lt 0 (Int.unsigned offset) ID_SC_range).
× assumption.
× inversion H7. }
unfold f_mcs_lock_get_index_body; subst.
destruct lock_id_val as [lock_id_val | [lock_id_val | lock_id_val]].
- remember lock_id_val as offset_range.
clear Heqoffset_range.
apply offset_range1 in offset_range.
unfold index2Z in H7.
rewrite lock_id_val in H7.
simpl in H7.
destruct (zle_lt 0 (Int.unsigned offset) ID_AT_range);
try (inv H7; fail).
inversion H7.
replace (0 + Int.unsigned offset) with (Int.unsigned offset) in H5; try omega.
rewrite H5 in ×.
subst.
destruct a.
unfold ID_AT_range in ×.
esplit; repeat vcgen.
rewrite zlt_true.
+ repeat vcgen.
+ repeat vcgen.
+ repeat vcgen.
+ repeat vcgen.
+ simpl.
simpl in ×.
assert (Int.eq Int.one Int.zero = false) by vcgen.
rewrite H10.
simpl.
assert (Int.unsigned lock_index = 0).
{ omega. }
assert (lock_index = Int.repr (Int.unsigned lock_index)).
{ rewrite Int.repr_unsigned; reflexivity. }
rewrite H11 in H12.
rewrite H12.
repeat f_equal.
repeat vcgen.
- remember lock_id_val as offset_range.
clear Heqoffset_range.
apply offset_range2 in offset_range.
unfold index2Z in H7.
Opaque Z.add Z.mul.
rewrite lock_id_val in H7.
simpl in H7.
destruct (zle_lt 0 (Int.unsigned offset) ID_TCB_range);
try (inv H7; fail).
inversion H7.
subst.
destruct a.
unfold ID_TCB_range in ×.
generalize max_unsigned_val; intros muval.
esplit; repeat vcgen.
+ repeat vcgen.
rewrite zlt_true.
repeat vcgen.
repeat vcgen.
+ repeat vcgen.
+ repeat vcgen.
+ repeat vcgen.
unfold ID_AT_range in ×.
simpl.
discharge_cmp.
assert (lock_index = Int.repr (Int.unsigned lock_index)).
{ rewrite Int.repr_unsigned; reflexivity. }
rewrite H10.
repeat f_equal.
assumption.
- remember lock_id_val as offset_range.
clear Heqoffset_range.
apply offset_range3 in offset_range.
unfold index2Z in H7.
rewrite lock_id_val in H7.
simpl in H7.
destruct (zle_lt 0 (Int.unsigned offset) ID_SC_range);
try (inv H7; fail).
inversion H7.
subst.
destruct a.
unfold ID_SC_range in ×.
generalize max_unsigned_val; intros muval.
unfold lock_TCB_range in ×.
unfold ID_AT_range in ×. unfold ID_TCB_range in ×.
esplit; repeat vcgen.
+ repeat vcgen.
rewrite zlt_true.
repeat vcgen.
omega.
+ repeat vcgen.
+ repeat vcgen.
+ repeat vcgen.
simpl.
discharge_cmp.
assert (lock_index = Int.repr (Int.unsigned lock_index)).
{ rewrite Int.repr_unsigned; reflexivity. }
rewrite H10.
repeat f_equal.
assumption.
Qed.
End MCSLOCKGETINDEXBODY.
Theorem mcs_lock_get_index_code_correct:
spec_le (mcs_lock_get_index ↦ mcs_lock_get_index_spec_low) (〚mcs_lock_get_index ↦ f_mcs_lock_get_index 〛L).
Proof.
fbigstep_pre L.
fbigstep (mcs_lock_get_index_body_correct (Genv.globalenv p) m´0 labd labd´
(PTree.empty _)
(bind_parameter_temps´ (fn_params f_mcs_lock_get_index)
(Vint lock_id::Vint offset::nil)
(create_undef_temps (fn_temps f_mcs_lock_get_index)))) muval.
Qed.
End MCSLOCKGETINDEX.
End WithPrimitives.
End MMCSLOCKINTROCODE.
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 MMCSLockIntroCSource.
Require Import MMCSLockIntro.
Require Import MCSLockAbsIntroGenSpec.
Require Import CalMCSLock.
Require Import AbstractDataType.
Lemma multi_log_double_update:
∀ d ml1 ml2,
(d {multi_log: ml1}) {multi_log: ml2} = d {multi_log: ml2}.
Proof.
intros.
unfold update_multi_log; simpl.
reflexivity.
Qed.
Lemma ikern_remain :
∀ d ml, ikern d = ikern (d {multi_log: ml}).
Proof. intros; simpl; auto. Qed.
Lemma ihost_remain:
∀ d ml, ihost d = ihost (d {multi_log: ml}).
Proof. intros; simpl; auto. Qed.
Module MMCSLOCKINTROCODE.
Section WithPrimitives.
Context `{real_params: RealParams}.
Context `{mcs_oracle_prop: MCSOracleProp}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
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 MCSGETNEXT.
Let L: compatlayer (cdata RData) :=
mcs_log ↦ gensem mcs_log_spec
⊕ mcs_GET_NEXT ↦ gensem mcs_GET_NEXT_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section MCSGETNEXTBODY.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable bmcs_GET_NEXT: block.
Hypothesis hmcs_GET_NEXT1 : Genv.find_symbol ge mcs_GET_NEXT = Some bmcs_GET_NEXT.
Hypothesis hmcs_GET_NEXT2 : Genv.find_funct_ptr ge bmcs_GET_NEXT =
Some (External (EF_external mcs_GET_NEXT
(signature_of_type (Tcons tint (Tcons tint Tnil))
tint cc_default))
(Tcons tint (Tcons tint Tnil)) tint cc_default).
Variable bmcs_log: block.
Hypothesis hmcs_log1 : Genv.find_symbol ge mcs_log = Some bmcs_log.
Hypothesis hmcs_log2 : Genv.find_funct_ptr ge bmcs_log =
Some (External (EF_external mcs_log
(signature_of_type (Tcons tint (Tcons tint Tnil))
Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
Lemma mcs_get_next_body_correct: ∀ m d d´ env le lock_index cpuid next,
env = PTree.empty _ →
PTree.get _lock_index le = Some (Vint lock_index) →
PTree.get _cpuid le = Some (Vint cpuid) →
mcs_get_next_spec (Int.unsigned lock_index) (Int.unsigned cpuid) d = Some (d´, (Int.unsigned next)) →
kernel_mode d →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_mcs_get_next_body E0 le´ (m, d´)
(Out_return (Some (Vint next, tint))).
Proof.
intros.
functional inversion H2; subst.
unfold f_mcs_get_next_body; subst.
esplit; repeat vcgen.
- unfold mcs_log_spec.
rewrite H7, H8, H9, H10, H11.
unfold l´ in H12.
unfold l1 in H12.
unfold to in H12.
Transparent CalMCSLock.
simpl in H12.
subdestruct ; try (inv H12; fail).
reflexivity.
- unfold mcs_GET_NEXT_spec; repeat vcgen.
rewrite <- ikern_remain.
rewrite <- ihost_remain.
rewrite H7, H8, H9, H10.
simpl; rewrite ZMap.gss.
unfold l´ in H12.
unfold l1 in H12.
unfold to in H12.
Transparent CalMCSLock.
simpl in H12.
subdestruct ; try (inv H12; fail).
inv H12.
rewrite H13.
destruct (ZMap.get (Int.unsigned cpuid) node_pool).
inversion H13; subst.
rewrite multi_log_double_update.
rewrite ZMap.set2.
repeat vcgen.
Qed.
End MCSGETNEXTBODY.
Theorem mcs_get_next_code_correct:
spec_le (mcs_get_next ↦ mcs_get_next_spec_low) (〚mcs_get_next ↦ f_mcs_get_next 〛L).
Proof.
fbigstep_pre L.
fbigstep (mcs_get_next_body_correct s (Genv.globalenv p) makeglobalenv
b1 Hb1fs Hb1fp
b0 Hb0fs Hb0fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_mcs_get_next)
(Vint lock_index::Vint cpuid::nil)
(create_undef_temps (fn_temps f_mcs_get_next)))) muval.
Qed.
End MCSGETNEXT.
Section MCSSETNEXT.
Let L: compatlayer (cdata RData) :=
mcs_log ↦ gensem mcs_log_spec
⊕ mcs_SET_NEXT ↦ gensem mcs_SET_NEXT_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section MCSSETNEXTBODY.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable bmcs_SET_NEXT: block.
Hypothesis hmcs_SET_NEXT1 : Genv.find_symbol ge mcs_SET_NEXT = Some bmcs_SET_NEXT.
Hypothesis hmcs_SET_NEXT2 : Genv.find_funct_ptr ge bmcs_SET_NEXT =
Some (External (EF_external mcs_SET_NEXT
(signature_of_type
(Tcons tint (Tcons tint (Tcons tint Tnil)))
Tvoid cc_default))
(Tcons tint (Tcons tint (Tcons tint Tnil))) Tvoid cc_default).
Variable bmcs_log: block.
Hypothesis hmcs_log1 : Genv.find_symbol ge mcs_log = Some bmcs_log.
Hypothesis hmcs_log2 : Genv.find_funct_ptr ge bmcs_log =
Some (External (EF_external mcs_log
(signature_of_type (Tcons tint (Tcons tint Tnil))
Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
Lemma mcs_set_next_body_correct: ∀ m d d´ env le lock_index cpuid prev_id,
env = PTree.empty _ →
PTree.get _lock_index le = Some (Vint lock_index) →
PTree.get _cpuid le = Some (Vint cpuid) →
PTree.get _prev_id le = Some (Vint prev_id) →
mcs_set_next_spec (Int.unsigned lock_index) (Int.unsigned cpuid) (Int.unsigned prev_id) d
= Some d´ →
kernel_mode d →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_mcs_set_next_body E0 le´ (m, d´) Out_normal.
Proof.
intros.
functional inversion H3; subst.
unfold f_mcs_set_next_body; subst.
esplit; repeat vcgen.
- unfold mcs_log_spec.
rewrite H7, H8, H9, H10, H12.
unfold l1 in H13.
unfold to in H13.
rewrite H13.
reflexivity.
- unfold mcs_SET_NEXT_spec; repeat vcgen.
rewrite <- ikern_remain.
rewrite <- ihost_remain.
rewrite H7, H8, H9, H10, H11.
simpl; rewrite ZMap.gss.
rewrite multi_log_double_update.
simpl; rewrite ZMap.set2.
unfold l´; unfold l1; unfold to.
reflexivity.
Qed.
End MCSSETNEXTBODY.
Theorem mcs_set_next_code_correct:
spec_le (mcs_set_next ↦ mcs_set_next_spec_low) (〚mcs_set_next ↦ f_mcs_set_next 〛L).
Proof.
fbigstep_pre L.
fbigstep (mcs_set_next_body_correct s (Genv.globalenv p) makeglobalenv
b1 Hb1fs Hb1fp
b0 Hb0fs Hb0fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_mcs_set_next)
(Vint lock_index::Vint cpuid::Vint prev_id::nil)
(create_undef_temps (fn_temps f_mcs_set_next)))) muval.
Qed.
End MCSSETNEXT.
Section MCSGETBUSY.
Let L: compatlayer (cdata RData) :=
mcs_log ↦ gensem mcs_log_spec
⊕ mcs_GET_BUSY ↦ gensem mcs_GET_BUSY_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section MCSGETBUSYBODY.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable bmcs_GET_BUSY: block.
Hypothesis hmcs_GET_BUSY1 : Genv.find_symbol ge mcs_GET_BUSY = Some bmcs_GET_BUSY.
Hypothesis hmcs_GET_BUSY2 : Genv.find_funct_ptr ge bmcs_GET_BUSY =
Some (External (EF_external mcs_GET_BUSY
(signature_of_type (Tcons tint (Tcons tint Tnil))
tint cc_default))
(Tcons tint (Tcons tint Tnil)) tint cc_default).
Variable bmcs_log: block.
Hypothesis hmcs_log1 : Genv.find_symbol ge mcs_log = Some bmcs_log.
Hypothesis hmcs_log2 : Genv.find_funct_ptr ge bmcs_log =
Some (External (EF_external mcs_log
(signature_of_type (Tcons tint (Tcons tint Tnil))
Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
Lemma mcs_get_busy_body_correct: ∀ m d d´ env le lock_index cpuid busy,
env = PTree.empty _ →
PTree.get _lock_index le = Some (Vint lock_index) →
PTree.get _cpuid le = Some (Vint cpuid) →
mcs_get_busy_spec (Int.unsigned lock_index) (Int.unsigned cpuid) d = Some (d´, (Int.unsigned busy)) →
kernel_mode d →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_mcs_get_busy_body E0 le´ (m, d´)
(Out_return (Some (Vint busy, tint))).
Proof.
intros.
functional inversion H2; subst.
- unfold f_mcs_get_busy_body; subst.
esplit; repeat vcgen.
+ unfold mcs_log_spec.
rewrite H7, H8, H9, H10, H11.
unfold l´ in H12.
unfold l1 in H12.
unfold to in H12.
rewrite H12.
reflexivity.
+ unfold mcs_GET_BUSY_spec; repeat vcgen.
rewrite <- ikern_remain.
rewrite <- ihost_remain.
rewrite H7, H8, H9, H10.
simpl; rewrite ZMap.gss.
unfold l´ in H12.
unfold l1 in H12.
unfold to in H12.
rewrite H12.
rewrite H13.
destruct (ZMap.get (Int.unsigned cpuid) node_pool).
inversion H13; subst.
rewrite multi_log_double_update.
rewrite ZMap.set2.
rewrite <- H6.
reflexivity.
- unfold f_mcs_get_busy_body; subst.
esplit; repeat vcgen.
+ unfold mcs_log_spec.
rewrite H7, H8, H9, H10, H11.
unfold l´ in H12.
unfold l1 in H12.
unfold to in H12.
rewrite H12.
reflexivity.
+ unfold mcs_GET_BUSY_spec; repeat vcgen.
rewrite <- ikern_remain.
rewrite <- ihost_remain.
rewrite H7, H8, H9, H10.
simpl; rewrite ZMap.gss.
unfold l´ in H12.
unfold l1 in H12.
unfold to in H12.
rewrite H12.
rewrite H13.
destruct (ZMap.get (Int.unsigned cpuid) node_pool).
inv H13.
rewrite multi_log_double_update.
rewrite ZMap.set2.
rewrite <- H6.
unfold l´; unfold l1; unfold to.
reflexivity.
Qed.
End MCSGETBUSYBODY.
Theorem mcs_get_busy_code_correct:
spec_le (mcs_get_busy ↦ mcs_get_busy_spec_low) (〚mcs_get_busy ↦ f_mcs_get_busy 〛L).
Proof.
fbigstep_pre L.
fbigstep (mcs_get_busy_body_correct s (Genv.globalenv p) makeglobalenv
b1 Hb1fs Hb1fp
b0 Hb0fs Hb0fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_mcs_get_busy)
(Vint lock_index::Vint cpuid::nil)
(create_undef_temps (fn_temps f_mcs_get_busy)))) muval.
Qed.
End MCSGETBUSY.
Section MCSSETBUSY.
Let L: compatlayer (cdata RData) :=
mcs_log ↦ gensem mcs_log_spec
⊕ mcs_SET_BUSY ↦ gensem mcs_SET_BUSY_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section MCSSETBUSYBODY.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable bmcs_SET_BUSY: block.
Hypothesis hmcs_SET_BUSY1 : Genv.find_symbol ge mcs_SET_BUSY = Some bmcs_SET_BUSY.
Hypothesis hmcs_SET_BUSY2 : Genv.find_funct_ptr ge bmcs_SET_BUSY =
Some (External (EF_external mcs_SET_BUSY
(signature_of_type
(Tcons tint (Tcons tint Tnil))
Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
Variable bmcs_log: block.
Hypothesis hmcs_log1 : Genv.find_symbol ge mcs_log = Some bmcs_log.
Hypothesis hmcs_log2 : Genv.find_funct_ptr ge bmcs_log =
Some (External (EF_external mcs_log
(signature_of_type (Tcons tint (Tcons tint Tnil))
Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
Lemma mcs_set_busy_body_correct: ∀ m d d´ env le lock_index cpuid,
env = PTree.empty _ →
PTree.get _lock_index le = Some (Vint lock_index) →
PTree.get _cpuid le = Some (Vint cpuid) →
mcs_set_busy_spec (Int.unsigned lock_index) (Int.unsigned cpuid) d = Some d´ →
kernel_mode d →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_mcs_set_busy_body E0 le´ (m, d´) Out_normal.
Proof.
intros.
functional inversion H2; subst.
unfold f_mcs_set_busy_body; subst.
esplit; repeat vcgen.
- unfold mcs_log_spec.
rewrite H6, H7, H8, H9, H10.
unfold l1 in H11.
unfold to in H11.
rewrite H11.
reflexivity.
- unfold mcs_SET_BUSY_spec; repeat vcgen.
rewrite <- ikern_remain.
rewrite <- ihost_remain.
rewrite H6, H7, H8, H9.
simpl; rewrite ZMap.gss.
rewrite multi_log_double_update.
simpl; rewrite ZMap.set2.
unfold l1 in H11; unfold to in H11.
rewrite H11; unfold l´; unfold l1; unfold to.
rewrite H12.
rewrite zle_lt_true; try omega.
reflexivity.
Qed.
End MCSSETBUSYBODY.
Theorem mcs_set_busy_code_correct:
spec_le (mcs_set_busy ↦ mcs_set_busy_spec_low) (〚mcs_set_busy ↦ f_mcs_set_busy 〛L).
Proof.
fbigstep_pre L.
fbigstep (mcs_set_busy_body_correct s (Genv.globalenv p) makeglobalenv
b1 Hb1fs Hb1fp
b0 Hb0fs Hb0fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_mcs_set_busy)
(Vint lock_index::Vint cpuid::nil)
(create_undef_temps (fn_temps f_mcs_set_busy)))) muval.
Qed.
End MCSSETBUSY.
Section MCSSWAPTAIL.
Let L: compatlayer (cdata RData) :=
mcs_log ↦ gensem mcs_log_spec
⊕ mcs_SWAP_TAIL ↦ gensem mcs_SWAP_TAIL_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section MCSSWAPTAILBODY.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable bmcs_SWAP_TAIL: block.
Hypothesis hmcs_SWAP_TAIL1 : Genv.find_symbol ge mcs_SWAP_TAIL = Some bmcs_SWAP_TAIL.
Hypothesis hmcs_SWAP_TAIL2 : Genv.find_funct_ptr ge bmcs_SWAP_TAIL =
Some (External (EF_external mcs_SWAP_TAIL
(signature_of_type (Tcons tint (Tcons tint (Tcons tint Tnil)))
tint cc_default))
(Tcons tint (Tcons tint (Tcons tint Tnil))) tint cc_default).
Variable bmcs_log: block.
Hypothesis hmcs_log1 : Genv.find_symbol ge mcs_log = Some bmcs_log.
Hypothesis hmcs_log2 : Genv.find_funct_ptr ge bmcs_log =
Some (External (EF_external mcs_log
(signature_of_type (Tcons tint (Tcons tint Tnil))
Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
Lemma mcs_swap_tail_body_correct: ∀ m d d´ env le bound lock_index cpuid old_tail,
env = PTree.empty _ →
PTree.get _bound le = Some (Vint bound) →
PTree.get _lock_index le = Some (Vint lock_index) →
PTree.get _cpuid le = Some (Vint cpuid) →
mcs_swap_tail_spec (Int.unsigned bound) (Int.unsigned lock_index) (Int.unsigned cpuid) d
= Some (d´, (Int.unsigned old_tail)) →
kernel_mode d →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_mcs_swap_tail_body E0 le´ (m, d´)
(Out_return (Some (Vint old_tail, tint))).
Proof.
intros.
functional inversion H3; subst.
- unfold f_mcs_swap_tail_body; subst.
esplit; repeat vcgen.
× unfold mcs_log_spec.
rewrite H8, H9, H10, H11, H12.
unfold l1 in H13.
unfold to in H13.
rewrite H13.
reflexivity.
× unfold mcs_SWAP_TAIL_spec; repeat vcgen.
rewrite <- ikern_remain.
rewrite <- ihost_remain.
rewrite H8, H9, H10, H11.
simpl; rewrite ZMap.gss.
unfold l1 in H13.
unfold to in H13.
rewrite H13.
rewrite multi_log_double_update.
rewrite ZMap.set2.
unfold l´; simpl.
rewrite zle_le_true; try omega.
rewrite _x4.
unfold NULL.
rewrite zeq_true; try omega.
repeat vcgen.
- unfold f_mcs_swap_tail_body; subst.
esplit; repeat vcgen.
× unfold mcs_log_spec.
rewrite H8, H9, H10, H11, H12.
unfold l1 in H13.
unfold to in H13.
rewrite H13.
reflexivity.
× unfold mcs_SWAP_TAIL_spec; repeat vcgen.
rewrite <- ikern_remain.
rewrite <- ihost_remain.
rewrite H8, H9, H10, H11.
simpl; rewrite ZMap.gss.
unfold l1 in H13.
unfold to in H13.
rewrite H13.
rewrite zeq_false; try omega.
rewrite multi_log_double_update.
rewrite ZMap.set2.
unfold l´; simpl.
rewrite zle_le_true; try omega.
repeat vcgen.
Qed.
End MCSSWAPTAILBODY.
Theorem mcs_swap_tail_code_correct:
spec_le (mcs_swap_tail ↦ mcs_swap_tail_spec_low) (〚mcs_swap_tail ↦ f_mcs_swap_tail 〛L).
Proof.
fbigstep_pre L.
fbigstep (mcs_swap_tail_body_correct s (Genv.globalenv p) makeglobalenv
b1 Hb1fs Hb1fp
b0 Hb0fs Hb0fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_mcs_swap_tail)
(Vint bound::Vint lock_index::Vint cpuid::nil)
(create_undef_temps (fn_temps f_mcs_swap_tail)))) muval.
Qed.
End MCSSWAPTAIL.
Section MCSCASTAIL.
Let L: compatlayer (cdata RData) :=
mcs_log ↦ gensem mcs_log_spec
⊕ mcs_CAS_TAIL ↦ gensem mcs_CAS_TAIL_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section MCSCASTAILBODY.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable bmcs_CAS_TAIL: block.
Hypothesis hmcs_CAS_TAIL1 : Genv.find_symbol ge mcs_CAS_TAIL = Some bmcs_CAS_TAIL.
Hypothesis hmcs_CAS_TAIL2 : Genv.find_funct_ptr ge bmcs_CAS_TAIL =
Some (External (EF_external mcs_CAS_TAIL
(signature_of_type (Tcons tint (Tcons tint Tnil))
tint cc_default))
(Tcons tint (Tcons tint Tnil)) tint cc_default).
Variable bmcs_log: block.
Hypothesis hmcs_log1 : Genv.find_symbol ge mcs_log = Some bmcs_log.
Hypothesis hmcs_log2 : Genv.find_funct_ptr ge bmcs_log =
Some (External (EF_external mcs_log
(signature_of_type (Tcons tint (Tcons tint Tnil))
Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
Lemma mcs_cas_tail_body_correct: ∀ m d d´ env le lock_index cpuid success,
env = PTree.empty _ →
PTree.get _lock_index le = Some (Vint lock_index) →
PTree.get _cpuid le = Some (Vint cpuid) →
mcs_cas_tail_spec (Int.unsigned lock_index) (Int.unsigned cpuid) d = Some (d´, (Int.unsigned success)) →
kernel_mode d →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_mcs_cas_tail_body E0 le´ (m, d´)
(Out_return (Some (Vint success, tint))).
Proof.
intros.
functional inversion H2; subst.
- unfold f_mcs_cas_tail_body; subst.
esplit; repeat vcgen.
+ unfold mcs_log_spec.
rewrite H7, H8, H9, H10, H11.
unfold l1 in H12.
unfold to in H12.
rewrite H12.
reflexivity.
+ unfold mcs_CAS_TAIL_spec; repeat vcgen.
rewrite <- ikern_remain.
rewrite <- ihost_remain.
rewrite H7, H8, H9, H10.
rewrite <- H6.
simpl; rewrite ZMap.gss.
unfold l1 in H12.
unfold to in H12.
rewrite H12, H13.
rewrite multi_log_double_update.
rewrite ZMap.set2.
unfold l1; unfold to.
repeat vcgen.
- unfold f_mcs_cas_tail_body; subst.
esplit; repeat vcgen.
+ unfold mcs_log_spec.
rewrite H7, H8, H9, H10, H11.
unfold l1 in H12.
unfold to in H12.
rewrite H12.
reflexivity.
+ unfold mcs_CAS_TAIL_spec; repeat vcgen.
rewrite <- ikern_remain.
rewrite <- ihost_remain.
rewrite H7, H8, H9, H10.
rewrite <- H6.
simpl; rewrite ZMap.gss.
unfold l1 in H12.
unfold to in H12.
rewrite H12, H13.
rewrite multi_log_double_update.
rewrite ZMap.set2.
unfold l1; unfold to.
repeat vcgen.
Qed.
End MCSCASTAILBODY.
Theorem mcs_cas_tail_code_correct:
spec_le (mcs_cas_tail ↦ mcs_cas_tail_spec_low) (〚mcs_cas_tail ↦ f_mcs_cas_tail 〛L).
Proof.
fbigstep_pre L.
fbigstep (mcs_cas_tail_body_correct s (Genv.globalenv p) makeglobalenv
b1 Hb1fs Hb1fp
b0 Hb0fs Hb0fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_mcs_cas_tail)
(Vint lock_index::Vint cpuid::nil)
(create_undef_temps (fn_temps f_mcs_cas_tail)))) muval.
Qed.
End MCSCASTAIL.
Section MCSLOCKGETINDEX.
Lemma lock_AT_start_val: lock_AT_start = 0.
Proof. reflexivity. Qed.
Lemma ID_AT_range_val: ID_AT_range = 1.
Proof. unfold ID_AT_range; reflexivity. Qed.
Lemma lock_TCB_start_val : lock_TCB_start = 1.
Proof. unfold lock_TCB_start; reflexivity. Qed.
Lemma num_chan_val: num_chan = num_chan.
Proof. reflexivity. Qed.
Lemma ID_TCB_range_val: ID_TCB_range = num_chan.
Proof. unfold ID_TCB_range; reflexivity. Qed.
Lemma lock_TCB_range_val: lock_TCB_range = num_chan + 1.
Proof. unfold lock_TCB_range; simpl; reflexivity. Qed.
Lemma lock_SC_start_val: lock_SC_start = num_chan + 1.
Proof. unfold lock_SC_start. rewrite lock_TCB_range_val. reflexivity. Qed.
Lemma lock_range_val: lock_range = num_chan + num_chan + 1.
Proof. unfold lock_range; simpl; reflexivity. Qed.
Let L: compatlayer (cdata RData) := ∅.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section MCSLOCKGETINDEXBODY.
Context `{Hwb: WritableBlockOps}.
Variables (ge: genv).
Lemma mcs_lock_get_index_body_correct:
∀ m d d´ env le lock_id offset lock_index,
env = PTree.empty _ →
PTree.get _lock_id le = Some (Vint lock_id) →
PTree.get _offset le = Some (Vint offset) →
mcs_lock_get_index_spec (Int.unsigned lock_id) (Int.unsigned offset) d
= Some (d´, (Int.unsigned lock_index)) →
kernel_mode d →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_mcs_lock_get_index_body E0 le´ (m, d´)
(Out_return (Some (Vint lock_index, tint))).
Proof.
intros.
functional inversion H2; subst.
assert (lock_id_val: (Int.unsigned lock_id) = ID_AT ∨
(Int.unsigned lock_id) = ID_TCB ∨
(Int.unsigned lock_id) = ID_SC).
{ clearAllExceptOne H7.
unfold index2Z in H7.
unfold index_range in ×.
destruct (Int.unsigned lock_id); try tauto; try (inversion H7; fail).
destruct p; try tauto; try (inversion H7; fail).
destruct p; try tauto; try (inversion H7). }
Opaque Z.add Z.mul.
assert (offset_range1: (Int.unsigned lock_id) = ID_AT →
0 ≤ (Int.unsigned offset) < ID_AT_range).
{ intros.
destruct lock_id_val as [lock_id_val | [lock_id_val | lock_id_val]].
- unfold index2Z in H7.
rewrite H in H7.
simpl in H7.
destruct (zle_lt 0 (Int.unsigned offset) ID_AT_range).
× assumption.
× inversion H7.
- rewrite lock_id_val in H.
inversion H.
- rewrite lock_id_val in H.
inversion H. }
assert (offset_range2: (Int.unsigned lock_id) = ID_TCB →
0 ≤ (Int.unsigned offset) < ID_TCB_range).
{ intros.
destruct lock_id_val as [lock_id_val | [lock_id_val | lock_id_val]].
- rewrite lock_id_val in H.
inversion H.
- unfold index2Z in H7.
rewrite H in H7.
simpl in H7.
destruct (zle_lt 0 (Int.unsigned offset) ID_TCB_range).
× assumption.
× inversion H7.
- rewrite lock_id_val in H.
inversion H. }
assert (offset_range3: (Int.unsigned lock_id) = ID_SC →
0 ≤ (Int.unsigned offset) < ID_SC_range).
{ intros.
destruct lock_id_val as [lock_id_val | [lock_id_val | lock_id_val]].
- rewrite lock_id_val in H.
inversion H.
- rewrite lock_id_val in H.
inversion H.
- unfold index2Z in H7.
rewrite H in H7.
simpl in H7.
destruct (zle_lt 0 (Int.unsigned offset) ID_SC_range).
× assumption.
× inversion H7. }
unfold f_mcs_lock_get_index_body; subst.
destruct lock_id_val as [lock_id_val | [lock_id_val | lock_id_val]].
- remember lock_id_val as offset_range.
clear Heqoffset_range.
apply offset_range1 in offset_range.
unfold index2Z in H7.
rewrite lock_id_val in H7.
simpl in H7.
destruct (zle_lt 0 (Int.unsigned offset) ID_AT_range);
try (inv H7; fail).
inversion H7.
replace (0 + Int.unsigned offset) with (Int.unsigned offset) in H5; try omega.
rewrite H5 in ×.
subst.
destruct a.
unfold ID_AT_range in ×.
esplit; repeat vcgen.
rewrite zlt_true.
+ repeat vcgen.
+ repeat vcgen.
+ repeat vcgen.
+ repeat vcgen.
+ simpl.
simpl in ×.
assert (Int.eq Int.one Int.zero = false) by vcgen.
rewrite H10.
simpl.
assert (Int.unsigned lock_index = 0).
{ omega. }
assert (lock_index = Int.repr (Int.unsigned lock_index)).
{ rewrite Int.repr_unsigned; reflexivity. }
rewrite H11 in H12.
rewrite H12.
repeat f_equal.
repeat vcgen.
- remember lock_id_val as offset_range.
clear Heqoffset_range.
apply offset_range2 in offset_range.
unfold index2Z in H7.
Opaque Z.add Z.mul.
rewrite lock_id_val in H7.
simpl in H7.
destruct (zle_lt 0 (Int.unsigned offset) ID_TCB_range);
try (inv H7; fail).
inversion H7.
subst.
destruct a.
unfold ID_TCB_range in ×.
generalize max_unsigned_val; intros muval.
esplit; repeat vcgen.
+ repeat vcgen.
rewrite zlt_true.
repeat vcgen.
repeat vcgen.
+ repeat vcgen.
+ repeat vcgen.
+ repeat vcgen.
unfold ID_AT_range in ×.
simpl.
discharge_cmp.
assert (lock_index = Int.repr (Int.unsigned lock_index)).
{ rewrite Int.repr_unsigned; reflexivity. }
rewrite H10.
repeat f_equal.
assumption.
- remember lock_id_val as offset_range.
clear Heqoffset_range.
apply offset_range3 in offset_range.
unfold index2Z in H7.
rewrite lock_id_val in H7.
simpl in H7.
destruct (zle_lt 0 (Int.unsigned offset) ID_SC_range);
try (inv H7; fail).
inversion H7.
subst.
destruct a.
unfold ID_SC_range in ×.
generalize max_unsigned_val; intros muval.
unfold lock_TCB_range in ×.
unfold ID_AT_range in ×. unfold ID_TCB_range in ×.
esplit; repeat vcgen.
+ repeat vcgen.
rewrite zlt_true.
repeat vcgen.
omega.
+ repeat vcgen.
+ repeat vcgen.
+ repeat vcgen.
simpl.
discharge_cmp.
assert (lock_index = Int.repr (Int.unsigned lock_index)).
{ rewrite Int.repr_unsigned; reflexivity. }
rewrite H10.
repeat f_equal.
assumption.
Qed.
End MCSLOCKGETINDEXBODY.
Theorem mcs_lock_get_index_code_correct:
spec_le (mcs_lock_get_index ↦ mcs_lock_get_index_spec_low) (〚mcs_lock_get_index ↦ f_mcs_lock_get_index 〛L).
Proof.
fbigstep_pre L.
fbigstep (mcs_lock_get_index_body_correct (Genv.globalenv p) m´0 labd labd´
(PTree.empty _)
(bind_parameter_temps´ (fn_params f_mcs_lock_get_index)
(Vint lock_id::Vint offset::nil)
(create_undef_temps (fn_temps f_mcs_lock_get_index)))) muval.
Qed.
End MCSLOCKGETINDEX.
End WithPrimitives.
End MMCSLOCKINTROCODE.