Library mcertikos.objects.ObjMultiprocessor
Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import FlatMemory.
Require Import AbstractDataType.
Require Import Integers.
Require Import Values.
Require Import Constant.
Require Export MultiProcessorSemantics.
Require Import GlobIdent.
Require Import CalTicketLock.
Require Import RealParams.
Require Import CommonTactic.
Require Import DeviceStateDataType.
Require Import ObjInterruptDriver.
Section MULTIPROCESSOR.
primitve: trap into the kernel mode from user mode
Function get_CPU_ID_spec (adt: RData): option Z :=
match (ikern adt, ihost adt) with
| (true, true) ⇒ Some (CPU_ID adt)
| _ ⇒ None
end.
match (ikern adt, ihost adt) with
| (true, true) ⇒ Some (CPU_ID adt)
| _ ⇒ None
end.
primitve: get the current thread id
Function get_curid_spec (adt: RData): option Z :=
match (ikern adt, ihost adt) with
| (true, true) ⇒ Some (ZMap.get (CPU_ID adt) (cid adt))
| _ ⇒ None
end.
match (ikern adt, ihost adt) with
| (true, true) ⇒ Some (ZMap.get (CPU_ID adt) (cid adt))
| _ ⇒ None
end.
primitve: set the currect thread id to be
Function set_curid_spec (i: Z) (adt: RData) : option RData :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 i num_proc then
Some adt {cid: ZMap.set (CPU_ID adt) i (cid adt)}
else None
| _ ⇒ None
end.
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 i num_proc then
Some adt {cid: ZMap.set (CPU_ID adt) i (cid adt)}
else None
| _ ⇒ None
end.
primitve: set the currect thread id to be
Function set_curid_init_spec (i: Z) (adt: RData) : option RData :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 i TOTAL_CPU then
Some adt {cid: ZMap.set i (i+1) (cid adt)}
else None
| _ ⇒ None
end.
Section SHARED_PRIM.
Function release_shared0_spec (valid_arg: Z → option positive) (index ofs :Z)
(e: (list Integers.Byte.int)) (adt: RData) :=
let cpu := CPU_ID adt in
match (ikern adt, ihost adt, index2Z index ofs, valid_arg index) with
| (true, true, Some abid, Some id) ⇒
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
match CalValidBit l with
| Some (PullBy i) ⇒
if zeq i cpu then
Some (adt {multi_log: ZMap.set abid (MultiDef ((TEVENT cpu (TSHARED (OMEME e))) :: l)) (multi_log adt)})
else None
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
Definition acquire_shared0_spec (valid_arg: Z → option positive) (index ofs:Z) (adt: RData):
option (RData × positive × (option (list Integers.Byte.int))) :=
let cpu := CPU_ID adt in
match (ikern adt, ihost adt, index2Z index ofs, valid_arg index) with
| (true, true, Some abid, Some id) ⇒
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
match CalValidBit l with
| Some FreeToPull ⇒
match GetSharedMemEvent l with
| Some e ⇒ Some (adt {multi_log: ZMap.set abid (MultiDef ((TEVENT cpu (TSHARED OPULL)) :: l)) (multi_log adt)}
, id, Some e)
| _ ⇒ Some (adt {multi_log: ZMap.set abid (MultiDef ((TEVENT cpu (TSHARED OPULL)) :: l)) (multi_log adt)}
, id, None)
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
End SHARED_PRIM.
Section MULTI_LOG_PRIM.
Function incr_now_spec (index ofs:Z) (adt: RData) : option RData :=
match (ikern adt, ihost adt, index2Z index ofs) with
| (true, true, Some abid) ⇒
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
let cpu := CPU_ID adt in
Some adt {multi_log: ZMap.set abid (MultiDef ((TEVENT cpu (TTICKET INC_NOW)):: l)) (multi_log adt)}
| _ ⇒ None
end
| _ ⇒ None
end.
Definition log_incr_spec (index ofs:Z) (adt: RData) : option RData :=
let cpu := CPU_ID adt in
match (ikern adt, ihost adt, index2Z index ofs) with
| (true, true, Some abid) ⇒
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
Some adt {multi_log: ZMap.set abid (MultiDef ((TEVENT cpu (TTICKET INC_NOW)):: l)) (multi_log adt)}
| _ ⇒ None
end
| _ ⇒ None
end.
Definition log_hold_spec (index ofs:Z) (adt: RData) : option RData :=
let cpu := CPU_ID adt in
match (ikern adt, ihost adt, index2Z index ofs) with
| (true, true, Some abid) ⇒
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
Some adt {multi_log: ZMap.set abid (MultiDef ((TEVENT cpu (TTICKET HOLD_LOCK)):: l)) (multi_log adt)}
| _ ⇒ None
end
| _ ⇒ None
end.
Function init_ticket_spec (index ofs:Z) (adt: RData) : option RData :=
match (ikern adt, ihost adt, index2Z index ofs) with
| (true, true, Some abid) ⇒
Some adt {multi_log: ZMap.set abid (MultiDef nil) (multi_log adt)}
| _ ⇒ None
end.
Function log_init_spec (index ofs:Z) (adt: RData) : option RData :=
match (ikern adt, ihost adt, index2Z index ofs) with
| (true, true, Some abid) ⇒
Some adt {multi_log: ZMap.set abid (MultiDef nil) (multi_log adt)}
| _ ⇒ None
end.
Section WITHREAL.
Context `{real_params: RealParams}.
Function ticket_lock_init_spec (mbi_adt: Z) (adt: RData) : option RData :=
match (pg adt, ikern adt, ihost adt, init adt, in_intr adt) with
| (false, true, true, false, false) ⇒
let n := adt.(ioapic).(s).(IoApicMaxIntr) + 1 in
if zeq n (Zlength (adt.(ioapic).(s).(IoApicIrqs))) then
if zeq n (Zlength (adt.(ioapic).(s).(IoApicEnables))) then
Some adt {ioapic/s: ioapic_init_aux adt.(ioapic).(s) (Z.to_nat (n - 1))}
{lapic: (mkLApicData
(mkLApicState 0 NoIntr (LapicMaxLvt (s (lapic adt))) true
(32 + 7) true true true 0 50 false 0))
{l1: l1 (lapic adt)}
{l2: l2 (lapic adt)}
{l3: l3 (lapic adt)}
}
{ioapic / s / CurrentIrq: None} {MM: real_mm} {MMSize: real_size} {vmxinfo: real_vmxinfo} {init: true}
{multi_log: real_multi_log (multi_log adt)}
else
None
else
None
| _ ⇒ None
end.
End WITHREAL.
Definition incr_ticket_spec (bound index ofs:Z) (adt: RData) : option (RData× Z) :=
match (ikern adt, ihost adt, index2Z index ofs) with
| (true, true, Some abid) ⇒
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
let cpu := CPU_ID adt in
let to := ZMap.get abid (multi_oracle adt) in
let l1 := (to cpu l) ++ l in
let l´ := (TEVENT cpu (TTICKET (INC_TICKET (Z.to_nat bound)))) :: l1 in
match CalTicketLockWraparound l1 with
| Some (t, n, _) ⇒
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}, t)
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
Definition atomic_FAI_spec (bound index ofs:Z) (adt: RData) : option (RData× (Z × Z)) :=
let cpu := CPU_ID adt in
match (ikern adt, ihost adt, index2Z index ofs) with
| (true, true, Some abid) ⇒
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
let to := ZMap.get abid (multi_oracle adt) in
let l1 := (to cpu l) ++ l in
let l´ := (TEVENT cpu (TTICKET (INC_TICKET (Z.to_nat bound)))) :: l1 in
match CalTicketLockWraparound l1 with
| Some (t, n, _) ⇒
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}, (t,n))
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
Definition read_now_spec (index ofs:Z) (adt: RData) : option (Z) :=
match (ikern adt, ihost adt, index2Z index ofs) with
| (true, true, Some abid) ⇒
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
let to := ZMap.get abid (multi_oracle adt) in
match CalTicketLock l with
| Some (t, n, _ ) ⇒ Some n
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
Definition get_now_spec (index ofs:Z) (adt: RData) : option (RData× Z) :=
match (ikern adt, ihost adt, index2Z index ofs) with
| (true, true, Some abid) ⇒
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
let cpu := CPU_ID adt in
let to := ZMap.get abid (multi_oracle adt) in
let l1 := (to cpu l) ++ l in
let l´ := (TEVENT cpu (TTICKET GET_NOW)) :: l1 in
match CalTicketLockWraparound l´ with
| Some (t, n, _) ⇒
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}, n)
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
Definition log_get_spec (index ofs:Z) (adt: RData) : option (RData× (Z × Z)) :=
match (ikern adt, ihost adt, index2Z index ofs) with
| (true, true, Some abid) ⇒
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
let cpu := CPU_ID adt in
let to := ZMap.get abid (multi_oracle adt) in
let l1 := (to cpu l) ++ l in
let l´ := (TEVENT cpu (TTICKET GET_NOW)) :: l1 in
match CalTicketLockWraparound l´ with
| Some (t, n, _) ⇒
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}, (t,n))
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
End MULTI_LOG_PRIM.
Section HIGH_TICKET_LOCK_PRIM.
Section WITHWAITTIME.
Context `{waittime: WaitTime}.
Definition wait_lock_spec (bound index ofs :Z) (adt: RData) : option RData :=
match (ikern adt, ihost adt, index2Z index ofs) with
| (true, true, Some abid) ⇒
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
let cpu := CPU_ID adt in
let to := ZMap.get abid (multi_oracle adt) in
let l1 := (to cpu l) ++ l in
let l2 := (TEVENT cpu (TTICKET (INC_TICKET (Z.to_nat bound)))) :: l1 in
match CalTicketLock l2 with
| Some (t, n, tq) ⇒
if zlt t (n + TOTAL_CPU + 1) then
match CalTicketWait (CalWaitTime tq) cpu (t - 1) l2 to with
| Some l´ ⇒
Some adt {multi_log: ZMap.set abid (MultiDef ((TEVENT cpu (TTICKET HOLD_LOCK)) :: l´)) (multi_log adt)}
| _ ⇒ None
end
else None
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
Definition wait_lock_spec_wraparound (bound index ofs :Z) (adt: RData) : option RData :=
match (ikern adt, ihost adt, index2Z index ofs) with
| (true, true, Some abid) ⇒
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
let cpu := CPU_ID adt in
let to := ZMap.get abid (multi_oracle adt) in
let l1 := (to cpu l) ++ l in
let l2 := (TEVENT cpu (TTICKET (INC_TICKET (Z.to_nat bound)))) :: l1 in
match CalTicketLockWraparound l2 with
| Some (t, n, tq) ⇒
match CalTicketWaitWraparound (CalWaitTime tq) cpu (Int.unsigned (Int.repr (t - 1))) l2 to with
| Some l´ ⇒
Some adt {multi_log: ZMap.set abid (MultiDef ((TEVENT cpu (TTICKET HOLD_LOCK)) :: l´)) (multi_log adt)}
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
End WITHWAITTIME.
Function pass_lock_spec (index ofs :Z) (adt: RData) : option RData :=
match (ikern adt, ihost adt, index2Z index ofs) with
| (true, true, Some abid) ⇒
let cpu := CPU_ID adt in
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
let l´ := (TEVENT cpu (TTICKET INC_NOW)):: l in
Some adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
| _ ⇒ None
end
| _ ⇒ None
end.
End HIGH_TICKET_LOCK_PRIM.
End MULTIPROCESSOR.
Notation acquire_shared0_spec0 := (acquire_shared0_spec Shared2ID0).
Notation release_shared0_spec0 := (release_shared0_spec Shared2ID0).
Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.compat.CompatLayers.
Require Import CommonTactic.
Require Import RefinementTactic.
Require Import AuxLemma.
Require Import LAsmModuleSemAux.
Section OBJ_SIM.
Context `{data : CompatData RData}.
Context `{data0 : CompatData RData}.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Notation HDATAOps := (cdata (cdata_prf := data) RData).
Notation LDATAOps := (cdata (cdata_prf := data0) RData).
Context `{rel_prf: CompatRel _ (memory_model_ops:= memory_model_ops) _
(stencil_ops:= stencil_ops) HDATAOps LDATAOps}.
Section GET_CID_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_cid}.
Context {re3: relate_impl_CPU_ID}.
Lemma get_curid_exist:
∀ s habd labd z f,
get_curid_spec habd = Some z
→ relate_AbData s f habd labd
→ get_curid_spec labd = Some z.
Proof.
unfold get_curid_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H; subrewrite.
Qed.
Lemma get_curid_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem get_curid_spec)
(id ↦ gensem get_curid_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
erewrite get_curid_exist; eauto. reflexivity.
Qed.
End GET_CID_SIM.
Section SET_CURID_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_cid}.
Context {re3: relate_impl_CPU_ID}.
Lemma set_curid_exist:
∀ s i habd habd´ labd f,
set_curid_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, set_curid_spec i labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold set_curid_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_cid_update. assumption.
Qed.
Context {mt1: match_impl_cid}.
Lemma set_curid_match:
∀ s i d d´ m f,
set_curid_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold set_curid_spec; intros. subdestruct.
inv H. eapply match_impl_cid_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) set_curid_spec}.
Context {inv0: PreservesInvariants (HD:= data0) set_curid_spec}.
Lemma set_curid_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem set_curid_spec)
(id ↦ gensem set_curid_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit set_curid_exist; eauto 1. intros [labd´ [HP HM]].
match_external_states_simpl.
eapply set_curid_match; eauto.
Qed.
End SET_CURID_SIM.
Section SET_CURID_INIT_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_cid}.
Context {re3: relate_impl_CPU_ID}.
Lemma set_curid_init_exist:
∀ s i habd habd´ labd f,
set_curid_init_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, set_curid_init_spec i labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold set_curid_init_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto.
intros.
revert H; subrewrite.
subdestruct.
inv HQ.
refine_split´; trivial.
eapply relate_impl_cid_update.
assumption.
Qed.
Context {mt1: match_impl_cid}.
Lemma set_curid_init_match:
∀ s i d d´ m f,
set_curid_init_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold set_curid_init_spec; intros.
subdestruct.
inv H.
eapply match_impl_cid_update.
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) set_curid_init_spec}.
Context {inv0: PreservesInvariants (HD:= data0) set_curid_init_spec}.
Lemma set_curid_init_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem set_curid_init_spec)
(id ↦ gensem set_curid_init_spec).
Proof.
intros.
layer_sim_simpl.
compatsim_simpl (@match_AbData). intros.
exploit set_curid_init_exist; eauto 1.
intros [labd´ [HP HM]].
match_external_states_simpl.
eapply set_curid_init_match; eauto.
Qed.
End SET_CURID_INIT_SIM.
Section MULTI_SIM.
Context {re1: relate_impl_iflags}.
Section CPU_SIM.
Context {re2: relate_impl_CPU_ID}.
Lemma get_CPU_ID_exist:
∀ s habd labd v f,
get_CPU_ID_spec habd = Some v
→ relate_AbData s f habd labd
→ get_CPU_ID_spec labd = Some v.
Proof.
unfold get_CPU_ID_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H; subrewrite.
Qed.
Lemma get_CPU_ID_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem get_CPU_ID_spec) (id ↦ gensem get_CPU_ID_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
unfold get_CPU_ID_spec in ×.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_CPU_ID_eq; eauto; intros.
revert H2; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
Qed.
End CPU_SIM.
Section LOG_HOLD_SIM.
Context {re3: relate_impl_multi_oracle}.
Context {re30: relate_impl_multi_log}.
Context {mt2: match_impl_multi_log}.
Context {re300: relate_impl_CPU_ID}.
Lemma log_hold_exist:
∀ s i ofs habd habd´ labd f,
log_hold_spec i ofs habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, log_hold_spec i ofs labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold log_hold_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_multi_log_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H; subrewrite.
subdestruct; inv HQ; refine_split´; trivial.
eapply relate_impl_multi_log_update; trivial.
Qed.
Lemma log_hold_match:
∀ s i ofs d d´ m f,
log_hold_spec i ofs d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold log_hold_spec; intros.
subdestruct; inv H.
eapply match_impl_multi_log_update; trivial.
Qed.
Context {inv: PreservesInvariants (HD:= data) log_hold_spec}.
Context {inv0: PreservesInvariants (HD:= data0) log_hold_spec}.
Lemma log_hold_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem log_hold_spec)
(id ↦ gensem log_hold_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit log_hold_exist; eauto 1. intros [labd´ [HP HM]].
match_external_states_simpl.
eapply log_hold_match; eauto.
Qed.
End LOG_HOLD_SIM.
Section REALSE0_SIM.
Context `{valid_arg: Z → option positive}.
Context {re3001: relate_impl_multi_log}.
Context {mt2001: match_impl_multi_log}.
Context {re300: relate_impl_CPU_ID}.
Lemma release_shared0_exist:
∀ s i ofs e habd habd´ labd f,
release_shared0_spec valid_arg i ofs e habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, release_shared0_spec valid_arg i ofs e labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold release_shared0_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_multi_log_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_multi_log_update. assumption.
Qed.
Lemma release_shared0_match:
∀ s i ofs e d d´ m f,
release_shared0_spec valid_arg i ofs e d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold release_shared0_spec; intros. subdestruct.
inv H.
eapply match_impl_multi_log_update.
assumption.
Qed.
Context {inv: ReleaseInvariants (data_ops:= data_ops) (release_shared0_spec valid_arg)}.
Context {inv0: ReleaseInvariants (data_ops:= data_ops0) (release_shared0_spec valid_arg)}.
Local Open Scope Z_scope.
Lemma release_shared0_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_release_lock_compatsem id (release_shared0_spec valid_arg))
(id ↦ primcall_release_lock_compatsem id (release_shared0_spec valid_arg)).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit release_shared0_exist; eauto 1; intros (labd´ & HP & HM).
eapply (extcall_args_with_data (D:= HDATAOps) d1) in H11.
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
refine_split.
- econstructor; try eapply H7; eauto; try (eapply reg_symbol_inject; eassumption).
exploit Mem.loadbytes_inject; eauto.
{ eapply stencil_find_symbol_inject´; eauto. }
intros (bytes2 & HLD & Hlist).
eapply list_forall2_bytelist_inject_eq in Hlist. subst.
change (0 + 0) with 0 in HLD. trivial.
- repeat (econstructor; eauto).
+ eapply release_shared0_match; eauto.
+ subst rs´. val_inject_simpl.
Qed.
End REALSE0_SIM.
Section ACQUIRE_SHARED0_SIM.
Context `{valid_arg: Z → option positive}.
Context {re3: relate_impl_multi_oracle}.
Context {re3001: relate_impl_multi_log}.
Context {re300: relate_impl_CPU_ID}.
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 i TOTAL_CPU then
Some adt {cid: ZMap.set i (i+1) (cid adt)}
else None
| _ ⇒ None
end.
Section SHARED_PRIM.
Function release_shared0_spec (valid_arg: Z → option positive) (index ofs :Z)
(e: (list Integers.Byte.int)) (adt: RData) :=
let cpu := CPU_ID adt in
match (ikern adt, ihost adt, index2Z index ofs, valid_arg index) with
| (true, true, Some abid, Some id) ⇒
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
match CalValidBit l with
| Some (PullBy i) ⇒
if zeq i cpu then
Some (adt {multi_log: ZMap.set abid (MultiDef ((TEVENT cpu (TSHARED (OMEME e))) :: l)) (multi_log adt)})
else None
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
Definition acquire_shared0_spec (valid_arg: Z → option positive) (index ofs:Z) (adt: RData):
option (RData × positive × (option (list Integers.Byte.int))) :=
let cpu := CPU_ID adt in
match (ikern adt, ihost adt, index2Z index ofs, valid_arg index) with
| (true, true, Some abid, Some id) ⇒
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
match CalValidBit l with
| Some FreeToPull ⇒
match GetSharedMemEvent l with
| Some e ⇒ Some (adt {multi_log: ZMap.set abid (MultiDef ((TEVENT cpu (TSHARED OPULL)) :: l)) (multi_log adt)}
, id, Some e)
| _ ⇒ Some (adt {multi_log: ZMap.set abid (MultiDef ((TEVENT cpu (TSHARED OPULL)) :: l)) (multi_log adt)}
, id, None)
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
End SHARED_PRIM.
Section MULTI_LOG_PRIM.
Function incr_now_spec (index ofs:Z) (adt: RData) : option RData :=
match (ikern adt, ihost adt, index2Z index ofs) with
| (true, true, Some abid) ⇒
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
let cpu := CPU_ID adt in
Some adt {multi_log: ZMap.set abid (MultiDef ((TEVENT cpu (TTICKET INC_NOW)):: l)) (multi_log adt)}
| _ ⇒ None
end
| _ ⇒ None
end.
Definition log_incr_spec (index ofs:Z) (adt: RData) : option RData :=
let cpu := CPU_ID adt in
match (ikern adt, ihost adt, index2Z index ofs) with
| (true, true, Some abid) ⇒
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
Some adt {multi_log: ZMap.set abid (MultiDef ((TEVENT cpu (TTICKET INC_NOW)):: l)) (multi_log adt)}
| _ ⇒ None
end
| _ ⇒ None
end.
Definition log_hold_spec (index ofs:Z) (adt: RData) : option RData :=
let cpu := CPU_ID adt in
match (ikern adt, ihost adt, index2Z index ofs) with
| (true, true, Some abid) ⇒
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
Some adt {multi_log: ZMap.set abid (MultiDef ((TEVENT cpu (TTICKET HOLD_LOCK)):: l)) (multi_log adt)}
| _ ⇒ None
end
| _ ⇒ None
end.
Function init_ticket_spec (index ofs:Z) (adt: RData) : option RData :=
match (ikern adt, ihost adt, index2Z index ofs) with
| (true, true, Some abid) ⇒
Some adt {multi_log: ZMap.set abid (MultiDef nil) (multi_log adt)}
| _ ⇒ None
end.
Function log_init_spec (index ofs:Z) (adt: RData) : option RData :=
match (ikern adt, ihost adt, index2Z index ofs) with
| (true, true, Some abid) ⇒
Some adt {multi_log: ZMap.set abid (MultiDef nil) (multi_log adt)}
| _ ⇒ None
end.
Section WITHREAL.
Context `{real_params: RealParams}.
Function ticket_lock_init_spec (mbi_adt: Z) (adt: RData) : option RData :=
match (pg adt, ikern adt, ihost adt, init adt, in_intr adt) with
| (false, true, true, false, false) ⇒
let n := adt.(ioapic).(s).(IoApicMaxIntr) + 1 in
if zeq n (Zlength (adt.(ioapic).(s).(IoApicIrqs))) then
if zeq n (Zlength (adt.(ioapic).(s).(IoApicEnables))) then
Some adt {ioapic/s: ioapic_init_aux adt.(ioapic).(s) (Z.to_nat (n - 1))}
{lapic: (mkLApicData
(mkLApicState 0 NoIntr (LapicMaxLvt (s (lapic adt))) true
(32 + 7) true true true 0 50 false 0))
{l1: l1 (lapic adt)}
{l2: l2 (lapic adt)}
{l3: l3 (lapic adt)}
}
{ioapic / s / CurrentIrq: None} {MM: real_mm} {MMSize: real_size} {vmxinfo: real_vmxinfo} {init: true}
{multi_log: real_multi_log (multi_log adt)}
else
None
else
None
| _ ⇒ None
end.
End WITHREAL.
Definition incr_ticket_spec (bound index ofs:Z) (adt: RData) : option (RData× Z) :=
match (ikern adt, ihost adt, index2Z index ofs) with
| (true, true, Some abid) ⇒
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
let cpu := CPU_ID adt in
let to := ZMap.get abid (multi_oracle adt) in
let l1 := (to cpu l) ++ l in
let l´ := (TEVENT cpu (TTICKET (INC_TICKET (Z.to_nat bound)))) :: l1 in
match CalTicketLockWraparound l1 with
| Some (t, n, _) ⇒
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}, t)
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
Definition atomic_FAI_spec (bound index ofs:Z) (adt: RData) : option (RData× (Z × Z)) :=
let cpu := CPU_ID adt in
match (ikern adt, ihost adt, index2Z index ofs) with
| (true, true, Some abid) ⇒
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
let to := ZMap.get abid (multi_oracle adt) in
let l1 := (to cpu l) ++ l in
let l´ := (TEVENT cpu (TTICKET (INC_TICKET (Z.to_nat bound)))) :: l1 in
match CalTicketLockWraparound l1 with
| Some (t, n, _) ⇒
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}, (t,n))
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
Definition read_now_spec (index ofs:Z) (adt: RData) : option (Z) :=
match (ikern adt, ihost adt, index2Z index ofs) with
| (true, true, Some abid) ⇒
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
let to := ZMap.get abid (multi_oracle adt) in
match CalTicketLock l with
| Some (t, n, _ ) ⇒ Some n
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
Definition get_now_spec (index ofs:Z) (adt: RData) : option (RData× Z) :=
match (ikern adt, ihost adt, index2Z index ofs) with
| (true, true, Some abid) ⇒
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
let cpu := CPU_ID adt in
let to := ZMap.get abid (multi_oracle adt) in
let l1 := (to cpu l) ++ l in
let l´ := (TEVENT cpu (TTICKET GET_NOW)) :: l1 in
match CalTicketLockWraparound l´ with
| Some (t, n, _) ⇒
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}, n)
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
Definition log_get_spec (index ofs:Z) (adt: RData) : option (RData× (Z × Z)) :=
match (ikern adt, ihost adt, index2Z index ofs) with
| (true, true, Some abid) ⇒
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
let cpu := CPU_ID adt in
let to := ZMap.get abid (multi_oracle adt) in
let l1 := (to cpu l) ++ l in
let l´ := (TEVENT cpu (TTICKET GET_NOW)) :: l1 in
match CalTicketLockWraparound l´ with
| Some (t, n, _) ⇒
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}, (t,n))
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
End MULTI_LOG_PRIM.
Section HIGH_TICKET_LOCK_PRIM.
Section WITHWAITTIME.
Context `{waittime: WaitTime}.
Definition wait_lock_spec (bound index ofs :Z) (adt: RData) : option RData :=
match (ikern adt, ihost adt, index2Z index ofs) with
| (true, true, Some abid) ⇒
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
let cpu := CPU_ID adt in
let to := ZMap.get abid (multi_oracle adt) in
let l1 := (to cpu l) ++ l in
let l2 := (TEVENT cpu (TTICKET (INC_TICKET (Z.to_nat bound)))) :: l1 in
match CalTicketLock l2 with
| Some (t, n, tq) ⇒
if zlt t (n + TOTAL_CPU + 1) then
match CalTicketWait (CalWaitTime tq) cpu (t - 1) l2 to with
| Some l´ ⇒
Some adt {multi_log: ZMap.set abid (MultiDef ((TEVENT cpu (TTICKET HOLD_LOCK)) :: l´)) (multi_log adt)}
| _ ⇒ None
end
else None
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
Definition wait_lock_spec_wraparound (bound index ofs :Z) (adt: RData) : option RData :=
match (ikern adt, ihost adt, index2Z index ofs) with
| (true, true, Some abid) ⇒
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
let cpu := CPU_ID adt in
let to := ZMap.get abid (multi_oracle adt) in
let l1 := (to cpu l) ++ l in
let l2 := (TEVENT cpu (TTICKET (INC_TICKET (Z.to_nat bound)))) :: l1 in
match CalTicketLockWraparound l2 with
| Some (t, n, tq) ⇒
match CalTicketWaitWraparound (CalWaitTime tq) cpu (Int.unsigned (Int.repr (t - 1))) l2 to with
| Some l´ ⇒
Some adt {multi_log: ZMap.set abid (MultiDef ((TEVENT cpu (TTICKET HOLD_LOCK)) :: l´)) (multi_log adt)}
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
End WITHWAITTIME.
Function pass_lock_spec (index ofs :Z) (adt: RData) : option RData :=
match (ikern adt, ihost adt, index2Z index ofs) with
| (true, true, Some abid) ⇒
let cpu := CPU_ID adt in
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
let l´ := (TEVENT cpu (TTICKET INC_NOW)):: l in
Some adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
| _ ⇒ None
end
| _ ⇒ None
end.
End HIGH_TICKET_LOCK_PRIM.
End MULTIPROCESSOR.
Notation acquire_shared0_spec0 := (acquire_shared0_spec Shared2ID0).
Notation release_shared0_spec0 := (release_shared0_spec Shared2ID0).
Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.compat.CompatLayers.
Require Import CommonTactic.
Require Import RefinementTactic.
Require Import AuxLemma.
Require Import LAsmModuleSemAux.
Section OBJ_SIM.
Context `{data : CompatData RData}.
Context `{data0 : CompatData RData}.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Notation HDATAOps := (cdata (cdata_prf := data) RData).
Notation LDATAOps := (cdata (cdata_prf := data0) RData).
Context `{rel_prf: CompatRel _ (memory_model_ops:= memory_model_ops) _
(stencil_ops:= stencil_ops) HDATAOps LDATAOps}.
Section GET_CID_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_cid}.
Context {re3: relate_impl_CPU_ID}.
Lemma get_curid_exist:
∀ s habd labd z f,
get_curid_spec habd = Some z
→ relate_AbData s f habd labd
→ get_curid_spec labd = Some z.
Proof.
unfold get_curid_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H; subrewrite.
Qed.
Lemma get_curid_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem get_curid_spec)
(id ↦ gensem get_curid_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
erewrite get_curid_exist; eauto. reflexivity.
Qed.
End GET_CID_SIM.
Section SET_CURID_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_cid}.
Context {re3: relate_impl_CPU_ID}.
Lemma set_curid_exist:
∀ s i habd habd´ labd f,
set_curid_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, set_curid_spec i labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold set_curid_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_cid_update. assumption.
Qed.
Context {mt1: match_impl_cid}.
Lemma set_curid_match:
∀ s i d d´ m f,
set_curid_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold set_curid_spec; intros. subdestruct.
inv H. eapply match_impl_cid_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) set_curid_spec}.
Context {inv0: PreservesInvariants (HD:= data0) set_curid_spec}.
Lemma set_curid_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem set_curid_spec)
(id ↦ gensem set_curid_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit set_curid_exist; eauto 1. intros [labd´ [HP HM]].
match_external_states_simpl.
eapply set_curid_match; eauto.
Qed.
End SET_CURID_SIM.
Section SET_CURID_INIT_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_cid}.
Context {re3: relate_impl_CPU_ID}.
Lemma set_curid_init_exist:
∀ s i habd habd´ labd f,
set_curid_init_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, set_curid_init_spec i labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold set_curid_init_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto.
intros.
revert H; subrewrite.
subdestruct.
inv HQ.
refine_split´; trivial.
eapply relate_impl_cid_update.
assumption.
Qed.
Context {mt1: match_impl_cid}.
Lemma set_curid_init_match:
∀ s i d d´ m f,
set_curid_init_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold set_curid_init_spec; intros.
subdestruct.
inv H.
eapply match_impl_cid_update.
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) set_curid_init_spec}.
Context {inv0: PreservesInvariants (HD:= data0) set_curid_init_spec}.
Lemma set_curid_init_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem set_curid_init_spec)
(id ↦ gensem set_curid_init_spec).
Proof.
intros.
layer_sim_simpl.
compatsim_simpl (@match_AbData). intros.
exploit set_curid_init_exist; eauto 1.
intros [labd´ [HP HM]].
match_external_states_simpl.
eapply set_curid_init_match; eauto.
Qed.
End SET_CURID_INIT_SIM.
Section MULTI_SIM.
Context {re1: relate_impl_iflags}.
Section CPU_SIM.
Context {re2: relate_impl_CPU_ID}.
Lemma get_CPU_ID_exist:
∀ s habd labd v f,
get_CPU_ID_spec habd = Some v
→ relate_AbData s f habd labd
→ get_CPU_ID_spec labd = Some v.
Proof.
unfold get_CPU_ID_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H; subrewrite.
Qed.
Lemma get_CPU_ID_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem get_CPU_ID_spec) (id ↦ gensem get_CPU_ID_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
unfold get_CPU_ID_spec in ×.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_CPU_ID_eq; eauto; intros.
revert H2; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
Qed.
End CPU_SIM.
Section LOG_HOLD_SIM.
Context {re3: relate_impl_multi_oracle}.
Context {re30: relate_impl_multi_log}.
Context {mt2: match_impl_multi_log}.
Context {re300: relate_impl_CPU_ID}.
Lemma log_hold_exist:
∀ s i ofs habd habd´ labd f,
log_hold_spec i ofs habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, log_hold_spec i ofs labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold log_hold_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_multi_log_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H; subrewrite.
subdestruct; inv HQ; refine_split´; trivial.
eapply relate_impl_multi_log_update; trivial.
Qed.
Lemma log_hold_match:
∀ s i ofs d d´ m f,
log_hold_spec i ofs d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold log_hold_spec; intros.
subdestruct; inv H.
eapply match_impl_multi_log_update; trivial.
Qed.
Context {inv: PreservesInvariants (HD:= data) log_hold_spec}.
Context {inv0: PreservesInvariants (HD:= data0) log_hold_spec}.
Lemma log_hold_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem log_hold_spec)
(id ↦ gensem log_hold_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit log_hold_exist; eauto 1. intros [labd´ [HP HM]].
match_external_states_simpl.
eapply log_hold_match; eauto.
Qed.
End LOG_HOLD_SIM.
Section REALSE0_SIM.
Context `{valid_arg: Z → option positive}.
Context {re3001: relate_impl_multi_log}.
Context {mt2001: match_impl_multi_log}.
Context {re300: relate_impl_CPU_ID}.
Lemma release_shared0_exist:
∀ s i ofs e habd habd´ labd f,
release_shared0_spec valid_arg i ofs e habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, release_shared0_spec valid_arg i ofs e labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold release_shared0_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_multi_log_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_multi_log_update. assumption.
Qed.
Lemma release_shared0_match:
∀ s i ofs e d d´ m f,
release_shared0_spec valid_arg i ofs e d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold release_shared0_spec; intros. subdestruct.
inv H.
eapply match_impl_multi_log_update.
assumption.
Qed.
Context {inv: ReleaseInvariants (data_ops:= data_ops) (release_shared0_spec valid_arg)}.
Context {inv0: ReleaseInvariants (data_ops:= data_ops0) (release_shared0_spec valid_arg)}.
Local Open Scope Z_scope.
Lemma release_shared0_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_release_lock_compatsem id (release_shared0_spec valid_arg))
(id ↦ primcall_release_lock_compatsem id (release_shared0_spec valid_arg)).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit release_shared0_exist; eauto 1; intros (labd´ & HP & HM).
eapply (extcall_args_with_data (D:= HDATAOps) d1) in H11.
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
refine_split.
- econstructor; try eapply H7; eauto; try (eapply reg_symbol_inject; eassumption).
exploit Mem.loadbytes_inject; eauto.
{ eapply stencil_find_symbol_inject´; eauto. }
intros (bytes2 & HLD & Hlist).
eapply list_forall2_bytelist_inject_eq in Hlist. subst.
change (0 + 0) with 0 in HLD. trivial.
- repeat (econstructor; eauto).
+ eapply release_shared0_match; eauto.
+ subst rs´. val_inject_simpl.
Qed.
End REALSE0_SIM.
Section ACQUIRE_SHARED0_SIM.
Context `{valid_arg: Z → option positive}.
Context {re3: relate_impl_multi_oracle}.
Context {re3001: relate_impl_multi_log}.
Context {re300: relate_impl_CPU_ID}.
In order to prove the simulation for acquire_shared0, we
need to know that the match relation is preserved whenever
the log evolved in the following way.
Definition acquire_shared0_log_update_match :=
fun (l l´: MultiLog) ⇒
∀ t n tq,
CalTicketLockWraparound l = Some (t, n, tq) →
∃ t´ n´ tq´,
CalTicketLockWraparound l´ = Some (t´, n´, tq´) ∧
Int.repr t´ = Int.repr t ∧
Int.repr n´ = Int.repr n.
Context {mt2001:match_impl_multi_log_one acquire_shared0_log_update_match}.
Lemma acquire_shared0_exist:
∀ s i ofs habd habd´ labd f p l,
acquire_shared0_spec valid_arg i ofs habd = Some (habd´, p, l)
→ relate_AbData s f habd labd
→ (∃ labd´, acquire_shared0_spec valid_arg i ofs labd = Some (labd´, p, l) ∧
relate_AbData s f habd´ labd´)
∧ valid_arg i = Some p.
Proof.
unfold acquire_shared0_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_multi_oracle_eq; eauto. intros.
exploit relate_impl_multi_log_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H; subrewrite. subdestruct.
- inv HQ. refine_split´; trivial.
eapply relate_impl_multi_log_update.
assumption.
- inv HQ. refine_split´; trivial.
eapply relate_impl_multi_log_update. assumption.
Qed.
Lemma acquire_shared0_match:
∀ s i ofs d d´ m f p l,
acquire_shared0_spec valid_arg i ofs d = Some (d´, p, l)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold acquire_shared0_spec; intros. subdestruct.
- inv H.
eapply match_impl_multi_log_one_update; eauto.
intros t n tq Hl0.
simpl.
rewrite Hl0.
repeat econstructor; rewrite Int.repr_unsigned; eauto.
- inv H. trivial.
eapply match_impl_multi_log_one_update; eauto.
intros t n tq Hl0.
simpl.
rewrite Hl0.
repeat econstructor; rewrite Int.repr_unsigned; eauto.
Qed.
Context {inv: SAcquireInvariants (data_ops:= data_ops) (acquire_shared0_spec valid_arg)}.
Context {inv0: SAcquireInvariants (data_ops:= data_ops0) (acquire_shared0_spec valid_arg)}.
Context `{valid_id: positive → bool}.
Context `{valid_id_args:
∀ i id,
valid_arg i = Some id →
valid_id id = true}.
Lemma acquire_shared0_sim:
∀
(HMatch:
∀ i,
In i new_glbl → valid_id i = false)
id,
sim (crel RData RData)
(id ↦ primcall_acquire_shared_compatsem (acquire_shared0_spec valid_arg))
(id ↦ primcall_acquire_shared_compatsem (acquire_shared0_spec valid_arg)).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit acquire_shared0_exist; eauto 1; intros ((labd´ & HP & HM) & HS).
eapply (extcall_args_with_data (D:= HDATAOps) d1) in H10.
destruct l; subst.
{
exploit Mem.storebytes_mapped_inject; eauto.
{ eapply stencil_find_symbol_inject´; eauto. }
{ eapply list_forall2_bytelist_inject; eauto. }
intros (m2´ & Hst & Hinj).
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
match_external_states_simpl.
- simpl. trivial.
-
eapply storebytes_match_correct; eauto.
eapply acquire_shared0_match; eauto.
intros. exploit HMatch; eauto. intros.
destruct (peq i id0).
+ subst. eapply valid_id_args in HS. congruence.
+ red; intros; subst. elim n.
eapply (genv_vars_inj s i id0); eauto.
-
erewrite Mem.nextblock_storebytes; eauto.
eapply Mem.nextblock_storebytes in Hst; eauto.
rewrite Hst. assumption.
-
intros. red; intros.
eapply match_newglob_noperm; eauto.
eapply Mem.perm_storebytes_2; eauto.
-
erewrite Mem.nextblock_storebytes; eauto.
-
subst rs´.
val_inject_simpl.
}
{
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
match_external_states_simpl.
-
eapply acquire_shared0_match; eauto.
-
subst rs´. val_inject_simpl.
}
Qed.
End ACQUIRE_SHARED0_SIM.
Section ACQUIRE_SHARED0_SIM_MCS.
Context `{valid_arg: Z → option positive}.
Context {re3: relate_impl_multi_oracle}.
Context {re3001: relate_impl_multi_log}.
Context {re300: relate_impl_CPU_ID}.
In order to prove the simulation for acquire_shared0, we
need to know that the match relation is preserved whenever
the log evolved in the following way.
Definition acquire_shared0_log_update_match_mcs :=
fun (l l´: MultiLog) ⇒
∀ la np tq bs0 ne0 bs1 ne1 bs2 ne2 bs3 ne3 bs4 ne4 bs5 ne5 bs6 ne6 bs7 ne7
(Hcal: CalMCSLock l = Some (MCSLOCK la np tq))
(Hnc0: ZMap.get 0%Z np = (bs0, ne0))
(Hnc1: ZMap.get 1%Z np = (bs1, ne1))
(Hnc2: ZMap.get 2%Z np = (bs2, ne2))
(Hnc3: ZMap.get 3%Z np = (bs3, ne3))
(Hnc4: ZMap.get 4%Z np = (bs4, ne4))
(Hnc5: ZMap.get 5%Z np = (bs5, ne5))
(Hnc6: ZMap.get 6%Z np = (bs6, ne6))
(Hnc7: ZMap.get 7%Z np = (bs7, ne7)),
∃ la´ np´ tq´ bs0´ ne0´ bs1´ ne1´ bs2´ ne2´ bs3´ ne3´ bs4´ ne4´ bs5´ ne5´ bs6´ ne6´ bs7´ ne7´,
CalMCSLock l´ = Some (MCSLOCK la´ np´ tq´) ∧
ZMap.get 0%Z np´ = (bs0´, ne0´) ∧
ZMap.get 1%Z np´ = (bs1´, ne1´) ∧
ZMap.get 2%Z np´ = (bs2´, ne2´) ∧
ZMap.get 3%Z np´ = (bs3´, ne3´) ∧
ZMap.get 4%Z np´ = (bs4´, ne4´) ∧
ZMap.get 5%Z np´ = (bs5´, ne5´) ∧
ZMap.get 6%Z np´ = (bs6´, ne6´) ∧
ZMap.get 7%Z np´ = (bs7´, ne7´) ∧
la = la´ ∧
Int.repr (BooltoZ bs0) = Int.repr (BooltoZ bs0´) ∧ Int.repr ne0 = Int.repr ne0´ ∧
Int.repr (BooltoZ bs1) = Int.repr (BooltoZ bs1´) ∧ Int.repr ne1 = Int.repr ne1´ ∧
Int.repr (BooltoZ bs2) = Int.repr (BooltoZ bs2´) ∧ Int.repr ne2 = Int.repr ne2´ ∧
Int.repr (BooltoZ bs3) = Int.repr (BooltoZ bs3´) ∧ Int.repr ne3 = Int.repr ne3´ ∧
Int.repr (BooltoZ bs4) = Int.repr (BooltoZ bs4´) ∧ Int.repr ne4 = Int.repr ne4´ ∧
Int.repr (BooltoZ bs5) = Int.repr (BooltoZ bs5´) ∧ Int.repr ne5 = Int.repr ne5´ ∧
Int.repr (BooltoZ bs6) = Int.repr (BooltoZ bs6´) ∧ Int.repr ne6 = Int.repr ne6´ ∧
Int.repr (BooltoZ bs7) = Int.repr (BooltoZ bs7´) ∧ Int.repr ne7 = Int.repr ne7´.
Context {mt2001:match_impl_multi_log_one acquire_shared0_log_update_match_mcs}.
Lemma acquire_shared0_mcs_exist:
∀ s i ofs habd habd´ labd f p l,
acquire_shared0_spec valid_arg i ofs habd = Some (habd´, p, l)
→ relate_AbData s f habd labd
→ (∃ labd´, acquire_shared0_spec valid_arg i ofs labd = Some (labd´, p, l) ∧
relate_AbData s f habd´ labd´)
∧ valid_arg i = Some p.
Proof.
unfold acquire_shared0_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_multi_oracle_eq; eauto. intros.
exploit relate_impl_multi_log_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H; subrewrite. subdestruct.
- inv HQ. refine_split´; trivial.
eapply relate_impl_multi_log_update.
assumption.
- inv HQ. refine_split´; trivial.
eapply relate_impl_multi_log_update. assumption.
Qed.
Lemma acquire_shared0_mcs_match:
∀ s i ofs d d´ m f p l,
acquire_shared0_spec valid_arg i ofs d = Some (d´, p, l)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold acquire_shared0_spec; intros. subdestruct.
- inv H.
eapply match_impl_multi_log_one_update; eauto.
intros la np tq bs0 ne0 bs1 ne1 bs2 ne2 bs3 ne3 bs4 ne4 bs5 ne5 bs6 ne6 bs7 ne7.
intros.
simpl.
refine_split´; eauto.
simpl.
Transparent CalMCSLock.
simpl.
rewrite Hcal; eauto.
- inv H. trivial.
eapply match_impl_multi_log_one_update; eauto.
intros la np tq bs0 ne0 bs1 ne1 bs2 ne2 bs3 ne3 bs4 ne4 bs5 ne5 bs6 ne6 bs7 ne7.
intros.
refine_split´; eauto.
simpl.
rewrite Hcal; eauto.
Qed.
Context {inv: SAcquireInvariants (data_ops:= data_ops) (acquire_shared0_spec valid_arg)}.
Context {inv0: SAcquireInvariants (data_ops:= data_ops0) (acquire_shared0_spec valid_arg)}.
Context `{valid_id: positive → bool}.
Context `{valid_id_args:
∀ i id,
valid_arg i = Some id →
valid_id id = true}.
Lemma acquire_shared0_mcs_sim:
∀
(HMatch:
∀ i,
In i new_glbl → valid_id i = false)
id,
sim (crel RData RData)
(id ↦ primcall_acquire_shared_compatsem (acquire_shared0_spec valid_arg))
(id ↦ primcall_acquire_shared_compatsem (acquire_shared0_spec valid_arg)).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit acquire_shared0_mcs_exist; eauto 1; intros ((labd´ & HP & HM) & HS).
eapply (extcall_args_with_data (D:= HDATAOps) d1) in H10.
destruct l; subst.
{
exploit Mem.storebytes_mapped_inject; eauto.
{ eapply stencil_find_symbol_inject´; eauto. }
{ eapply list_forall2_bytelist_inject; eauto. }
intros (m2´ & Hst & Hinj).
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
match_external_states_simpl.
- simpl. trivial.
-
eapply storebytes_match_correct; eauto.
eapply acquire_shared0_mcs_match; eauto.
intros. exploit HMatch; eauto. intros.
destruct (peq i id0).
+ subst. eapply valid_id_args in HS. congruence.
+ red; intros; subst. elim n.
eapply (genv_vars_inj s i id0); eauto.
-
erewrite Mem.nextblock_storebytes; eauto.
eapply Mem.nextblock_storebytes in Hst; eauto.
rewrite Hst. assumption.
-
intros. red; intros.
eapply match_newglob_noperm; eauto.
eapply Mem.perm_storebytes_2; eauto.
-
erewrite Mem.nextblock_storebytes; eauto.
-
subst rs´.
val_inject_simpl.
}
{
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
match_external_states_simpl.
-
eapply acquire_shared0_mcs_match; eauto.
-
subst rs´. val_inject_simpl.
}
Qed.
End ACQUIRE_SHARED0_SIM_MCS.
End MULTI_SIM.
End OBJ_SIM.