Library mcertikos.layerlib.MultiProcessorSemantics
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.
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 acquire_lock.
Variable acquire_lock_spec: Z → Z → Z → RData → option (RData × positive × (option (list Integers.Byte.int))).
Inductive primcall_acquire_lock_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| prim_acquire_lock_sem_intro_mem:
∀ rs sig m m´ adt adt´ bound index ofs id l b b_PC,
acquire_lock_spec (Int.unsigned bound) (Int.unsigned index) (Int.unsigned ofs) adt = Some (adt´, id, l)
→ find_symbol s id = Some b
→ match l with
| Some l´ ⇒ Mem.storebytes m b 0 (ByteList l´) = Some m´
| _ ⇒ m´ = m
end
→ sig = mksignature (AST.Tint::AST.Tint::AST.Tint::nil) None cc_default
→ extcall_arguments rs m sig (Vint bound :: Vint index :: Vint ofs ::nil)
→ ∀ (Hsymbol: find_symbol s acquire_lock = Some b_PC)
(HPC: rs PC = Vptr b_PC Int.zero),
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
primcall_acquire_lock_sem s rs (m, adt) (rs´#RA <- Vundef#PC <- (rs RA)) (m´, adt´).
Class AcquireInvariants :=
{
acquire_lock_low_level_invariant n bound i ofs d d´ e e´:
acquire_lock_spec bound i ofs d = Some (d´, e, e´) →
low_level_invariant n d →
low_level_invariant n d´;
acquire_lock_high_level_invariant bound i ofs d d´ e e´:
acquire_lock_spec bound i ofs d = Some (d´, e, e´) →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: AcquireInvariants}.
Local Instance primcall_acquire_lock_sem_propertes:
PrimcallProperties primcall_acquire_lock_sem.
Proof.
constructor; intros; inv H.
-
inv H0. subst rs´ rs´0.
destruct l; args_list_inv;
split; try congruence.
Qed.
Local Instance primcall_acquire_lock_sem_invariants:
PrimcallInvariants primcall_acquire_lock_sem.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
Local Opaque undef_regs destroyed_at_call.
destruct l; subst.
{
constructor; lift_unfold; eauto;
erewrite Mem.nextblock_storebytes; eauto.
{
eapply Mem.storebytes_inject_neutral; eauto.
+ eapply list_forall2_bytelist_inject.
+ specialize (genv_symb_range _ _ _ H2). intros.
xomega.
}
{
subst rs´0.
val_inject_simpl.
}
}
{
constructor; lift_unfold; eauto.
subst rs´0.
val_inject_simpl.
}
+
repeat apply set_reg_wt;
try constructor; try assumption; simpl.
eapply inv_reg_wt. subst rs´0.
eapply undef_regs_wt.
eapply undef_regs_wt. trivial.
-
eapply acquire_lock_low_level_invariant; eauto.
destruct l; subst; trivial.
erewrite Mem.nextblock_storebytes; eauto.
-
eapply acquire_lock_high_level_invariant; eauto.
Qed.
Definition primcall_acquire_lock_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_acquire_lock_sem;
sprimcall_sig := mksignature (AST.Tint::AST.Tint::AST.Tint::nil) None cc_default;
sprimcall_valid s := true
|};
sprimcall_name := Some acquire_lock;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End acquire_lock.
Section acquire_shared.
Variable acquire_shared_spec: Z → Z → RData → option (RData × positive × (option (list Integers.Byte.int))).
Inductive primcall_acquire_shared_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| prim_acquire_shared_sem_intro_mem:
∀ rs sig m m´ adt adt´ index ofs id l b b_PC,
acquire_shared_spec (Int.unsigned index) (Int.unsigned ofs) adt = Some (adt´, id, l)
→ find_symbol s id = Some b
→ match l with
| Some l´ ⇒ Mem.storebytes m b 0 (ByteList l´) = Some m´
| _ ⇒ m´ = m
end
→ sig = mksignature (AST.Tint::AST.Tint::nil) None cc_default
→ extcall_arguments rs m sig (Vint index :: Vint ofs :: nil)
→ ∀ (Hsymbol: find_symbol s acquire_shared = Some b_PC)
(HPC: rs PC = Vptr b_PC Int.zero),
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
primcall_acquire_shared_sem s rs (m, adt) (rs´#RA <- Vundef#PC <- (rs RA)) (m´, adt´).
Class SAcquireInvariants :=
{
acquire_shared_low_level_invariant n i ofs d d´ e e´:
acquire_shared_spec i ofs d = Some (d´, e, e´) →
low_level_invariant n d →
low_level_invariant n d´;
acquire_shared_high_level_invariant i ofs d d´ e e´:
acquire_shared_spec i ofs d = Some (d´, e, e´) →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: SAcquireInvariants}.
Local Instance primcall_acquire_shared_sem_propertes:
PrimcallProperties primcall_acquire_shared_sem.
Proof.
constructor; intros; inv H.
-
inv H0. subst rs´ rs´0.
destruct l; args_list_inv;
split; try congruence.
Qed.
Local Instance primcall_acquire_shared_sem_invariants:
PrimcallInvariants primcall_acquire_shared_sem.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
Local Opaque undef_regs destroyed_at_call.
destruct l; subst.
{
constructor; lift_unfold; eauto;
erewrite Mem.nextblock_storebytes; eauto.
{
eapply Mem.storebytes_inject_neutral; eauto.
+ eapply list_forall2_bytelist_inject.
+ specialize (genv_symb_range _ _ _ H2). intros.
xomega.
}
{
subst rs´0.
val_inject_simpl.
}
}
{
constructor; lift_unfold; eauto.
subst rs´0.
val_inject_simpl.
}
+
repeat apply set_reg_wt;
try constructor; try assumption; simpl.
eapply inv_reg_wt. subst rs´0.
eapply undef_regs_wt.
eapply undef_regs_wt. trivial.
-
eapply acquire_shared_low_level_invariant; eauto.
destruct l; subst; trivial.
erewrite Mem.nextblock_storebytes; eauto.
-
eapply acquire_shared_high_level_invariant; eauto.
Qed.
Definition primcall_acquire_shared_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_acquire_shared_sem;
sprimcall_sig := mksignature (AST.Tint::AST.Tint::nil) None cc_default;
sprimcall_valid s := true
|};
sprimcall_name := Some acquire_shared;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End acquire_shared.
Function id2size (id: Z) :=
match id with
| ID_AT ⇒ Some (maxpage × 8, AT_LOC)
| ID_TCB ⇒ Some (num_proc × 16 + num_chan × 8, TCBPool_LOC)
| ID_SC ⇒ Some (num_chan × 16, SYNCCHPOOL_LOC)
| _ ⇒ None
end.
Section release_lock.
Variable release_lock: ident.
Variable release_lock_spec: Z → Z → (list Integers.Byte.int) → RData → option RData.
Inductive primcall_release_lock_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| prim_release_lock_sem_intro_mem:
∀ rs sig m adt adt´ index ofs id l b b_PC size,
release_lock_spec (Int.unsigned index) (Int.unsigned ofs) l adt = Some adt´
→ find_symbol s id = Some b
→ id2size (Int.unsigned index) = Some (size, id)
→ Mem.loadbytes m b 0 size = Some (ByteList l)
→ sig = mksignature (AST.Tint::AST.Tint::nil) None cc_default
→ extcall_arguments rs m sig (Vint index :: Vint ofs ::nil)
→ ∀ (Hsymbol: find_symbol s release_lock = Some b_PC)
(HPC: rs PC = Vptr b_PC Int.zero),
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
primcall_release_lock_sem s rs (m, adt) (rs´#RA <- Vundef#PC <- (rs RA)) (m, adt´).
Class ReleaseInvariants :=
{
release_lock_low_level_invariant n i ofs d d´ e:
release_lock_spec i ofs e d = Some d´ →
low_level_invariant n d →
low_level_invariant n d´;
release_lock_high_level_invariant i ofs d d´ e:
release_lock_spec i ofs e d = Some d´ →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: ReleaseInvariants}.
Local Instance primcall_release_lock_sem_propertes:
PrimcallProperties primcall_release_lock_sem.
Proof.
constructor; intros; inv H.
-
inv H0. args_list_inv. eapply ByteList_eq in H0; inv H0.
args_list_inv.
subst rs´ rs´0.
split; try congruence.
Qed.
Local Instance primcall_release_lock_sem_invariants:
PrimcallInvariants primcall_release_lock_sem.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
Local Opaque undef_regs destroyed_at_call.
constructor; lift_unfold; eauto.
subst rs´0.
val_inject_simpl.
+
repeat apply set_reg_wt;
try constructor; try assumption; simpl.
eapply inv_reg_wt. subst rs´0.
eapply undef_regs_wt.
eapply undef_regs_wt. trivial.
-
eapply release_lock_low_level_invariant; eauto.
-
eapply release_lock_high_level_invariant; eauto.
Qed.
Definition primcall_release_lock_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_release_lock_sem;
sprimcall_sig := mksignature (AST.Tint::AST.Tint::nil) None cc_default;
sprimcall_valid s := true
|};
sprimcall_name := Some release_lock;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End release_lock.
Section atomic_FAI.
Variable atomic_FAI_spec: Z → Z → Z → RData → (option (RData× (Z × Z))).
Inductive primcall_atomic_FAI_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| prim_atomic_FAI_sem_intro_mem:
∀ rs sig m m0 m´ adt adt´ bound i ofs b n t pos
(Hspec: atomic_FAI_spec (Int.unsigned bound) (Int.unsigned i) (Int.unsigned ofs)
adt = Some (adt´, (t, n)))
(Hsymbol: find_symbol s TICKET_LOCK_LOC = Some b)
(Hpos: index2Z (Int.unsigned i) (Int.unsigned ofs) = Some pos)
(Hstore0: Mem.store Mint32 m b (pos × 8) (Vint (Int.repr (t + 1))) = Some m0)
(Hstore1: Mem.store Mint32 m0 b (pos × 8 + 4) (Vint (Int.repr n)) = 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 i ::Vint ofs :: nil)),
primcall_atomic_FAI_sem s rs (m, adt) (rs#RA <- Vundef#PC <- (rs RA)#EAX <- (Vint (Int.repr t))) (m´, adt´).
Class AtomicFAIInvariants :=
{
atomic_FAI_low_level_invariant n bound i ofs d d´ e e´:
atomic_FAI_spec bound i ofs d = Some (d´, (e, e´)) →
low_level_invariant n d →
low_level_invariant n d´;
atomic_FAI_high_level_invariant bound i ofs d d´ e e´:
atomic_FAI_spec bound i ofs d = Some (d´, (e, e´)) →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: AtomicFAIInvariants}.
Local Instance primcall_atomic_FAI_sem_propertes:
PrimcallProperties primcall_atomic_FAI_sem.
Proof.
constructor; intros; inv H.
-
inv H0. args_list_inv.
split; try congruence.
Qed.
Local Instance primcall_atomic_FAI_sem_invariants:
PrimcallInvariants primcall_atomic_FAI_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 Hstore0; eauto.
eapply Mem.nextblock_store in Hstore1; 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.
+ xomega.
+ xomega.
}
{
rewrite Heq.
val_inject_simpl.
}
+
repeat apply set_reg_wt;
try constructor; try assumption; simpl.
eapply inv_reg_wt.
-
eapply atomic_FAI_low_level_invariant; eauto.
eapply Mem.nextblock_store in Hstore0; eauto.
eapply Mem.nextblock_store in Hstore1; eauto.
rewrite Hstore1, Hstore0. assumption.
-
eapply atomic_FAI_high_level_invariant; eauto.
Qed.
Definition primcall_atomic_FAI_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_atomic_FAI_sem;
sprimcall_sig := mksignature (AST.Tint::AST.Tint::AST.Tint::nil) (Some AST.Tint) cc_default;
sprimcall_valid s := true
|};
sprimcall_name := Some atomic_FAI;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End atomic_FAI.
Section atomic_GET.
Variable atomic_GET_spec: Z → Z → RData → (option (RData× (Z × Z))).
Inductive primcall_atomic_GET_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| prim_atomic_GET_sem_intro_mem:
∀ rs sig m m0 m´ adt adt´ i ofs b n t pos
(Hspec: atomic_GET_spec (Int.unsigned i) (Int.unsigned ofs) adt = Some (adt´, (t, n)))
(Hsymbol: find_symbol s TICKET_LOCK_LOC = Some b)
(Hpos: index2Z (Int.unsigned i) (Int.unsigned ofs) = Some pos)
(Hstore0: Mem.store Mint32 m b (pos × 8) (Vint (Int.repr t)) = Some m0)
(Hstore1: Mem.store Mint32 m0 b (pos × 8 + 4) (Vint (Int.repr n)) = Some m´)
(Hsig: sig = mksignature (AST.Tint::AST.Tint::nil) (Some AST.Tint) cc_default)
(Harg: extcall_arguments rs m sig (Vint i ::Vint ofs :: nil)),
primcall_atomic_GET_sem s rs (m, adt) (rs#RA <- Vundef#PC <- (rs RA) #EAX <- (Vint (Int.repr n))) (m´, adt´).
Class AtomicGETInvariants :=
{
atomic_GET_low_level_invariant n i ofs d d´ e e´:
atomic_GET_spec i ofs d = Some (d´, (e, e´)) →
low_level_invariant n d →
low_level_invariant n d´;
atomic_GET_high_level_invariant i ofs d d´ e e´:
atomic_GET_spec i ofs d = Some (d´, (e, e´)) →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: AtomicGETInvariants}.
Local Instance primcall_atomic_GET_sem_propertes:
PrimcallProperties primcall_atomic_GET_sem.
Proof.
constructor; intros; inv H.
-
inv H0. args_list_inv.
split; try congruence.
Qed.
Local Instance primcall_atomic_GET_sem_invariants:
PrimcallInvariants primcall_atomic_GET_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 Hstore0; eauto.
eapply Mem.nextblock_store in Hstore1; 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.
+ xomega.
+ xomega.
}
{
rewrite Heq.
val_inject_simpl.
}
+
repeat apply set_reg_wt;
try constructor; try assumption; simpl.
eapply inv_reg_wt.
-
eapply atomic_GET_low_level_invariant; eauto.
eapply Mem.nextblock_store in Hstore0; eauto.
eapply Mem.nextblock_store in Hstore1; eauto.
rewrite Hstore1, Hstore0. assumption.
-
eapply atomic_GET_high_level_invariant; eauto.
Qed.
Definition primcall_atomic_GET_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_atomic_GET_sem;
sprimcall_sig := mksignature (AST.Tint::AST.Tint::nil) (Some AST.Tint) cc_default;
sprimcall_valid s := true
|};
sprimcall_name := Some log_get;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End atomic_GET.
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.
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 acquire_lock.
Variable acquire_lock_spec: Z → Z → Z → RData → option (RData × positive × (option (list Integers.Byte.int))).
Inductive primcall_acquire_lock_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| prim_acquire_lock_sem_intro_mem:
∀ rs sig m m´ adt adt´ bound index ofs id l b b_PC,
acquire_lock_spec (Int.unsigned bound) (Int.unsigned index) (Int.unsigned ofs) adt = Some (adt´, id, l)
→ find_symbol s id = Some b
→ match l with
| Some l´ ⇒ Mem.storebytes m b 0 (ByteList l´) = Some m´
| _ ⇒ m´ = m
end
→ sig = mksignature (AST.Tint::AST.Tint::AST.Tint::nil) None cc_default
→ extcall_arguments rs m sig (Vint bound :: Vint index :: Vint ofs ::nil)
→ ∀ (Hsymbol: find_symbol s acquire_lock = Some b_PC)
(HPC: rs PC = Vptr b_PC Int.zero),
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
primcall_acquire_lock_sem s rs (m, adt) (rs´#RA <- Vundef#PC <- (rs RA)) (m´, adt´).
Class AcquireInvariants :=
{
acquire_lock_low_level_invariant n bound i ofs d d´ e e´:
acquire_lock_spec bound i ofs d = Some (d´, e, e´) →
low_level_invariant n d →
low_level_invariant n d´;
acquire_lock_high_level_invariant bound i ofs d d´ e e´:
acquire_lock_spec bound i ofs d = Some (d´, e, e´) →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: AcquireInvariants}.
Local Instance primcall_acquire_lock_sem_propertes:
PrimcallProperties primcall_acquire_lock_sem.
Proof.
constructor; intros; inv H.
-
inv H0. subst rs´ rs´0.
destruct l; args_list_inv;
split; try congruence.
Qed.
Local Instance primcall_acquire_lock_sem_invariants:
PrimcallInvariants primcall_acquire_lock_sem.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
Local Opaque undef_regs destroyed_at_call.
destruct l; subst.
{
constructor; lift_unfold; eauto;
erewrite Mem.nextblock_storebytes; eauto.
{
eapply Mem.storebytes_inject_neutral; eauto.
+ eapply list_forall2_bytelist_inject.
+ specialize (genv_symb_range _ _ _ H2). intros.
xomega.
}
{
subst rs´0.
val_inject_simpl.
}
}
{
constructor; lift_unfold; eauto.
subst rs´0.
val_inject_simpl.
}
+
repeat apply set_reg_wt;
try constructor; try assumption; simpl.
eapply inv_reg_wt. subst rs´0.
eapply undef_regs_wt.
eapply undef_regs_wt. trivial.
-
eapply acquire_lock_low_level_invariant; eauto.
destruct l; subst; trivial.
erewrite Mem.nextblock_storebytes; eauto.
-
eapply acquire_lock_high_level_invariant; eauto.
Qed.
Definition primcall_acquire_lock_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_acquire_lock_sem;
sprimcall_sig := mksignature (AST.Tint::AST.Tint::AST.Tint::nil) None cc_default;
sprimcall_valid s := true
|};
sprimcall_name := Some acquire_lock;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End acquire_lock.
Section acquire_shared.
Variable acquire_shared_spec: Z → Z → RData → option (RData × positive × (option (list Integers.Byte.int))).
Inductive primcall_acquire_shared_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| prim_acquire_shared_sem_intro_mem:
∀ rs sig m m´ adt adt´ index ofs id l b b_PC,
acquire_shared_spec (Int.unsigned index) (Int.unsigned ofs) adt = Some (adt´, id, l)
→ find_symbol s id = Some b
→ match l with
| Some l´ ⇒ Mem.storebytes m b 0 (ByteList l´) = Some m´
| _ ⇒ m´ = m
end
→ sig = mksignature (AST.Tint::AST.Tint::nil) None cc_default
→ extcall_arguments rs m sig (Vint index :: Vint ofs :: nil)
→ ∀ (Hsymbol: find_symbol s acquire_shared = Some b_PC)
(HPC: rs PC = Vptr b_PC Int.zero),
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
primcall_acquire_shared_sem s rs (m, adt) (rs´#RA <- Vundef#PC <- (rs RA)) (m´, adt´).
Class SAcquireInvariants :=
{
acquire_shared_low_level_invariant n i ofs d d´ e e´:
acquire_shared_spec i ofs d = Some (d´, e, e´) →
low_level_invariant n d →
low_level_invariant n d´;
acquire_shared_high_level_invariant i ofs d d´ e e´:
acquire_shared_spec i ofs d = Some (d´, e, e´) →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: SAcquireInvariants}.
Local Instance primcall_acquire_shared_sem_propertes:
PrimcallProperties primcall_acquire_shared_sem.
Proof.
constructor; intros; inv H.
-
inv H0. subst rs´ rs´0.
destruct l; args_list_inv;
split; try congruence.
Qed.
Local Instance primcall_acquire_shared_sem_invariants:
PrimcallInvariants primcall_acquire_shared_sem.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
Local Opaque undef_regs destroyed_at_call.
destruct l; subst.
{
constructor; lift_unfold; eauto;
erewrite Mem.nextblock_storebytes; eauto.
{
eapply Mem.storebytes_inject_neutral; eauto.
+ eapply list_forall2_bytelist_inject.
+ specialize (genv_symb_range _ _ _ H2). intros.
xomega.
}
{
subst rs´0.
val_inject_simpl.
}
}
{
constructor; lift_unfold; eauto.
subst rs´0.
val_inject_simpl.
}
+
repeat apply set_reg_wt;
try constructor; try assumption; simpl.
eapply inv_reg_wt. subst rs´0.
eapply undef_regs_wt.
eapply undef_regs_wt. trivial.
-
eapply acquire_shared_low_level_invariant; eauto.
destruct l; subst; trivial.
erewrite Mem.nextblock_storebytes; eauto.
-
eapply acquire_shared_high_level_invariant; eauto.
Qed.
Definition primcall_acquire_shared_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_acquire_shared_sem;
sprimcall_sig := mksignature (AST.Tint::AST.Tint::nil) None cc_default;
sprimcall_valid s := true
|};
sprimcall_name := Some acquire_shared;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End acquire_shared.
Function id2size (id: Z) :=
match id with
| ID_AT ⇒ Some (maxpage × 8, AT_LOC)
| ID_TCB ⇒ Some (num_proc × 16 + num_chan × 8, TCBPool_LOC)
| ID_SC ⇒ Some (num_chan × 16, SYNCCHPOOL_LOC)
| _ ⇒ None
end.
Section release_lock.
Variable release_lock: ident.
Variable release_lock_spec: Z → Z → (list Integers.Byte.int) → RData → option RData.
Inductive primcall_release_lock_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| prim_release_lock_sem_intro_mem:
∀ rs sig m adt adt´ index ofs id l b b_PC size,
release_lock_spec (Int.unsigned index) (Int.unsigned ofs) l adt = Some adt´
→ find_symbol s id = Some b
→ id2size (Int.unsigned index) = Some (size, id)
→ Mem.loadbytes m b 0 size = Some (ByteList l)
→ sig = mksignature (AST.Tint::AST.Tint::nil) None cc_default
→ extcall_arguments rs m sig (Vint index :: Vint ofs ::nil)
→ ∀ (Hsymbol: find_symbol s release_lock = Some b_PC)
(HPC: rs PC = Vptr b_PC Int.zero),
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
primcall_release_lock_sem s rs (m, adt) (rs´#RA <- Vundef#PC <- (rs RA)) (m, adt´).
Class ReleaseInvariants :=
{
release_lock_low_level_invariant n i ofs d d´ e:
release_lock_spec i ofs e d = Some d´ →
low_level_invariant n d →
low_level_invariant n d´;
release_lock_high_level_invariant i ofs d d´ e:
release_lock_spec i ofs e d = Some d´ →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: ReleaseInvariants}.
Local Instance primcall_release_lock_sem_propertes:
PrimcallProperties primcall_release_lock_sem.
Proof.
constructor; intros; inv H.
-
inv H0. args_list_inv. eapply ByteList_eq in H0; inv H0.
args_list_inv.
subst rs´ rs´0.
split; try congruence.
Qed.
Local Instance primcall_release_lock_sem_invariants:
PrimcallInvariants primcall_release_lock_sem.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
Local Opaque undef_regs destroyed_at_call.
constructor; lift_unfold; eauto.
subst rs´0.
val_inject_simpl.
+
repeat apply set_reg_wt;
try constructor; try assumption; simpl.
eapply inv_reg_wt. subst rs´0.
eapply undef_regs_wt.
eapply undef_regs_wt. trivial.
-
eapply release_lock_low_level_invariant; eauto.
-
eapply release_lock_high_level_invariant; eauto.
Qed.
Definition primcall_release_lock_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_release_lock_sem;
sprimcall_sig := mksignature (AST.Tint::AST.Tint::nil) None cc_default;
sprimcall_valid s := true
|};
sprimcall_name := Some release_lock;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End release_lock.
Section atomic_FAI.
Variable atomic_FAI_spec: Z → Z → Z → RData → (option (RData× (Z × Z))).
Inductive primcall_atomic_FAI_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| prim_atomic_FAI_sem_intro_mem:
∀ rs sig m m0 m´ adt adt´ bound i ofs b n t pos
(Hspec: atomic_FAI_spec (Int.unsigned bound) (Int.unsigned i) (Int.unsigned ofs)
adt = Some (adt´, (t, n)))
(Hsymbol: find_symbol s TICKET_LOCK_LOC = Some b)
(Hpos: index2Z (Int.unsigned i) (Int.unsigned ofs) = Some pos)
(Hstore0: Mem.store Mint32 m b (pos × 8) (Vint (Int.repr (t + 1))) = Some m0)
(Hstore1: Mem.store Mint32 m0 b (pos × 8 + 4) (Vint (Int.repr n)) = 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 i ::Vint ofs :: nil)),
primcall_atomic_FAI_sem s rs (m, adt) (rs#RA <- Vundef#PC <- (rs RA)#EAX <- (Vint (Int.repr t))) (m´, adt´).
Class AtomicFAIInvariants :=
{
atomic_FAI_low_level_invariant n bound i ofs d d´ e e´:
atomic_FAI_spec bound i ofs d = Some (d´, (e, e´)) →
low_level_invariant n d →
low_level_invariant n d´;
atomic_FAI_high_level_invariant bound i ofs d d´ e e´:
atomic_FAI_spec bound i ofs d = Some (d´, (e, e´)) →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: AtomicFAIInvariants}.
Local Instance primcall_atomic_FAI_sem_propertes:
PrimcallProperties primcall_atomic_FAI_sem.
Proof.
constructor; intros; inv H.
-
inv H0. args_list_inv.
split; try congruence.
Qed.
Local Instance primcall_atomic_FAI_sem_invariants:
PrimcallInvariants primcall_atomic_FAI_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 Hstore0; eauto.
eapply Mem.nextblock_store in Hstore1; 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.
+ xomega.
+ xomega.
}
{
rewrite Heq.
val_inject_simpl.
}
+
repeat apply set_reg_wt;
try constructor; try assumption; simpl.
eapply inv_reg_wt.
-
eapply atomic_FAI_low_level_invariant; eauto.
eapply Mem.nextblock_store in Hstore0; eauto.
eapply Mem.nextblock_store in Hstore1; eauto.
rewrite Hstore1, Hstore0. assumption.
-
eapply atomic_FAI_high_level_invariant; eauto.
Qed.
Definition primcall_atomic_FAI_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_atomic_FAI_sem;
sprimcall_sig := mksignature (AST.Tint::AST.Tint::AST.Tint::nil) (Some AST.Tint) cc_default;
sprimcall_valid s := true
|};
sprimcall_name := Some atomic_FAI;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End atomic_FAI.
Section atomic_GET.
Variable atomic_GET_spec: Z → Z → RData → (option (RData× (Z × Z))).
Inductive primcall_atomic_GET_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| prim_atomic_GET_sem_intro_mem:
∀ rs sig m m0 m´ adt adt´ i ofs b n t pos
(Hspec: atomic_GET_spec (Int.unsigned i) (Int.unsigned ofs) adt = Some (adt´, (t, n)))
(Hsymbol: find_symbol s TICKET_LOCK_LOC = Some b)
(Hpos: index2Z (Int.unsigned i) (Int.unsigned ofs) = Some pos)
(Hstore0: Mem.store Mint32 m b (pos × 8) (Vint (Int.repr t)) = Some m0)
(Hstore1: Mem.store Mint32 m0 b (pos × 8 + 4) (Vint (Int.repr n)) = Some m´)
(Hsig: sig = mksignature (AST.Tint::AST.Tint::nil) (Some AST.Tint) cc_default)
(Harg: extcall_arguments rs m sig (Vint i ::Vint ofs :: nil)),
primcall_atomic_GET_sem s rs (m, adt) (rs#RA <- Vundef#PC <- (rs RA) #EAX <- (Vint (Int.repr n))) (m´, adt´).
Class AtomicGETInvariants :=
{
atomic_GET_low_level_invariant n i ofs d d´ e e´:
atomic_GET_spec i ofs d = Some (d´, (e, e´)) →
low_level_invariant n d →
low_level_invariant n d´;
atomic_GET_high_level_invariant i ofs d d´ e e´:
atomic_GET_spec i ofs d = Some (d´, (e, e´)) →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: AtomicGETInvariants}.
Local Instance primcall_atomic_GET_sem_propertes:
PrimcallProperties primcall_atomic_GET_sem.
Proof.
constructor; intros; inv H.
-
inv H0. args_list_inv.
split; try congruence.
Qed.
Local Instance primcall_atomic_GET_sem_invariants:
PrimcallInvariants primcall_atomic_GET_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 Hstore0; eauto.
eapply Mem.nextblock_store in Hstore1; 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.
+ xomega.
+ xomega.
}
{
rewrite Heq.
val_inject_simpl.
}
+
repeat apply set_reg_wt;
try constructor; try assumption; simpl.
eapply inv_reg_wt.
-
eapply atomic_GET_low_level_invariant; eauto.
eapply Mem.nextblock_store in Hstore0; eauto.
eapply Mem.nextblock_store in Hstore1; eauto.
rewrite Hstore1, Hstore0. assumption.
-
eapply atomic_GET_high_level_invariant; eauto.
Qed.
Definition primcall_atomic_GET_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_atomic_GET_sem;
sprimcall_sig := mksignature (AST.Tint::AST.Tint::nil) (Some AST.Tint) cc_default;
sprimcall_valid s := true
|};
sprimcall_name := Some log_get;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End atomic_GET.
End Semantics.