Library mcertikos.mcslock.MCSSemantics
This file defines the general semantics for primitives at all layers
Require Import Coqlib.
Require Import Maps.
Require Import Globalenvs.
Require Import AsmX.
Require Import Values.
Require Import MemoryX.
Require Import Events.
Require Import AST.
Require Import AuxStateDataType.
Require Import Constant.
Require Import FlatMemory.
Require Import GlobIdent.
Require Import Integers.
Require Import Conventions.
Require Import LAsm.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import compcert.cfrontend.Ctypes.
Require Import compcert.cfrontend.Cop.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compat.CompatLayers.
Require Export mCertiKOSType.
Require Export GlobalOracleProp.
Require Import CalMCSLock.
Ltac args_list_inv :=
repeat match goal with
| [ HAN: extcall_arguments _ _ _ ?l |- _] ⇒
inv HAN
| [ HAN: extcall_arg _ _ _ _ |- _] ⇒
inv HAN
| [ HAN: list_forall2 _ _ _ |- _] ⇒
inv HAN
| [HA1: ?a = _, HA2: ?a = _ |- _ ] ⇒
rewrite HA2 in HA1; inv HA1
end.
Section Semantics.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context {RData} `{HD: CompatData RData}.
Local Open Scope Z_scope.
Section WITHMEM.
Lemma storebytes_empty_exists´:
∀ m b ofs,
∃ m´, Mem.storebytes m b ofs nil = Some m´.
Proof.
intros.
eapply Mem.range_perm_storebytes; eauto.
intros i.
simpl. intros. omega.
Qed.
Lemma storebytes_empty_exists:
∀ m b ofs,
Mem.storebytes m b ofs nil = Some m.
Proof.
intros.
specialize (storebytes_empty_exists´ m b ofs).
intros (m´ & Hst).
rewrite Hst.
eapply storebytes_empty in Hst. inv Hst. trivial.
Qed.
End WITHMEM.
Section atomic_mcs_log.
Variable atomic_mcs_log_spec: Z → Z → RData → option (RData × Z ×
(Z × Z × Z × Z × Z × Z × Z × Z) ×
(Z × Z × Z × Z × Z × Z × Z × Z)).
Inductive primcall_atomic_mcs_log_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| prim_atomic_mcs_log_sem_intro_mem:
∀ rs sig m m_la m0_bs m0_ne m1_bs m1_ne m2_bs m2_ne m3_bs m3_ne m4_bs m4_ne m5_bs m5_ne m6_bs m6_ne m7_bs m´
adt adt´ lock_index cpuid b bs0 bs1 bs2 bs3 bs4 bs5 bs6 bs7 ne0 ne1 ne2 ne3 ne4 ne5 ne6 ne7 la
(Hspec: atomic_mcs_log_spec (Int.unsigned lock_index) (Int.unsigned cpuid) adt
= Some (adt´, la, (bs0, bs1, bs2, bs3, bs4, bs5, bs6, bs7), (ne0, ne1, ne2, ne3, ne4, ne5, ne6, ne7)))
(Hsymbol: find_symbol s MCS_LOCK_LOC = Some b)
(Hstore_la: Mem.store Mint32 m b (tail_pos (Int.unsigned lock_index)) (Vint (Int.repr la)) = Some m_la)
(Hstore_busy0: Mem.store Mint32 m_la b (busy_pos (Int.unsigned lock_index) 0) (Vint (Int.repr bs0)) = Some m0_bs)
(Hstore_next0: Mem.store Mint32 m0_bs b (next_pos (Int.unsigned lock_index) 0) (Vint (Int.repr ne0)) = Some m0_ne)
(Hstore_busy1: Mem.store Mint32 m0_ne b (busy_pos (Int.unsigned lock_index) 1) (Vint (Int.repr bs1)) = Some m1_bs)
(Hstore_next1: Mem.store Mint32 m1_bs b (next_pos (Int.unsigned lock_index) 1) (Vint (Int.repr ne1)) = Some m1_ne)
(Hstore_busy2: Mem.store Mint32 m1_ne b (busy_pos (Int.unsigned lock_index) 2) (Vint (Int.repr bs2)) = Some m2_bs)
(Hstore_next2: Mem.store Mint32 m2_bs b (next_pos (Int.unsigned lock_index) 2) (Vint (Int.repr ne2)) = Some m2_ne)
(Hstore_busy3: Mem.store Mint32 m2_ne b (busy_pos (Int.unsigned lock_index) 3) (Vint (Int.repr bs3)) = Some m3_bs)
(Hstore_next3: Mem.store Mint32 m3_bs b (next_pos (Int.unsigned lock_index) 3) (Vint (Int.repr ne3)) = Some m3_ne)
(Hstore_busy4: Mem.store Mint32 m3_ne b (busy_pos (Int.unsigned lock_index) 4) (Vint (Int.repr bs4)) = Some m4_bs)
(Hstore_next4: Mem.store Mint32 m4_bs b (next_pos (Int.unsigned lock_index) 4) (Vint (Int.repr ne4)) = Some m4_ne)
(Hstore_busy5: Mem.store Mint32 m4_ne b (busy_pos (Int.unsigned lock_index) 5) (Vint (Int.repr bs5)) = Some m5_bs)
(Hstore_next5: Mem.store Mint32 m5_bs b (next_pos (Int.unsigned lock_index) 5) (Vint (Int.repr ne5)) = Some m5_ne)
(Hstore_busy6: Mem.store Mint32 m5_ne b (busy_pos (Int.unsigned lock_index) 6) (Vint (Int.repr bs6)) = Some m6_bs)
(Hstore_next6: Mem.store Mint32 m6_bs b (next_pos (Int.unsigned lock_index) 6) (Vint (Int.repr ne6)) = Some m6_ne)
(Hstore_busy7: Mem.store Mint32 m6_ne b (busy_pos (Int.unsigned lock_index) 7) (Vint (Int.repr bs7)) = Some m7_bs)
(Hstore_next7: Mem.store Mint32 m7_bs b (next_pos (Int.unsigned lock_index) 7) (Vint (Int.repr ne7)) = Some m´)
(Hsig: sig = mksignature (AST.Tint::AST.Tint::nil) None cc_default)
(Harg: extcall_arguments rs m sig (Vint lock_index :: Vint cpuid :: nil)),
primcall_atomic_mcs_log_sem s rs (m, adt) (rs#RA <- Vundef#PC <- (rs RA)) (m´, adt´).
Class AtomicmcslogInvariants :=
{
atomic_mcs_log_low_level_invariant n lock_index cpuid d d´ la
bs0 bs1 bs2 bs3 bs4 bs5 bs6 bs7
ne0 ne1 ne2 ne3 ne4 ne5 ne6 ne7:
atomic_mcs_log_spec lock_index cpuid d = Some (d´, la,
(bs0, bs1, bs2, bs3, bs4, bs5, bs6, bs7),
(ne0, ne1, ne2, ne3, ne4, ne5, ne6, ne7))→
low_level_invariant n d →
low_level_invariant n d´;
atomic_mcs_log_high_level_invariant lock_index cpuid d d´ la
bs0 bs1 bs2 bs3 bs4 bs5 bs6 bs7
ne0 ne1 ne2 ne3 ne4 ne5 ne6 ne7:
atomic_mcs_log_spec lock_index cpuid d = Some (d´, la,
(bs0, bs1, bs2, bs3, bs4, bs5, bs6, bs7),
(ne0, ne1, ne2, ne3, ne4, ne5, ne6, ne7)) →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: AtomicmcslogInvariants}.
Local Instance primcall_atomic_mcs_log_sem_propertes:
PrimcallProperties primcall_atomic_mcs_log_sem.
Proof.
constructor; intros; inv H.
-
inv H0.
args_list_inv.
split; try congruence.
Qed.
Local Instance primcall_atomic_mcs_log_sem_invariants:
PrimcallInvariants primcall_atomic_mcs_log_sem.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
assert (Heq: Mem.nextblock m´0 = Mem.nextblock m0).
{
eapply Mem.nextblock_store in Hstore_la; eauto.
eapply Mem.nextblock_store in Hstore_busy0; eauto.
eapply Mem.nextblock_store in Hstore_next0; eauto.
eapply Mem.nextblock_store in Hstore_busy1; eauto.
eapply Mem.nextblock_store in Hstore_next1; eauto.
eapply Mem.nextblock_store in Hstore_busy2; eauto.
eapply Mem.nextblock_store in Hstore_next2; eauto.
eapply Mem.nextblock_store in Hstore_busy3; eauto.
eapply Mem.nextblock_store in Hstore_next3; eauto.
eapply Mem.nextblock_store in Hstore_busy4; eauto.
eapply Mem.nextblock_store in Hstore_next4; eauto.
eapply Mem.nextblock_store in Hstore_busy5; eauto.
eapply Mem.nextblock_store in Hstore_next5; eauto.
eapply Mem.nextblock_store in Hstore_busy6; eauto.
eapply Mem.nextblock_store in Hstore_next6; eauto.
eapply Mem.nextblock_store in Hstore_busy7; eauto.
eapply Mem.nextblock_store in Hstore_next7; eauto.
congruence.
}
assert (Hle: (genv_next s ≤ Mem.nextblock m´0)%positive).
{
rewrite Heq. assumption.
}
constructor; lift_unfold; eauto.
{
pose proof (genv_symb_range _ _ _ Hsymbol) as Hle´.
rewrite Heq.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
+ xomega.
+ xomega.
+ xomega.
+ xomega.
+ xomega.
+ xomega.
+ xomega.
+ xomega.
+ xomega.
+ xomega.
+ xomega.
+ xomega.
+ xomega.
+ xomega.
+ xomega.
+ xomega.
+ xomega.
}
{
rewrite Heq.
val_inject_simpl.
}
+
repeat apply set_reg_wt;
try constructor; try assumption; simpl.
eapply inv_reg_wt.
-
eapply atomic_mcs_log_low_level_invariant; eauto.
eapply Mem.nextblock_store in Hstore_la; eauto.
eapply Mem.nextblock_store in Hstore_busy0; eauto.
eapply Mem.nextblock_store in Hstore_next0; eauto.
eapply Mem.nextblock_store in Hstore_busy1; eauto.
eapply Mem.nextblock_store in Hstore_next1; eauto.
eapply Mem.nextblock_store in Hstore_busy2; eauto.
eapply Mem.nextblock_store in Hstore_next2; eauto.
eapply Mem.nextblock_store in Hstore_busy3; eauto.
eapply Mem.nextblock_store in Hstore_next3; eauto.
eapply Mem.nextblock_store in Hstore_busy4; eauto.
eapply Mem.nextblock_store in Hstore_next4; eauto.
eapply Mem.nextblock_store in Hstore_busy5; eauto.
eapply Mem.nextblock_store in Hstore_next5; eauto.
eapply Mem.nextblock_store in Hstore_busy6; eauto.
eapply Mem.nextblock_store in Hstore_next6; eauto.
eapply Mem.nextblock_store in Hstore_busy7; eauto.
eapply Mem.nextblock_store in Hstore_next7; eauto.
rewrite Hstore_next7, Hstore_busy7, Hstore_next6, Hstore_busy6, Hstore_next5, Hstore_busy5.
rewrite Hstore_next4, Hstore_busy4, Hstore_next3, Hstore_busy3, Hstore_next2, Hstore_busy2.
rewrite Hstore_next1, Hstore_busy1, Hstore_next0, Hstore_busy0, Hstore_la.
assumption.
-
eapply atomic_mcs_log_high_level_invariant; eauto.
Qed.
Definition primcall_atomic_mcs_log_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_atomic_mcs_log_sem;
sprimcall_sig := mksignature (AST.Tint::AST.Tint::nil) None cc_default;
sprimcall_valid s := true
|};
sprimcall_name := Some atomic_mcs_log;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End atomic_mcs_log.
Section atomic_mcs_SWAP.
Variable atomic_mcs_SWAP_spec: Z → Z → Z → RData → (option (RData × Z)).
Inductive primcall_atomic_mcs_SWAP_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| prim_atomic_mcs_SWAP_sem_intro_mem:
∀ rs sig m m0 m1 m´ adt adt´ bound lock_index cpuid b prev_last
(Hspec: atomic_mcs_SWAP_spec (Int.unsigned bound) (Int.unsigned lock_index) (Int.unsigned cpuid) adt
= Some (adt´, Int.unsigned prev_last))
(Hsymbol: find_symbol s MCS_LOCK_LOC = Some b)
(Hstore_la: Mem.store Mint32 m b (tail_pos (Int.unsigned lock_index)) (Vint cpuid) = Some m0)
(Hstore_next: Mem.store Mint32 m0 b (next_pos (Int.unsigned lock_index) (Int.unsigned cpuid))
(Vint (Int.repr NULL)) = Some m1)
(Hstore_busy: Mem.store Mint32 m1 b (busy_pos (Int.unsigned lock_index) (Int.unsigned cpuid))
(Vint Int.one) = Some m´)
(Hsig: sig = mksignature (AST.Tint::AST.Tint::AST.Tint::nil) (Some AST.Tint) cc_default)
(Harg: extcall_arguments rs m sig (Vint bound :: Vint lock_index :: Vint cpuid :: nil)),
primcall_atomic_mcs_SWAP_sem s rs (m, adt) (rs#RA <- Vundef#PC <- (rs RA)#EAX <- (Vint prev_last)) (m´, adt´).
Class AtomicmcsSWAPInvariants :=
{
atomic_mcs_SWAP_low_level_invariant n bound lock_index cpuid d d´ r:
atomic_mcs_SWAP_spec bound lock_index cpuid d = Some (d´, r) →
low_level_invariant n d →
low_level_invariant n d´;
atomic_mcs_SWAP_high_level_invariant bound lock_index cpuid d d´ r:
atomic_mcs_SWAP_spec bound lock_index cpuid d = Some (d´, r) →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: AtomicmcsSWAPInvariants}.
Local Instance primcall_atomic_mcs_SWAP_sem_propertes:
PrimcallProperties primcall_atomic_mcs_SWAP_sem.
Proof.
constructor; intros; inv H.
-
inv H0.
args_list_inv.
split; try congruence.
rewrite <- Int.repr_unsigned with prev_last.
rewrite <- Int.repr_unsigned with prev_last0.
try congruence.
Qed.
Local Instance primcall_atomic_mcs_SWAP_sem_invariants:
PrimcallInvariants primcall_atomic_mcs_SWAP_sem.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
assert (Heq: Mem.nextblock m´0 = Mem.nextblock m0).
{
eapply Mem.nextblock_store in Hstore_la; eauto.
eapply Mem.nextblock_store in Hstore_next; eauto.
eapply Mem.nextblock_store in Hstore_busy; eauto.
congruence.
}
assert (Hle: (genv_next s ≤ Mem.nextblock m´0)%positive).
{
rewrite Heq. assumption.
}
constructor; lift_unfold; eauto.
{
pose proof (genv_symb_range _ _ _ Hsymbol) as Hle´.
rewrite Heq.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
+ xomega.
+ xomega.
+ xomega.
}
{
rewrite Heq.
val_inject_simpl.
}
+
repeat apply set_reg_wt;
try constructor; try assumption; simpl.
eapply inv_reg_wt.
-
eapply atomic_mcs_SWAP_low_level_invariant; eauto.
eapply Mem.nextblock_store in Hstore_la; eauto.
eapply Mem.nextblock_store in Hstore_next; eauto.
eapply Mem.nextblock_store in Hstore_busy; eauto.
rewrite Hstore_busy, Hstore_next, Hstore_la. assumption.
-
eapply atomic_mcs_SWAP_high_level_invariant; eauto.
Qed.
Definition primcall_atomic_mcs_SWAP_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_atomic_mcs_SWAP_sem;
sprimcall_sig := mksignature (AST.Tint::AST.Tint::AST.Tint::nil) (Some AST.Tint) cc_default;
sprimcall_valid s := true
|};
sprimcall_name := Some atomic_mcs_SWAP;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End atomic_mcs_SWAP.
Section atomic_mcs_CAS.
Variable atomic_mcs_CAS_spec: Z → Z → RData → (option (RData × (Z × Z))).
Inductive primcall_atomic_mcs_CAS_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| prim_atomic_mcs_CAS_sem_intro_mem:
∀ rs sig m m´ adt adt´ lock_index cpuid b new_la succeed
(Hspec: atomic_mcs_CAS_spec (Int.unsigned lock_index) (Int.unsigned cpuid) adt
= Some (adt´, (new_la, (Int.unsigned succeed))))
(Hsymbol: find_symbol s MCS_LOCK_LOC = Some b)
(Hstore_la: Mem.store Mint32 m b (tail_pos (Int.unsigned lock_index))
(Vint (Int.repr new_la)) = Some m´)
(Hsig: sig = mksignature (AST.Tint::AST.Tint::nil) (Some AST.Tint) cc_default)
(Harg: extcall_arguments rs m sig (Vint lock_index :: Vint cpuid :: nil)),
primcall_atomic_mcs_CAS_sem s rs (m, adt) (rs#RA <- Vundef#PC <- (rs RA)#EAX <- (Vint succeed)) (m´, adt´).
Class AtomicmcsCASInvariants :=
{
atomic_mcs_CAS_low_level_invariant n lock_index cpuid d d´ r r´:
atomic_mcs_CAS_spec lock_index cpuid d = Some (d´, (r, r´)) →
low_level_invariant n d →
low_level_invariant n d´;
atomic_mcs_CAS_high_level_invariant lock_index cpuid d d´ r r´:
atomic_mcs_CAS_spec lock_index cpuid d = Some (d´, (r, r´)) →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: AtomicmcsCASInvariants}.
Local Instance primcall_atomic_mcs_CAS_sem_propertes:
PrimcallProperties primcall_atomic_mcs_CAS_sem.
Proof.
constructor; intros; inv H.
-
inv H0. args_list_inv.
split; try congruence.
rewrite <- Int.repr_unsigned with succeed.
rewrite <- Int.repr_unsigned with succeed0.
congruence.
Qed.
Local Instance primcall_atomic_mcs_CAS_sem_invariants:
PrimcallInvariants primcall_atomic_mcs_CAS_sem.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
assert (Heq: Mem.nextblock m´0 = Mem.nextblock m0).
{
eapply Mem.nextblock_store in Hstore_la; eauto.
}
assert (Hle: (genv_next s ≤ Mem.nextblock m´0)%positive).
{
rewrite Heq. assumption.
}
constructor; lift_unfold; eauto.
{
pose proof (genv_symb_range _ _ _ Hsymbol) as Hle´.
rewrite Heq.
eapply Mem.store_inject_neutral; eauto.
+ xomega.
}
{
rewrite Heq.
val_inject_simpl.
}
+
repeat apply set_reg_wt;
try constructor; try assumption; simpl.
eapply inv_reg_wt.
-
eapply atomic_mcs_CAS_low_level_invariant; eauto.
eapply Mem.nextblock_store in Hstore_la; eauto.
rewrite Hstore_la. assumption.
-
eapply atomic_mcs_CAS_high_level_invariant; eauto.
Qed.
Definition primcall_atomic_mcs_CAS_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_atomic_mcs_CAS_sem;
sprimcall_sig := mksignature (AST.Tint::AST.Tint::nil) (Some AST.Tint) cc_default;
sprimcall_valid s := true
|};
sprimcall_name := Some atomic_mcs_CAS;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End atomic_mcs_CAS.
End Semantics.
Require Import Maps.
Require Import Globalenvs.
Require Import AsmX.
Require Import Values.
Require Import MemoryX.
Require Import Events.
Require Import AST.
Require Import AuxStateDataType.
Require Import Constant.
Require Import FlatMemory.
Require Import GlobIdent.
Require Import Integers.
Require Import Conventions.
Require Import LAsm.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import compcert.cfrontend.Ctypes.
Require Import compcert.cfrontend.Cop.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compat.CompatLayers.
Require Export mCertiKOSType.
Require Export GlobalOracleProp.
Require Import CalMCSLock.
Ltac args_list_inv :=
repeat match goal with
| [ HAN: extcall_arguments _ _ _ ?l |- _] ⇒
inv HAN
| [ HAN: extcall_arg _ _ _ _ |- _] ⇒
inv HAN
| [ HAN: list_forall2 _ _ _ |- _] ⇒
inv HAN
| [HA1: ?a = _, HA2: ?a = _ |- _ ] ⇒
rewrite HA2 in HA1; inv HA1
end.
Section Semantics.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context {RData} `{HD: CompatData RData}.
Local Open Scope Z_scope.
Section WITHMEM.
Lemma storebytes_empty_exists´:
∀ m b ofs,
∃ m´, Mem.storebytes m b ofs nil = Some m´.
Proof.
intros.
eapply Mem.range_perm_storebytes; eauto.
intros i.
simpl. intros. omega.
Qed.
Lemma storebytes_empty_exists:
∀ m b ofs,
Mem.storebytes m b ofs nil = Some m.
Proof.
intros.
specialize (storebytes_empty_exists´ m b ofs).
intros (m´ & Hst).
rewrite Hst.
eapply storebytes_empty in Hst. inv Hst. trivial.
Qed.
End WITHMEM.
Section atomic_mcs_log.
Variable atomic_mcs_log_spec: Z → Z → RData → option (RData × Z ×
(Z × Z × Z × Z × Z × Z × Z × Z) ×
(Z × Z × Z × Z × Z × Z × Z × Z)).
Inductive primcall_atomic_mcs_log_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| prim_atomic_mcs_log_sem_intro_mem:
∀ rs sig m m_la m0_bs m0_ne m1_bs m1_ne m2_bs m2_ne m3_bs m3_ne m4_bs m4_ne m5_bs m5_ne m6_bs m6_ne m7_bs m´
adt adt´ lock_index cpuid b bs0 bs1 bs2 bs3 bs4 bs5 bs6 bs7 ne0 ne1 ne2 ne3 ne4 ne5 ne6 ne7 la
(Hspec: atomic_mcs_log_spec (Int.unsigned lock_index) (Int.unsigned cpuid) adt
= Some (adt´, la, (bs0, bs1, bs2, bs3, bs4, bs5, bs6, bs7), (ne0, ne1, ne2, ne3, ne4, ne5, ne6, ne7)))
(Hsymbol: find_symbol s MCS_LOCK_LOC = Some b)
(Hstore_la: Mem.store Mint32 m b (tail_pos (Int.unsigned lock_index)) (Vint (Int.repr la)) = Some m_la)
(Hstore_busy0: Mem.store Mint32 m_la b (busy_pos (Int.unsigned lock_index) 0) (Vint (Int.repr bs0)) = Some m0_bs)
(Hstore_next0: Mem.store Mint32 m0_bs b (next_pos (Int.unsigned lock_index) 0) (Vint (Int.repr ne0)) = Some m0_ne)
(Hstore_busy1: Mem.store Mint32 m0_ne b (busy_pos (Int.unsigned lock_index) 1) (Vint (Int.repr bs1)) = Some m1_bs)
(Hstore_next1: Mem.store Mint32 m1_bs b (next_pos (Int.unsigned lock_index) 1) (Vint (Int.repr ne1)) = Some m1_ne)
(Hstore_busy2: Mem.store Mint32 m1_ne b (busy_pos (Int.unsigned lock_index) 2) (Vint (Int.repr bs2)) = Some m2_bs)
(Hstore_next2: Mem.store Mint32 m2_bs b (next_pos (Int.unsigned lock_index) 2) (Vint (Int.repr ne2)) = Some m2_ne)
(Hstore_busy3: Mem.store Mint32 m2_ne b (busy_pos (Int.unsigned lock_index) 3) (Vint (Int.repr bs3)) = Some m3_bs)
(Hstore_next3: Mem.store Mint32 m3_bs b (next_pos (Int.unsigned lock_index) 3) (Vint (Int.repr ne3)) = Some m3_ne)
(Hstore_busy4: Mem.store Mint32 m3_ne b (busy_pos (Int.unsigned lock_index) 4) (Vint (Int.repr bs4)) = Some m4_bs)
(Hstore_next4: Mem.store Mint32 m4_bs b (next_pos (Int.unsigned lock_index) 4) (Vint (Int.repr ne4)) = Some m4_ne)
(Hstore_busy5: Mem.store Mint32 m4_ne b (busy_pos (Int.unsigned lock_index) 5) (Vint (Int.repr bs5)) = Some m5_bs)
(Hstore_next5: Mem.store Mint32 m5_bs b (next_pos (Int.unsigned lock_index) 5) (Vint (Int.repr ne5)) = Some m5_ne)
(Hstore_busy6: Mem.store Mint32 m5_ne b (busy_pos (Int.unsigned lock_index) 6) (Vint (Int.repr bs6)) = Some m6_bs)
(Hstore_next6: Mem.store Mint32 m6_bs b (next_pos (Int.unsigned lock_index) 6) (Vint (Int.repr ne6)) = Some m6_ne)
(Hstore_busy7: Mem.store Mint32 m6_ne b (busy_pos (Int.unsigned lock_index) 7) (Vint (Int.repr bs7)) = Some m7_bs)
(Hstore_next7: Mem.store Mint32 m7_bs b (next_pos (Int.unsigned lock_index) 7) (Vint (Int.repr ne7)) = Some m´)
(Hsig: sig = mksignature (AST.Tint::AST.Tint::nil) None cc_default)
(Harg: extcall_arguments rs m sig (Vint lock_index :: Vint cpuid :: nil)),
primcall_atomic_mcs_log_sem s rs (m, adt) (rs#RA <- Vundef#PC <- (rs RA)) (m´, adt´).
Class AtomicmcslogInvariants :=
{
atomic_mcs_log_low_level_invariant n lock_index cpuid d d´ la
bs0 bs1 bs2 bs3 bs4 bs5 bs6 bs7
ne0 ne1 ne2 ne3 ne4 ne5 ne6 ne7:
atomic_mcs_log_spec lock_index cpuid d = Some (d´, la,
(bs0, bs1, bs2, bs3, bs4, bs5, bs6, bs7),
(ne0, ne1, ne2, ne3, ne4, ne5, ne6, ne7))→
low_level_invariant n d →
low_level_invariant n d´;
atomic_mcs_log_high_level_invariant lock_index cpuid d d´ la
bs0 bs1 bs2 bs3 bs4 bs5 bs6 bs7
ne0 ne1 ne2 ne3 ne4 ne5 ne6 ne7:
atomic_mcs_log_spec lock_index cpuid d = Some (d´, la,
(bs0, bs1, bs2, bs3, bs4, bs5, bs6, bs7),
(ne0, ne1, ne2, ne3, ne4, ne5, ne6, ne7)) →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: AtomicmcslogInvariants}.
Local Instance primcall_atomic_mcs_log_sem_propertes:
PrimcallProperties primcall_atomic_mcs_log_sem.
Proof.
constructor; intros; inv H.
-
inv H0.
args_list_inv.
split; try congruence.
Qed.
Local Instance primcall_atomic_mcs_log_sem_invariants:
PrimcallInvariants primcall_atomic_mcs_log_sem.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
assert (Heq: Mem.nextblock m´0 = Mem.nextblock m0).
{
eapply Mem.nextblock_store in Hstore_la; eauto.
eapply Mem.nextblock_store in Hstore_busy0; eauto.
eapply Mem.nextblock_store in Hstore_next0; eauto.
eapply Mem.nextblock_store in Hstore_busy1; eauto.
eapply Mem.nextblock_store in Hstore_next1; eauto.
eapply Mem.nextblock_store in Hstore_busy2; eauto.
eapply Mem.nextblock_store in Hstore_next2; eauto.
eapply Mem.nextblock_store in Hstore_busy3; eauto.
eapply Mem.nextblock_store in Hstore_next3; eauto.
eapply Mem.nextblock_store in Hstore_busy4; eauto.
eapply Mem.nextblock_store in Hstore_next4; eauto.
eapply Mem.nextblock_store in Hstore_busy5; eauto.
eapply Mem.nextblock_store in Hstore_next5; eauto.
eapply Mem.nextblock_store in Hstore_busy6; eauto.
eapply Mem.nextblock_store in Hstore_next6; eauto.
eapply Mem.nextblock_store in Hstore_busy7; eauto.
eapply Mem.nextblock_store in Hstore_next7; eauto.
congruence.
}
assert (Hle: (genv_next s ≤ Mem.nextblock m´0)%positive).
{
rewrite Heq. assumption.
}
constructor; lift_unfold; eauto.
{
pose proof (genv_symb_range _ _ _ Hsymbol) as Hle´.
rewrite Heq.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
+ xomega.
+ xomega.
+ xomega.
+ xomega.
+ xomega.
+ xomega.
+ xomega.
+ xomega.
+ xomega.
+ xomega.
+ xomega.
+ xomega.
+ xomega.
+ xomega.
+ xomega.
+ xomega.
+ xomega.
}
{
rewrite Heq.
val_inject_simpl.
}
+
repeat apply set_reg_wt;
try constructor; try assumption; simpl.
eapply inv_reg_wt.
-
eapply atomic_mcs_log_low_level_invariant; eauto.
eapply Mem.nextblock_store in Hstore_la; eauto.
eapply Mem.nextblock_store in Hstore_busy0; eauto.
eapply Mem.nextblock_store in Hstore_next0; eauto.
eapply Mem.nextblock_store in Hstore_busy1; eauto.
eapply Mem.nextblock_store in Hstore_next1; eauto.
eapply Mem.nextblock_store in Hstore_busy2; eauto.
eapply Mem.nextblock_store in Hstore_next2; eauto.
eapply Mem.nextblock_store in Hstore_busy3; eauto.
eapply Mem.nextblock_store in Hstore_next3; eauto.
eapply Mem.nextblock_store in Hstore_busy4; eauto.
eapply Mem.nextblock_store in Hstore_next4; eauto.
eapply Mem.nextblock_store in Hstore_busy5; eauto.
eapply Mem.nextblock_store in Hstore_next5; eauto.
eapply Mem.nextblock_store in Hstore_busy6; eauto.
eapply Mem.nextblock_store in Hstore_next6; eauto.
eapply Mem.nextblock_store in Hstore_busy7; eauto.
eapply Mem.nextblock_store in Hstore_next7; eauto.
rewrite Hstore_next7, Hstore_busy7, Hstore_next6, Hstore_busy6, Hstore_next5, Hstore_busy5.
rewrite Hstore_next4, Hstore_busy4, Hstore_next3, Hstore_busy3, Hstore_next2, Hstore_busy2.
rewrite Hstore_next1, Hstore_busy1, Hstore_next0, Hstore_busy0, Hstore_la.
assumption.
-
eapply atomic_mcs_log_high_level_invariant; eauto.
Qed.
Definition primcall_atomic_mcs_log_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_atomic_mcs_log_sem;
sprimcall_sig := mksignature (AST.Tint::AST.Tint::nil) None cc_default;
sprimcall_valid s := true
|};
sprimcall_name := Some atomic_mcs_log;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End atomic_mcs_log.
Section atomic_mcs_SWAP.
Variable atomic_mcs_SWAP_spec: Z → Z → Z → RData → (option (RData × Z)).
Inductive primcall_atomic_mcs_SWAP_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| prim_atomic_mcs_SWAP_sem_intro_mem:
∀ rs sig m m0 m1 m´ adt adt´ bound lock_index cpuid b prev_last
(Hspec: atomic_mcs_SWAP_spec (Int.unsigned bound) (Int.unsigned lock_index) (Int.unsigned cpuid) adt
= Some (adt´, Int.unsigned prev_last))
(Hsymbol: find_symbol s MCS_LOCK_LOC = Some b)
(Hstore_la: Mem.store Mint32 m b (tail_pos (Int.unsigned lock_index)) (Vint cpuid) = Some m0)
(Hstore_next: Mem.store Mint32 m0 b (next_pos (Int.unsigned lock_index) (Int.unsigned cpuid))
(Vint (Int.repr NULL)) = Some m1)
(Hstore_busy: Mem.store Mint32 m1 b (busy_pos (Int.unsigned lock_index) (Int.unsigned cpuid))
(Vint Int.one) = Some m´)
(Hsig: sig = mksignature (AST.Tint::AST.Tint::AST.Tint::nil) (Some AST.Tint) cc_default)
(Harg: extcall_arguments rs m sig (Vint bound :: Vint lock_index :: Vint cpuid :: nil)),
primcall_atomic_mcs_SWAP_sem s rs (m, adt) (rs#RA <- Vundef#PC <- (rs RA)#EAX <- (Vint prev_last)) (m´, adt´).
Class AtomicmcsSWAPInvariants :=
{
atomic_mcs_SWAP_low_level_invariant n bound lock_index cpuid d d´ r:
atomic_mcs_SWAP_spec bound lock_index cpuid d = Some (d´, r) →
low_level_invariant n d →
low_level_invariant n d´;
atomic_mcs_SWAP_high_level_invariant bound lock_index cpuid d d´ r:
atomic_mcs_SWAP_spec bound lock_index cpuid d = Some (d´, r) →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: AtomicmcsSWAPInvariants}.
Local Instance primcall_atomic_mcs_SWAP_sem_propertes:
PrimcallProperties primcall_atomic_mcs_SWAP_sem.
Proof.
constructor; intros; inv H.
-
inv H0.
args_list_inv.
split; try congruence.
rewrite <- Int.repr_unsigned with prev_last.
rewrite <- Int.repr_unsigned with prev_last0.
try congruence.
Qed.
Local Instance primcall_atomic_mcs_SWAP_sem_invariants:
PrimcallInvariants primcall_atomic_mcs_SWAP_sem.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
assert (Heq: Mem.nextblock m´0 = Mem.nextblock m0).
{
eapply Mem.nextblock_store in Hstore_la; eauto.
eapply Mem.nextblock_store in Hstore_next; eauto.
eapply Mem.nextblock_store in Hstore_busy; eauto.
congruence.
}
assert (Hle: (genv_next s ≤ Mem.nextblock m´0)%positive).
{
rewrite Heq. assumption.
}
constructor; lift_unfold; eauto.
{
pose proof (genv_symb_range _ _ _ Hsymbol) as Hle´.
rewrite Heq.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
eapply Mem.store_inject_neutral; eauto.
+ xomega.
+ xomega.
+ xomega.
}
{
rewrite Heq.
val_inject_simpl.
}
+
repeat apply set_reg_wt;
try constructor; try assumption; simpl.
eapply inv_reg_wt.
-
eapply atomic_mcs_SWAP_low_level_invariant; eauto.
eapply Mem.nextblock_store in Hstore_la; eauto.
eapply Mem.nextblock_store in Hstore_next; eauto.
eapply Mem.nextblock_store in Hstore_busy; eauto.
rewrite Hstore_busy, Hstore_next, Hstore_la. assumption.
-
eapply atomic_mcs_SWAP_high_level_invariant; eauto.
Qed.
Definition primcall_atomic_mcs_SWAP_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_atomic_mcs_SWAP_sem;
sprimcall_sig := mksignature (AST.Tint::AST.Tint::AST.Tint::nil) (Some AST.Tint) cc_default;
sprimcall_valid s := true
|};
sprimcall_name := Some atomic_mcs_SWAP;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End atomic_mcs_SWAP.
Section atomic_mcs_CAS.
Variable atomic_mcs_CAS_spec: Z → Z → RData → (option (RData × (Z × Z))).
Inductive primcall_atomic_mcs_CAS_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| prim_atomic_mcs_CAS_sem_intro_mem:
∀ rs sig m m´ adt adt´ lock_index cpuid b new_la succeed
(Hspec: atomic_mcs_CAS_spec (Int.unsigned lock_index) (Int.unsigned cpuid) adt
= Some (adt´, (new_la, (Int.unsigned succeed))))
(Hsymbol: find_symbol s MCS_LOCK_LOC = Some b)
(Hstore_la: Mem.store Mint32 m b (tail_pos (Int.unsigned lock_index))
(Vint (Int.repr new_la)) = Some m´)
(Hsig: sig = mksignature (AST.Tint::AST.Tint::nil) (Some AST.Tint) cc_default)
(Harg: extcall_arguments rs m sig (Vint lock_index :: Vint cpuid :: nil)),
primcall_atomic_mcs_CAS_sem s rs (m, adt) (rs#RA <- Vundef#PC <- (rs RA)#EAX <- (Vint succeed)) (m´, adt´).
Class AtomicmcsCASInvariants :=
{
atomic_mcs_CAS_low_level_invariant n lock_index cpuid d d´ r r´:
atomic_mcs_CAS_spec lock_index cpuid d = Some (d´, (r, r´)) →
low_level_invariant n d →
low_level_invariant n d´;
atomic_mcs_CAS_high_level_invariant lock_index cpuid d d´ r r´:
atomic_mcs_CAS_spec lock_index cpuid d = Some (d´, (r, r´)) →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: AtomicmcsCASInvariants}.
Local Instance primcall_atomic_mcs_CAS_sem_propertes:
PrimcallProperties primcall_atomic_mcs_CAS_sem.
Proof.
constructor; intros; inv H.
-
inv H0. args_list_inv.
split; try congruence.
rewrite <- Int.repr_unsigned with succeed.
rewrite <- Int.repr_unsigned with succeed0.
congruence.
Qed.
Local Instance primcall_atomic_mcs_CAS_sem_invariants:
PrimcallInvariants primcall_atomic_mcs_CAS_sem.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
assert (Heq: Mem.nextblock m´0 = Mem.nextblock m0).
{
eapply Mem.nextblock_store in Hstore_la; eauto.
}
assert (Hle: (genv_next s ≤ Mem.nextblock m´0)%positive).
{
rewrite Heq. assumption.
}
constructor; lift_unfold; eauto.
{
pose proof (genv_symb_range _ _ _ Hsymbol) as Hle´.
rewrite Heq.
eapply Mem.store_inject_neutral; eauto.
+ xomega.
}
{
rewrite Heq.
val_inject_simpl.
}
+
repeat apply set_reg_wt;
try constructor; try assumption; simpl.
eapply inv_reg_wt.
-
eapply atomic_mcs_CAS_low_level_invariant; eauto.
eapply Mem.nextblock_store in Hstore_la; eauto.
rewrite Hstore_la. assumption.
-
eapply atomic_mcs_CAS_high_level_invariant; eauto.
Qed.
Definition primcall_atomic_mcs_CAS_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_atomic_mcs_CAS_sem;
sprimcall_sig := mksignature (AST.Tint::AST.Tint::nil) (Some AST.Tint) cc_default;
sprimcall_valid s := true
|};
sprimcall_name := Some atomic_mcs_CAS;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End atomic_mcs_CAS.
End Semantics.