Library mcertikos.mcslock.MMCSLockAbsIntro
This file defines the abstract data and the primitives for the PAbQueue layer,
which will introduce abstraction of kernel context
Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Stacklayout.
Require Import Globalenvs.
Require Import AsmX.
Require Import Smallstep.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import FlatMemory.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import RealParams.
Require Import PrimSemantics.
Require Import LAsm.
Require Import LoadStoreSem1.
Require Import XOmega.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import AbstractDataType.
Require Export MMCSLockIntro.
Require Import ObjMCSLock.
Require Import ObjMultiprocessor.
Require Import INVLemmaQSLock.
Require Import CalMCSLockLemmas.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Stacklayout.
Require Import Globalenvs.
Require Import AsmX.
Require Import Smallstep.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import FlatMemory.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import RealParams.
Require Import PrimSemantics.
Require Import LAsm.
Require Import LoadStoreSem1.
Require Import XOmega.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import AbstractDataType.
Require Export MMCSLockIntro.
Require Import ObjMCSLock.
Require Import ObjMultiprocessor.
Require Import INVLemmaQSLock.
Require Import CalMCSLockLemmas.
Section WITHMEM.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Context `{mcs_oracle_prop: MCSOracleProp}.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Context `{mcs_oracle_prop: MCSOracleProp}.
**Definition of the invariants at MPTNew layer 0th page map is reserved for the kernel thread
Record high_level_invariant (abd: RData) :=
mkInvariant {
CPU_ID_range: 0 ≤ (CPU_ID abd) < TOTAL_CPU;
valid_curid: 0 ≤ ZMap.get (CPU_ID abd) (cid abd) < num_proc;
valid_multi_log_pool_mcs_inv : valid_MCS_log_pool (multi_log abd);
valid_multi_oracle_pool_mcs_inv : valid_multi_oracle_pool_mcs (multi_oracle abd)
}.
mkInvariant {
CPU_ID_range: 0 ≤ (CPU_ID abd) < TOTAL_CPU;
valid_curid: 0 ≤ ZMap.get (CPU_ID abd) (cid abd) < num_proc;
valid_multi_log_pool_mcs_inv : valid_MCS_log_pool (multi_log abd);
valid_multi_oracle_pool_mcs_inv : valid_multi_oracle_pool_mcs (multi_oracle abd)
}.
Global Instance mmcslockabsintro_data_ops : CompatDataOps RData :=
{
empty_data := init_adt mcs_oracle_init0;
high_level_invariant := high_level_invariant;
low_level_invariant := low_level_invariant;
kernel_mode adt := ikern adt = true ∧ ihost adt = true
}.
{
empty_data := init_adt mcs_oracle_init0;
high_level_invariant := high_level_invariant;
low_level_invariant := low_level_invariant;
kernel_mode adt := ikern adt = true ∧ ihost adt = true
}.
Section Property_Abstract_Data.
Lemma empty_data_high_level_invariant:
high_level_invariant (init_adt mcs_oracle_init0).
Proof.
constructor; trivial; simpl.
- apply current_CPU_ID_range.
- rewrite ZMap.gi; intuition.
- eapply valid_MCS_log_pool_init.
- eapply valid_mcs_oracle0.
Qed.
Lemma empty_data_high_level_invariant:
high_level_invariant (init_adt mcs_oracle_init0).
Proof.
constructor; trivial; simpl.
- apply current_CPU_ID_range.
- rewrite ZMap.gi; intuition.
- eapply valid_MCS_log_pool_init.
- eapply valid_mcs_oracle0.
Qed.
Global Instance mmcslockabsintro_data_prf : CompatData RData.
Proof.
constructor.
- apply low_level_invariant_incr.
- apply empty_data_low_level_invariant.
- apply empty_data_high_level_invariant.
Qed.
End Property_Abstract_Data.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Section AuxLemma.
Lemma CalMCSLock_pre´:
∀ el l mcs,
CalMCSLock (el::l) = Some mcs →
∃ mcs´, CalMCSLock l = Some mcs´.
Proof.
intros.
Transparent CalMCSLock.
simpl in H; subdestruct; eauto.
Qed.
Lemma CalMCSLock_pre:
∀ l l´ mcs,
CalMCSLock (l++l´) = Some mcs →
∃ mcs´, CalMCSLock l´ = Some mcs´.
Proof.
induction l; intros; simpl; [ eauto | ].
Opaque CalMCSLock.
simpl in H.
eapply CalMCSLock_pre´ in H.
destruct H as (mcs´, H).
eapply IHl in H; eauto.
Qed.
End AuxLemma.
Proof.
constructor.
- apply low_level_invariant_incr.
- apply empty_data_low_level_invariant.
- apply empty_data_high_level_invariant.
Qed.
End Property_Abstract_Data.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Section AuxLemma.
Lemma CalMCSLock_pre´:
∀ el l mcs,
CalMCSLock (el::l) = Some mcs →
∃ mcs´, CalMCSLock l = Some mcs´.
Proof.
intros.
Transparent CalMCSLock.
simpl in H; subdestruct; eauto.
Qed.
Lemma CalMCSLock_pre:
∀ l l´ mcs,
CalMCSLock (l++l´) = Some mcs →
∃ mcs´, CalMCSLock l´ = Some mcs´.
Proof.
induction l; intros; simpl; [ eauto | ].
Opaque CalMCSLock.
simpl in H.
eapply CalMCSLock_pre´ in H.
destruct H as (mcs´, H).
eapply IHl in H; eauto.
Qed.
End AuxLemma.
Section INV.
Section FRESH_PRIM.
Global Instance mcs_lock_init_inv : PreservesInvariants ticket_lock_init_spec.
Proof.
unfold ticket_lock_init_spec.
constructor; simpl; intros until d´; intros Hsem; intros Hinv; inv_generic_sem Hsem.
- inv Hinv; subdestruct; inv H0; subst; constructor; simpl;
trivial; intros; try congruence.
- inv Hinv; subdestruct; inv H0.
subst.
constructor.
+ simpl; auto.
+ simpl; auto.
+ simpl; eapply real_valid_MCS_log_pool; auto.
+ simpl; auto.
- inv Hinv; subdestruct; inv H0; subst; constructor; simpl;
trivial; intros; try congruence.
Qed.
Global Instance mcs_get_next_inv : PreservesInvariants mcs_get_next_spec.
Proof.
preserves_invariants_simpl_auto1.
- unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv0.
unfold valid_MCS_log_pool.
intros.
case_eq (zeq i1 (Int.unsigned i)); intros.
+ subst.
rewrite ZMap.gss in Hdef; eauto.
inv Hdef.
assert (mcs_l1: ∃ mcs1, CalMCSLock l = Some mcs1).
{ eapply CalMCSLock_pre´ in Hdestruct4.
destruct Hdestruct4 as (mcs´´, Hdestruct4).
eauto using CalMCSLock_pre. }
assert (mcs_l2: ∃ mcs2,
CalMCSLock (ZMap.get (Int.unsigned i) (multi_oracle d)
(Int.unsigned i0) l ++ l) = Some mcs2).
{ eapply CalMCSLock_pre´ in Hdestruct4; eauto. }
destruct mcs_l1 as (mcs1, mcs_l1).
destruct mcs_l2 as (mcs2, mcs_l2).
assert (valid_mcs_l1: valid_MCS_log l).
{ eapply valid_multi_log_pool_mcs_inv0 in Hdestruct3; eauto. }
assert (valid_mcs_l2: valid_MCS_log (ZMap.get (Int.unsigned i) (multi_oracle d)
(Int.unsigned i0) l ++ l)).
{ eapply valid_multi_oracle_pool_mcs_inv0; eauto. }
Transparent CalMCSLock.
simpl in Hdestruct4.
rewrite mcs_l2 in Hdestruct4.
subdestruct.
unfold valid_MCS_log; simpl; intros.
rewrite mcs_l2 in H0.
inv H0.
unfold valid_MCS_log in valid_mcs_l2.
eapply valid_mcs_l2; eauto.
+ rewrite ZMap.gso in Hdef; eauto.
Qed.
Global Instance mcs_set_next_inv : PreservesInvariants mcs_set_next_spec.
Proof.
preserves_invariants_simpl_auto1.
- unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv0.
unfold valid_MCS_log_pool.
intros.
case_eq (zeq i2 (Int.unsigned i)); intros.
+ subst.
rewrite ZMap.gss in Hdef; eauto.
inv Hdef.
assert (mcs_l: ∃ mcs´, CalMCSLock l = Some mcs´).
{ eapply CalMCSLock_pre in Hdestruct5; eauto. }
destruct mcs_l as (mcs´, mcs_l).
assert (valid_mcs_l1: valid_MCS_log l).
{ eapply valid_multi_log_pool_mcs_inv0 in Hdestruct4; eauto. }
assert (valid_mcs_l2: valid_MCS_log (ZMap.get (Int.unsigned i) (multi_oracle d)
(Int.unsigned i0) l ++ l)).
{ eapply valid_multi_oracle_pool_mcs_inv0; eauto. }
unfold valid_MCS_log; simpl; intros.
rewrite Hdestruct5 in H0.
destruct m.
remember (ZMap.get (Int.unsigned i1) lock_array) as ndi1.
destruct ndi1.
inv H0.
unfold MCSCorrect_range.
intros.
inv Hmcs.
unfold valid_MCS_log in valid_mcs_l2.
unfold MCSCorrect_range in valid_mcs_l2.
assert (mcs_eq: MCSLOCK tl lock_array bnd = MCSLOCK tl lock_array bnd) by reflexivity.
eapply valid_mcs_l2 in mcs_eq; eauto.
destruct mcs_eq as (mcs_eq1 & mcs_eq2).
split; try tauto.
intros.
case_eq (zeq i2 (Int.unsigned i1)).
× intros; subst.
rewrite ZMap.gss; eauto.
simpl; omega.
× intros.
rewrite ZMap.gso; eauto.
+ rewrite ZMap.gso in Hdef; eauto.
Qed.
Global Instance mcs_get_busy_inv : PreservesInvariants mcs_get_busy_spec.
Proof.
preserves_invariants_simpl_auto1.
- unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv0.
unfold valid_MCS_log_pool.
intros.
case_eq (zeq i1 (Int.unsigned i)); intros.
+ subst.
rewrite ZMap.gss in Hdef; eauto.
inv Hdef.
assert (mcs_l: ∃ mcs´, CalMCSLock l = Some mcs´).
{ eapply CalMCSLock_pre in Hdestruct4; eauto. }
destruct mcs_l as (mcs´, mcs_l).
assert (valid_mcs_l1: valid_MCS_log l).
{ eapply valid_multi_log_pool_mcs_inv0; eauto. }
assert (valid_mcs_l2: valid_MCS_log (ZMap.get (Int.unsigned i) (multi_oracle d)
(Int.unsigned i0) l ++ l)).
{ eapply valid_multi_oracle_pool_mcs_inv0; eauto. }
unfold valid_MCS_log; simpl; intros.
rewrite Hdestruct4 in H0.
inv H0.
unfold valid_MCS_log in valid_mcs_l2.
eapply valid_mcs_l2; eauto.
+ rewrite ZMap.gso in Hdef; eauto.
- unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv0.
unfold valid_MCS_log_pool.
intros.
case_eq (zeq i1 (Int.unsigned i)); intros.
+ subst.
rewrite ZMap.gss in Hdef; eauto.
inv Hdef.
assert (mcs_l: ∃ mcs´, CalMCSLock l = Some mcs´).
{ eapply CalMCSLock_pre in Hdestruct4; eauto. }
destruct mcs_l as (mcs´, mcs_l).
assert (valid_mcs_l1: valid_MCS_log l).
{ eapply valid_multi_log_pool_mcs_inv0; eauto. }
assert (valid_mcs_l2: valid_MCS_log (ZMap.get (Int.unsigned i) (multi_oracle d)
(Int.unsigned i0) l ++ l)).
{ eapply valid_multi_oracle_pool_mcs_inv0; eauto. }
unfold valid_MCS_log; simpl; intros.
rewrite Hdestruct4 in H0.
inv H0.
unfold valid_MCS_log in valid_mcs_l2.
eapply valid_mcs_l2; eauto.
+ rewrite ZMap.gso in Hdef; eauto.
Qed.
Global Instance mcs_set_busy_inv : PreservesInvariants mcs_set_busy_spec.
Proof.
preserves_invariants_simpl_auto1.
- unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv0.
unfold valid_MCS_log_pool.
intros.
case_eq (zeq i1 (Int.unsigned i)); intros.
+ subst.
rewrite ZMap.gss in Hdef; eauto.
inv Hdef.
assert (mcs_l: ∃ mcs´, CalMCSLock l = Some mcs´).
{ eapply CalMCSLock_pre in Hdestruct4; eauto. }
destruct mcs_l as (mcs´, mcs_l).
assert (valid_mcs_l1: valid_MCS_log l).
{ eapply valid_multi_log_pool_mcs_inv0; eauto. }
assert (valid_mcs_l2: valid_MCS_log (ZMap.get (Int.unsigned i) (multi_oracle d)
(Int.unsigned i0) l ++ l)).
{ eapply valid_multi_oracle_pool_mcs_inv0; eauto. }
unfold valid_MCS_log; simpl; intros.
rewrite Hdestruct4 in H0.
rewrite Hdestruct6 in H0.
remember (ZMap.get z lock_array) as ndz.
destruct ndz.
inv H0.
unfold MCSCorrect_range.
intros.
inv Hmcs.
unfold valid_MCS_log in valid_mcs_l2.
unfold MCSCorrect_range in valid_mcs_l2.
assert (mcs_eq: MCSLOCK tl lock_array bounds = MCSLOCK tl lock_array bounds)
by reflexivity.
eapply valid_mcs_l2 in mcs_eq; eauto.
destruct mcs_eq as (mcs_eq1 & mcs_eq2).
split; try tauto.
intros.
case_eq (zeq i1 z).
× intros; subst.
rewrite ZMap.gss; eauto.
simpl.
eapply mcs_eq2 in H0.
rewrite <- Heqndz in H0; simpl in H0.
omega.
× intros.
rewrite ZMap.gso; eauto.
+ rewrite ZMap.gso in Hdef; eauto.
Qed.
Global Instance mcs_swap_tail_inv : PreservesInvariants mcs_swap_tail_spec.
Proof.
preserves_invariants_simpl_auto1.
- unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv0.
unfold valid_MCS_log_pool.
intros.
case_eq (zeq i2 (Int.unsigned i0)); intros.
+ subst.
rewrite ZMap.gss in Hdef; eauto.
inv Hdef.
assert (mcs_l: ∃ mcs´, CalMCSLock l = Some mcs´).
{ eapply CalMCSLock_pre in Hdestruct4; eauto. }
destruct mcs_l as (mcs´, mcs_l).
assert (valid_mcs_l1: valid_MCS_log l).
{ eapply valid_multi_log_pool_mcs_inv0; eauto. }
assert (valid_mcs_l2: valid_MCS_log (ZMap.get (Int.unsigned i0) (multi_oracle d)
(Int.unsigned i1) l ++ l)).
{ eapply valid_multi_oracle_pool_mcs_inv0; eauto. }
unfold valid_MCS_log; simpl; intros.
rewrite Hdestruct4 in H0.
inv H0.
unfold MCSCorrect_range.
intros.
inv Hmcs.
unfold valid_MCS_log in valid_mcs_l2.
unfold MCSCorrect_range in valid_mcs_l2.
assert (mcs_eq: MCSLOCK NULL lock_array bounds = MCSLOCK NULL lock_array bounds)
by reflexivity.
eapply valid_mcs_l2 in mcs_eq; eauto.
destruct mcs_eq as (mcs_eq1 & mcs_eq2).
split; intros; try omega.
case_eq (zeq i2 (Int.unsigned i1)).
× intros; subst.
rewrite ZMap.gss; eauto.
× intros.
rewrite ZMap.gso; eauto.
+ rewrite ZMap.gso in Hdef; eauto.
- unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv0.
unfold valid_MCS_log_pool.
intros.
case_eq (zeq i2 (Int.unsigned i0)); intros.
+ subst.
rewrite ZMap.gss in Hdef; eauto.
inv Hdef.
assert (mcs_l: ∃ mcs´, CalMCSLock l = Some mcs´).
{ eapply CalMCSLock_pre in Hdestruct4; eauto. }
destruct mcs_l as (mcs´, mcs_l).
assert (valid_mcs_l1: valid_MCS_log l).
{ eapply valid_multi_log_pool_mcs_inv0; eauto. }
assert (valid_mcs_l2: valid_MCS_log (ZMap.get (Int.unsigned i0) (multi_oracle d)
(Int.unsigned i1) l ++ l)).
{ eapply valid_multi_oracle_pool_mcs_inv0; eauto. }
unfold valid_MCS_log; simpl; intros.
rewrite Hdestruct4 in H0.
inv H0.
unfold MCSCorrect_range.
intros.
inv Hmcs.
unfold valid_MCS_log in valid_mcs_l2.
unfold MCSCorrect_range in valid_mcs_l2.
assert (mcs_eq: MCSLOCK (Int.unsigned z) lock_array bounds
= MCSLOCK (Int.unsigned z) lock_array bounds)
by reflexivity.
eapply valid_mcs_l2 in mcs_eq; eauto.
destruct mcs_eq as (mcs_eq1 & mcs_eq2).
split; intros; try omega.
case_eq (zeq i2 (Int.unsigned i1)).
× intros; subst.
rewrite ZMap.gss; eauto.
simpl; unfold CalMCSLock.NULL; omega.
× intros.
rewrite ZMap.gso; eauto.
+ rewrite ZMap.gso in Hdef; eauto.
Qed.
Global Instance mcs_cas_tail_inv : PreservesInvariants mcs_cas_tail_spec.
Proof.
preserves_invariants_simpl_auto1.
- unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv0.
unfold valid_MCS_log_pool.
intros.
case_eq (zeq i1 (Int.unsigned i)); intros.
+ subst.
rewrite ZMap.gss in Hdef; eauto.
inv Hdef.
assert (mcs_l: ∃ mcs´, CalMCSLock l = Some mcs´).
{ eapply CalMCSLock_pre in Hdestruct4; eauto. }
destruct mcs_l as (mcs´, mcs_l).
assert (valid_mcs_l1: valid_MCS_log l).
{ eapply valid_multi_log_pool_mcs_inv0; eauto. }
assert (valid_mcs_l2: valid_MCS_log (ZMap.get (Int.unsigned i) (multi_oracle d)
(Int.unsigned i0) l ++ l)).
{ eapply valid_multi_oracle_pool_mcs_inv0; eauto. }
unfold valid_MCS_log; simpl; intros.
rewrite Hdestruct4 in H0.
subdestruct.
inv H0.
unfold MCSCorrect_range.
intros.
inv Hmcs.
unfold valid_MCS_log in valid_mcs_l2.
unfold MCSCorrect_range in valid_mcs_l2.
assert (mcs_eq: MCSLOCK (Int.unsigned i0) lock_arr bounds
= MCSLOCK (Int.unsigned i0) lock_arr bounds)
by reflexivity.
eapply valid_mcs_l2 in mcs_eq; eauto.
destruct mcs_eq as (mcs_eq1 & mcs_eq2).
split; intros; try (unfold CalMCSLock.NULL; omega).
eapply mcs_eq2; auto.
+ rewrite ZMap.gso in Hdef; eauto.
- unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv0.
unfold valid_MCS_log_pool.
intros.
case_eq (zeq i1 (Int.unsigned i)); intros.
+ subst.
rewrite ZMap.gss in Hdef; eauto.
inv Hdef.
assert (mcs_l: ∃ mcs´, CalMCSLock l = Some mcs´).
{ eapply CalMCSLock_pre in Hdestruct4; eauto. }
destruct mcs_l as (mcs´, mcs_l).
assert (valid_mcs_l1: valid_MCS_log l).
{ eapply valid_multi_log_pool_mcs_inv0; eauto. }
assert (valid_mcs_l2: valid_MCS_log (ZMap.get (Int.unsigned i) (multi_oracle d)
(Int.unsigned i0) l ++ l)).
{ eapply valid_multi_oracle_pool_mcs_inv0; eauto. }
unfold valid_MCS_log; simpl; intros.
rewrite Hdestruct4 in H0.
subdestruct.
inv H0.
unfold MCSCorrect_range.
intros.
inv Hmcs.
unfold valid_MCS_log in valid_mcs_l2.
unfold MCSCorrect_range in valid_mcs_l2.
assert (mcs_eq: MCSLOCK tl lock_arr bnd
= MCSLOCK tl lock_arr bnd)
by reflexivity.
eapply valid_mcs_l2 in mcs_eq; eauto.
+ rewrite ZMap.gso in Hdef; eauto.
Qed.
Global Instance mcs_lock_get_index_inv : PreservesInvariants mcs_lock_get_index_spec.
Proof.
preserves_invariants_simpl_auto1.
Qed.
End FRESH_PRIM.
Section PASSTHROUGH_PRIM.
Global Instance acquire_shared_inv: SAcquireInvariants acquire_shared0_spec0.
Proof.
constructor; unfold acquire_shared0_spec; intros;
subdestruct; inv H; inv H0; constructor; auto;
exploit index2Z_in_lock_range; eauto; intros; simpl in *;
unfold valid_MCS_log_pool; intros;
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv0.
Transparent CalMCSLock.
- case_eq (zeq i0 z); intros; subst.
+ rewrite ZMap.gss in Hdef; inv Hdef.
unfold valid_MCS_log.
generalize (valid_multi_log_pool_mcs_inv0 _ _ Hrange Hdestruct3); intros.
unfold valid_MCS_log in H1.
simpl in *; subdestruct; inv H2.
eapply H1; auto.
+ rewrite ZMap.gso in Hdef; auto; eapply valid_multi_log_pool_mcs_inv0 in Hdef; eauto.
- case_eq (zeq i0 z); intros; subst.
+ rewrite ZMap.gss in Hdef; inv Hdef.
unfold valid_MCS_log.
generalize (valid_multi_log_pool_mcs_inv0 _ _ Hrange Hdestruct3); intros.
unfold valid_MCS_log in H1.
simpl in *; subdestruct; inv H2.
eapply H1; auto.
+ rewrite ZMap.gso in Hdef; auto; eapply valid_multi_log_pool_mcs_inv0 in Hdef; eauto.
Qed.
Global Instance release_shared_inv: ReleaseInvariants release_shared0_spec0.
Proof.
constructor; unfold release_shared0_spec; intros; subdestruct;
inv H; inv H0; constructor; auto;
exploit index2Z_in_lock_range; eauto; intros; simpl in *;
unfold valid_MCS_log_pool; intros;
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv0.
case_eq (zeq i0 z); intros; subst.
- rewrite ZMap.gss in Hdef; inv Hdef.
unfold valid_MCS_log.
generalize (valid_multi_log_pool_mcs_inv0 _ _ Hrange Hdestruct3); intros.
unfold valid_MCS_log in H1.
simpl in *; subdestruct; inv H2.
eapply H1; auto.
- rewrite ZMap.gso in Hdef; auto; eapply valid_multi_log_pool_mcs_inv0 in Hdef; eauto.
Qed.
Global Instance setPG_inv: PreservesInvariants setPG_spec.
Proof.
preserves_invariants_simpl_auto.
Qed.
Global Instance fstore_inv: PreservesInvariants fstore´_spec.
Proof.
preserves_invariants_simpl_auto.
Qed.
Global Instance setCR3_inv: SetCR3Invariants setCR3_spec.
Proof.
constructor; intros.
- functional inversion H; inv H0; constructor; trivial.
- functional inversion H; inv H0; constructor; auto.
- functional inversion H; simpl in *; assumption.
Qed.
Global Instance trapin_inv: PrimInvariants trapin_spec.
Proof.
PrimInvariants_simpl_auto.
Qed.
Global Instance trapout_inv: PrimInvariants trapout´_spec.
Proof.
PrimInvariants_simpl_auto.
Qed.
Global Instance hostin_inv: PrimInvariants hostin_spec.
Proof.
PrimInvariants_simpl_auto.
Qed.
Global Instance hostout_inv: PrimInvariants hostout´_spec.
Proof.
PrimInvariants_simpl_auto.
Qed.
Global Instance set_curid_inv: PreservesInvariants set_curid_spec.
Proof.
preserves_invariants_simpl_auto; eauto 2.
- rewrite ZMap.gss. auto.
Qed.
Global Instance set_curid_init_inv: PreservesInvariants set_curid_init_spec.
Proof.
preserves_invariants_simpl_auto; eauto 2.
case_eq (zeq (CPU_ID d) (Int.unsigned i)); intros; subst.
- rewrite e; rewrite ZMap.gss; omega.
- rewrite ZMap.gso; auto.
Qed.
Global Instance cli_inv: PreservesInvariants cli_spec.
Proof.
econstructor; intros; inv H; functional inversion H1; subst.
- inv H0; constructor; trivial.
- inv H0; constructor; auto.
- simpl in *; assumption.
Qed.
Global Instance sti_inv: PreservesInvariants sti_spec.
Proof.
econstructor; intros; inv H; functional inversion H1; subst.
- inv H0; constructor; trivial.
- inv H0; constructor; auto.
- simpl in *; assumption.
Qed.
Require Import FutureTactic.
Global Instance serial_in_inv: PreservesInvariants serial_in_spec.
Proof.
preserves_invariants_subst low_level_invariant high_level_invariant;
try eauto using valid_multi_log_pool_mcs_inv0;
try eauto using valid_multi_oracle_pool_mcs_inv0.
Qed.
Global Instance serial_out_inv: PreservesInvariants serial_out_spec.
Proof.
preserves_invariants_subst low_level_invariant high_level_invariant;
try eauto using valid_multi_log_pool_mcs_inv0;
try eauto using valid_multi_oracle_pool_mcs_inv0.
Qed.
Global Instance serial_hw_intr_inv: PreservesInvariants serial_hw_intr_spec.
Proof.
preserves_invariants_nested low_level_invariant high_level_invariant;
try eauto using valid_multi_log_pool_mcs_inv0;
try eauto using valid_multi_oracle_pool_mcs_inv0.
Qed.
Global Instance ic_intr_inv: PreservesInvariants ic_intr_spec.
Proof.
preserves_invariants_nested low_level_invariant high_level_invariant;
try eauto using valid_multi_log_pool_mcs_inv0;
try eauto using valid_multi_oracle_pool_mcs_inv0.
Qed.
Global Instance keyboard_in_inv: PreservesInvariants keyboard_in_spec.
Proof.
preserves_invariants_subst low_level_invariant high_level_invariant;
try eauto using valid_multi_log_pool_mcs_inv0;
try eauto using valid_multi_oracle_pool_mcs_inv0.
Qed.
Global Instance keyboard_hw_intr_inv: PreservesInvariants keyboard_hw_intr_spec.
Proof.
preserves_invariants_nested low_level_invariant high_level_invariant;
try eauto using valid_multi_log_pool_mcs_inv0;
try eauto using valid_multi_oracle_pool_mcs_inv0.
Qed.
Global Instance ioapic_read_inv: PreservesInvariants ioapic_read_spec.
Proof.
preserves_invariants_simpl low_level_invariant high_level_invariant;
try eauto using valid_multi_log_pool_mcs_inv0;
try eauto using valid_multi_oracle_pool_mcs_inv0.
Qed.
Global Instance ioapic_write_inv: PreservesInvariants ioapic_write_spec.
Proof.
preserves_invariants_simpl low_level_invariant high_level_invariant;
try eauto using valid_multi_log_pool_mcs_inv0;
try eauto using valid_multi_oracle_pool_mcs_inv0.
Qed.
Global Instance lapic_read_inv: PreservesInvariants lapic_read_spec.
Proof.
preserves_invariants_simpl low_level_invariant high_level_invariant;
try eauto using valid_multi_log_pool_mcs_inv0;
try eauto using valid_multi_oracle_pool_mcs_inv0.
Qed.
Global Instance lapic_write_inv: PreservesInvariants lapic_write_spec.
Proof.
preserves_invariants_simpl low_level_invariant high_level_invariant;
try eauto using valid_multi_log_pool_mcs_inv0;
try eauto using valid_multi_oracle_pool_mcs_inv0.
Qed.
Global Instance iret_inv: PreservesInvariants iret_spec.
Proof.
preserves_invariants_direct low_level_invariant high_level_invariant; eauto 2.
Qed.
Global Instance local_irq_save_inv: PreservesInvariants local_irq_save_spec.
Proof.
preserves_invariants_simpl low_level_invariant high_level_invariant; eauto 2.
Qed.
Global Instance local_irq_restore_inv: PreservesInvariants local_irq_restore_spec.
Proof.
preserves_invariants_simpl low_level_invariant high_level_invariant; eauto 2.
Qed.
Global Instance save_context_inv: SaveContextInvariants save_context_spec.
Proof.
constructor; intros.
-
inv H0. unfold save_context_spec; simpl. inv H1.
constructor; simpl; trivial.
induction (tf d).
simpl.
constructor.
constructor.
simpl.
apply inv_reg_wt.
simpl.
inv inv_inject_neutral.
eapply inv_reg_inject_neutral; auto.
constructor.
constructor.
inv tf_INJECT.
assumption.
eapply IHt; auto.
inv tf_INJECT.
assumption.
-
inv H0. unfold save_context_spec; simpl.
constructor; simpl; trivial.
Qed.
Global Instance restore_context_inv: RestoreContextInvariants restore_context_spec.
Proof.
constructor; intros.
-
inv H0. functional inversion H; inv H1;
constructor; simpl; trivial.
rewrite H4 in ×.
clear H4 H.
generalize dependent _x.
induction _x0.
intros.
simpl in ×.
constructor.
intros.
simpl in ×.
constructor.
inv tf_INJECT.
assumption.
eapply IH_x0; auto.
inv tf_INJECT; assumption.
-
inv H0. functional inversion H; subst;
constructor; simpl; trivial.
Qed.
Global Instance proc_create_postinit_inv:
PreservesInvariants proc_create_postinit_spec.
Proof.
preserves_invariants_simpl low_level_invariant high_level_invariant; eauto 2.
Qed.
End PASSTHROUGH_PRIM.
End INV.
Definition exec_loadex {F V} := exec_loadex1 (F := F) (V := V).
Definition exec_storeex {F V} := exec_storeex1 (flatmem_store:= flatmem_store´) (F := F) (V := V).
Global Instance flatmem_store_inv: FlatmemStoreInvariant (flatmem_store:= flatmem_store´).
Proof.
split; inversion 1; intros.
- functional inversion H0; constructor; auto.
- functional inversion H1; constructor; auto.
Qed.
Global Instance trapinfo_set_inv: TrapinfoSetInvariant.
Proof.
split; inversion 1; intros; constructor; auto.
Qed.
Global Instance page_copy_inv: PreservesInvariants page_copy´´´_spec.
Proof.
preserves_invariants_simpl_auto.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv0.
unfold valid_MCS_log_pool.
intros.
case_eq (zeq i2 abid); intros; subst.
- rewrite ZMap.gss in Hdef.
inv Hdef.
eapply valid_multi_log_pool_mcs_inv0 in H7; eauto.
unfold valid_MCS_log in H7.
unfold valid_MCS_log.
intros.
Transparent CalMCSLock.
simpl in H9.
destruct (CalMCSLock l) eqn:?; try (inv H9; fail).
inv H9.
eapply H7; eauto.
- rewrite ZMap.gso in Hdef; eauto.
Qed.
Global Instance page_copy_back_inv: PreservesInvariants page_copy_back´_spec.
Proof.
preserves_invariants_simpl_auto.
Qed.
Section FRESH_PRIM.
Global Instance mcs_lock_init_inv : PreservesInvariants ticket_lock_init_spec.
Proof.
unfold ticket_lock_init_spec.
constructor; simpl; intros until d´; intros Hsem; intros Hinv; inv_generic_sem Hsem.
- inv Hinv; subdestruct; inv H0; subst; constructor; simpl;
trivial; intros; try congruence.
- inv Hinv; subdestruct; inv H0.
subst.
constructor.
+ simpl; auto.
+ simpl; auto.
+ simpl; eapply real_valid_MCS_log_pool; auto.
+ simpl; auto.
- inv Hinv; subdestruct; inv H0; subst; constructor; simpl;
trivial; intros; try congruence.
Qed.
Global Instance mcs_get_next_inv : PreservesInvariants mcs_get_next_spec.
Proof.
preserves_invariants_simpl_auto1.
- unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv0.
unfold valid_MCS_log_pool.
intros.
case_eq (zeq i1 (Int.unsigned i)); intros.
+ subst.
rewrite ZMap.gss in Hdef; eauto.
inv Hdef.
assert (mcs_l1: ∃ mcs1, CalMCSLock l = Some mcs1).
{ eapply CalMCSLock_pre´ in Hdestruct4.
destruct Hdestruct4 as (mcs´´, Hdestruct4).
eauto using CalMCSLock_pre. }
assert (mcs_l2: ∃ mcs2,
CalMCSLock (ZMap.get (Int.unsigned i) (multi_oracle d)
(Int.unsigned i0) l ++ l) = Some mcs2).
{ eapply CalMCSLock_pre´ in Hdestruct4; eauto. }
destruct mcs_l1 as (mcs1, mcs_l1).
destruct mcs_l2 as (mcs2, mcs_l2).
assert (valid_mcs_l1: valid_MCS_log l).
{ eapply valid_multi_log_pool_mcs_inv0 in Hdestruct3; eauto. }
assert (valid_mcs_l2: valid_MCS_log (ZMap.get (Int.unsigned i) (multi_oracle d)
(Int.unsigned i0) l ++ l)).
{ eapply valid_multi_oracle_pool_mcs_inv0; eauto. }
Transparent CalMCSLock.
simpl in Hdestruct4.
rewrite mcs_l2 in Hdestruct4.
subdestruct.
unfold valid_MCS_log; simpl; intros.
rewrite mcs_l2 in H0.
inv H0.
unfold valid_MCS_log in valid_mcs_l2.
eapply valid_mcs_l2; eauto.
+ rewrite ZMap.gso in Hdef; eauto.
Qed.
Global Instance mcs_set_next_inv : PreservesInvariants mcs_set_next_spec.
Proof.
preserves_invariants_simpl_auto1.
- unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv0.
unfold valid_MCS_log_pool.
intros.
case_eq (zeq i2 (Int.unsigned i)); intros.
+ subst.
rewrite ZMap.gss in Hdef; eauto.
inv Hdef.
assert (mcs_l: ∃ mcs´, CalMCSLock l = Some mcs´).
{ eapply CalMCSLock_pre in Hdestruct5; eauto. }
destruct mcs_l as (mcs´, mcs_l).
assert (valid_mcs_l1: valid_MCS_log l).
{ eapply valid_multi_log_pool_mcs_inv0 in Hdestruct4; eauto. }
assert (valid_mcs_l2: valid_MCS_log (ZMap.get (Int.unsigned i) (multi_oracle d)
(Int.unsigned i0) l ++ l)).
{ eapply valid_multi_oracle_pool_mcs_inv0; eauto. }
unfold valid_MCS_log; simpl; intros.
rewrite Hdestruct5 in H0.
destruct m.
remember (ZMap.get (Int.unsigned i1) lock_array) as ndi1.
destruct ndi1.
inv H0.
unfold MCSCorrect_range.
intros.
inv Hmcs.
unfold valid_MCS_log in valid_mcs_l2.
unfold MCSCorrect_range in valid_mcs_l2.
assert (mcs_eq: MCSLOCK tl lock_array bnd = MCSLOCK tl lock_array bnd) by reflexivity.
eapply valid_mcs_l2 in mcs_eq; eauto.
destruct mcs_eq as (mcs_eq1 & mcs_eq2).
split; try tauto.
intros.
case_eq (zeq i2 (Int.unsigned i1)).
× intros; subst.
rewrite ZMap.gss; eauto.
simpl; omega.
× intros.
rewrite ZMap.gso; eauto.
+ rewrite ZMap.gso in Hdef; eauto.
Qed.
Global Instance mcs_get_busy_inv : PreservesInvariants mcs_get_busy_spec.
Proof.
preserves_invariants_simpl_auto1.
- unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv0.
unfold valid_MCS_log_pool.
intros.
case_eq (zeq i1 (Int.unsigned i)); intros.
+ subst.
rewrite ZMap.gss in Hdef; eauto.
inv Hdef.
assert (mcs_l: ∃ mcs´, CalMCSLock l = Some mcs´).
{ eapply CalMCSLock_pre in Hdestruct4; eauto. }
destruct mcs_l as (mcs´, mcs_l).
assert (valid_mcs_l1: valid_MCS_log l).
{ eapply valid_multi_log_pool_mcs_inv0; eauto. }
assert (valid_mcs_l2: valid_MCS_log (ZMap.get (Int.unsigned i) (multi_oracle d)
(Int.unsigned i0) l ++ l)).
{ eapply valid_multi_oracle_pool_mcs_inv0; eauto. }
unfold valid_MCS_log; simpl; intros.
rewrite Hdestruct4 in H0.
inv H0.
unfold valid_MCS_log in valid_mcs_l2.
eapply valid_mcs_l2; eauto.
+ rewrite ZMap.gso in Hdef; eauto.
- unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv0.
unfold valid_MCS_log_pool.
intros.
case_eq (zeq i1 (Int.unsigned i)); intros.
+ subst.
rewrite ZMap.gss in Hdef; eauto.
inv Hdef.
assert (mcs_l: ∃ mcs´, CalMCSLock l = Some mcs´).
{ eapply CalMCSLock_pre in Hdestruct4; eauto. }
destruct mcs_l as (mcs´, mcs_l).
assert (valid_mcs_l1: valid_MCS_log l).
{ eapply valid_multi_log_pool_mcs_inv0; eauto. }
assert (valid_mcs_l2: valid_MCS_log (ZMap.get (Int.unsigned i) (multi_oracle d)
(Int.unsigned i0) l ++ l)).
{ eapply valid_multi_oracle_pool_mcs_inv0; eauto. }
unfold valid_MCS_log; simpl; intros.
rewrite Hdestruct4 in H0.
inv H0.
unfold valid_MCS_log in valid_mcs_l2.
eapply valid_mcs_l2; eauto.
+ rewrite ZMap.gso in Hdef; eauto.
Qed.
Global Instance mcs_set_busy_inv : PreservesInvariants mcs_set_busy_spec.
Proof.
preserves_invariants_simpl_auto1.
- unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv0.
unfold valid_MCS_log_pool.
intros.
case_eq (zeq i1 (Int.unsigned i)); intros.
+ subst.
rewrite ZMap.gss in Hdef; eauto.
inv Hdef.
assert (mcs_l: ∃ mcs´, CalMCSLock l = Some mcs´).
{ eapply CalMCSLock_pre in Hdestruct4; eauto. }
destruct mcs_l as (mcs´, mcs_l).
assert (valid_mcs_l1: valid_MCS_log l).
{ eapply valid_multi_log_pool_mcs_inv0; eauto. }
assert (valid_mcs_l2: valid_MCS_log (ZMap.get (Int.unsigned i) (multi_oracle d)
(Int.unsigned i0) l ++ l)).
{ eapply valid_multi_oracle_pool_mcs_inv0; eauto. }
unfold valid_MCS_log; simpl; intros.
rewrite Hdestruct4 in H0.
rewrite Hdestruct6 in H0.
remember (ZMap.get z lock_array) as ndz.
destruct ndz.
inv H0.
unfold MCSCorrect_range.
intros.
inv Hmcs.
unfold valid_MCS_log in valid_mcs_l2.
unfold MCSCorrect_range in valid_mcs_l2.
assert (mcs_eq: MCSLOCK tl lock_array bounds = MCSLOCK tl lock_array bounds)
by reflexivity.
eapply valid_mcs_l2 in mcs_eq; eauto.
destruct mcs_eq as (mcs_eq1 & mcs_eq2).
split; try tauto.
intros.
case_eq (zeq i1 z).
× intros; subst.
rewrite ZMap.gss; eauto.
simpl.
eapply mcs_eq2 in H0.
rewrite <- Heqndz in H0; simpl in H0.
omega.
× intros.
rewrite ZMap.gso; eauto.
+ rewrite ZMap.gso in Hdef; eauto.
Qed.
Global Instance mcs_swap_tail_inv : PreservesInvariants mcs_swap_tail_spec.
Proof.
preserves_invariants_simpl_auto1.
- unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv0.
unfold valid_MCS_log_pool.
intros.
case_eq (zeq i2 (Int.unsigned i0)); intros.
+ subst.
rewrite ZMap.gss in Hdef; eauto.
inv Hdef.
assert (mcs_l: ∃ mcs´, CalMCSLock l = Some mcs´).
{ eapply CalMCSLock_pre in Hdestruct4; eauto. }
destruct mcs_l as (mcs´, mcs_l).
assert (valid_mcs_l1: valid_MCS_log l).
{ eapply valid_multi_log_pool_mcs_inv0; eauto. }
assert (valid_mcs_l2: valid_MCS_log (ZMap.get (Int.unsigned i0) (multi_oracle d)
(Int.unsigned i1) l ++ l)).
{ eapply valid_multi_oracle_pool_mcs_inv0; eauto. }
unfold valid_MCS_log; simpl; intros.
rewrite Hdestruct4 in H0.
inv H0.
unfold MCSCorrect_range.
intros.
inv Hmcs.
unfold valid_MCS_log in valid_mcs_l2.
unfold MCSCorrect_range in valid_mcs_l2.
assert (mcs_eq: MCSLOCK NULL lock_array bounds = MCSLOCK NULL lock_array bounds)
by reflexivity.
eapply valid_mcs_l2 in mcs_eq; eauto.
destruct mcs_eq as (mcs_eq1 & mcs_eq2).
split; intros; try omega.
case_eq (zeq i2 (Int.unsigned i1)).
× intros; subst.
rewrite ZMap.gss; eauto.
× intros.
rewrite ZMap.gso; eauto.
+ rewrite ZMap.gso in Hdef; eauto.
- unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv0.
unfold valid_MCS_log_pool.
intros.
case_eq (zeq i2 (Int.unsigned i0)); intros.
+ subst.
rewrite ZMap.gss in Hdef; eauto.
inv Hdef.
assert (mcs_l: ∃ mcs´, CalMCSLock l = Some mcs´).
{ eapply CalMCSLock_pre in Hdestruct4; eauto. }
destruct mcs_l as (mcs´, mcs_l).
assert (valid_mcs_l1: valid_MCS_log l).
{ eapply valid_multi_log_pool_mcs_inv0; eauto. }
assert (valid_mcs_l2: valid_MCS_log (ZMap.get (Int.unsigned i0) (multi_oracle d)
(Int.unsigned i1) l ++ l)).
{ eapply valid_multi_oracle_pool_mcs_inv0; eauto. }
unfold valid_MCS_log; simpl; intros.
rewrite Hdestruct4 in H0.
inv H0.
unfold MCSCorrect_range.
intros.
inv Hmcs.
unfold valid_MCS_log in valid_mcs_l2.
unfold MCSCorrect_range in valid_mcs_l2.
assert (mcs_eq: MCSLOCK (Int.unsigned z) lock_array bounds
= MCSLOCK (Int.unsigned z) lock_array bounds)
by reflexivity.
eapply valid_mcs_l2 in mcs_eq; eauto.
destruct mcs_eq as (mcs_eq1 & mcs_eq2).
split; intros; try omega.
case_eq (zeq i2 (Int.unsigned i1)).
× intros; subst.
rewrite ZMap.gss; eauto.
simpl; unfold CalMCSLock.NULL; omega.
× intros.
rewrite ZMap.gso; eauto.
+ rewrite ZMap.gso in Hdef; eauto.
Qed.
Global Instance mcs_cas_tail_inv : PreservesInvariants mcs_cas_tail_spec.
Proof.
preserves_invariants_simpl_auto1.
- unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv0.
unfold valid_MCS_log_pool.
intros.
case_eq (zeq i1 (Int.unsigned i)); intros.
+ subst.
rewrite ZMap.gss in Hdef; eauto.
inv Hdef.
assert (mcs_l: ∃ mcs´, CalMCSLock l = Some mcs´).
{ eapply CalMCSLock_pre in Hdestruct4; eauto. }
destruct mcs_l as (mcs´, mcs_l).
assert (valid_mcs_l1: valid_MCS_log l).
{ eapply valid_multi_log_pool_mcs_inv0; eauto. }
assert (valid_mcs_l2: valid_MCS_log (ZMap.get (Int.unsigned i) (multi_oracle d)
(Int.unsigned i0) l ++ l)).
{ eapply valid_multi_oracle_pool_mcs_inv0; eauto. }
unfold valid_MCS_log; simpl; intros.
rewrite Hdestruct4 in H0.
subdestruct.
inv H0.
unfold MCSCorrect_range.
intros.
inv Hmcs.
unfold valid_MCS_log in valid_mcs_l2.
unfold MCSCorrect_range in valid_mcs_l2.
assert (mcs_eq: MCSLOCK (Int.unsigned i0) lock_arr bounds
= MCSLOCK (Int.unsigned i0) lock_arr bounds)
by reflexivity.
eapply valid_mcs_l2 in mcs_eq; eauto.
destruct mcs_eq as (mcs_eq1 & mcs_eq2).
split; intros; try (unfold CalMCSLock.NULL; omega).
eapply mcs_eq2; auto.
+ rewrite ZMap.gso in Hdef; eauto.
- unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv0.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv0.
unfold valid_MCS_log_pool.
intros.
case_eq (zeq i1 (Int.unsigned i)); intros.
+ subst.
rewrite ZMap.gss in Hdef; eauto.
inv Hdef.
assert (mcs_l: ∃ mcs´, CalMCSLock l = Some mcs´).
{ eapply CalMCSLock_pre in Hdestruct4; eauto. }
destruct mcs_l as (mcs´, mcs_l).
assert (valid_mcs_l1: valid_MCS_log l).
{ eapply valid_multi_log_pool_mcs_inv0; eauto. }
assert (valid_mcs_l2: valid_MCS_log (ZMap.get (Int.unsigned i) (multi_oracle d)
(Int.unsigned i0) l ++ l)).
{ eapply valid_multi_oracle_pool_mcs_inv0; eauto. }
unfold valid_MCS_log; simpl; intros.
rewrite Hdestruct4 in H0.
subdestruct.
inv H0.
unfold MCSCorrect_range.
intros.
inv Hmcs.
unfold valid_MCS_log in valid_mcs_l2.
unfold MCSCorrect_range in valid_mcs_l2.
assert (mcs_eq: MCSLOCK tl lock_arr bnd
= MCSLOCK tl lock_arr bnd)
by reflexivity.
eapply valid_mcs_l2 in mcs_eq; eauto.
+ rewrite ZMap.gso in Hdef; eauto.
Qed.
Global Instance mcs_lock_get_index_inv : PreservesInvariants mcs_lock_get_index_spec.
Proof.
preserves_invariants_simpl_auto1.
Qed.
End FRESH_PRIM.
Section PASSTHROUGH_PRIM.
Global Instance acquire_shared_inv: SAcquireInvariants acquire_shared0_spec0.
Proof.
constructor; unfold acquire_shared0_spec; intros;
subdestruct; inv H; inv H0; constructor; auto;
exploit index2Z_in_lock_range; eauto; intros; simpl in *;
unfold valid_MCS_log_pool; intros;
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv0.
Transparent CalMCSLock.
- case_eq (zeq i0 z); intros; subst.
+ rewrite ZMap.gss in Hdef; inv Hdef.
unfold valid_MCS_log.
generalize (valid_multi_log_pool_mcs_inv0 _ _ Hrange Hdestruct3); intros.
unfold valid_MCS_log in H1.
simpl in *; subdestruct; inv H2.
eapply H1; auto.
+ rewrite ZMap.gso in Hdef; auto; eapply valid_multi_log_pool_mcs_inv0 in Hdef; eauto.
- case_eq (zeq i0 z); intros; subst.
+ rewrite ZMap.gss in Hdef; inv Hdef.
unfold valid_MCS_log.
generalize (valid_multi_log_pool_mcs_inv0 _ _ Hrange Hdestruct3); intros.
unfold valid_MCS_log in H1.
simpl in *; subdestruct; inv H2.
eapply H1; auto.
+ rewrite ZMap.gso in Hdef; auto; eapply valid_multi_log_pool_mcs_inv0 in Hdef; eauto.
Qed.
Global Instance release_shared_inv: ReleaseInvariants release_shared0_spec0.
Proof.
constructor; unfold release_shared0_spec; intros; subdestruct;
inv H; inv H0; constructor; auto;
exploit index2Z_in_lock_range; eauto; intros; simpl in *;
unfold valid_MCS_log_pool; intros;
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv0.
case_eq (zeq i0 z); intros; subst.
- rewrite ZMap.gss in Hdef; inv Hdef.
unfold valid_MCS_log.
generalize (valid_multi_log_pool_mcs_inv0 _ _ Hrange Hdestruct3); intros.
unfold valid_MCS_log in H1.
simpl in *; subdestruct; inv H2.
eapply H1; auto.
- rewrite ZMap.gso in Hdef; auto; eapply valid_multi_log_pool_mcs_inv0 in Hdef; eauto.
Qed.
Global Instance setPG_inv: PreservesInvariants setPG_spec.
Proof.
preserves_invariants_simpl_auto.
Qed.
Global Instance fstore_inv: PreservesInvariants fstore´_spec.
Proof.
preserves_invariants_simpl_auto.
Qed.
Global Instance setCR3_inv: SetCR3Invariants setCR3_spec.
Proof.
constructor; intros.
- functional inversion H; inv H0; constructor; trivial.
- functional inversion H; inv H0; constructor; auto.
- functional inversion H; simpl in *; assumption.
Qed.
Global Instance trapin_inv: PrimInvariants trapin_spec.
Proof.
PrimInvariants_simpl_auto.
Qed.
Global Instance trapout_inv: PrimInvariants trapout´_spec.
Proof.
PrimInvariants_simpl_auto.
Qed.
Global Instance hostin_inv: PrimInvariants hostin_spec.
Proof.
PrimInvariants_simpl_auto.
Qed.
Global Instance hostout_inv: PrimInvariants hostout´_spec.
Proof.
PrimInvariants_simpl_auto.
Qed.
Global Instance set_curid_inv: PreservesInvariants set_curid_spec.
Proof.
preserves_invariants_simpl_auto; eauto 2.
- rewrite ZMap.gss. auto.
Qed.
Global Instance set_curid_init_inv: PreservesInvariants set_curid_init_spec.
Proof.
preserves_invariants_simpl_auto; eauto 2.
case_eq (zeq (CPU_ID d) (Int.unsigned i)); intros; subst.
- rewrite e; rewrite ZMap.gss; omega.
- rewrite ZMap.gso; auto.
Qed.
Global Instance cli_inv: PreservesInvariants cli_spec.
Proof.
econstructor; intros; inv H; functional inversion H1; subst.
- inv H0; constructor; trivial.
- inv H0; constructor; auto.
- simpl in *; assumption.
Qed.
Global Instance sti_inv: PreservesInvariants sti_spec.
Proof.
econstructor; intros; inv H; functional inversion H1; subst.
- inv H0; constructor; trivial.
- inv H0; constructor; auto.
- simpl in *; assumption.
Qed.
Require Import FutureTactic.
Global Instance serial_in_inv: PreservesInvariants serial_in_spec.
Proof.
preserves_invariants_subst low_level_invariant high_level_invariant;
try eauto using valid_multi_log_pool_mcs_inv0;
try eauto using valid_multi_oracle_pool_mcs_inv0.
Qed.
Global Instance serial_out_inv: PreservesInvariants serial_out_spec.
Proof.
preserves_invariants_subst low_level_invariant high_level_invariant;
try eauto using valid_multi_log_pool_mcs_inv0;
try eauto using valid_multi_oracle_pool_mcs_inv0.
Qed.
Global Instance serial_hw_intr_inv: PreservesInvariants serial_hw_intr_spec.
Proof.
preserves_invariants_nested low_level_invariant high_level_invariant;
try eauto using valid_multi_log_pool_mcs_inv0;
try eauto using valid_multi_oracle_pool_mcs_inv0.
Qed.
Global Instance ic_intr_inv: PreservesInvariants ic_intr_spec.
Proof.
preserves_invariants_nested low_level_invariant high_level_invariant;
try eauto using valid_multi_log_pool_mcs_inv0;
try eauto using valid_multi_oracle_pool_mcs_inv0.
Qed.
Global Instance keyboard_in_inv: PreservesInvariants keyboard_in_spec.
Proof.
preserves_invariants_subst low_level_invariant high_level_invariant;
try eauto using valid_multi_log_pool_mcs_inv0;
try eauto using valid_multi_oracle_pool_mcs_inv0.
Qed.
Global Instance keyboard_hw_intr_inv: PreservesInvariants keyboard_hw_intr_spec.
Proof.
preserves_invariants_nested low_level_invariant high_level_invariant;
try eauto using valid_multi_log_pool_mcs_inv0;
try eauto using valid_multi_oracle_pool_mcs_inv0.
Qed.
Global Instance ioapic_read_inv: PreservesInvariants ioapic_read_spec.
Proof.
preserves_invariants_simpl low_level_invariant high_level_invariant;
try eauto using valid_multi_log_pool_mcs_inv0;
try eauto using valid_multi_oracle_pool_mcs_inv0.
Qed.
Global Instance ioapic_write_inv: PreservesInvariants ioapic_write_spec.
Proof.
preserves_invariants_simpl low_level_invariant high_level_invariant;
try eauto using valid_multi_log_pool_mcs_inv0;
try eauto using valid_multi_oracle_pool_mcs_inv0.
Qed.
Global Instance lapic_read_inv: PreservesInvariants lapic_read_spec.
Proof.
preserves_invariants_simpl low_level_invariant high_level_invariant;
try eauto using valid_multi_log_pool_mcs_inv0;
try eauto using valid_multi_oracle_pool_mcs_inv0.
Qed.
Global Instance lapic_write_inv: PreservesInvariants lapic_write_spec.
Proof.
preserves_invariants_simpl low_level_invariant high_level_invariant;
try eauto using valid_multi_log_pool_mcs_inv0;
try eauto using valid_multi_oracle_pool_mcs_inv0.
Qed.
Global Instance iret_inv: PreservesInvariants iret_spec.
Proof.
preserves_invariants_direct low_level_invariant high_level_invariant; eauto 2.
Qed.
Global Instance local_irq_save_inv: PreservesInvariants local_irq_save_spec.
Proof.
preserves_invariants_simpl low_level_invariant high_level_invariant; eauto 2.
Qed.
Global Instance local_irq_restore_inv: PreservesInvariants local_irq_restore_spec.
Proof.
preserves_invariants_simpl low_level_invariant high_level_invariant; eauto 2.
Qed.
Global Instance save_context_inv: SaveContextInvariants save_context_spec.
Proof.
constructor; intros.
-
inv H0. unfold save_context_spec; simpl. inv H1.
constructor; simpl; trivial.
induction (tf d).
simpl.
constructor.
constructor.
simpl.
apply inv_reg_wt.
simpl.
inv inv_inject_neutral.
eapply inv_reg_inject_neutral; auto.
constructor.
constructor.
inv tf_INJECT.
assumption.
eapply IHt; auto.
inv tf_INJECT.
assumption.
-
inv H0. unfold save_context_spec; simpl.
constructor; simpl; trivial.
Qed.
Global Instance restore_context_inv: RestoreContextInvariants restore_context_spec.
Proof.
constructor; intros.
-
inv H0. functional inversion H; inv H1;
constructor; simpl; trivial.
rewrite H4 in ×.
clear H4 H.
generalize dependent _x.
induction _x0.
intros.
simpl in ×.
constructor.
intros.
simpl in ×.
constructor.
inv tf_INJECT.
assumption.
eapply IH_x0; auto.
inv tf_INJECT; assumption.
-
inv H0. functional inversion H; subst;
constructor; simpl; trivial.
Qed.
Global Instance proc_create_postinit_inv:
PreservesInvariants proc_create_postinit_spec.
Proof.
preserves_invariants_simpl low_level_invariant high_level_invariant; eauto 2.
Qed.
End PASSTHROUGH_PRIM.
End INV.
Definition exec_loadex {F V} := exec_loadex1 (F := F) (V := V).
Definition exec_storeex {F V} := exec_storeex1 (flatmem_store:= flatmem_store´) (F := F) (V := V).
Global Instance flatmem_store_inv: FlatmemStoreInvariant (flatmem_store:= flatmem_store´).
Proof.
split; inversion 1; intros.
- functional inversion H0; constructor; auto.
- functional inversion H1; constructor; auto.
Qed.
Global Instance trapinfo_set_inv: TrapinfoSetInvariant.
Proof.
split; inversion 1; intros; constructor; auto.
Qed.
Global Instance page_copy_inv: PreservesInvariants page_copy´´´_spec.
Proof.
preserves_invariants_simpl_auto.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv0.
unfold valid_MCS_log_pool.
intros.
case_eq (zeq i2 abid); intros; subst.
- rewrite ZMap.gss in Hdef.
inv Hdef.
eapply valid_multi_log_pool_mcs_inv0 in H7; eauto.
unfold valid_MCS_log in H7.
unfold valid_MCS_log.
intros.
Transparent CalMCSLock.
simpl in H9.
destruct (CalMCSLock l) eqn:?; try (inv H9; fail).
inv H9.
eapply H7; eauto.
- rewrite ZMap.gso in Hdef; eauto.
Qed.
Global Instance page_copy_back_inv: PreservesInvariants page_copy_back´_spec.
Proof.
preserves_invariants_simpl_auto.
Qed.
Definition mmcslockabsintro_fresh : compatlayer (cdata RData) :=
ticket_lock_init ↦ gensem ticket_lock_init_spec
⊕ mcs_get_next ↦ gensem mcs_get_next_spec
⊕ mcs_set_next ↦ gensem mcs_set_next_spec
⊕ mcs_get_busy ↦ gensem mcs_get_busy_spec
⊕ mcs_set_busy ↦ gensem mcs_set_busy_spec
⊕ mcs_swap_tail ↦ gensem mcs_swap_tail_spec
⊕ mcs_cas_tail ↦ gensem mcs_cas_tail_spec
⊕ mcs_lock_get_index ↦ gensem mcs_lock_get_index_spec.
Definition mmcslockabsintro_passthrough : compatlayer (cdata RData) :=
fload ↦ gensem fload´_spec
⊕ fstore ↦ gensem fstore´_spec
⊕ page_copy ↦ gensem page_copy´´´_spec
⊕ page_copy_back ↦ gensem page_copy_back´_spec
⊕ vmxinfo_get ↦ gensem vmxinfo_get_spec
⊕ set_pg ↦ gensem setPG_spec
⊕ set_cr3 ↦ setCR3_compatsem setCR3_spec
⊕ get_size ↦ gensem MMSize
⊕ is_usable ↦ gensem is_mm_usable_spec
⊕ get_mms ↦ gensem get_mm_s_spec
⊕ get_mml ↦ gensem get_mm_l_spec
⊕ get_CPU_ID ↦ gensem get_CPU_ID_spec
⊕ release_shared ↦ primcall_release_lock_compatsem release_shared release_shared0_spec0
⊕ acquire_shared ↦ primcall_acquire_shared_compatsem acquire_shared0_spec0
⊕ get_curid ↦ gensem get_curid_spec
⊕ set_curid ↦ gensem set_curid_spec
⊕ set_curid_init ↦ gensem set_curid_init_spec
⊕ trap_in ↦ primcall_general_compatsem trapin_spec
⊕ trap_out ↦ primcall_general_compatsem trapout´_spec
⊕ host_in ↦ primcall_general_compatsem hostin_spec
⊕ host_out ↦ primcall_general_compatsem hostout´_spec
⊕ proc_create_postinit ↦ gensem proc_create_postinit_spec
⊕ trap_get ↦ primcall_trap_info_get_compatsem trap_info_get_spec
⊕ trap_set ↦ primcall_trap_info_ret_compatsem trap_info_ret_spec
⊕ serial_irq_check ↦ gensem serial_irq_check_spec
⊕ iret ↦ gensem iret_spec
⊕ cli ↦ gensem cli_spec
⊕ sti ↦ gensem sti_spec
⊕ serial_irq_current ↦ gensem serial_irq_current_spec
⊕ ic_intr ↦ gensem ic_intr_spec
⊕ save_context ↦ primcall_save_context_compatsem save_context_spec
⊕ restore_context ↦ primcall_restore_context_compatsem restore_context_spec
⊕ local_irq_save ↦ gensem local_irq_save_spec
⊕ local_irq_restore ↦ gensem local_irq_restore_spec
⊕ serial_in ↦ gensem serial_in_spec
ticket_lock_init ↦ gensem ticket_lock_init_spec
⊕ mcs_get_next ↦ gensem mcs_get_next_spec
⊕ mcs_set_next ↦ gensem mcs_set_next_spec
⊕ mcs_get_busy ↦ gensem mcs_get_busy_spec
⊕ mcs_set_busy ↦ gensem mcs_set_busy_spec
⊕ mcs_swap_tail ↦ gensem mcs_swap_tail_spec
⊕ mcs_cas_tail ↦ gensem mcs_cas_tail_spec
⊕ mcs_lock_get_index ↦ gensem mcs_lock_get_index_spec.
Definition mmcslockabsintro_passthrough : compatlayer (cdata RData) :=
fload ↦ gensem fload´_spec
⊕ fstore ↦ gensem fstore´_spec
⊕ page_copy ↦ gensem page_copy´´´_spec
⊕ page_copy_back ↦ gensem page_copy_back´_spec
⊕ vmxinfo_get ↦ gensem vmxinfo_get_spec
⊕ set_pg ↦ gensem setPG_spec
⊕ set_cr3 ↦ setCR3_compatsem setCR3_spec
⊕ get_size ↦ gensem MMSize
⊕ is_usable ↦ gensem is_mm_usable_spec
⊕ get_mms ↦ gensem get_mm_s_spec
⊕ get_mml ↦ gensem get_mm_l_spec
⊕ get_CPU_ID ↦ gensem get_CPU_ID_spec
⊕ release_shared ↦ primcall_release_lock_compatsem release_shared release_shared0_spec0
⊕ acquire_shared ↦ primcall_acquire_shared_compatsem acquire_shared0_spec0
⊕ get_curid ↦ gensem get_curid_spec
⊕ set_curid ↦ gensem set_curid_spec
⊕ set_curid_init ↦ gensem set_curid_init_spec
⊕ trap_in ↦ primcall_general_compatsem trapin_spec
⊕ trap_out ↦ primcall_general_compatsem trapout´_spec
⊕ host_in ↦ primcall_general_compatsem hostin_spec
⊕ host_out ↦ primcall_general_compatsem hostout´_spec
⊕ proc_create_postinit ↦ gensem proc_create_postinit_spec
⊕ trap_get ↦ primcall_trap_info_get_compatsem trap_info_get_spec
⊕ trap_set ↦ primcall_trap_info_ret_compatsem trap_info_ret_spec
⊕ serial_irq_check ↦ gensem serial_irq_check_spec
⊕ iret ↦ gensem iret_spec
⊕ cli ↦ gensem cli_spec
⊕ sti ↦ gensem sti_spec
⊕ serial_irq_current ↦ gensem serial_irq_current_spec
⊕ ic_intr ↦ gensem ic_intr_spec
⊕ save_context ↦ primcall_save_context_compatsem save_context_spec
⊕ restore_context ↦ primcall_restore_context_compatsem restore_context_spec
⊕ local_irq_save ↦ gensem local_irq_save_spec
⊕ local_irq_restore ↦ gensem local_irq_restore_spec
⊕ serial_in ↦ gensem serial_in_spec
serial device
serial device
serial device
ioapic device
ioapic device
lapic device
lapic device
⊕ accessors ↦ {| exec_load := @exec_loadex; exec_store := @exec_storeex |}.
Definition mmcslockabsintro : compatlayer (cdata RData) := mmcslockabsintro_fresh ⊕ mmcslockabsintro_passthrough.
End WITHMEM.
Definition mmcslockabsintro : compatlayer (cdata RData) := mmcslockabsintro_fresh ⊕ mmcslockabsintro_passthrough.
End WITHMEM.