Library mcertikos.mcslock.MCSLockIntroGenLink
Require Import LinkTemplate.
Require Import MMCSLockIntro.
Require Import MCSLockIntroGen.
Require Import MCSLockIntroGenLinkSource.
Require Import MCSMCurID.
Require Import MCSMCurIDCSource.
Require Import MCSMCurIDCode.
Require Import MCSLockIntroGenAsm.
Require Import CDataTypes.
Section WITHCOMPCERTIKOS.
Context `{compcertikos_prf: CompCertiKOS} `{real_params_prf: RealParams}.
Context `{mcs_oracle_prop: MCSOracleProp}.
Lemma mcs_lock_st_size_val : mcs_lock_st_size = 576.
Proof.
reflexivity.
Qed.
Lemma lock_range_val : lock_range = num_chan + num_chan + 1.
Proof. reflexivity. Qed.
Lemma make_program_find_symbol (CTXT md : module)(m : mem) s :
(p <- make_program s (CTXT ⊕ (md
⊕ MCS_LOCK_LOC ↦ mcslock_loc_type) ⊕ ∅) (mcurid ⊕ L64);
ret (Genv.init_mem p) = OK (Some m))
→ ∃ b, find_symbol s MCS_LOCK_LOC = Some b ∧
∀ index, 0 ≤ index < lock_range →
Mem.valid_access m Mint32 b (tail_pos index) Writable ∧
Mem.valid_access m Mint32 b (next_pos index 0) Writable ∧
Mem.valid_access m Mint32 b (busy_pos index 0) Writable ∧
Mem.valid_access m Mint32 b (next_pos index 1) Writable ∧
Mem.valid_access m Mint32 b (busy_pos index 1) Writable ∧
Mem.valid_access m Mint32 b (next_pos index 2) Writable ∧
Mem.valid_access m Mint32 b (busy_pos index 2) Writable ∧
Mem.valid_access m Mint32 b (next_pos index 3) Writable ∧
Mem.valid_access m Mint32 b (busy_pos index 3) Writable ∧
Mem.valid_access m Mint32 b (next_pos index 4) Writable ∧
Mem.valid_access m Mint32 b (busy_pos index 4) Writable ∧
Mem.valid_access m Mint32 b (next_pos index 5) Writable ∧
Mem.valid_access m Mint32 b (busy_pos index 5) Writable ∧
Mem.valid_access m Mint32 b (next_pos index 6) Writable ∧
Mem.valid_access m Mint32 b (busy_pos index 6) Writable ∧
Mem.valid_access m Mint32 b (next_pos index 7) Writable ∧
Mem.valid_access m Mint32 b (busy_pos index 7) Writable.
Proof.
intros mkprog; inv_monad´ mkprog.
assert (mkgenv := make_program_make_globalenv _ _ _ _ mkprog0).
pose proof mkgenv as mkgenv´.
eapply make_globalenv_stencil_matches in mkgenv´.
inv_make_globalenv mkgenv. subst.
rewrite (stencil_matches_symbols _ _ mkgenv´) in ×. inv mkgenv´.
eexists; split; try eassumption.
specialize (Genv.init_mem_characterization _ _ Hbvi H0); eauto.
unfold Genv.perm_globvar; simpl; intros [Hperm _].
change (Z.max 1198656 0) with 1198656 in Hperm.
intros; repeat split; try (unfold next_pos); try (unfold busy_pos); try (unfold tail_pos); try rewrite lock_range_val in ×.
- unfold Mem.range_perm; intros; apply Hperm.
simpl in H.
unfold mcs_lock_st_size in H1.
replace ((8 × (2 + 14) + (15 + 1)) × 4) with 576 in H1; try ring.
unfold size_chunk in H1.
omega.
- unfold mcs_lock_st_size.
replace ((8 × (2 + 14) + (15 + 1)) × 4 × index) with ((index × 144) × 4) by ring.
eexists; reflexivity.
- unfold Mem.range_perm; intros; apply Hperm.
unfold mcs_lock_st_size in H1.
replace ((8 × (2 + 14) + (15 + 1)) × 4) with 576 in H1; try ring.
unfold size_chunk in H1.
omega.
- unfold mcs_lock_st_size.
unfold mcs_node_st_size.
replace ((8 × (2 + 14) + (15 + 1)) × 4 × index + 64 + 64 × 0) with ((index × 144 + 16) × 4) by ring.
eexists; reflexivity.
- unfold Mem.range_perm; intros; apply Hperm.
unfold mcs_lock_st_size in H1.
replace ((8 × (2 + 14) + (15 + 1)) × 4) with 576 in H1; try ring.
unfold size_chunk in H1.
omega.
- unfold mcs_lock_st_size.
unfold mcs_node_st_size.
replace ((8 × (2 + 14) + (15 + 1)) × 4 × index + 64 + 64 × 0 + 4) with ((index × 144 + 16 + 1) × 4) by ring.
eexists; reflexivity.
- unfold Mem.range_perm; intros; apply Hperm.
unfold mcs_lock_st_size in H1.
unfold mcs_node_st_size in H1.
replace ((8 × (2 + 14) + (15 + 1)) × 4) with 576 in H1; try ring.
unfold size_chunk in H1.
omega.
- unfold mcs_lock_st_size.
unfold mcs_node_st_size.
replace ((8 × (2 + 14) + (15 + 1)) × 4 × index + 64 + 64 × 1) with ((index × 144 + 16 + 16) × 4) by ring.
eexists; reflexivity.
- unfold Mem.range_perm; intros; apply Hperm.
unfold mcs_lock_st_size in H1.
unfold mcs_node_st_size in H1.
replace ((8 × (2 + 14) + (15 + 1)) × 4) with 576 in H1; try ring.
unfold size_chunk in H1.
omega.
- unfold mcs_lock_st_size.
unfold mcs_node_st_size.
replace ((8 × (2 + 14) + (15 + 1)) × 4 × index + 64 + 64 × 1 + 4) with ((index × 144 + 16 + 16 + 1) × 4) by ring.
eexists; reflexivity.
- unfold Mem.range_perm; intros; apply Hperm.
unfold mcs_lock_st_size in H1.
unfold mcs_node_st_size in H1.
replace ((8 × (2 + 14) + (15 + 1)) × 4) with 576 in H1; try ring.
unfold size_chunk in H1.
omega.
- unfold mcs_lock_st_size.
unfold mcs_node_st_size.
replace ((8 × (2 + 14) + (15 + 1)) × 4 × index + 64 + 64 × 2) with ((index × 144 + 16 + 16 × 2) × 4) by ring.
eexists; reflexivity.
- unfold Mem.range_perm; intros; apply Hperm.
unfold mcs_lock_st_size in H1.
unfold mcs_node_st_size in H1.
replace ((8 × (2 + 14) + (15 + 1)) × 4) with 576 in H1; try ring.
unfold size_chunk in H1.
omega.
- unfold mcs_lock_st_size.
unfold mcs_node_st_size.
replace ((8 × (2 + 14) + (15 + 1)) × 4 × index + 64 + 64 × 2 + 4) with ((index × 144 + 16 + 16 × 2 + 1) × 4) by ring.
eexists; reflexivity.
- unfold Mem.range_perm; intros; apply Hperm.
unfold mcs_lock_st_size in H1.
unfold mcs_node_st_size in H1.
replace ((8 × (2 + 14) + (15 + 1)) × 4) with 576 in H1; try ring.
unfold size_chunk in H1.
omega.
- unfold mcs_lock_st_size.
unfold mcs_node_st_size.
replace ((8 × (2 + 14) + (15 + 1)) × 4 × index + 64 + 64 × 3) with ((index × 144 + 16 + 16 × 3) × 4) by ring.
eexists; reflexivity.
- unfold Mem.range_perm; intros; apply Hperm.
unfold mcs_lock_st_size in H1.
unfold mcs_node_st_size in H1.
replace ((8 × (2 + 14) + (15 + 1)) × 4) with 576 in H1; try ring.
unfold size_chunk in H1.
omega.
- unfold mcs_lock_st_size.
unfold mcs_node_st_size.
replace ((8 × (2 + 14) + (15 + 1)) × 4 × index + 64 + 64 × 3 + 4) with ((index × 144 + 16 + 16 × 3 + 1) × 4) by ring.
eexists; reflexivity.
- unfold Mem.range_perm; intros; apply Hperm.
unfold mcs_lock_st_size in H1.
unfold mcs_node_st_size in H1.
replace ((8 × (2 + 14) + (15 + 1)) × 4) with 576 in H1; try ring.
unfold size_chunk in H1.
omega.
- unfold mcs_lock_st_size.
unfold mcs_node_st_size.
replace ((8 × (2 + 14) + (15 + 1)) × 4 × index + 64 + 64 × 4) with ((index × 144 + 16 + 16 × 4) × 4) by ring.
eexists; reflexivity.
- unfold Mem.range_perm; intros; apply Hperm.
unfold mcs_lock_st_size in H1.
unfold mcs_node_st_size in H1.
replace ((8 × (2 + 14) + (15 + 1)) × 4) with 576 in H1; try ring.
unfold size_chunk in H1.
omega.
- unfold mcs_lock_st_size.
unfold mcs_node_st_size.
replace ((8 × (2 + 14) + (15 + 1)) × 4 × index + 64 + 64 × 4 + 4) with ((index × 144 + 16 + 16 × 4 + 1) × 4) by ring.
eexists; reflexivity.
- unfold Mem.range_perm; intros; apply Hperm.
unfold mcs_lock_st_size in H1.
unfold mcs_node_st_size in H1.
replace ((8 × (2 + 14) + (15 + 1)) × 4) with 576 in H1; try ring.
unfold size_chunk in H1.
omega.
- unfold mcs_lock_st_size.
unfold mcs_node_st_size.
replace ((8 × (2 + 14) + (15 + 1)) × 4 × index + 64 + 64 × 5) with ((index × 144 + 16 + 16 × 5) × 4) by ring.
eexists; reflexivity.
- unfold Mem.range_perm; intros; apply Hperm.
unfold mcs_lock_st_size in H1.
unfold mcs_node_st_size in H1.
replace ((8 × (2 + 14) + (15 + 1)) × 4) with 576 in H1; try ring.
unfold size_chunk in H1.
omega.
- unfold mcs_lock_st_size.
unfold mcs_node_st_size.
replace ((8 × (2 + 14) + (15 + 1)) × 4 × index + 64 + 64 × 5 + 4) with ((index × 144 + 16 + 16 × 5 + 1) × 4) by ring.
eexists; reflexivity.
- unfold Mem.range_perm; intros; apply Hperm.
unfold mcs_lock_st_size in H1.
unfold mcs_node_st_size in H1.
replace ((8 × (2 + 14) + (15 + 1)) × 4) with 576 in H1; try ring.
unfold size_chunk in H1.
omega.
- unfold mcs_lock_st_size.
unfold mcs_node_st_size.
replace ((8 × (2 + 14) + (15 + 1)) × 4 × index + 64 + 64 × 6) with ((index × 144 + 16 + 16 × 6) × 4) by ring.
eexists; reflexivity.
- unfold Mem.range_perm; intros; apply Hperm.
unfold mcs_lock_st_size in H1.
unfold mcs_node_st_size in H1.
replace ((8 × (2 + 14) + (15 + 1)) × 4) with 576 in H1; try ring.
unfold size_chunk in H1.
omega.
- unfold mcs_lock_st_size.
unfold mcs_node_st_size.
replace ((8 × (2 + 14) + (15 + 1)) × 4 × index + 64 + 64 × 6 + 4) with ((index × 144 + 16 + 16 × 6 + 1) × 4) by ring.
eexists; reflexivity.
- unfold Mem.range_perm; intros; apply Hperm.
unfold mcs_lock_st_size in H1.
unfold mcs_node_st_size in H1.
replace ((8 × (2 + 14) + (15 + 1)) × 4) with 576 in H1; try ring.
unfold size_chunk in H1.
omega.
- unfold mcs_lock_st_size.
unfold mcs_node_st_size.
replace ((8 × (2 + 14) + (15 + 1)) × 4 × index + 64 + 64 × 7) with ((index × 144 + 16 + 16 × 7) × 4) by ring.
eexists; reflexivity.
- unfold Mem.range_perm; intros; apply Hperm.
unfold mcs_lock_st_size in H1.
unfold mcs_node_st_size in H1.
replace ((8 × (2 + 14) + (15 + 1)) × 4) with 576 in H1; try ring.
unfold size_chunk in H1.
omega.
- unfold mcs_lock_st_size.
unfold mcs_node_st_size.
replace ((8 × (2 + 14) + (15 + 1)) × 4 × index + 64 + 64 × 7 + 4) with ((index × 144 + 16 + 16 × 7 + 1) × 4) by ring.
eexists; reflexivity.
Qed.
Lemma init_correct:
init_correct_type MMCSLockIntro_module mcurid mmcslockintro.
Proof.
init_correct.
-
exploit make_program_find_symbol; eauto.
intros (b´ & find_symbol_MCS_LCOK_LOC & access).
rename b into b3; rename b2 into b.
assert (b´ = b) by congruence; subst.
econstructor; try eassumption; intros.
specialize (access _ Hvalid).
destruct access as (acc_la & acc_ne0 & acc_bs0 & acc_ne1 & acc_bs1 & acc_ne2 & acc_bs2 & acc_ne3 & acc_bs3
& acc_ne4 & acc_bs4 & acc_ne5 & acc_bs5 & acc_ne6 & acc_bs6 & acc_ne7 & acc_bs7).
assert (readable_la : Mem.valid_access m2 Mint32 b (tail_pos lock_index) Readable).
{ eapply Mem.valid_access_implies; try eassumption; econstructor. }
assert (readable_ne0 : Mem.valid_access m2 Mint32 b (next_pos lock_index 0) Readable).
{ eapply Mem.valid_access_implies; try eassumption; econstructor. }
assert (readable_bs0 : Mem.valid_access m2 Mint32 b (busy_pos lock_index 0) Readable).
{ eapply Mem.valid_access_implies; try eassumption; econstructor. }
assert (readable_ne1 : Mem.valid_access m2 Mint32 b (next_pos lock_index 1) Readable).
{ eapply Mem.valid_access_implies; try eassumption; econstructor. }
assert (readable_bs1 : Mem.valid_access m2 Mint32 b (busy_pos lock_index 1) Readable).
{ eapply Mem.valid_access_implies; try eassumption; econstructor. }
assert (readable_ne2 : Mem.valid_access m2 Mint32 b (next_pos lock_index 2) Readable).
{ eapply Mem.valid_access_implies; try eassumption; econstructor. }
assert (readable_bs2 : Mem.valid_access m2 Mint32 b (busy_pos lock_index 2) Readable).
{ eapply Mem.valid_access_implies; try eassumption; econstructor. }
assert (readable_ne3 : Mem.valid_access m2 Mint32 b (next_pos lock_index 3) Readable).
{ eapply Mem.valid_access_implies; try eassumption; econstructor. }
assert (readable_bs3 : Mem.valid_access m2 Mint32 b (busy_pos lock_index 3) Readable).
{ eapply Mem.valid_access_implies; try eassumption; econstructor. }
assert (readable_ne4 : Mem.valid_access m2 Mint32 b (next_pos lock_index 4) Readable).
{ eapply Mem.valid_access_implies; try eassumption; econstructor. }
assert (readable_bs4 : Mem.valid_access m2 Mint32 b (busy_pos lock_index 4) Readable).
{ eapply Mem.valid_access_implies; try eassumption; econstructor. }
assert (readable_ne5 : Mem.valid_access m2 Mint32 b (next_pos lock_index 5) Readable).
{ eapply Mem.valid_access_implies; try eassumption; econstructor. }
assert (readable_bs5 : Mem.valid_access m2 Mint32 b (busy_pos lock_index 5) Readable).
{ eapply Mem.valid_access_implies; try eassumption; econstructor. }
assert (readable_ne6 : Mem.valid_access m2 Mint32 b (next_pos lock_index 6) Readable).
{ eapply Mem.valid_access_implies; try eassumption; econstructor. }
assert (readable_bs6 : Mem.valid_access m2 Mint32 b (busy_pos lock_index 6) Readable).
{ eapply Mem.valid_access_implies; try eassumption; econstructor. }
assert (readable_ne7 : Mem.valid_access m2 Mint32 b (next_pos lock_index 7) Readable).
{ eapply Mem.valid_access_implies; try eassumption; econstructor. }
assert (readable_bs7 : Mem.valid_access m2 Mint32 b (busy_pos lock_index 7) Readable).
{ eapply Mem.valid_access_implies; try eassumption; econstructor. }
destruct (Mem.valid_access_load _ _ _ _ readable_la) as [v_la load_la].
destruct (Mem.valid_access_load _ _ _ _ readable_ne0) as [v_ne0 load_ne0].
destruct (Mem.valid_access_load _ _ _ _ readable_bs0) as [v_bs0 load_bs0].
destruct (Mem.valid_access_load _ _ _ _ readable_ne1) as [v_ne1 load_ne1].
destruct (Mem.valid_access_load _ _ _ _ readable_bs1) as [v_bs1 load_bs1].
destruct (Mem.valid_access_load _ _ _ _ readable_ne2) as [v_ne2 load_ne2].
destruct (Mem.valid_access_load _ _ _ _ readable_bs2) as [v_bs2 load_bs2].
destruct (Mem.valid_access_load _ _ _ _ readable_ne3) as [v_ne3 load_ne3].
destruct (Mem.valid_access_load _ _ _ _ readable_bs3) as [v_bs3 load_bs3].
destruct (Mem.valid_access_load _ _ _ _ readable_ne4) as [v_ne4 load_ne4].
destruct (Mem.valid_access_load _ _ _ _ readable_bs4) as [v_bs4 load_bs4].
destruct (Mem.valid_access_load _ _ _ _ readable_ne5) as [v_ne5 load_ne5].
destruct (Mem.valid_access_load _ _ _ _ readable_bs5) as [v_bs5 load_bs5].
destruct (Mem.valid_access_load _ _ _ _ readable_ne6) as [v_ne6 load_ne6].
destruct (Mem.valid_access_load _ _ _ _ readable_bs6) as [v_bs6 load_bs6].
destruct (Mem.valid_access_load _ _ _ _ readable_ne7) as [v_ne7 load_ne7].
destruct (Mem.valid_access_load _ _ _ _ readable_bs7) as [v_bs7 load_bs7].
∃ v_la, v_bs0, v_ne0, v_bs1, v_ne1, v_bs2, v_ne2, v_bs3, v_ne3,
v_bs4, v_ne4, v_bs5, v_ne5, v_bs6, v_ne6, v_bs7, v_ne7.
repeat (split; [ eassumption|]).
rewrite ZMap.gi.
econstructor.
Qed.
Lemma link_correct_aux:
link_correct_aux_type MMCSLockIntro_module mcurid mmcslockintro.
Proof.
link_correct_aux.
- link_cfunction mcs_init_node_spec_ref MMCSMCurIDCODE.mcs_init_node_code_correct.
- link_cfunction mcs_GET_NEXT_spec_ref MMCSMCurIDCODE.mcs_GET_NEXT_code_correct.
- link_cfunction mcs_SET_NEXT_spec_ref MMCSMCurIDCODE.mcs_SET_NEXT_code_correct.
- link_cfunction mcs_GET_BUSY_spec_ref MMCSMCurIDCODE.mcs_GET_BUSY_code_correct.
- link_cfunction mcs_SET_BUSY_spec_ref MMCSMCurIDCODE.mcs_SET_BUSY_code_correct.
- link_asmfunction mcs_log_spec_ref mcs_log_code_correct.
- link_asmfunction mcs_SWAP_TAIL_spec_ref mcs_SWAP_TAIL_code_correct.
- link_asmfunction mcs_CAS_TAIL_spec_ref mcs_CAS_TAIL_code_correct.
- apply passthrough_correct.
Qed.
Theorem cl_backward_simulation:
cl_backward_simulation_type MMCSLockIntro_module mcurid mmcslockintro.
Proof.
cl_backward_simulation init_correct link_correct_aux.
Qed.
Theorem make_program_exists:
make_program_exist_type MMCSLockIntro_module mcurid mmcslockintro.
Proof.
make_program_exists link_correct_aux.
Qed.
End WITHCOMPCERTIKOS.
Require Import MMCSLockIntro.
Require Import MCSLockIntroGen.
Require Import MCSLockIntroGenLinkSource.
Require Import MCSMCurID.
Require Import MCSMCurIDCSource.
Require Import MCSMCurIDCode.
Require Import MCSLockIntroGenAsm.
Require Import CDataTypes.
Section WITHCOMPCERTIKOS.
Context `{compcertikos_prf: CompCertiKOS} `{real_params_prf: RealParams}.
Context `{mcs_oracle_prop: MCSOracleProp}.
Lemma mcs_lock_st_size_val : mcs_lock_st_size = 576.
Proof.
reflexivity.
Qed.
Lemma lock_range_val : lock_range = num_chan + num_chan + 1.
Proof. reflexivity. Qed.
Lemma make_program_find_symbol (CTXT md : module)(m : mem) s :
(p <- make_program s (CTXT ⊕ (md
⊕ MCS_LOCK_LOC ↦ mcslock_loc_type) ⊕ ∅) (mcurid ⊕ L64);
ret (Genv.init_mem p) = OK (Some m))
→ ∃ b, find_symbol s MCS_LOCK_LOC = Some b ∧
∀ index, 0 ≤ index < lock_range →
Mem.valid_access m Mint32 b (tail_pos index) Writable ∧
Mem.valid_access m Mint32 b (next_pos index 0) Writable ∧
Mem.valid_access m Mint32 b (busy_pos index 0) Writable ∧
Mem.valid_access m Mint32 b (next_pos index 1) Writable ∧
Mem.valid_access m Mint32 b (busy_pos index 1) Writable ∧
Mem.valid_access m Mint32 b (next_pos index 2) Writable ∧
Mem.valid_access m Mint32 b (busy_pos index 2) Writable ∧
Mem.valid_access m Mint32 b (next_pos index 3) Writable ∧
Mem.valid_access m Mint32 b (busy_pos index 3) Writable ∧
Mem.valid_access m Mint32 b (next_pos index 4) Writable ∧
Mem.valid_access m Mint32 b (busy_pos index 4) Writable ∧
Mem.valid_access m Mint32 b (next_pos index 5) Writable ∧
Mem.valid_access m Mint32 b (busy_pos index 5) Writable ∧
Mem.valid_access m Mint32 b (next_pos index 6) Writable ∧
Mem.valid_access m Mint32 b (busy_pos index 6) Writable ∧
Mem.valid_access m Mint32 b (next_pos index 7) Writable ∧
Mem.valid_access m Mint32 b (busy_pos index 7) Writable.
Proof.
intros mkprog; inv_monad´ mkprog.
assert (mkgenv := make_program_make_globalenv _ _ _ _ mkprog0).
pose proof mkgenv as mkgenv´.
eapply make_globalenv_stencil_matches in mkgenv´.
inv_make_globalenv mkgenv. subst.
rewrite (stencil_matches_symbols _ _ mkgenv´) in ×. inv mkgenv´.
eexists; split; try eassumption.
specialize (Genv.init_mem_characterization _ _ Hbvi H0); eauto.
unfold Genv.perm_globvar; simpl; intros [Hperm _].
change (Z.max 1198656 0) with 1198656 in Hperm.
intros; repeat split; try (unfold next_pos); try (unfold busy_pos); try (unfold tail_pos); try rewrite lock_range_val in ×.
- unfold Mem.range_perm; intros; apply Hperm.
simpl in H.
unfold mcs_lock_st_size in H1.
replace ((8 × (2 + 14) + (15 + 1)) × 4) with 576 in H1; try ring.
unfold size_chunk in H1.
omega.
- unfold mcs_lock_st_size.
replace ((8 × (2 + 14) + (15 + 1)) × 4 × index) with ((index × 144) × 4) by ring.
eexists; reflexivity.
- unfold Mem.range_perm; intros; apply Hperm.
unfold mcs_lock_st_size in H1.
replace ((8 × (2 + 14) + (15 + 1)) × 4) with 576 in H1; try ring.
unfold size_chunk in H1.
omega.
- unfold mcs_lock_st_size.
unfold mcs_node_st_size.
replace ((8 × (2 + 14) + (15 + 1)) × 4 × index + 64 + 64 × 0) with ((index × 144 + 16) × 4) by ring.
eexists; reflexivity.
- unfold Mem.range_perm; intros; apply Hperm.
unfold mcs_lock_st_size in H1.
replace ((8 × (2 + 14) + (15 + 1)) × 4) with 576 in H1; try ring.
unfold size_chunk in H1.
omega.
- unfold mcs_lock_st_size.
unfold mcs_node_st_size.
replace ((8 × (2 + 14) + (15 + 1)) × 4 × index + 64 + 64 × 0 + 4) with ((index × 144 + 16 + 1) × 4) by ring.
eexists; reflexivity.
- unfold Mem.range_perm; intros; apply Hperm.
unfold mcs_lock_st_size in H1.
unfold mcs_node_st_size in H1.
replace ((8 × (2 + 14) + (15 + 1)) × 4) with 576 in H1; try ring.
unfold size_chunk in H1.
omega.
- unfold mcs_lock_st_size.
unfold mcs_node_st_size.
replace ((8 × (2 + 14) + (15 + 1)) × 4 × index + 64 + 64 × 1) with ((index × 144 + 16 + 16) × 4) by ring.
eexists; reflexivity.
- unfold Mem.range_perm; intros; apply Hperm.
unfold mcs_lock_st_size in H1.
unfold mcs_node_st_size in H1.
replace ((8 × (2 + 14) + (15 + 1)) × 4) with 576 in H1; try ring.
unfold size_chunk in H1.
omega.
- unfold mcs_lock_st_size.
unfold mcs_node_st_size.
replace ((8 × (2 + 14) + (15 + 1)) × 4 × index + 64 + 64 × 1 + 4) with ((index × 144 + 16 + 16 + 1) × 4) by ring.
eexists; reflexivity.
- unfold Mem.range_perm; intros; apply Hperm.
unfold mcs_lock_st_size in H1.
unfold mcs_node_st_size in H1.
replace ((8 × (2 + 14) + (15 + 1)) × 4) with 576 in H1; try ring.
unfold size_chunk in H1.
omega.
- unfold mcs_lock_st_size.
unfold mcs_node_st_size.
replace ((8 × (2 + 14) + (15 + 1)) × 4 × index + 64 + 64 × 2) with ((index × 144 + 16 + 16 × 2) × 4) by ring.
eexists; reflexivity.
- unfold Mem.range_perm; intros; apply Hperm.
unfold mcs_lock_st_size in H1.
unfold mcs_node_st_size in H1.
replace ((8 × (2 + 14) + (15 + 1)) × 4) with 576 in H1; try ring.
unfold size_chunk in H1.
omega.
- unfold mcs_lock_st_size.
unfold mcs_node_st_size.
replace ((8 × (2 + 14) + (15 + 1)) × 4 × index + 64 + 64 × 2 + 4) with ((index × 144 + 16 + 16 × 2 + 1) × 4) by ring.
eexists; reflexivity.
- unfold Mem.range_perm; intros; apply Hperm.
unfold mcs_lock_st_size in H1.
unfold mcs_node_st_size in H1.
replace ((8 × (2 + 14) + (15 + 1)) × 4) with 576 in H1; try ring.
unfold size_chunk in H1.
omega.
- unfold mcs_lock_st_size.
unfold mcs_node_st_size.
replace ((8 × (2 + 14) + (15 + 1)) × 4 × index + 64 + 64 × 3) with ((index × 144 + 16 + 16 × 3) × 4) by ring.
eexists; reflexivity.
- unfold Mem.range_perm; intros; apply Hperm.
unfold mcs_lock_st_size in H1.
unfold mcs_node_st_size in H1.
replace ((8 × (2 + 14) + (15 + 1)) × 4) with 576 in H1; try ring.
unfold size_chunk in H1.
omega.
- unfold mcs_lock_st_size.
unfold mcs_node_st_size.
replace ((8 × (2 + 14) + (15 + 1)) × 4 × index + 64 + 64 × 3 + 4) with ((index × 144 + 16 + 16 × 3 + 1) × 4) by ring.
eexists; reflexivity.
- unfold Mem.range_perm; intros; apply Hperm.
unfold mcs_lock_st_size in H1.
unfold mcs_node_st_size in H1.
replace ((8 × (2 + 14) + (15 + 1)) × 4) with 576 in H1; try ring.
unfold size_chunk in H1.
omega.
- unfold mcs_lock_st_size.
unfold mcs_node_st_size.
replace ((8 × (2 + 14) + (15 + 1)) × 4 × index + 64 + 64 × 4) with ((index × 144 + 16 + 16 × 4) × 4) by ring.
eexists; reflexivity.
- unfold Mem.range_perm; intros; apply Hperm.
unfold mcs_lock_st_size in H1.
unfold mcs_node_st_size in H1.
replace ((8 × (2 + 14) + (15 + 1)) × 4) with 576 in H1; try ring.
unfold size_chunk in H1.
omega.
- unfold mcs_lock_st_size.
unfold mcs_node_st_size.
replace ((8 × (2 + 14) + (15 + 1)) × 4 × index + 64 + 64 × 4 + 4) with ((index × 144 + 16 + 16 × 4 + 1) × 4) by ring.
eexists; reflexivity.
- unfold Mem.range_perm; intros; apply Hperm.
unfold mcs_lock_st_size in H1.
unfold mcs_node_st_size in H1.
replace ((8 × (2 + 14) + (15 + 1)) × 4) with 576 in H1; try ring.
unfold size_chunk in H1.
omega.
- unfold mcs_lock_st_size.
unfold mcs_node_st_size.
replace ((8 × (2 + 14) + (15 + 1)) × 4 × index + 64 + 64 × 5) with ((index × 144 + 16 + 16 × 5) × 4) by ring.
eexists; reflexivity.
- unfold Mem.range_perm; intros; apply Hperm.
unfold mcs_lock_st_size in H1.
unfold mcs_node_st_size in H1.
replace ((8 × (2 + 14) + (15 + 1)) × 4) with 576 in H1; try ring.
unfold size_chunk in H1.
omega.
- unfold mcs_lock_st_size.
unfold mcs_node_st_size.
replace ((8 × (2 + 14) + (15 + 1)) × 4 × index + 64 + 64 × 5 + 4) with ((index × 144 + 16 + 16 × 5 + 1) × 4) by ring.
eexists; reflexivity.
- unfold Mem.range_perm; intros; apply Hperm.
unfold mcs_lock_st_size in H1.
unfold mcs_node_st_size in H1.
replace ((8 × (2 + 14) + (15 + 1)) × 4) with 576 in H1; try ring.
unfold size_chunk in H1.
omega.
- unfold mcs_lock_st_size.
unfold mcs_node_st_size.
replace ((8 × (2 + 14) + (15 + 1)) × 4 × index + 64 + 64 × 6) with ((index × 144 + 16 + 16 × 6) × 4) by ring.
eexists; reflexivity.
- unfold Mem.range_perm; intros; apply Hperm.
unfold mcs_lock_st_size in H1.
unfold mcs_node_st_size in H1.
replace ((8 × (2 + 14) + (15 + 1)) × 4) with 576 in H1; try ring.
unfold size_chunk in H1.
omega.
- unfold mcs_lock_st_size.
unfold mcs_node_st_size.
replace ((8 × (2 + 14) + (15 + 1)) × 4 × index + 64 + 64 × 6 + 4) with ((index × 144 + 16 + 16 × 6 + 1) × 4) by ring.
eexists; reflexivity.
- unfold Mem.range_perm; intros; apply Hperm.
unfold mcs_lock_st_size in H1.
unfold mcs_node_st_size in H1.
replace ((8 × (2 + 14) + (15 + 1)) × 4) with 576 in H1; try ring.
unfold size_chunk in H1.
omega.
- unfold mcs_lock_st_size.
unfold mcs_node_st_size.
replace ((8 × (2 + 14) + (15 + 1)) × 4 × index + 64 + 64 × 7) with ((index × 144 + 16 + 16 × 7) × 4) by ring.
eexists; reflexivity.
- unfold Mem.range_perm; intros; apply Hperm.
unfold mcs_lock_st_size in H1.
unfold mcs_node_st_size in H1.
replace ((8 × (2 + 14) + (15 + 1)) × 4) with 576 in H1; try ring.
unfold size_chunk in H1.
omega.
- unfold mcs_lock_st_size.
unfold mcs_node_st_size.
replace ((8 × (2 + 14) + (15 + 1)) × 4 × index + 64 + 64 × 7 + 4) with ((index × 144 + 16 + 16 × 7 + 1) × 4) by ring.
eexists; reflexivity.
Qed.
Lemma init_correct:
init_correct_type MMCSLockIntro_module mcurid mmcslockintro.
Proof.
init_correct.
-
exploit make_program_find_symbol; eauto.
intros (b´ & find_symbol_MCS_LCOK_LOC & access).
rename b into b3; rename b2 into b.
assert (b´ = b) by congruence; subst.
econstructor; try eassumption; intros.
specialize (access _ Hvalid).
destruct access as (acc_la & acc_ne0 & acc_bs0 & acc_ne1 & acc_bs1 & acc_ne2 & acc_bs2 & acc_ne3 & acc_bs3
& acc_ne4 & acc_bs4 & acc_ne5 & acc_bs5 & acc_ne6 & acc_bs6 & acc_ne7 & acc_bs7).
assert (readable_la : Mem.valid_access m2 Mint32 b (tail_pos lock_index) Readable).
{ eapply Mem.valid_access_implies; try eassumption; econstructor. }
assert (readable_ne0 : Mem.valid_access m2 Mint32 b (next_pos lock_index 0) Readable).
{ eapply Mem.valid_access_implies; try eassumption; econstructor. }
assert (readable_bs0 : Mem.valid_access m2 Mint32 b (busy_pos lock_index 0) Readable).
{ eapply Mem.valid_access_implies; try eassumption; econstructor. }
assert (readable_ne1 : Mem.valid_access m2 Mint32 b (next_pos lock_index 1) Readable).
{ eapply Mem.valid_access_implies; try eassumption; econstructor. }
assert (readable_bs1 : Mem.valid_access m2 Mint32 b (busy_pos lock_index 1) Readable).
{ eapply Mem.valid_access_implies; try eassumption; econstructor. }
assert (readable_ne2 : Mem.valid_access m2 Mint32 b (next_pos lock_index 2) Readable).
{ eapply Mem.valid_access_implies; try eassumption; econstructor. }
assert (readable_bs2 : Mem.valid_access m2 Mint32 b (busy_pos lock_index 2) Readable).
{ eapply Mem.valid_access_implies; try eassumption; econstructor. }
assert (readable_ne3 : Mem.valid_access m2 Mint32 b (next_pos lock_index 3) Readable).
{ eapply Mem.valid_access_implies; try eassumption; econstructor. }
assert (readable_bs3 : Mem.valid_access m2 Mint32 b (busy_pos lock_index 3) Readable).
{ eapply Mem.valid_access_implies; try eassumption; econstructor. }
assert (readable_ne4 : Mem.valid_access m2 Mint32 b (next_pos lock_index 4) Readable).
{ eapply Mem.valid_access_implies; try eassumption; econstructor. }
assert (readable_bs4 : Mem.valid_access m2 Mint32 b (busy_pos lock_index 4) Readable).
{ eapply Mem.valid_access_implies; try eassumption; econstructor. }
assert (readable_ne5 : Mem.valid_access m2 Mint32 b (next_pos lock_index 5) Readable).
{ eapply Mem.valid_access_implies; try eassumption; econstructor. }
assert (readable_bs5 : Mem.valid_access m2 Mint32 b (busy_pos lock_index 5) Readable).
{ eapply Mem.valid_access_implies; try eassumption; econstructor. }
assert (readable_ne6 : Mem.valid_access m2 Mint32 b (next_pos lock_index 6) Readable).
{ eapply Mem.valid_access_implies; try eassumption; econstructor. }
assert (readable_bs6 : Mem.valid_access m2 Mint32 b (busy_pos lock_index 6) Readable).
{ eapply Mem.valid_access_implies; try eassumption; econstructor. }
assert (readable_ne7 : Mem.valid_access m2 Mint32 b (next_pos lock_index 7) Readable).
{ eapply Mem.valid_access_implies; try eassumption; econstructor. }
assert (readable_bs7 : Mem.valid_access m2 Mint32 b (busy_pos lock_index 7) Readable).
{ eapply Mem.valid_access_implies; try eassumption; econstructor. }
destruct (Mem.valid_access_load _ _ _ _ readable_la) as [v_la load_la].
destruct (Mem.valid_access_load _ _ _ _ readable_ne0) as [v_ne0 load_ne0].
destruct (Mem.valid_access_load _ _ _ _ readable_bs0) as [v_bs0 load_bs0].
destruct (Mem.valid_access_load _ _ _ _ readable_ne1) as [v_ne1 load_ne1].
destruct (Mem.valid_access_load _ _ _ _ readable_bs1) as [v_bs1 load_bs1].
destruct (Mem.valid_access_load _ _ _ _ readable_ne2) as [v_ne2 load_ne2].
destruct (Mem.valid_access_load _ _ _ _ readable_bs2) as [v_bs2 load_bs2].
destruct (Mem.valid_access_load _ _ _ _ readable_ne3) as [v_ne3 load_ne3].
destruct (Mem.valid_access_load _ _ _ _ readable_bs3) as [v_bs3 load_bs3].
destruct (Mem.valid_access_load _ _ _ _ readable_ne4) as [v_ne4 load_ne4].
destruct (Mem.valid_access_load _ _ _ _ readable_bs4) as [v_bs4 load_bs4].
destruct (Mem.valid_access_load _ _ _ _ readable_ne5) as [v_ne5 load_ne5].
destruct (Mem.valid_access_load _ _ _ _ readable_bs5) as [v_bs5 load_bs5].
destruct (Mem.valid_access_load _ _ _ _ readable_ne6) as [v_ne6 load_ne6].
destruct (Mem.valid_access_load _ _ _ _ readable_bs6) as [v_bs6 load_bs6].
destruct (Mem.valid_access_load _ _ _ _ readable_ne7) as [v_ne7 load_ne7].
destruct (Mem.valid_access_load _ _ _ _ readable_bs7) as [v_bs7 load_bs7].
∃ v_la, v_bs0, v_ne0, v_bs1, v_ne1, v_bs2, v_ne2, v_bs3, v_ne3,
v_bs4, v_ne4, v_bs5, v_ne5, v_bs6, v_ne6, v_bs7, v_ne7.
repeat (split; [ eassumption|]).
rewrite ZMap.gi.
econstructor.
Qed.
Lemma link_correct_aux:
link_correct_aux_type MMCSLockIntro_module mcurid mmcslockintro.
Proof.
link_correct_aux.
- link_cfunction mcs_init_node_spec_ref MMCSMCurIDCODE.mcs_init_node_code_correct.
- link_cfunction mcs_GET_NEXT_spec_ref MMCSMCurIDCODE.mcs_GET_NEXT_code_correct.
- link_cfunction mcs_SET_NEXT_spec_ref MMCSMCurIDCODE.mcs_SET_NEXT_code_correct.
- link_cfunction mcs_GET_BUSY_spec_ref MMCSMCurIDCODE.mcs_GET_BUSY_code_correct.
- link_cfunction mcs_SET_BUSY_spec_ref MMCSMCurIDCODE.mcs_SET_BUSY_code_correct.
- link_asmfunction mcs_log_spec_ref mcs_log_code_correct.
- link_asmfunction mcs_SWAP_TAIL_spec_ref mcs_SWAP_TAIL_code_correct.
- link_asmfunction mcs_CAS_TAIL_spec_ref mcs_CAS_TAIL_code_correct.
- apply passthrough_correct.
Qed.
Theorem cl_backward_simulation:
cl_backward_simulation_type MMCSLockIntro_module mcurid mmcslockintro.
Proof.
cl_backward_simulation init_correct link_correct_aux.
Qed.
Theorem make_program_exists:
make_program_exist_type MMCSLockIntro_module mcurid mmcslockintro.
Proof.
make_program_exists link_correct_aux.
Qed.
End WITHCOMPCERTIKOS.