Library mcertikos.mcslock.MMCSLockOp
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 MMCSLockAbsIntro.
Require Import ObjMCSLock.
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 MMCSLockAbsIntro.
Require Import ObjMCSLock.
Section WITHMEM.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Context `{mcs_oracle_prop: MCSOracleProp}.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{fairness: WaitTime}.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Context `{mcs_oracle_prop: MCSOracleProp}.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{fairness: WaitTime}.
Section INV.
Lemma CalMCS_RelWaitPreserveInv:
∀ cur_loop_index lock_index d pre_log res,
ihost d = true →
ikern d = true →
0 ≤ lock_index < lock_range →
high_level_invariant d →
ZMap.get lock_index (multi_log d) = MultiDef pre_log →
CalMCS_RelWait cur_loop_index (CPU_ID d) pre_log
(ZMap.get lock_index (multi_oracle d)) = Some res →
valid_MCS_log res.
Proof.
induction cur_loop_index; intros.
- Transparent CalMCS_RelWait.
simpl in H4.
inv H4.
- simpl in H4.
subdestruct.
+ assert (new_ikern:
ikern (d {multi_log:
ZMap.set lock_index
(MultiDef
(TEVENT (CPU_ID d) (TTICKET GET_NEXT)
:: ZMap.get lock_index
(multi_oracle d) (CPU_ID d) pre_log ++ pre_log))
(multi_log d)}) = true).
{ simpl; auto. }
eapply IHcur_loop_index in new_ikern; eauto;
[ | simpl; rewrite ZMap.gss; auto].
inv H2.
econstructor; simpl; eauto.
intros.
unfold valid_MCS_log_pool.
intros.
simpl in new_ikern.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
case_eq (zeq i lock_index); subst; intros.
× subst; rewrite ZMap.gss in Hdef; inv Hdef.
assert (valid_MCS_log pre_log).
{ eapply valid_multi_log_pool_mcs_inv; eauto. }
unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
eapply valid_multi_oracle_pool_mcs_inv with (i := lock_index) (i0 := (CPU_ID d)) in H5;
auto.
unfold valid_MCS_log in H5; unfold valid_MCS_log.
intros; simpl.
unfold MCSCorrect_range in H5; unfold MCSCorrect_range.
intros.
Transparent CalMCSLock.
simpl in H6; subdestruct.
inv Hmcs; inv H6.
eapply H5; eauto.
× rewrite ZMap.gso in Hdef; eauto.
+ inv H4.
assert (intermid_valid:
valid_MCS_log (TEVENT (CPU_ID d) (TTICKET GET_NEXT)
:: ZMap.get lock_index (multi_oracle d) (CPU_ID d)
pre_log ++ pre_log)).
{ inv H2.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
assert (valid_MCS_log pre_log).
{ eapply valid_multi_log_pool_mcs_inv; eauto. }
unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
eapply valid_multi_oracle_pool_mcs_inv with (i := lock_index) (i0 := (CPU_ID d)) in H2; auto.
unfold valid_MCS_log in H2; unfold valid_MCS_log.
intros.
simpl in H4.
subdestruct.
subst.
inv H4.
eapply H2; eauto. }
inv H2.
unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
eapply valid_multi_oracle_pool_mcs_inv with (i := lock_index) (i0 := (CPU_ID d))
in intermid_valid; auto.
unfold valid_MCS_log in intermid_valid; unfold valid_MCS_log.
unfold MCSCorrect_range in intermid_valid; unfold MCSCorrect_range.
intros.
simpl in H2; subdestruct.
inv Hmcs; inv H2; inv Hdestruct3.
assert (MCSLOCK tail0 lock_array0 bounds0 = MCSLOCK tail0 lock_array0 bounds0).
{ reflexivity. }
eapply intermid_valid in H2; destruct H2; try eauto.
split; try tauto.
intros.
case_eq (zeq i z1); intros.
× subst. rewrite ZMap.gss; simpl; auto.
eapply H4 in H5.
rewrite Hdestruct8 in H5.
simpl; trivial.
× rewrite ZMap.gso; simpl; auto.
Opaque CalMCS_RelWait CalMCSLock.
Qed.
Lemma CalMCS_AcqWaitPreserveInv:
∀ cur_loop_index lock_index d pre_log res,
ihost d = true →
ikern d = true →
0 ≤ lock_index < lock_range →
high_level_invariant d →
ZMap.get lock_index (multi_log d) = MultiDef pre_log →
CalMCS_AcqWait cur_loop_index (CPU_ID d) pre_log
(ZMap.get lock_index (multi_oracle d)) = Some res →
valid_MCS_log res.
Proof.
induction cur_loop_index; intros.
- Transparent CalMCS_AcqWait.
simpl in H4.
inv H4.
- simpl in H4.
subdestruct.
+ assert (new_ikern:
ikern (d {multi_log:
ZMap.set lock_index
(MultiDef
(TEVENT (CPU_ID d) (TTICKET (GET_BUSY true))
:: ZMap.get lock_index
(multi_oracle d) (CPU_ID d) pre_log ++ pre_log))
(multi_log d)}) = true).
{ simpl; auto. }
eapply IHcur_loop_index in new_ikern; eauto;
[ | simpl; rewrite ZMap.gss; auto].
inv H2.
econstructor; simpl; eauto.
intros.
unfold valid_MCS_log_pool.
intros.
simpl in new_ikern.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
case_eq (zeq i lock_index); subst; intros.
× subst; rewrite ZMap.gss in Hdef; inv Hdef.
assert (valid_MCS_log pre_log).
{ eapply valid_multi_log_pool_mcs_inv; eauto. }
unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
eapply valid_multi_oracle_pool_mcs_inv with (i := lock_index) (i0 := (CPU_ID d)) in H5;
auto.
unfold valid_MCS_log in H5; unfold valid_MCS_log.
intros; simpl.
unfold MCSCorrect_range in H5; unfold MCSCorrect_range.
intros.
Transparent CalMCSLock.
simpl in H6; subdestruct.
inv Hmcs; inv H6; inv Hdestruct.
eapply H5; eauto.
× rewrite ZMap.gso in Hdef; eauto.
+ inv H4.
inv H2.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
assert (valid_MCS_log pre_log).
{ eapply valid_multi_log_pool_mcs_inv; eauto. }
unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
eapply valid_multi_oracle_pool_mcs_inv with (i := lock_index) (i0 := (CPU_ID d)) in H2; auto.
unfold valid_MCS_log in H3; unfold valid_MCS_log.
intros.
simpl in H4.
subdestruct.
inv H4.
eapply H2; eauto.
Qed.
Global Instance mcs_pass_lock_inv: PreservesInvariants mcs_pass_lock_spec.
Proof.
preserves_invariants_simpl_auto1.
- assert (true = true) by reflexivity.
assert (lock_range_val: 0 ≤ z < lock_range).
{ unfold index2Z in Hdestruct1.
unfold lock_range. unfold ID_AT_range, ID_TCB_range, ID_SC_range.
Opaque Z.add Z.mul.
subdestruct.
unfold index_range in Hdestruct4.
inv Hdestruct1.
subdestruct.
- unfold index_incrange in Hdestruct7.
inv Hdestruct7.
unfold ID_AT_range in Hdestruct4; inv Hdestruct4.
omega.
- unfold ID_SC_range in Hdestruct4.
inv Hdestruct4.
unfold index_incrange in Hdestruct7.
unfold lock_TCB_range in Hdestruct7; inv Hdestruct7.
unfold ID_AT_range, ID_TCB_range; omega.
- unfold ID_TCB_range in Hdestruct4; inv Hdestruct4.
unfold index_incrange in Hdestruct7; inv Hdestruct7.
unfold ID_AT_range; omega. }
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
generalize lock_range_val; intro lock_range_val´.
eapply valid_multi_log_pool_mcs_inv in lock_range_val; eauto.
unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
eapply valid_multi_oracle_pool_mcs_inv with (i := z) (i0 := CPU_ID d)
in lock_range_val; eauto.
unfold valid_MCS_log_pool.
intros.
case_eq (zeq i1 z); intros.
+ unfold valid_MCS_log.
unfold valid_MCS_log in lock_range_val.
intros.
unfold MCSCorrect_range in ×.
intros.
subst.
rewrite ZMap.gss in Hdef.
inv Hdef.
Transparent CalMCSLock.
simpl in H1.
subdestruct.
inv H1.
inv Hdestruct3.
assert ((MCSLOCK (CPU_ID d) lock_array bounds) =
(MCSLOCK (CPU_ID d) lock_array bounds)) by reflexivity.
eapply lock_range_val in H1; eauto.
destruct H1.
split; unfold NULL; eauto; omega.
+ rewrite ZMap.gso in Hdef; inv Hdef; eauto.
- assert (lock_range_val: 0 ≤ z < lock_range).
{ unfold index2Z in Hdestruct1.
unfold lock_range. unfold ID_AT_range, ID_TCB_range, ID_SC_range.
Opaque Z.add Z.mul.
subdestruct.
unfold index_range in Hdestruct4.
inv Hdestruct1.
subdestruct.
- unfold index_incrange in Hdestruct9.
inv Hdestruct9.
unfold ID_AT_range in Hdestruct4; inv Hdestruct4.
omega.
- unfold ID_SC_range in Hdestruct4.
inv Hdestruct4.
unfold index_incrange in Hdestruct9.
unfold lock_TCB_range in Hdestruct9; inv Hdestruct9.
unfold ID_AT_range, ID_TCB_range; omega.
- unfold ID_TCB_range in Hdestruct4; inv Hdestruct4.
unfold index_incrange in Hdestruct9; inv Hdestruct9.
unfold ID_AT_range; omega. }
assert (high_level_invariant
(d {multi_log :
ZMap.set z
(MultiDef
(TEVENT (CPU_ID d) (TTICKET (CAS_TAIL false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l))
(multi_log d)})).
{ econstructor; simpl; try auto.
intros.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
assert (valid_MCS_log l).
eapply valid_multi_log_pool_mcs_inv; eauto.
eapply valid_multi_oracle_pool_mcs_inv with (i := z) (i0 := (CPU_ID d)) in H; auto.
unfold valid_MCS_log in H; unfold valid_MCS_log_pool.
intros.
case_eq (zeq i1 z); intros; subst.
+ rewrite ZMap.gss in Hdef; auto.
inv Hdef.
unfold MCSCorrect_range in H.
unfold valid_MCS_log.
intros.
unfold MCSCorrect_range.
intros.
simpl in H1.
subdestruct.
inv Hmcs; inv H1.
inv Hdestruct3.
assert (MCSLOCK tail lock_array bounds = MCSLOCK tail lock_array bounds) by reflexivity.
eapply H in H1; eauto.
+ rewrite ZMap.gso in Hdef; auto.
eapply valid_multi_log_pool_mcs_inv with (i := i1); auto. }
assert (ZMap.get z
(multi_log
d
{multi_log
: ZMap.set z
(MultiDef
(TEVENT (CPU_ID d) (TTICKET (CAS_TAIL false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l))
(multi_log d)}) =
MultiDef
(TEVENT (CPU_ID d) (TTICKET (CAS_TAIL false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l)).
{ simpl.
rewrite ZMap.gss; auto. }
eapply CalMCS_RelWaitPreserveInv in H0; eauto.
unfold valid_MCS_log_pool.
intros.
case_eq (zeq i1 z); intros; subst.
+ rewrite ZMap.gss in Hdef; auto.
inv Hdef; auto.
+ rewrite ZMap.gso in Hdef; auto.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
eapply valid_multi_log_pool_mcs_inv with (i := i1); auto.
Qed.
Global Instance mcs_wait_lock_inv : PreservesInvariants mcs_wait_lock_spec.
Proof.
preserves_invariants_simpl_auto1.
- assert (lock_range_val: 0 ≤ z < lock_range).
{ unfold index2Z in Hdestruct1.
unfold lock_range. unfold ID_AT_range, ID_TCB_range, ID_SC_range.
Opaque Z.add Z.mul.
subdestruct.
unfold index_range in Hdestruct4.
inv Hdestruct1.
subdestruct.
- unfold index_incrange in Hdestruct7.
inv Hdestruct7.
unfold ID_AT_range in Hdestruct4; inv Hdestruct4.
omega.
- unfold ID_SC_range in Hdestruct4.
inv Hdestruct4.
unfold index_incrange in Hdestruct7.
unfold lock_TCB_range in Hdestruct7; inv Hdestruct7.
unfold ID_AT_range, ID_TCB_range; omega.
- unfold ID_TCB_range in Hdestruct4; inv Hdestruct4.
unfold index_incrange in Hdestruct7; inv Hdestruct7.
unfold ID_AT_range; omega. }
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
generalize lock_range_val; intro lock_range_val´.
eapply valid_multi_log_pool_mcs_inv in lock_range_val; eauto.
unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
eapply valid_multi_oracle_pool_mcs_inv with (i := z) (i0 := CPU_ID d)
in lock_range_val; eauto.
unfold valid_MCS_log_pool.
intros.
case_eq (zeq i2 z); intros.
+ unfold valid_MCS_log.
unfold valid_MCS_log in lock_range_val.
intros.
unfold MCSCorrect_range in ×.
intros.
subst.
rewrite ZMap.gss in Hdef.
inv Hdef.
Transparent CalMCSLock.
simpl in H0.
subdestruct.
inv H0.
inv Hdestruct3.
assert ((MCSLOCK NULL lock_array bounds) =
(MCSLOCK NULL lock_array bounds)) by reflexivity.
eapply lock_range_val in H0; eauto.
destruct H0.
split; unfold NULL; eauto; try omega.
intros.
case_eq (zeq i2 (CPU_ID d)); intros.
× subst.
rewrite ZMap.gss; auto.
× rewrite ZMap.gso; auto.
+ rewrite ZMap.gso in Hdef; inv Hdef; eauto.
- assert (lock_range_val: 0 ≤ z < lock_range).
{ unfold index2Z in Hdestruct1.
unfold lock_range. unfold ID_AT_range, ID_TCB_range, ID_SC_range.
Opaque Z.add Z.mul.
subdestruct.
unfold index_range in Hdestruct4.
inv Hdestruct1.
subdestruct.
- unfold index_incrange in Hdestruct8.
inv Hdestruct8.
unfold ID_AT_range in Hdestruct4; inv Hdestruct4.
omega.
- unfold ID_SC_range in Hdestruct4.
inv Hdestruct4.
unfold index_incrange in Hdestruct8.
unfold lock_TCB_range in Hdestruct8; inv Hdestruct8.
unfold ID_AT_range, ID_TCB_range; omega.
- unfold ID_TCB_range in Hdestruct4; inv Hdestruct4.
unfold index_incrange in Hdestruct8; inv Hdestruct8.
unfold ID_AT_range; omega. }
assert (high_level_invariant
(d {multi_log :
ZMap.set z
(MultiDef
(TEVENT (CPU_ID d) (TTICKET (SET_NEXT tail))
:: ZMap.get z (multi_oracle d) (CPU_ID d)
(TEVENT (CPU_ID d)
(TTICKET
(SWAP_TAIL (nat_of_Z (Int.unsigned i)) false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l)
++
TEVENT (CPU_ID d)
(TTICKET
(SWAP_TAIL (nat_of_Z (Int.unsigned i)) false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l))
(multi_log d)})).
{ econstructor; simpl; try auto.
intros.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
assert (valid_MCS_log l).
eapply valid_multi_log_pool_mcs_inv; eauto.
eapply valid_multi_oracle_pool_mcs_inv with (i := z) (i0 := (CPU_ID d)) in H; auto.
assert (valid_MCS_log
(TEVENT (CPU_ID d)
(TTICKET (SWAP_TAIL (nat_of_Z (Int.unsigned i)) false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l)).
{ simpl.
unfold valid_MCS_log; intros.
unfold valid_MCS_log in H.
unfold MCSCorrect_range in H; unfold MCSCorrect_range.
simpl in H0; subdestruct.
inv H0.
inv Hdestruct3.
assert (MCSLOCK tail lock_array bounds = MCSLOCK tail lock_array bounds) by reflexivity.
eapply H in H0; eauto.
intros.
inv Hmcs.
split; try omega.
intros.
case_eq (zeq i2 (CPU_ID d)); intros; subst.
+ rewrite ZMap.gss; simpl; unfold NULL; omega.
+ rewrite ZMap.gso; auto.
destruct H0.
apply H3 in H1; simpl in H3; auto. }
eapply valid_multi_oracle_pool_mcs_inv with (i := z) (i0 := (CPU_ID d)) in H0; auto.
unfold valid_MCS_log in H0; unfold valid_MCS_log_pool.
intros.
case_eq (zeq i2 z); intros; subst.
+ rewrite ZMap.gss in Hdef; auto.
inv Hdef.
unfold MCSCorrect_range in H0.
unfold valid_MCS_log.
intros.
unfold MCSCorrect_range.
intros.
simpl in H2.
subdestruct.
inv Hmcs; inv H2.
assert (MCSLOCK tl lock_array0 bnd = MCSLOCK tl lock_array0 bnd) by reflexivity.
eapply H0 in H2; eauto.
destruct H2.
split; auto.
intros.
case_eq (zeq i2 tail).
× intros; subst.
rewrite ZMap.gss.
simpl; omega.
× intros.
rewrite ZMap.gso; auto.
+ rewrite ZMap.gso in Hdef; auto.
eapply valid_multi_log_pool_mcs_inv with (i := i2); auto. }
assert (ZMap.get z
(multi_log
d {multi_log
: ZMap.set z
(MultiDef
(TEVENT (CPU_ID d) (TTICKET (SET_NEXT tail))
:: ZMap.get z (multi_oracle d) (CPU_ID d)
(TEVENT (CPU_ID d)
(TTICKET
(SWAP_TAIL (nat_of_Z (Int.unsigned i))
false))
:: ZMap.get z (multi_oracle d) (CPU_ID d)
l ++ l) ++
TEVENT (CPU_ID d)
(TTICKET
(SWAP_TAIL (nat_of_Z (Int.unsigned i)) false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l))
(multi_log d)}) =
(MultiDef
(TEVENT (CPU_ID d) (TTICKET (SET_NEXT tail))
:: ZMap.get z (multi_oracle d) (CPU_ID d)
(TEVENT (CPU_ID d)
(TTICKET
(SWAP_TAIL (nat_of_Z (Int.unsigned i))
false))
:: ZMap.get z (multi_oracle d) (CPU_ID d)
l ++ l) ++
TEVENT (CPU_ID d)
(TTICKET
(SWAP_TAIL (nat_of_Z (Int.unsigned i)) false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l))).
{ simpl.
rewrite ZMap.gss; auto. }
eapply CalMCS_AcqWaitPreserveInv in H0; eauto.
unfold valid_MCS_log_pool.
intros.
case_eq (zeq i2 z); intros; subst.
+ rewrite ZMap.gss in Hdef; auto.
inv Hdef; auto.
+ rewrite ZMap.gso in Hdef; auto.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
eapply valid_multi_log_pool_mcs_inv with (i := i2); auto.
Qed.
End INV.
Lemma CalMCS_RelWaitPreserveInv:
∀ cur_loop_index lock_index d pre_log res,
ihost d = true →
ikern d = true →
0 ≤ lock_index < lock_range →
high_level_invariant d →
ZMap.get lock_index (multi_log d) = MultiDef pre_log →
CalMCS_RelWait cur_loop_index (CPU_ID d) pre_log
(ZMap.get lock_index (multi_oracle d)) = Some res →
valid_MCS_log res.
Proof.
induction cur_loop_index; intros.
- Transparent CalMCS_RelWait.
simpl in H4.
inv H4.
- simpl in H4.
subdestruct.
+ assert (new_ikern:
ikern (d {multi_log:
ZMap.set lock_index
(MultiDef
(TEVENT (CPU_ID d) (TTICKET GET_NEXT)
:: ZMap.get lock_index
(multi_oracle d) (CPU_ID d) pre_log ++ pre_log))
(multi_log d)}) = true).
{ simpl; auto. }
eapply IHcur_loop_index in new_ikern; eauto;
[ | simpl; rewrite ZMap.gss; auto].
inv H2.
econstructor; simpl; eauto.
intros.
unfold valid_MCS_log_pool.
intros.
simpl in new_ikern.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
case_eq (zeq i lock_index); subst; intros.
× subst; rewrite ZMap.gss in Hdef; inv Hdef.
assert (valid_MCS_log pre_log).
{ eapply valid_multi_log_pool_mcs_inv; eauto. }
unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
eapply valid_multi_oracle_pool_mcs_inv with (i := lock_index) (i0 := (CPU_ID d)) in H5;
auto.
unfold valid_MCS_log in H5; unfold valid_MCS_log.
intros; simpl.
unfold MCSCorrect_range in H5; unfold MCSCorrect_range.
intros.
Transparent CalMCSLock.
simpl in H6; subdestruct.
inv Hmcs; inv H6.
eapply H5; eauto.
× rewrite ZMap.gso in Hdef; eauto.
+ inv H4.
assert (intermid_valid:
valid_MCS_log (TEVENT (CPU_ID d) (TTICKET GET_NEXT)
:: ZMap.get lock_index (multi_oracle d) (CPU_ID d)
pre_log ++ pre_log)).
{ inv H2.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
assert (valid_MCS_log pre_log).
{ eapply valid_multi_log_pool_mcs_inv; eauto. }
unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
eapply valid_multi_oracle_pool_mcs_inv with (i := lock_index) (i0 := (CPU_ID d)) in H2; auto.
unfold valid_MCS_log in H2; unfold valid_MCS_log.
intros.
simpl in H4.
subdestruct.
subst.
inv H4.
eapply H2; eauto. }
inv H2.
unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
eapply valid_multi_oracle_pool_mcs_inv with (i := lock_index) (i0 := (CPU_ID d))
in intermid_valid; auto.
unfold valid_MCS_log in intermid_valid; unfold valid_MCS_log.
unfold MCSCorrect_range in intermid_valid; unfold MCSCorrect_range.
intros.
simpl in H2; subdestruct.
inv Hmcs; inv H2; inv Hdestruct3.
assert (MCSLOCK tail0 lock_array0 bounds0 = MCSLOCK tail0 lock_array0 bounds0).
{ reflexivity. }
eapply intermid_valid in H2; destruct H2; try eauto.
split; try tauto.
intros.
case_eq (zeq i z1); intros.
× subst. rewrite ZMap.gss; simpl; auto.
eapply H4 in H5.
rewrite Hdestruct8 in H5.
simpl; trivial.
× rewrite ZMap.gso; simpl; auto.
Opaque CalMCS_RelWait CalMCSLock.
Qed.
Lemma CalMCS_AcqWaitPreserveInv:
∀ cur_loop_index lock_index d pre_log res,
ihost d = true →
ikern d = true →
0 ≤ lock_index < lock_range →
high_level_invariant d →
ZMap.get lock_index (multi_log d) = MultiDef pre_log →
CalMCS_AcqWait cur_loop_index (CPU_ID d) pre_log
(ZMap.get lock_index (multi_oracle d)) = Some res →
valid_MCS_log res.
Proof.
induction cur_loop_index; intros.
- Transparent CalMCS_AcqWait.
simpl in H4.
inv H4.
- simpl in H4.
subdestruct.
+ assert (new_ikern:
ikern (d {multi_log:
ZMap.set lock_index
(MultiDef
(TEVENT (CPU_ID d) (TTICKET (GET_BUSY true))
:: ZMap.get lock_index
(multi_oracle d) (CPU_ID d) pre_log ++ pre_log))
(multi_log d)}) = true).
{ simpl; auto. }
eapply IHcur_loop_index in new_ikern; eauto;
[ | simpl; rewrite ZMap.gss; auto].
inv H2.
econstructor; simpl; eauto.
intros.
unfold valid_MCS_log_pool.
intros.
simpl in new_ikern.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
case_eq (zeq i lock_index); subst; intros.
× subst; rewrite ZMap.gss in Hdef; inv Hdef.
assert (valid_MCS_log pre_log).
{ eapply valid_multi_log_pool_mcs_inv; eauto. }
unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
eapply valid_multi_oracle_pool_mcs_inv with (i := lock_index) (i0 := (CPU_ID d)) in H5;
auto.
unfold valid_MCS_log in H5; unfold valid_MCS_log.
intros; simpl.
unfold MCSCorrect_range in H5; unfold MCSCorrect_range.
intros.
Transparent CalMCSLock.
simpl in H6; subdestruct.
inv Hmcs; inv H6; inv Hdestruct.
eapply H5; eauto.
× rewrite ZMap.gso in Hdef; eauto.
+ inv H4.
inv H2.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
assert (valid_MCS_log pre_log).
{ eapply valid_multi_log_pool_mcs_inv; eauto. }
unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
eapply valid_multi_oracle_pool_mcs_inv with (i := lock_index) (i0 := (CPU_ID d)) in H2; auto.
unfold valid_MCS_log in H3; unfold valid_MCS_log.
intros.
simpl in H4.
subdestruct.
inv H4.
eapply H2; eauto.
Qed.
Global Instance mcs_pass_lock_inv: PreservesInvariants mcs_pass_lock_spec.
Proof.
preserves_invariants_simpl_auto1.
- assert (true = true) by reflexivity.
assert (lock_range_val: 0 ≤ z < lock_range).
{ unfold index2Z in Hdestruct1.
unfold lock_range. unfold ID_AT_range, ID_TCB_range, ID_SC_range.
Opaque Z.add Z.mul.
subdestruct.
unfold index_range in Hdestruct4.
inv Hdestruct1.
subdestruct.
- unfold index_incrange in Hdestruct7.
inv Hdestruct7.
unfold ID_AT_range in Hdestruct4; inv Hdestruct4.
omega.
- unfold ID_SC_range in Hdestruct4.
inv Hdestruct4.
unfold index_incrange in Hdestruct7.
unfold lock_TCB_range in Hdestruct7; inv Hdestruct7.
unfold ID_AT_range, ID_TCB_range; omega.
- unfold ID_TCB_range in Hdestruct4; inv Hdestruct4.
unfold index_incrange in Hdestruct7; inv Hdestruct7.
unfold ID_AT_range; omega. }
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
generalize lock_range_val; intro lock_range_val´.
eapply valid_multi_log_pool_mcs_inv in lock_range_val; eauto.
unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
eapply valid_multi_oracle_pool_mcs_inv with (i := z) (i0 := CPU_ID d)
in lock_range_val; eauto.
unfold valid_MCS_log_pool.
intros.
case_eq (zeq i1 z); intros.
+ unfold valid_MCS_log.
unfold valid_MCS_log in lock_range_val.
intros.
unfold MCSCorrect_range in ×.
intros.
subst.
rewrite ZMap.gss in Hdef.
inv Hdef.
Transparent CalMCSLock.
simpl in H1.
subdestruct.
inv H1.
inv Hdestruct3.
assert ((MCSLOCK (CPU_ID d) lock_array bounds) =
(MCSLOCK (CPU_ID d) lock_array bounds)) by reflexivity.
eapply lock_range_val in H1; eauto.
destruct H1.
split; unfold NULL; eauto; omega.
+ rewrite ZMap.gso in Hdef; inv Hdef; eauto.
- assert (lock_range_val: 0 ≤ z < lock_range).
{ unfold index2Z in Hdestruct1.
unfold lock_range. unfold ID_AT_range, ID_TCB_range, ID_SC_range.
Opaque Z.add Z.mul.
subdestruct.
unfold index_range in Hdestruct4.
inv Hdestruct1.
subdestruct.
- unfold index_incrange in Hdestruct9.
inv Hdestruct9.
unfold ID_AT_range in Hdestruct4; inv Hdestruct4.
omega.
- unfold ID_SC_range in Hdestruct4.
inv Hdestruct4.
unfold index_incrange in Hdestruct9.
unfold lock_TCB_range in Hdestruct9; inv Hdestruct9.
unfold ID_AT_range, ID_TCB_range; omega.
- unfold ID_TCB_range in Hdestruct4; inv Hdestruct4.
unfold index_incrange in Hdestruct9; inv Hdestruct9.
unfold ID_AT_range; omega. }
assert (high_level_invariant
(d {multi_log :
ZMap.set z
(MultiDef
(TEVENT (CPU_ID d) (TTICKET (CAS_TAIL false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l))
(multi_log d)})).
{ econstructor; simpl; try auto.
intros.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
assert (valid_MCS_log l).
eapply valid_multi_log_pool_mcs_inv; eauto.
eapply valid_multi_oracle_pool_mcs_inv with (i := z) (i0 := (CPU_ID d)) in H; auto.
unfold valid_MCS_log in H; unfold valid_MCS_log_pool.
intros.
case_eq (zeq i1 z); intros; subst.
+ rewrite ZMap.gss in Hdef; auto.
inv Hdef.
unfold MCSCorrect_range in H.
unfold valid_MCS_log.
intros.
unfold MCSCorrect_range.
intros.
simpl in H1.
subdestruct.
inv Hmcs; inv H1.
inv Hdestruct3.
assert (MCSLOCK tail lock_array bounds = MCSLOCK tail lock_array bounds) by reflexivity.
eapply H in H1; eauto.
+ rewrite ZMap.gso in Hdef; auto.
eapply valid_multi_log_pool_mcs_inv with (i := i1); auto. }
assert (ZMap.get z
(multi_log
d
{multi_log
: ZMap.set z
(MultiDef
(TEVENT (CPU_ID d) (TTICKET (CAS_TAIL false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l))
(multi_log d)}) =
MultiDef
(TEVENT (CPU_ID d) (TTICKET (CAS_TAIL false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l)).
{ simpl.
rewrite ZMap.gss; auto. }
eapply CalMCS_RelWaitPreserveInv in H0; eauto.
unfold valid_MCS_log_pool.
intros.
case_eq (zeq i1 z); intros; subst.
+ rewrite ZMap.gss in Hdef; auto.
inv Hdef; auto.
+ rewrite ZMap.gso in Hdef; auto.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
eapply valid_multi_log_pool_mcs_inv with (i := i1); auto.
Qed.
Global Instance mcs_wait_lock_inv : PreservesInvariants mcs_wait_lock_spec.
Proof.
preserves_invariants_simpl_auto1.
- assert (lock_range_val: 0 ≤ z < lock_range).
{ unfold index2Z in Hdestruct1.
unfold lock_range. unfold ID_AT_range, ID_TCB_range, ID_SC_range.
Opaque Z.add Z.mul.
subdestruct.
unfold index_range in Hdestruct4.
inv Hdestruct1.
subdestruct.
- unfold index_incrange in Hdestruct7.
inv Hdestruct7.
unfold ID_AT_range in Hdestruct4; inv Hdestruct4.
omega.
- unfold ID_SC_range in Hdestruct4.
inv Hdestruct4.
unfold index_incrange in Hdestruct7.
unfold lock_TCB_range in Hdestruct7; inv Hdestruct7.
unfold ID_AT_range, ID_TCB_range; omega.
- unfold ID_TCB_range in Hdestruct4; inv Hdestruct4.
unfold index_incrange in Hdestruct7; inv Hdestruct7.
unfold ID_AT_range; omega. }
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
generalize lock_range_val; intro lock_range_val´.
eapply valid_multi_log_pool_mcs_inv in lock_range_val; eauto.
unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
eapply valid_multi_oracle_pool_mcs_inv with (i := z) (i0 := CPU_ID d)
in lock_range_val; eauto.
unfold valid_MCS_log_pool.
intros.
case_eq (zeq i2 z); intros.
+ unfold valid_MCS_log.
unfold valid_MCS_log in lock_range_val.
intros.
unfold MCSCorrect_range in ×.
intros.
subst.
rewrite ZMap.gss in Hdef.
inv Hdef.
Transparent CalMCSLock.
simpl in H0.
subdestruct.
inv H0.
inv Hdestruct3.
assert ((MCSLOCK NULL lock_array bounds) =
(MCSLOCK NULL lock_array bounds)) by reflexivity.
eapply lock_range_val in H0; eauto.
destruct H0.
split; unfold NULL; eauto; try omega.
intros.
case_eq (zeq i2 (CPU_ID d)); intros.
× subst.
rewrite ZMap.gss; auto.
× rewrite ZMap.gso; auto.
+ rewrite ZMap.gso in Hdef; inv Hdef; eauto.
- assert (lock_range_val: 0 ≤ z < lock_range).
{ unfold index2Z in Hdestruct1.
unfold lock_range. unfold ID_AT_range, ID_TCB_range, ID_SC_range.
Opaque Z.add Z.mul.
subdestruct.
unfold index_range in Hdestruct4.
inv Hdestruct1.
subdestruct.
- unfold index_incrange in Hdestruct8.
inv Hdestruct8.
unfold ID_AT_range in Hdestruct4; inv Hdestruct4.
omega.
- unfold ID_SC_range in Hdestruct4.
inv Hdestruct4.
unfold index_incrange in Hdestruct8.
unfold lock_TCB_range in Hdestruct8; inv Hdestruct8.
unfold ID_AT_range, ID_TCB_range; omega.
- unfold ID_TCB_range in Hdestruct4; inv Hdestruct4.
unfold index_incrange in Hdestruct8; inv Hdestruct8.
unfold ID_AT_range; omega. }
assert (high_level_invariant
(d {multi_log :
ZMap.set z
(MultiDef
(TEVENT (CPU_ID d) (TTICKET (SET_NEXT tail))
:: ZMap.get z (multi_oracle d) (CPU_ID d)
(TEVENT (CPU_ID d)
(TTICKET
(SWAP_TAIL (nat_of_Z (Int.unsigned i)) false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l)
++
TEVENT (CPU_ID d)
(TTICKET
(SWAP_TAIL (nat_of_Z (Int.unsigned i)) false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l))
(multi_log d)})).
{ econstructor; simpl; try auto.
intros.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
unfold valid_multi_oracle_pool_mcs in valid_multi_oracle_pool_mcs_inv.
unfold valid_multi_oracle_mcs in valid_multi_oracle_pool_mcs_inv.
assert (valid_MCS_log l).
eapply valid_multi_log_pool_mcs_inv; eauto.
eapply valid_multi_oracle_pool_mcs_inv with (i := z) (i0 := (CPU_ID d)) in H; auto.
assert (valid_MCS_log
(TEVENT (CPU_ID d)
(TTICKET (SWAP_TAIL (nat_of_Z (Int.unsigned i)) false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l)).
{ simpl.
unfold valid_MCS_log; intros.
unfold valid_MCS_log in H.
unfold MCSCorrect_range in H; unfold MCSCorrect_range.
simpl in H0; subdestruct.
inv H0.
inv Hdestruct3.
assert (MCSLOCK tail lock_array bounds = MCSLOCK tail lock_array bounds) by reflexivity.
eapply H in H0; eauto.
intros.
inv Hmcs.
split; try omega.
intros.
case_eq (zeq i2 (CPU_ID d)); intros; subst.
+ rewrite ZMap.gss; simpl; unfold NULL; omega.
+ rewrite ZMap.gso; auto.
destruct H0.
apply H3 in H1; simpl in H3; auto. }
eapply valid_multi_oracle_pool_mcs_inv with (i := z) (i0 := (CPU_ID d)) in H0; auto.
unfold valid_MCS_log in H0; unfold valid_MCS_log_pool.
intros.
case_eq (zeq i2 z); intros; subst.
+ rewrite ZMap.gss in Hdef; auto.
inv Hdef.
unfold MCSCorrect_range in H0.
unfold valid_MCS_log.
intros.
unfold MCSCorrect_range.
intros.
simpl in H2.
subdestruct.
inv Hmcs; inv H2.
assert (MCSLOCK tl lock_array0 bnd = MCSLOCK tl lock_array0 bnd) by reflexivity.
eapply H0 in H2; eauto.
destruct H2.
split; auto.
intros.
case_eq (zeq i2 tail).
× intros; subst.
rewrite ZMap.gss.
simpl; omega.
× intros.
rewrite ZMap.gso; auto.
+ rewrite ZMap.gso in Hdef; auto.
eapply valid_multi_log_pool_mcs_inv with (i := i2); auto. }
assert (ZMap.get z
(multi_log
d {multi_log
: ZMap.set z
(MultiDef
(TEVENT (CPU_ID d) (TTICKET (SET_NEXT tail))
:: ZMap.get z (multi_oracle d) (CPU_ID d)
(TEVENT (CPU_ID d)
(TTICKET
(SWAP_TAIL (nat_of_Z (Int.unsigned i))
false))
:: ZMap.get z (multi_oracle d) (CPU_ID d)
l ++ l) ++
TEVENT (CPU_ID d)
(TTICKET
(SWAP_TAIL (nat_of_Z (Int.unsigned i)) false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l))
(multi_log d)}) =
(MultiDef
(TEVENT (CPU_ID d) (TTICKET (SET_NEXT tail))
:: ZMap.get z (multi_oracle d) (CPU_ID d)
(TEVENT (CPU_ID d)
(TTICKET
(SWAP_TAIL (nat_of_Z (Int.unsigned i))
false))
:: ZMap.get z (multi_oracle d) (CPU_ID d)
l ++ l) ++
TEVENT (CPU_ID d)
(TTICKET
(SWAP_TAIL (nat_of_Z (Int.unsigned i)) false))
:: ZMap.get z (multi_oracle d) (CPU_ID d) l ++ l))).
{ simpl.
rewrite ZMap.gss; auto. }
eapply CalMCS_AcqWaitPreserveInv in H0; eauto.
unfold valid_MCS_log_pool.
intros.
case_eq (zeq i2 z); intros; subst.
+ rewrite ZMap.gss in Hdef; auto.
inv Hdef; auto.
+ rewrite ZMap.gso in Hdef; auto.
unfold valid_MCS_log_pool in valid_multi_log_pool_mcs_inv.
eapply valid_multi_log_pool_mcs_inv with (i := i2); auto.
Qed.
End INV.
Definition mmcslockop_fresh : compatlayer (cdata RData) :=
pass_lock ↦ gensem mcs_pass_lock_spec
⊕ wait_lock ↦ gensem mcs_wait_lock_spec.
Definition mmcslockop_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
⊕ ticket_lock_init ↦ gensem ticket_lock_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
pass_lock ↦ gensem mcs_pass_lock_spec
⊕ wait_lock ↦ gensem mcs_wait_lock_spec.
Definition mmcslockop_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
⊕ ticket_lock_init ↦ gensem ticket_lock_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 _ _ _ _ _ _ _ _ Hmwd);
exec_store := (@exec_storeex _ _ _ _ _ _ _ _ Hmwd) |}.
Definition mmcslockop : compatlayer (cdata RData) := mmcslockop_fresh ⊕ mmcslockop_passthrough.
End WITHMEM.
exec_store := (@exec_storeex _ _ _ _ _ _ _ _ Hmwd) |}.
Definition mmcslockop : compatlayer (cdata RData) := mmcslockop_fresh ⊕ mmcslockop_passthrough.
End WITHMEM.