Library mcertikos.mcslock.MMCSLockIntroCodeMCSLockInit
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 TacticsForTesting.
Require Import MMCSLockIntroCSource.
Require Import MMCSLockIntro.
Require Import MCSLockAbsIntroGenSpec.
Require Import CalMCSLock.
Require Import CalTicketLock.
Require Import AbstractDataType.
Require Import DeviceStateDataType.
Require Import ObjInterruptDriver.
Module MMCSLOCKINTROCODEMCSLOCKINIT.
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 MCSLOCKINIT.
Let L: compatlayer (cdata RData) :=
boot_loader ↦ gensem bootloader0_spec
⊕ mcs_init_node ↦ gensem mcs_init_node_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section MCSLOCKINITBODY.
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 TacticsForTesting.
Require Import MMCSLockIntroCSource.
Require Import MMCSLockIntro.
Require Import MCSLockAbsIntroGenSpec.
Require Import CalMCSLock.
Require Import CalTicketLock.
Require Import AbstractDataType.
Require Import DeviceStateDataType.
Require Import ObjInterruptDriver.
Module MMCSLOCKINTROCODEMCSLOCKINIT.
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 MCSLOCKINIT.
Let L: compatlayer (cdata RData) :=
boot_loader ↦ gensem bootloader0_spec
⊕ mcs_init_node ↦ gensem mcs_init_node_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section MCSLOCKINITBODY.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
boot_loader
Variable bboot_loader: block.
Hypothesis hboot_loader1 : Genv.find_symbol ge boot_loader = Some bboot_loader.
Hypothesis hboot_loader2 :
Genv.find_funct_ptr ge bboot_loader =
Some (External (EF_external boot_loader
(signature_of_type (Tcons tint Tnil) tvoid cc_default))
(Tcons tint Tnil) tvoid cc_default).
Hypothesis hboot_loader1 : Genv.find_symbol ge boot_loader = Some bboot_loader.
Hypothesis hboot_loader2 :
Genv.find_funct_ptr ge bboot_loader =
Some (External (EF_external boot_loader
(signature_of_type (Tcons tint Tnil) tvoid cc_default))
(Tcons tint Tnil) tvoid cc_default).
mcs_init_node
Variable bmcs_init_node: block.
Hypothesis hmcs_init_node1 : Genv.find_symbol ge mcs_init_node = Some bmcs_init_node.
Hypothesis hmcs_init_node2 :
Genv.find_funct_ptr ge bmcs_init_node =
Some (External (EF_external mcs_init_node
(signature_of_type (Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
Hypothesis hmcs_init_node1 : Genv.find_symbol ge mcs_init_node = Some bmcs_init_node.
Hypothesis hmcs_init_node2 :
Genv.find_funct_ptr ge bmcs_init_node =
Some (External (EF_external mcs_init_node
(signature_of_type (Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
Loop Proof
Definition mcs_lock_init_mk_rdata adt index :=
adt {multi_log: real_multi_log_pb (Z.to_nat index) (multi_log adt)}.
Lemma real_multi_log_pb_exists:
∀ n (d: RData), ∃ d´, (d {multi_log : real_multi_log_pb n (multi_log d)}) = d´.
Proof.
clearAll.
induction n; intros.
∃ (d {multi_log: real_multi_log_pb 0 (multi_log d)}); auto.
destruct IHn with d as (d´, H); simpl.
∃ (d {multi_log : ZMap.set (Z.of_nat n) (MultiDef nil)
(multi_log d´)}).
Opaque real_multi_log_pb.
clear IHn.
destruct d; destruct d´; simpl in ×.
inv H; simpl.
repeat f_equal.
Transparent real_multi_log_pb.
Qed.
Lemma real_multi_log_pb_flags_same :
∀ n d d´,
ikern d = true ∧ ihost d = true ∧ init d = true →
(d {multi_log: real_multi_log_pb n (multi_log d)} = d´) →
ikern d´ = true ∧ ihost d´ = true ∧ init d´ = true.
Proof.
Transparent real_multi_log_pb.
clearAll.
induction n; intros.
unfold real_multi_log_pb in H0.
destruct d; destruct d´.
inv H0; subst.
simpl in ×.
tauto.
destruct real_multi_log_pb_exists with (n := n) (d := d) as (d´´, H1).
eapply IHn with (2:= H1) in H.
simpl in H0.
clear IHn.
destruct d; destruct d´; destruct d´´; simpl in ×.
inv H1; inv H0; auto.
Qed.
Lemma mcs_lock_mk_rdata_flags_same :
∀ n d d´, ikern d = true ∧ ihost d = true ∧ init d = true→
mcs_lock_init_mk_rdata d n = d´ →
ikern d´ = true ∧ ihost d´ = true ∧ init d´ = true.
Proof.
clearAll.
unfold mcs_lock_init_mk_rdata.
intros.
eauto using real_multi_log_pb_flags_same.
Qed.
Section mcs_lock_init_loop_proof.
Variable minit: memb.
Variable adt: RData.
Hypothesis iikern: ikern adt = true.
Hypothesis iihost: ihost adt = true.
Hypothesis iinit: init adt = true.
Hypothesis hinv: high_level_invariant adt.
Definition mcs_lock_init_loop_body_P (le: temp_env) (m: mem): Prop :=
PTree.get _i le = Some (Vint Int.zero) ∧
ikern adt = true ∧
ihost adt = true ∧
init adt = true ∧
m = (minit, adt).
Definition mcs_lock_init_loop_body_Q (le : temp_env) (m: mem): Prop :=
m = (minit, mcs_lock_init_mk_rdata adt lock_range).
Lemma mcs_lock_init_loop_correct_aux : LoopProofSimpleWhile.t f_mcs_lock_init_while_condition
f_mcs_lock_init_while_body ge
(PTree.empty _)
(mcs_lock_init_loop_body_P)
(mcs_lock_init_loop_body_Q).
Proof.
generalize max_unsigned_val; intro muval.
assert (lock_range0: lock_range = (num_chan + num_chan + 1)) by (unfold lock_range; simpl; omega).
apply LoopProofSimpleWhile.make with
(W := Z)
(lt := fun z1 z2 ⇒ (0 ≤ z2 ∧ z1 < z2)%Z)
(I := fun le m w ⇒ ∃ i,
PTree.get _i le = Some (Vint i) ∧
0 ≤ Int.unsigned i ≤ lock_range ∧
ikern adt = true ∧
ihost adt = true ∧
init adt = true ∧
((Int.unsigned i = 0 ∧ m = (minit, adt)) ∨
(Int.unsigned i > 0 ∧ m = (minit, mcs_lock_init_mk_rdata adt (Int.unsigned i)))) ∧
w = lock_range - Int.unsigned i
).
- apply Zwf_well_founded.
- intros.
unfold mcs_lock_init_loop_body_P in H; subst.
destruct H as [_ile tmpH].
destruct tmpH as [iikern´ tmpH].
destruct tmpH as [iihost´ tmpH].
destruct tmpH as [iinit´ tmpH].
subst.
esplit.
esplit.
change (Int.zero) with (Int.repr 0) in _ile.
repeat vcgen.
- intros.
destruct H as [i tmpH].
destruct tmpH as [_ile tmpH].
destruct tmpH as [irange tmpH].
destruct tmpH as [iikern´ tmpH].
destruct tmpH as [iihost´ tmpH].
destruct tmpH as [iinit´ tmpH].
destruct tmpH as [icond H]; subst.
destruct irange as [ilow ihigh].
apply Zle_lt_or_eq in ihigh.
destruct m.
Caseeq ihigh; intros.
+
Caseeq icond; intros.
×
destruct H0.
inv H1.
esplit; esplit.
repeat vcgen.
esplit; esplit.
unfold f_mcs_lock_init_while_body; subst.
repeat vcgen.
∃ (num_chan + num_chan).
repeat vcgen.
esplit.
repeat vcgen.
right.
split.
omega.
unfold mcs_lock_init_mk_rdata.
simpl.
rewrite H0.
simpl.
reflexivity.
×
destruct H0.
inv H1.
esplit; esplit.
repeat vcgen.
esplit; esplit.
unfold f_mcs_lock_init_while_body; subst.
repeat vcgen.
unfold mcs_init_node_spec.
simpl.
rewrite iikern, iihost.
rewrite zle_lt_true.
reflexivity.
omega.
∃ ((num_chan + num_chan + 1) - Int.unsigned i - 1).
repeat vcgen.
esplit.
repeat vcgen.
right.
split.
omega.
f_equal.
unfold mcs_lock_init_mk_rdata; simpl.
change (Int.unsigned i + 1) with (Z.succ (Int.unsigned i)).
rewrite Z2Nat.inj_succ with (n:=(Int.unsigned i)) in *; [ | omega].
simpl.
rewrite Z2Nat.id; [ | assumption].
repeat vcgen.
+
unfold mcs_lock_init_loop_body_Q.
esplit; esplit.
repeat vcgen.
simpl.
Caseeq icond; intro icond´; destruct icond´ as [iv mval].
× exfalso; rewrite iv in H; inv H.
× rewrite H in mval; trivial.
Qed.
End mcs_lock_init_loop_proof.
Lemma mcs_lock_init_loop_correct: ∀ m d d´ le,
PTree.get _i le = Some (Vint Int.zero) →
ikern d = true →
ihost d = true →
init d = true →
d´ = mcs_lock_init_mk_rdata d lock_range →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem)
(Swhile f_mcs_lock_init_while_condition
f_mcs_lock_init_while_body) E0 le´ (m, d´) Out_normal.
Proof.
intros.
generalize (mcs_lock_init_loop_correct_aux m d H0 H1).
unfold mcs_lock_init_loop_body_P.
unfold mcs_lock_init_loop_body_Q.
intro LP.
refine (_ (LoopProofSimpleWhile.termination _ _ _ _ _ _ LP le (m, d) _)).
intro pre.
destruct pre as [le´´ tmppre].
destruct tmppre as [m´´ tmppre].
destruct tmppre as [stmp m´´val].
∃ le´´.
subst.
assumption.
auto.
Qed.
Lemma mcs_lock_init_body_correct:
∀ m d d´ env le mbi_adr,
env = PTree.empty _ →
PTree.get _mbi_adr le = Some (Vint mbi_adr) →
PTree.get _i le = Some Vundef →
ticket_lock_init_spec (Int.unsigned mbi_adr) d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_mcs_lock_init_body E0 le´ (m, d´) Out_normal.
Proof.
intros.
subst.
functional inversion H2; subst.
simpl in ×.
set (df := (((((((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: real_multi_log (multi_log d)}).
fold df in H2.
set (di := (((((((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})).
fold di in df.
exploit (mcs_lock_init_loop_correct m di df (PTree.set _i (Vint (Int.repr 0))
(set_opttemp None Vundef le)));
unfold di in *; simpl in *; try assumption.
- repeat vcgen.
- reflexivity.
- unfold mcs_lock_init_mk_rdata.
unfold df.
unfold real_multi_log.
Opaque real_multi_log_pb.
simpl.
reflexivity.
Transparent real_multi_log_pb.
-
intros.
fold di in H.
destruct H as (le´, H).
unfold f_mcs_lock_init_body; subst.
esplit.
repeat vcgen.
Qed.
End MCSLOCKINITBODY.
Theorem mcs_lock_init_code_correct:
spec_le (ticket_lock_init ↦ mcs_lock_init_spec_low) (〚ticket_lock_init ↦ f_mcs_lock_init 〛L).
Proof.
set (L´ := L) in ×.
unfold L in ×.
fbigstep_pre L´.
fbigstep (mcs_lock_init_body_correct s (Genv.globalenv p)
makeglobalenv b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_mcs_lock_init)
(Vint mbi_adr::nil)
(create_undef_temps (fn_temps f_mcs_lock_init)))) muval.
Qed.
End MCSLOCKINIT.
End WithPrimitives.
End MMCSLOCKINTROCODEMCSLOCKINIT.
adt {multi_log: real_multi_log_pb (Z.to_nat index) (multi_log adt)}.
Lemma real_multi_log_pb_exists:
∀ n (d: RData), ∃ d´, (d {multi_log : real_multi_log_pb n (multi_log d)}) = d´.
Proof.
clearAll.
induction n; intros.
∃ (d {multi_log: real_multi_log_pb 0 (multi_log d)}); auto.
destruct IHn with d as (d´, H); simpl.
∃ (d {multi_log : ZMap.set (Z.of_nat n) (MultiDef nil)
(multi_log d´)}).
Opaque real_multi_log_pb.
clear IHn.
destruct d; destruct d´; simpl in ×.
inv H; simpl.
repeat f_equal.
Transparent real_multi_log_pb.
Qed.
Lemma real_multi_log_pb_flags_same :
∀ n d d´,
ikern d = true ∧ ihost d = true ∧ init d = true →
(d {multi_log: real_multi_log_pb n (multi_log d)} = d´) →
ikern d´ = true ∧ ihost d´ = true ∧ init d´ = true.
Proof.
Transparent real_multi_log_pb.
clearAll.
induction n; intros.
unfold real_multi_log_pb in H0.
destruct d; destruct d´.
inv H0; subst.
simpl in ×.
tauto.
destruct real_multi_log_pb_exists with (n := n) (d := d) as (d´´, H1).
eapply IHn with (2:= H1) in H.
simpl in H0.
clear IHn.
destruct d; destruct d´; destruct d´´; simpl in ×.
inv H1; inv H0; auto.
Qed.
Lemma mcs_lock_mk_rdata_flags_same :
∀ n d d´, ikern d = true ∧ ihost d = true ∧ init d = true→
mcs_lock_init_mk_rdata d n = d´ →
ikern d´ = true ∧ ihost d´ = true ∧ init d´ = true.
Proof.
clearAll.
unfold mcs_lock_init_mk_rdata.
intros.
eauto using real_multi_log_pb_flags_same.
Qed.
Section mcs_lock_init_loop_proof.
Variable minit: memb.
Variable adt: RData.
Hypothesis iikern: ikern adt = true.
Hypothesis iihost: ihost adt = true.
Hypothesis iinit: init adt = true.
Hypothesis hinv: high_level_invariant adt.
Definition mcs_lock_init_loop_body_P (le: temp_env) (m: mem): Prop :=
PTree.get _i le = Some (Vint Int.zero) ∧
ikern adt = true ∧
ihost adt = true ∧
init adt = true ∧
m = (minit, adt).
Definition mcs_lock_init_loop_body_Q (le : temp_env) (m: mem): Prop :=
m = (minit, mcs_lock_init_mk_rdata adt lock_range).
Lemma mcs_lock_init_loop_correct_aux : LoopProofSimpleWhile.t f_mcs_lock_init_while_condition
f_mcs_lock_init_while_body ge
(PTree.empty _)
(mcs_lock_init_loop_body_P)
(mcs_lock_init_loop_body_Q).
Proof.
generalize max_unsigned_val; intro muval.
assert (lock_range0: lock_range = (num_chan + num_chan + 1)) by (unfold lock_range; simpl; omega).
apply LoopProofSimpleWhile.make with
(W := Z)
(lt := fun z1 z2 ⇒ (0 ≤ z2 ∧ z1 < z2)%Z)
(I := fun le m w ⇒ ∃ i,
PTree.get _i le = Some (Vint i) ∧
0 ≤ Int.unsigned i ≤ lock_range ∧
ikern adt = true ∧
ihost adt = true ∧
init adt = true ∧
((Int.unsigned i = 0 ∧ m = (minit, adt)) ∨
(Int.unsigned i > 0 ∧ m = (minit, mcs_lock_init_mk_rdata adt (Int.unsigned i)))) ∧
w = lock_range - Int.unsigned i
).
- apply Zwf_well_founded.
- intros.
unfold mcs_lock_init_loop_body_P in H; subst.
destruct H as [_ile tmpH].
destruct tmpH as [iikern´ tmpH].
destruct tmpH as [iihost´ tmpH].
destruct tmpH as [iinit´ tmpH].
subst.
esplit.
esplit.
change (Int.zero) with (Int.repr 0) in _ile.
repeat vcgen.
- intros.
destruct H as [i tmpH].
destruct tmpH as [_ile tmpH].
destruct tmpH as [irange tmpH].
destruct tmpH as [iikern´ tmpH].
destruct tmpH as [iihost´ tmpH].
destruct tmpH as [iinit´ tmpH].
destruct tmpH as [icond H]; subst.
destruct irange as [ilow ihigh].
apply Zle_lt_or_eq in ihigh.
destruct m.
Caseeq ihigh; intros.
+
Caseeq icond; intros.
×
destruct H0.
inv H1.
esplit; esplit.
repeat vcgen.
esplit; esplit.
unfold f_mcs_lock_init_while_body; subst.
repeat vcgen.
∃ (num_chan + num_chan).
repeat vcgen.
esplit.
repeat vcgen.
right.
split.
omega.
unfold mcs_lock_init_mk_rdata.
simpl.
rewrite H0.
simpl.
reflexivity.
×
destruct H0.
inv H1.
esplit; esplit.
repeat vcgen.
esplit; esplit.
unfold f_mcs_lock_init_while_body; subst.
repeat vcgen.
unfold mcs_init_node_spec.
simpl.
rewrite iikern, iihost.
rewrite zle_lt_true.
reflexivity.
omega.
∃ ((num_chan + num_chan + 1) - Int.unsigned i - 1).
repeat vcgen.
esplit.
repeat vcgen.
right.
split.
omega.
f_equal.
unfold mcs_lock_init_mk_rdata; simpl.
change (Int.unsigned i + 1) with (Z.succ (Int.unsigned i)).
rewrite Z2Nat.inj_succ with (n:=(Int.unsigned i)) in *; [ | omega].
simpl.
rewrite Z2Nat.id; [ | assumption].
repeat vcgen.
+
unfold mcs_lock_init_loop_body_Q.
esplit; esplit.
repeat vcgen.
simpl.
Caseeq icond; intro icond´; destruct icond´ as [iv mval].
× exfalso; rewrite iv in H; inv H.
× rewrite H in mval; trivial.
Qed.
End mcs_lock_init_loop_proof.
Lemma mcs_lock_init_loop_correct: ∀ m d d´ le,
PTree.get _i le = Some (Vint Int.zero) →
ikern d = true →
ihost d = true →
init d = true →
d´ = mcs_lock_init_mk_rdata d lock_range →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem)
(Swhile f_mcs_lock_init_while_condition
f_mcs_lock_init_while_body) E0 le´ (m, d´) Out_normal.
Proof.
intros.
generalize (mcs_lock_init_loop_correct_aux m d H0 H1).
unfold mcs_lock_init_loop_body_P.
unfold mcs_lock_init_loop_body_Q.
intro LP.
refine (_ (LoopProofSimpleWhile.termination _ _ _ _ _ _ LP le (m, d) _)).
intro pre.
destruct pre as [le´´ tmppre].
destruct tmppre as [m´´ tmppre].
destruct tmppre as [stmp m´´val].
∃ le´´.
subst.
assumption.
auto.
Qed.
Lemma mcs_lock_init_body_correct:
∀ m d d´ env le mbi_adr,
env = PTree.empty _ →
PTree.get _mbi_adr le = Some (Vint mbi_adr) →
PTree.get _i le = Some Vundef →
ticket_lock_init_spec (Int.unsigned mbi_adr) d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_mcs_lock_init_body E0 le´ (m, d´) Out_normal.
Proof.
intros.
subst.
functional inversion H2; subst.
simpl in ×.
set (df := (((((((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: real_multi_log (multi_log d)}).
fold df in H2.
set (di := (((((((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})).
fold di in df.
exploit (mcs_lock_init_loop_correct m di df (PTree.set _i (Vint (Int.repr 0))
(set_opttemp None Vundef le)));
unfold di in *; simpl in *; try assumption.
- repeat vcgen.
- reflexivity.
- unfold mcs_lock_init_mk_rdata.
unfold df.
unfold real_multi_log.
Opaque real_multi_log_pb.
simpl.
reflexivity.
Transparent real_multi_log_pb.
-
intros.
fold di in H.
destruct H as (le´, H).
unfold f_mcs_lock_init_body; subst.
esplit.
repeat vcgen.
Qed.
End MCSLOCKINITBODY.
Theorem mcs_lock_init_code_correct:
spec_le (ticket_lock_init ↦ mcs_lock_init_spec_low) (〚ticket_lock_init ↦ f_mcs_lock_init 〛L).
Proof.
set (L´ := L) in ×.
unfold L in ×.
fbigstep_pre L´.
fbigstep (mcs_lock_init_body_correct s (Genv.globalenv p)
makeglobalenv b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp
m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_mcs_lock_init)
(Vint mbi_adr::nil)
(create_undef_temps (fn_temps f_mcs_lock_init)))) muval.
Qed.
End MCSLOCKINIT.
End WithPrimitives.
End MMCSLOCKINTROCODEMCSLOCKINIT.