Library mcertikos.objects.ObjQLock
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.
Require Import ObjMultiprocessor.
Section MULTIPROCESSOR.
Section SHARED_PRIM.
Context `{waittime: WaitTime}.
Definition acquire_shared1_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 (lock adt) with
| LockOwn false⇒
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
match CalValidBit l with
| Some FreeToPull ⇒
let l´ := (TEVENT cpu (TSHARED OPULL)) :: l in
match Q_CalLock l´ with
| Some _ ⇒
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
{lock: ZMap.set abid (LockOwn true) (lock adt)},
id, GetSharedMemEvent l´)
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
Definition acquire_shared1_mcs_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 (lock adt) with
| LockOwn false⇒
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
match CalValidBit l with
| Some FreeToPull ⇒
let l´ := (TEVENT cpu (TSHARED OPULL)) :: l in
match QS_CalLock l´ with
| Some _ ⇒
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
{lock: ZMap.set abid (LockOwn true) (lock adt)},
id, GetSharedMemEvent l´)
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
Function release_shared1_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 (lock adt) with
| LockOwn true ⇒
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
match CalValidBit l with
| Some (PullBy i) ⇒
if zeq i cpu then
let l´ := (TEVENT cpu (TSHARED (OMEME e))) :: l in
match Q_CalLock l´ with
| Some _ ⇒
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
{lock: ZMap.set abid (LockOwn false) (lock adt)})
| _ ⇒ None
end
else None
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
Function release_shared1_mcs_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 (lock adt) with
| LockOwn true ⇒
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
match CalValidBit l with
| Some (PullBy i) ⇒
if zeq i cpu then
let l´ := (TEVENT cpu (TSHARED (OMEME e))) :: l in
match QS_CalLock l´ with
| Some _ ⇒
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
{lock: ZMap.set abid (LockOwn false) (lock adt)})
| _ ⇒ None
end
else None
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
Definition acquire_shared_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 (lock adt) with
| LockOwn false ⇒
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
let l´ := (TEVENT cpu (TSHARED OPULL)) :: l in
match H_CalLock l´ with
| Some _ ⇒
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
{lock: ZMap.set abid (LockOwn true) (lock adt)},
id, GetSharedMemEvent l´)
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
Function release_shared_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 (lock adt) with
| LockOwn true ⇒
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
let l´ := (TEVENT cpu (TSHARED (OMEME e))) :: l in
match H_CalLock l´ with
| Some _ ⇒
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
{lock: ZMap.set abid (LockOwn false) (lock adt)})
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
End SHARED_PRIM.
Section HIGH_TICKET_LOCK_PRIM.
Section WITHWAITTIME.
Context `{waittime: WaitTime}.
Definition wait_qlock_spec (bound 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), ZMap.get abid (lock adt) with
| MultiDef l, LockFalse ⇒
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 Q_CalLock l2 with
| Some (self_c, other_c, b, q, tq) ⇒
match Q_CalWait (CalWaitTime tq) cpu l2 to with
| Some l´ ⇒
let l´´ := (TEVENT cpu (TTICKET HOLD_LOCK)) :: l´ in
match Q_CalLock l´´ with
| Some _ ⇒
Some adt {multi_log: ZMap.set abid (MultiDef l´´) (multi_log adt)}
{lock: ZMap.set abid (LockOwn false) (lock adt)}
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _, _ ⇒ None
end
| _ ⇒ None
end.
Definition wait_hlock_spec (bound 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), ZMap.get abid (lock adt) with
| MultiDef l, LockFalse ⇒
let to := ZMap.get abid (multi_oracle adt) in
let l1 := (to cpu l) ++ l in
let l´ := (TEVENT cpu (TTICKET (WAIT_LOCK (Z.to_nat bound)))) :: l1 in
match H_CalLock l´ with
| Some _ ⇒
Some adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
{lock: ZMap.set abid (LockOwn false) (lock adt)}
| _ ⇒ None
end
| _, _ ⇒ None
end
| _ ⇒ None
end.
Definition acquire_lock_spec (valid_arg: Z → option positive) (bound 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 idm) ⇒
match ZMap.get abid (multi_log adt), ZMap.get abid (lock adt) with
| MultiDef l, LockFalse ⇒
let to := ZMap.get abid (multi_oracle adt) in
let l1 := (to cpu l) ++ l in
let l´ := (TEVENT cpu (TSHARED OPULL) ::
TEVENT cpu (TTICKET (WAIT_LOCK (Z.to_nat bound))) :: l1) in
match H_CalLock l´ with
| Some _ ⇒
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
{lock: ZMap.set abid (LockOwn true) (lock adt)}, idm, GetSharedMemEvent l´)
| _ ⇒ None
end
| _,_ ⇒ None
end
| _ ⇒ None
end.
End WITHWAITTIME.
Context `{waittime: WaitTime}.
Function pass_qlock_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), ZMap.get abid (lock adt) with
| MultiDef l, LockOwn false ⇒
let l´ := (TEVENT cpu (TTICKET INC_NOW)):: l in
match Q_CalLock l´ with
| Some _ ⇒ Some adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
{lock: ZMap.set abid LockFalse (lock adt)}
| _ ⇒ None
end
| _,_ ⇒ None
end
| _ ⇒ None
end.
Function pass_hlock_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), ZMap.get abid (lock adt) with
| MultiDef l, LockOwn false ⇒
let l´ := (TEVENT cpu (TTICKET REL_LOCK)):: l in
match H_CalLock l´ with
| Some _ ⇒ Some adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
{lock: ZMap.set abid LockFalse (lock adt)}
| _ ⇒ None
end
| _,_ ⇒ None
end
| _ ⇒ None
end.
Function release_lock_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), ZMap.get abid (lock adt) with
| MultiDef l, LockOwn true ⇒
let l´ := (TEVENT cpu (TTICKET REL_LOCK)):: (TEVENT cpu (TSHARED (OMEME e))) :: l in
match H_CalLock l´ with
| Some (_) ⇒ Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
{lock: ZMap.set abid LockFalse (lock adt)})
| _ ⇒ None
end
| _,_ ⇒ None
end
| _ ⇒ None
end.
Section WITHREAL.
Context `{real_params: RealParams}.
Function ticket_lock_init0_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)}
{lock: real_lock (lock adt)}
else
None
else
None
| _ ⇒ None
end.
End WITHREAL.
End HIGH_TICKET_LOCK_PRIM.
Section ACQUIRE_LOCK.
Context `{waittime: WaitTime}.
Definition acquire_lock_AT_spec (adt: RData) :=
let abid := 0 in
let cpu := CPU_ID adt in
match (ikern adt, ihost adt) with
| (true, true) ⇒
match ZMap.get abid (multi_log adt), ZMap.get abid (lock adt) with
| MultiDef l, LockFalse ⇒
let to := ZMap.get abid (multi_oracle adt) in
let l1 := (to cpu l) ++ l in
let l´ := TEVENT cpu (TSHARED OPULL) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: l1 in
match H_CalLock l´ with
| Some _ ⇒
match GetSharedAT l´ with
| Some e ⇒
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
{lock: ZMap.set abid (LockOwn true) (lock adt)}
{AT: e})
| _ ⇒
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
{lock: ZMap.set abid (LockOwn true) (lock adt)})
end
| _ ⇒ None
end
| _,_ ⇒ None
end
| _ ⇒ None
end.
Lemma acquire_lock_AT_lock_status:
∀ d d´,
acquire_lock_AT_spec d = Some d´ →
ZMap.get 0 (lock d´) = LockOwn true.
Proof.
unfold acquire_lock_AT_spec. intros.
subdestruct; inv H; simpl.
- rewrite ZMap.gss. trivial.
- rewrite ZMap.gss. trivial.
Qed.
Definition acquire_lock_TCB_spec (index: Z) (adt: RData) :=
let abid := (index + ID_AT_range) in
let cpu := CPU_ID adt in
match (ikern adt, ihost adt, pg adt) with
| (true, true, true) ⇒
if zle_lt 0 index num_chan then
match ZMap.get abid (multi_log adt), ZMap.get abid (lock adt) with
| MultiDef l, LockFalse ⇒
let to := ZMap.get abid (multi_oracle adt) in
let l1 := (to cpu l) ++ l in
let l´ := TEVENT cpu (TSHARED OPULL) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: l1 in
match H_CalLock l´ with
| Some _ ⇒
match GetSharedTCB l´ with
| Some (e1, e2) ⇒
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
{lock: ZMap.set abid (LockOwn true) (lock adt)}
{tcb: e1} {tdq: e2})
| _ ⇒
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
{lock: ZMap.set abid (LockOwn true) (lock adt)})
end
| _ ⇒ None
end
| _,_ ⇒ None
end
else None
| _ ⇒ None
end.
Lemma acquire_lock_TCB_lock_status:
∀ n d d´,
acquire_lock_TCB_spec n d = Some d´ →
ZMap.get (n + ID_AT_range) (lock d´) = LockOwn true.
Proof.
unfold acquire_lock_TCB_spec. intros.
subdestruct; inv H; simpl.
- rewrite ZMap.gss. trivial.
- rewrite ZMap.gss. trivial.
Qed.
Definition acquire_lock_ABTCB_spec (index: Z) (adt: RData) :=
let abid := (index + ID_AT_range) in
let cpu := CPU_ID adt in
match (ikern adt, ihost adt, pg adt) with
| (true, true, true) ⇒
if zle_lt 0 index num_chan then
match ZMap.get abid (multi_log adt), ZMap.get abid (lock adt) with
| MultiDef l, LockFalse ⇒
let to := ZMap.get abid (multi_oracle adt) in
let l1 := (to cpu l) ++ l in
let l´ := TEVENT cpu (TSHARED OPULL) ::TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: l1 in
match H_CalLock l´ with
| Some _ ⇒
match GetSharedABTCB l´ with
| Some (e1, e2) ⇒
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
{lock: ZMap.set abid (LockOwn true) (lock adt)}
{abtcb: e1} {abq: e2})
| _ ⇒
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
{lock: ZMap.set abid (LockOwn true) (lock adt)})
end
| _ ⇒ None
end
| _,_ ⇒ None
end
else None
| _ ⇒ None
end.
Lemma acquire_lock_ABTCB_lock_status:
∀ n d d´,
acquire_lock_ABTCB_spec n d = Some d´ →
ZMap.get (n + ID_AT_range) (lock d´) = LockOwn true.
Proof.
unfold acquire_lock_ABTCB_spec. intros.
subdestruct; inv H; simpl.
- rewrite ZMap.gss. trivial.
- rewrite ZMap.gss. trivial.
Qed.
Definition acquire_lock_SC_spec (index: Z) (adt: RData) :=
let abid := (index + lock_TCB_range) in
let cpu := CPU_ID adt in
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 index num_chan then
match ZMap.get abid (multi_log adt), ZMap.get abid (lock adt) with
| MultiDef l, LockFalse ⇒
let to := ZMap.get abid (multi_oracle adt) in
let l1 := (to cpu l) ++ l in
let l´ := TEVENT cpu (TSHARED OPULL) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: l1 in
match H_CalLock l´ with
| Some _ ⇒
match GetSharedSC l´ with
| Some e ⇒
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
{lock: ZMap.set abid (LockOwn true) (lock adt)}
{syncchpool: e})
| _ ⇒
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
{lock: ZMap.set abid (LockOwn true) (lock adt)})
end
| _ ⇒ None
end
| _,_ ⇒ None
end
else None
| _ ⇒ None
end.
Lemma acquire_lock_SC_lock_status:
∀ n d d´,
acquire_lock_SC_spec n d = Some d´ →
ZMap.get (n + lock_TCB_range) (lock d´) = LockOwn true.
Proof.
unfold acquire_lock_SC_spec. intros.
subdestruct; inv H; simpl.
- rewrite ZMap.gss. trivial.
- rewrite ZMap.gss. trivial.
Qed.
End ACQUIRE_LOCK.
Section RELEASE_LOCK.
Function release_lock_AT_spec (adt: RData) :=
let abid := 0 in
let cpu := CPU_ID adt in
match (ikern adt, ihost adt) with
| (true, true) ⇒
match ZMap.get abid (multi_log adt), ZMap.get abid (lock adt) with
| MultiDef l, LockOwn true ⇒
let l´ := (TEVENT cpu (TTICKET REL_LOCK)):: (TEVENT cpu (TSHARED (OATE (AT adt)))) :: l in
match H_CalLock l´ with
| Some _ ⇒
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
{lock: ZMap.set abid LockFalse (lock adt)})
| _ ⇒ None
end
| _,_ ⇒ None
end
| _ ⇒ None
end.
Function release_lock_TCB_spec (index: Z) (adt: RData) :=
let abid := (index + ID_AT_range) in
let cpu := CPU_ID adt in
match (ikern adt, ihost adt, pg adt) with
| (true, true, true) ⇒
if zle_lt 0 index num_chan then
match ZMap.get abid (multi_log adt), ZMap.get abid (lock adt) with
| MultiDef l, LockOwn true ⇒
let l´ := (TEVENT cpu (TTICKET REL_LOCK)):: (TEVENT cpu (TSHARED (OTCBE (tcb adt) (tdq adt)))) :: l in
match H_CalLock l´ with
| Some _ ⇒
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
{lock: ZMap.set abid LockFalse (lock adt)})
| _ ⇒ None
end
| _,_ ⇒ None
end
else None
| _ ⇒ None
end.
Function release_lock_ABTCB_spec (index: Z) (adt: RData) :=
let abid := (index + ID_AT_range) in
let cpu := CPU_ID adt in
match (ikern adt, ihost adt, pg adt) with
| (true, true, true) ⇒
if zle_lt 0 index num_chan then
match ZMap.get abid (multi_log adt), ZMap.get abid (lock adt) with
| MultiDef l, LockOwn true ⇒
let l´ := (TEVENT cpu (TTICKET REL_LOCK)):: (TEVENT cpu (TSHARED (OABTCBE (abtcb adt) (abq adt)))) :: l in
match H_CalLock l´ with
| Some _ ⇒
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
{lock: ZMap.set abid LockFalse (lock adt)})
| _ ⇒ None
end
| _,_ ⇒ None
end
else None
| _ ⇒ None
end.
Function release_lock_SC_spec (index:Z) (adt: RData) :=
let abid := (index + lock_TCB_range) in
let cpu := CPU_ID adt in
match (ikern adt, ihost adt, pg adt) with
| (true, true, true) ⇒
if zle_lt 0 index num_chan then
match ZMap.get abid (multi_log adt), ZMap.get abid (lock adt) with
| MultiDef l, LockOwn true ⇒
let e := TSHARED (OSCE (syncchpool adt)) in
let l´ := (TEVENT cpu (TTICKET REL_LOCK)):: (TEVENT cpu e) :: l in
match H_CalLock l´ with
| Some _ ⇒
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
{lock: ZMap.set abid LockFalse (lock adt)})
| _ ⇒ None
end
| _,_ ⇒ None
end
else None
| _ ⇒ None
end.
End RELEASE_LOCK.
End MULTIPROCESSOR.
Notation acquire_shared1_spec0 := (acquire_shared1_spec Shared2ID0).
Notation acquire_shared1_mcs_spec0 := (acquire_shared1_mcs_spec Shared2ID0).
Notation acquire_shared_spec0 := (acquire_shared_spec Shared2ID0).
Notation acquire_shared_spec1 := (acquire_shared_spec Shared2ID1).
Notation acquire_shared_spec2 := (acquire_shared_spec Shared2ID2).
Notation release_shared1_spec0 := (release_shared1_spec Shared2ID0).
Notation release_shared1_mcs_spec0 := (release_shared1_mcs_spec Shared2ID0).
Notation release_shared_spec0 := (release_shared_spec Shared2ID0).
Notation release_shared_spec1 := (release_shared_spec Shared2ID1).
Notation release_shared_spec2 := (release_shared_spec Shared2ID2).
Notation acquire_lock_spec0 := (acquire_lock_spec Shared2ID0).
Notation acquire_lock_spec1 := (acquire_lock_spec Shared2ID1).
Notation acquire_lock_spec2 := (acquire_lock_spec Shared2ID2).
Notation release_lock_spec0 := (release_lock_spec Shared2ID0).
Notation release_lock_spec1 := (release_lock_spec Shared2ID1).
Notation release_lock_spec2 := (release_lock_spec Shared2ID2).
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 MULTI_SIM.
Context {re1: relate_impl_iflags}.
Context {mt1: match_impl_lock}.
Context {re2: relate_impl_lock}.
Context {re400: relate_impl_CPU_ID}.
Section MEMINIT_SIM.
Context `{real_params: RealParams}.
Context {re200: relate_impl_init}.
Context {re5: relate_impl_MM}.
Context {re6: relate_impl_vmxinfo}.
Context {re20: relate_impl_multi_log}.
Context {re7: relate_impl_ioapic}.
Context {re8: relate_impl_lapic}.
Context {re9: relate_impl_in_intr}.
Lemma ticket_lock_init0_exist:
∀ s habd habd´ labd i f,
ticket_lock_init0_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, ticket_lock_init0_spec i labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ticket_lock_init0_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_lock_eq; eauto; intros.
exploit relate_impl_ioapic_eq; eauto; inversion 1.
exploit relate_impl_lapic_eq; eauto; inversion 1.
exploit relate_impl_in_intr_eq; eauto; inversion 1.
exploit relate_impl_multi_log_eq; eauto; intros.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
apply relate_impl_lock_update.
apply relate_impl_multi_log_update.
apply relate_impl_init_update.
apply relate_impl_vmxinfo_update.
apply relate_impl_MMSize_update.
apply relate_impl_MM_update.
apply relate_impl_ioapic_update.
apply relate_impl_lapic_update.
apply relate_impl_ioapic_update.
assumption.
Qed.
Context {mt10: match_impl_init}.
Context {mt4: match_impl_MM}.
Context {mt5: match_impl_vmxinfo}.
Context {mt50: match_impl_multi_log}.
Context {mt6: match_impl_ioapic}.
Context {mt7: match_impl_lapic}.
Lemma ticket_lock_init0_match:
∀ s d d´ m i f,
ticket_lock_init0_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ticket_lock_init0_spec; intros. subdestruct. inv H.
eapply match_impl_lock_update.
eapply match_impl_multi_log_update.
eapply match_impl_init_update.
eapply match_impl_vmxinfo_update.
eapply match_impl_MMSize_update.
eapply match_impl_MM_update.
eapply match_impl_ioapic_update.
eapply match_impl_lapic_update.
eapply match_impl_ioapic_update.
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) ticket_lock_init0_spec}.
Context {inv0: PreservesInvariants (HD:= data0) ticket_lock_init0_spec}.
Lemma ticket_lock_init0_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem ticket_lock_init0_spec)
(id ↦ gensem ticket_lock_init0_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit ticket_lock_init0_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply ticket_lock_init0_match; eauto.
Qed.
End MEMINIT_SIM.
Section REALSE_SIM.
Context `{valid_arg: Z → option positive}.
Context {re20: relate_impl_multi_log}.
Lemma release_shared_exist:
∀ s i ofs e habd habd´ labd f,
release_shared_spec valid_arg i ofs e habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, release_shared_spec valid_arg i ofs e labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold release_shared_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_multi_log_eq; eauto. intros.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_lock_update.
eapply relate_impl_multi_log_update. assumption.
Qed.
Context {mt50: match_impl_multi_log}.
Lemma release_shared_match:
∀ s i ofs e d d´ m f,
release_shared_spec valid_arg i ofs e d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold release_shared_spec; intros. subdestruct.
inv H.
eapply match_impl_lock_update.
eapply match_impl_multi_log_update.
assumption.
Qed.
Context {inv: ReleaseInvariants (data_ops:= data_ops) (release_shared_spec valid_arg)}.
Context {inv0: ReleaseInvariants (data_ops:= data_ops0) (release_shared_spec valid_arg)}.
Local Open Scope Z_scope.
Lemma release_shared_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_release_lock_compatsem id (release_shared_spec valid_arg))
(id ↦ primcall_release_lock_compatsem id (release_shared_spec valid_arg)).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit release_shared_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_shared_match; eauto.
+ subst rs´. val_inject_simpl.
Qed.
End REALSE_SIM.
Section RELEASE_LOCK_SC_SIM.
Context {re3: relate_impl_multi_oracle}.
Context {re30: relate_impl_multi_log}.
Context {mt2: match_impl_multi_log}.
Context `{waittime: WaitTime}.
Context {re4: relate_impl_syncchpool}.
Lemma release_lock_SC_exist:
∀ s n habd habd´ labd f,
release_lock_SC_spec n habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, release_lock_SC_spec n labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold release_lock_SC_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_lock_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_syncchpool_eq; eauto. intros.
revert H; subrewrite. subdestruct; inv HQ.
refine_split´; trivial.
eapply relate_impl_lock_update.
eapply relate_impl_multi_log_update.
assumption.
Qed.
Context {mt3: match_impl_syncchpool}.
Lemma release_lock_SC_match:
∀ s n d d´ m f,
release_lock_SC_spec n d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold release_lock_SC_spec; intros. subdestruct; inv H.
eapply match_impl_lock_update.
eapply match_impl_multi_log_update.
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) release_lock_SC_spec}.
Context {inv0: PreservesInvariants (HD:= data0) release_lock_SC_spec}.
Lemma release_lock_SC_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem release_lock_SC_spec)
(id ↦ gensem release_lock_SC_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit release_lock_SC_exist; eauto 1. intros [labd´ [HP HM]].
match_external_states_simpl.
eapply release_lock_SC_match; eauto.
Qed.
End RELEASE_LOCK_SC_SIM.
Section ACQUIRE_SHARED_SIM.
Context `{valid_arg: Z → option positive}.
Context {re3: relate_impl_multi_oracle}.
Context {re3001: relate_impl_multi_log}.
Context {mt2001: match_impl_multi_log}.
Context `{waittime: WaitTime}.
Lemma acquire_shared_exist:
∀ s index ofs habd habd´ labd f p l,
acquire_shared_spec valid_arg index ofs habd = Some (habd´, p, l)
→ relate_AbData s f habd labd
→ (∃ labd´, acquire_shared_spec valid_arg index ofs labd = Some (labd´, p, l) ∧
relate_AbData s f habd´ labd´)
∧ valid_arg index = Some p.
Proof.
unfold acquire_shared_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_lock_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H; subrewrite. subdestruct.
- inv HQ. refine_split´; trivial.
eapply relate_impl_lock_update; eauto.
eapply relate_impl_multi_log_update; eauto.
Qed.
Lemma acquire_shared_match:
∀ s index ofs d d´ m f p l,
acquire_shared_spec valid_arg index ofs d = Some (d´, p, l)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold acquire_shared_spec; intros. subdestruct.
- inv H.
eapply match_impl_lock_update; eauto.
eapply match_impl_multi_log_update; eauto.
Qed.
Context {inv: SAcquireInvariants (data_ops:= data_ops) (acquire_shared_spec valid_arg)}.
Context {inv0: SAcquireInvariants (data_ops:= data_ops0) (acquire_shared_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_shared_sim:
∀
(HMatch:
∀ i,
In i new_glbl → valid_id i = false)
id,
sim (crel RData RData)
(id ↦ primcall_acquire_shared_compatsem (acquire_shared_spec valid_arg))
(id ↦ primcall_acquire_shared_compatsem (acquire_shared_spec valid_arg)).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit acquire_shared_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_shared_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_shared_match; eauto.
-
subst rs´. val_inject_simpl.
}
Qed.
End ACQUIRE_SHARED_SIM.
Section REALSE_LOCK_SIM.
Context {re500: relate_impl_multi_log}.
Context {mt100: match_impl_multi_log}.
Context `{valid_arg: Z → option positive}.
Context `{valid_arg´: Z → option positive}.
Context `{valid_arg_imply:
∀ i id,
valid_arg i = Some id →
valid_arg´ i = Some id}.
Lemma release_lock_exist:
∀ s i ofs e habd habd´ labd f,
release_lock_spec valid_arg i ofs e habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, release_lock_spec valid_arg´ i ofs e labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold release_lock_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_multi_log_eq; eauto. intros.
specialize (valid_arg_imply i).
revert H; subrewrite.
subdestruct; rewrite (valid_arg_imply _ eq_refl); inv HQ; refine_split´; trivial;
try eapply relate_impl_lock_update;
try eapply relate_impl_multi_log_update;
trivial.
Qed.
Lemma release_lock_match:
∀ s i ofs e d d´ m f,
release_lock_spec valid_arg i ofs e d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold release_lock_spec; intros.
subdestruct; inv H; try eapply match_impl_lock_update;
try eapply match_impl_multi_log_update; trivial.
Qed.
Local Open Scope Z_scope.
Context {inv: ReleaseInvariants (data_ops:= data_ops) (release_lock_spec valid_arg)}.
Context {inv0: ReleaseInvariants (data_ops:= data_ops0) (release_lock_spec valid_arg´)}.
Lemma release_lock_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_release_lock_compatsem id (release_lock_spec valid_arg))
(id ↦ primcall_release_lock_compatsem id (release_lock_spec valid_arg´)).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit release_lock_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_lock_match; eauto.
+ subst rs´. val_inject_simpl.
Qed.
End REALSE_LOCK_SIM.
Section REALSE_LOCK_AT_SIM.
Context {re500: relate_impl_multi_log}.
Context {mt100: match_impl_multi_log}.
Context {re4: relate_impl_AT}.
Lemma release_lock_AT_exist:
∀ s habd habd´ labd f,
release_lock_AT_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, release_lock_AT_spec labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold release_lock_AT_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_multi_log_eq; eauto. intros.
exploit relate_impl_AT_eq; eauto. intros.
revert H; subrewrite.
subdestruct; inv HQ; refine_split´; trivial.
eapply relate_impl_lock_update.
eapply relate_impl_multi_log_update.
trivial.
Qed.
Lemma release_lock_AT_match:
∀ s d d´ m f,
release_lock_AT_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold release_lock_AT_spec; intros.
subdestruct; inv H; try eapply match_impl_lock_update;
try eapply match_impl_multi_log_update; trivial.
Qed.
Local Open Scope Z_scope.
Context {inv: PreservesInvariants (HD:= data) release_lock_AT_spec}.
Context {inv0: PreservesInvariants (HD:= data0) release_lock_AT_spec}.
Lemma release_lock_AT_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem release_lock_AT_spec)
(id ↦ gensem release_lock_AT_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit release_lock_AT_exist; eauto 1. intros [labd´ [HP HM]].
match_external_states_simpl.
eapply release_lock_AT_match; eauto.
Qed.
End REALSE_LOCK_AT_SIM.
Section REALSE_LOCK_TCB_SIM.
Context {re500: relate_impl_multi_log}.
Context {mt100: match_impl_multi_log}.
Context {re4: relate_impl_tcb}.
Context {re5: relate_impl_tdq}.
Lemma release_lock_TCB_exist:
∀ s habd habd´ labd i f,
release_lock_TCB_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, release_lock_TCB_spec i labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold release_lock_TCB_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_multi_log_eq; eauto. intros.
exploit relate_impl_tcb_eq; eauto. intros.
exploit relate_impl_tdq_eq; eauto. intros.
revert H; subrewrite.
subdestruct; inv HQ; refine_split´; trivial.
eapply relate_impl_lock_update.
eapply relate_impl_multi_log_update.
trivial.
Qed.
Lemma release_lock_TCB_match:
∀ s d d´ i m f,
release_lock_TCB_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold release_lock_TCB_spec; intros.
subdestruct; inv H; try eapply match_impl_lock_update;
try eapply match_impl_multi_log_update; trivial.
Qed.
Local Open Scope Z_scope.
Context {inv: PreservesInvariants (HD:= data) release_lock_TCB_spec}.
Context {inv0: PreservesInvariants (HD:= data0) release_lock_TCB_spec}.
Lemma release_lock_TCB_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem release_lock_TCB_spec)
(id ↦ gensem release_lock_TCB_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit release_lock_TCB_exist; eauto 1. intros [labd´ [HP HM]].
match_external_states_simpl.
eapply release_lock_TCB_match; eauto.
Qed.
End REALSE_LOCK_TCB_SIM.
Section REALSE_LOCK_ABTCB_SIM.
Context {re500: relate_impl_multi_log}.
Context {mt100: match_impl_multi_log}.
Context {re4: relate_impl_abtcb}.
Context {re5: relate_impl_abq}.
Lemma release_lock_ABTCB_exist:
∀ s habd habd´ labd i f,
release_lock_ABTCB_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, release_lock_ABTCB_spec i labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold release_lock_ABTCB_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_multi_log_eq; eauto. intros.
exploit relate_impl_abtcb_eq; eauto. intros.
exploit relate_impl_abq_eq; eauto. intros.
revert H; subrewrite.
subdestruct; inv HQ; refine_split´; trivial.
eapply relate_impl_lock_update.
eapply relate_impl_multi_log_update.
trivial.
Qed.
Lemma release_lock_ABTCB_match:
∀ s d d´ i m f,
release_lock_ABTCB_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold release_lock_ABTCB_spec; intros.
subdestruct; inv H; try eapply match_impl_lock_update;
try eapply match_impl_multi_log_update; trivial.
Qed.
Local Open Scope Z_scope.
Context {inv: PreservesInvariants (HD:= data) release_lock_ABTCB_spec}.
Context {inv0: PreservesInvariants (HD:= data0) release_lock_ABTCB_spec}.
Lemma release_lock_ABTCB_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem release_lock_ABTCB_spec)
(id ↦ gensem release_lock_ABTCB_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit release_lock_ABTCB_exist; eauto 1. intros [labd´ [HP HM]].
match_external_states_simpl.
eapply release_lock_ABTCB_match; eauto.
Qed.
End REALSE_LOCK_ABTCB_SIM.
Section ACQUIRE_SIM.
Context {re3: relate_impl_multi_oracle}.
Context {re30: relate_impl_multi_log}.
Context {mt2: match_impl_multi_log}.
Context `{waittime: WaitTime}.
Context `{valid_arg: Z → option positive}.
Context `{valid_arg´: Z → option positive}.
Context `{valid_arg_imply:
∀ i id,
valid_arg i = Some id →
valid_arg´ i = Some id}.
Lemma acquire_lock_exist:
∀ s bound i ofs habd habd´ labd f p l,
acquire_lock_spec valid_arg bound i ofs habd = Some (habd´, p, l)
→ relate_AbData s f habd labd
→ (∃ labd´, acquire_lock_spec valid_arg´ bound i ofs labd = Some (labd´, p, l) ∧
relate_AbData s f habd´ labd´)
∧ valid_arg i = Some p.
Proof.
unfold acquire_lock_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_lock_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
specialize (valid_arg_imply i).
revert H; subrewrite.
subdestruct; rewrite (valid_arg_imply _ eq_refl); inv HQ; refine_split´; trivial;
eapply relate_impl_lock_update;
eapply relate_impl_multi_log_update;
trivial.
Qed.
Lemma acquire_lock_match:
∀ s bound i ofs d d´ m f p l,
acquire_lock_spec valid_arg bound i ofs d = Some (d´, p, l)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold acquire_lock_spec; intros.
subdestruct; inv H;
eapply match_impl_lock_update;
eapply match_impl_multi_log_update;
trivial.
Qed.
Context {inv: AcquireInvariants (data_ops:= data_ops) (acquire_lock_spec valid_arg)}.
Context {inv0: AcquireInvariants (data_ops:= data_ops0) (acquire_lock_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_lock_sim:
∀
(HMatch:
∀ i,
In i new_glbl → valid_id i = false)
id,
sim (crel RData RData)
(id ↦ primcall_acquire_lock_compatsem (acquire_lock_spec valid_arg))
(id ↦ primcall_acquire_lock_compatsem (acquire_lock_spec valid_arg´)).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit acquire_lock_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_lock_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_lock_match; eauto.
-
subst rs´. val_inject_simpl.
}
Qed.
End ACQUIRE_SIM.
Section ACQUIRE_SIM0.
Context {re3: relate_impl_multi_oracle}.
Context {re30: relate_impl_multi_log}.
Context {mt2: match_impl_multi_log}.
Context `{waittime: WaitTime}.
Context {inv: AcquireInvariants (data_ops:= data_ops) acquire_lock_spec0}.
Context {inv0: AcquireInvariants (data_ops:= data_ops0) acquire_lock_spec0}.
Lemma Shared2ID0_imply:
∀ i id,
Shared2ID0 i = Some id → Shared2ID0 i = Some id.
Proof.
auto.
Qed.
Lemma acquire_lock_sim0:
∀
(HMatch:
∀ i,
In i new_glbl → CheckID0 i = false)
id,
sim (crel RData RData)
(id ↦ primcall_acquire_lock_compatsem acquire_lock_spec0)
(id ↦ primcall_acquire_lock_compatsem acquire_lock_spec0).
Proof.
eapply (acquire_lock_sim (valid_id_args:= Shared2ID_valid0) (valid_arg_imply:= Shared2ID0_imply)).
Qed.
End ACQUIRE_SIM0.
Section ACQUIRE_SIM1.
Context {re3: relate_impl_multi_oracle}.
Context {re30: relate_impl_multi_log}.
Context {mt2: match_impl_multi_log}.
Context `{waittime: WaitTime}.
Context {inv: AcquireInvariants (data_ops:= data_ops) acquire_lock_spec1}.
Context {inv0: AcquireInvariants (data_ops:= data_ops0) acquire_lock_spec1}.
Lemma Shared2ID1_imply:
∀ i id,
Shared2ID1 i = Some id → Shared2ID1 i = Some id.
Proof.
auto.
Qed.
Lemma acquire_lock_sim1:
∀
(HMatch:
∀ i,
In i new_glbl → CheckID1 i = false)
id,
sim (crel RData RData)
(id ↦ primcall_acquire_lock_compatsem acquire_lock_spec1)
(id ↦ primcall_acquire_lock_compatsem acquire_lock_spec1).
Proof.
eapply (acquire_lock_sim (valid_id_args:= Shared2ID_valid1) (valid_arg_imply:= Shared2ID1_imply)).
Qed.
End ACQUIRE_SIM1.
Section ACQUIRE_SIM2.
Context {re3: relate_impl_multi_oracle}.
Context {re30: relate_impl_multi_log}.
Context {mt2: match_impl_multi_log}.
Context `{waittime: WaitTime}.
Context {inv: AcquireInvariants (data_ops:= data_ops) acquire_lock_spec2}.
Context {inv0: AcquireInvariants (data_ops:= data_ops0) acquire_lock_spec2}.
Lemma Shared2ID2_imply:
∀ i id,
Shared2ID2 i = Some id → Shared2ID2 i = Some id.
Proof.
auto.
Qed.
Lemma acquire_lock_sim2:
∀
(HMatch:
∀ i,
In i new_glbl → CheckID2 i = false)
id,
sim (crel RData RData)
(id ↦ primcall_acquire_lock_compatsem acquire_lock_spec2)
(id ↦ primcall_acquire_lock_compatsem acquire_lock_spec2).
Proof.
eapply (acquire_lock_sim (valid_id_args:= Shared2ID_valid2) (valid_arg_imply:= Shared2ID2_imply)).
Qed.
End ACQUIRE_SIM2.
Section ACQUIRE_AT_SIM.
Context {re3: relate_impl_multi_oracle}.
Context {re30: relate_impl_multi_log}.
Context {mt2: match_impl_multi_log}.
Context `{waittime: WaitTime}.
Context {re4: relate_impl_AT}.
Lemma acquire_lock_AT_exist:
∀ s habd habd´ labd f,
acquire_lock_AT_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, acquire_lock_AT_spec labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold acquire_lock_AT_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_lock_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H; subrewrite.
subdestruct; inv HQ.
- refine_split´; trivial.
eapply relate_impl_AT_update.
eapply relate_impl_lock_update.
eapply relate_impl_multi_log_update.
assumption.
- refine_split´; trivial.
eapply relate_impl_lock_update.
eapply relate_impl_multi_log_update.
assumption.
Qed.
Context {mt3: match_impl_AT}.
Lemma acquire_lock_AT_match:
∀ s d d´ m f,
acquire_lock_AT_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold acquire_lock_AT_spec; intros.
subdestruct; inv H.
- eapply match_impl_AT_update.
eapply match_impl_lock_update.
eapply match_impl_multi_log_update.
assumption.
- eapply match_impl_lock_update.
eapply match_impl_multi_log_update.
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) acquire_lock_AT_spec}.
Context {inv0: PreservesInvariants (HD:= data0) acquire_lock_AT_spec}.
Lemma acquire_lock_AT_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem acquire_lock_AT_spec)
(id ↦ gensem acquire_lock_AT_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit acquire_lock_AT_exist; eauto 1. intros [labd´ [HP HM]].
match_external_states_simpl.
eapply acquire_lock_AT_match; eauto.
Qed.
End ACQUIRE_AT_SIM.
Section ACQUIRE_TCB_SIM.
Context {re3: relate_impl_multi_oracle}.
Context {re30: relate_impl_multi_log}.
Context {mt2: match_impl_multi_log}.
Context `{waittime: WaitTime}.
Context {re4: relate_impl_tcb}.
Context {re40: relate_impl_tdq}.
Lemma acquire_lock_TCB_exist:
∀ s n habd habd´ labd f,
acquire_lock_TCB_spec n habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, acquire_lock_TCB_spec n labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold acquire_lock_TCB_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_lock_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H; subrewrite.
subdestruct; inv HQ.
- refine_split´; trivial.
eapply relate_impl_tdq_update.
eapply relate_impl_tcb_update.
eapply relate_impl_lock_update.
eapply relate_impl_multi_log_update.
assumption.
- refine_split´; trivial.
eapply relate_impl_lock_update.
eapply relate_impl_multi_log_update.
assumption.
Qed.
Context {mt3: match_impl_tcb}.
Context {mt30: match_impl_tdq}.
Lemma acquire_lock_TCB_match:
∀ s n d d´ m f,
acquire_lock_TCB_spec n d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold acquire_lock_TCB_spec; intros.
subdestruct; inv H.
- eapply match_impl_tdq_update.
eapply match_impl_tcb_update.
eapply match_impl_lock_update.
eapply match_impl_multi_log_update.
assumption.
- eapply match_impl_lock_update.
eapply match_impl_multi_log_update.
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) acquire_lock_TCB_spec}.
Context {inv0: PreservesInvariants (HD:= data0) acquire_lock_TCB_spec}.
Lemma acquire_lock_TCB_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem acquire_lock_TCB_spec)
(id ↦ gensem acquire_lock_TCB_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit acquire_lock_TCB_exist; eauto 1. intros [labd´ [HP HM]].
match_external_states_simpl.
eapply acquire_lock_TCB_match; eauto.
Qed.
End ACQUIRE_TCB_SIM.
Section ACQUIRE_ABTCB_SIM.
Context {re3: relate_impl_multi_oracle}.
Context {re30: relate_impl_multi_log}.
Context {mt2: match_impl_multi_log}.
Context `{waittime: WaitTime}.
Context {re4: relate_impl_abtcb}.
Context {re40: relate_impl_abq}.
Lemma acquire_lock_ABTCB_exist:
∀ s n habd habd´ labd f,
acquire_lock_ABTCB_spec n habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, acquire_lock_ABTCB_spec n labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold acquire_lock_ABTCB_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_lock_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H; subrewrite.
subdestruct; inv HQ.
- refine_split´; trivial.
eapply relate_impl_abq_update.
eapply relate_impl_abtcb_update.
eapply relate_impl_lock_update.
eapply relate_impl_multi_log_update.
assumption.
- refine_split´; trivial.
eapply relate_impl_lock_update.
eapply relate_impl_multi_log_update.
assumption.
Qed.
Context {mt3: match_impl_abtcb}.
Context {mt30: match_impl_abq}.
Lemma acquire_lock_ABTCB_match:
∀ s n d d´ m f,
acquire_lock_ABTCB_spec n d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold acquire_lock_ABTCB_spec; intros.
subdestruct; inv H.
- eapply match_impl_abq_update.
eapply match_impl_abtcb_update.
eapply match_impl_lock_update.
eapply match_impl_multi_log_update.
assumption.
- eapply match_impl_lock_update.
eapply match_impl_multi_log_update.
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) acquire_lock_ABTCB_spec}.
Context {inv0: PreservesInvariants (HD:= data0) acquire_lock_ABTCB_spec}.
Lemma acquire_lock_ABTCB_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem acquire_lock_ABTCB_spec)
(id ↦ gensem acquire_lock_ABTCB_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit acquire_lock_ABTCB_exist; eauto 1. intros [labd´ [HP HM]].
match_external_states_simpl.
eapply acquire_lock_ABTCB_match; eauto.
Qed.
End ACQUIRE_ABTCB_SIM.
Section ACQUIRE_chan_SIM.
Context {re3: relate_impl_multi_oracle}.
Context {re30: relate_impl_multi_log}.
Context {mt2: match_impl_multi_log}.
Context `{waittime: WaitTime}.
Context {re4: relate_impl_syncchpool}.
Lemma acquire_lock_SC_exist:
∀ s n habd habd´ labd f,
acquire_lock_SC_spec n habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, acquire_lock_SC_spec n labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold acquire_lock_SC_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_lock_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H; subrewrite. subdestruct; inv HQ.
- refine_split´; trivial.
eapply relate_impl_syncchpool_update.
eapply relate_impl_lock_update.
eapply relate_impl_multi_log_update.
assumption.
- refine_split´; trivial.
eapply relate_impl_lock_update.
eapply relate_impl_multi_log_update.
assumption.
Qed.
Context {mt3: match_impl_syncchpool}.
Lemma acquire_lock_SC_match:
∀ s n d d´ m f,
acquire_lock_SC_spec n d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold acquire_lock_SC_spec; intros. subdestruct; inv H.
- eapply match_impl_syncchpool_update.
eapply match_impl_lock_update.
eapply match_impl_multi_log_update.
assumption.
- eapply match_impl_lock_update.
eapply match_impl_multi_log_update.
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) acquire_lock_SC_spec}.
Context {inv0: PreservesInvariants (HD:= data0) acquire_lock_SC_spec}.
Lemma acquire_lock_SC_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem acquire_lock_SC_spec)
(id ↦ gensem acquire_lock_SC_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit acquire_lock_SC_exist; eauto 1. intros [labd´ [HP HM]].
match_external_states_simpl.
eapply acquire_lock_SC_match; eauto.
Qed.
End ACQUIRE_chan_SIM.
End MULTI_SIM.
End OBJ_SIM.