Library mcertikos.mcslock.ObjMCSLock
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 Import GlobIdent.
Require Import RealParams.
Require Import CommonTactic.
Require Import DeviceStateDataType.
Require Import ObjInterruptDriver.
Require Import CalMCSLock.
Require Import CalTicketLock.
Require Export MCSSemantics.
Section MCS_SPECS.
Section MCS_INIT_PRIM.
Definition mcs_init_node_log_spec (abid:Z) (adt: RData) : option RData :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 abid lock_range
then Some adt {multi_log: ZMap.set abid (MultiDef nil) (multi_log adt)}
else None
| _ ⇒ None
end.
Function mcs_init_node_spec (abid: Z) (adt: RData) : option RData :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 abid lock_range
then Some adt {multi_log: ZMap.set abid (MultiDef nil) (multi_log adt)}
else None
| _ ⇒ None
end.
End MCS_INIT_PRIM.
Section MCS_ATOMIC_PRIM.
Definition atomic_mcs_log_spec (abid cpuid: Z) (adt: RData) :
option (RData × Z × (Z × Z × Z × Z × Z × Z × Z × Z) × (Z × Z × Z × Z × Z × Z × Z × Z)) :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 abid lock_range then
if zle_lt 0 cpuid TOTAL_CPU then
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
let to := ZMap.get abid (multi_oracle adt) in
let l´ := (to cpuid l) ++ l in
match CalMCSLock l´ with
| Some (MCSLOCK la np _) ⇒
let (b0, ne0) := ZMap.get 0 np in
let (b1, ne1) := ZMap.get 1 np in
let (b2, ne2) := ZMap.get 2 np in
let (b3, ne3) := ZMap.get 3 np in
let (b4, ne4) := ZMap.get 4 np in
let (b5, ne5) := ZMap.get 5 np in
let (b6, ne6) := ZMap.get 6 np in
let (b7, ne7) := ZMap.get 7 np in
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)},
la, (BooltoZ b0, BooltoZ b1, BooltoZ b2, BooltoZ b3,
BooltoZ b4, BooltoZ b5, BooltoZ b6, BooltoZ b7),
(ne0, ne1, ne2, ne3, ne4, ne5, ne6, ne7))
| _ ⇒ None
end
| _ ⇒ None
end
else None
else None
| _ ⇒ None
end.
Function atomic_mcs_SWAP_spec (bound abid cpuid: Z) (adt: RData) : option (RData × Z) :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 abid lock_range then
if zle_lt 0 cpuid TOTAL_CPU then
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
match CalMCSLock l with
| Some (MCSLOCK prev_last _ _) ⇒
if zle_le 0 prev_last TOTAL_CPU
then if zeq prev_last NULL
then let l´ := (TEVENT cpuid (TTICKET (SWAP_TAIL (nat_of_Z bound) true))) :: l in
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}, prev_last)
else let l´ := (TEVENT cpuid (TTICKET (SWAP_TAIL (nat_of_Z bound) false))) :: l in
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}, prev_last)
else None
| None ⇒ None
end
| _ ⇒ None
end
else None
else None
| _ ⇒ None
end.
Function atomic_mcs_CAS_spec (abid cpuid: Z) (adt: RData) : option (RData × (Z × Z)) :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 abid lock_range then
if zle_lt 0 cpuid TOTAL_CPU then
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
match CalMCSLock l with
| Some (MCSLOCK la _ _) ⇒
if (zeq la cpuid)
then Some (adt {multi_log: ZMap.set
abid (MultiDef ((TEVENT cpuid (TTICKET (CAS_TAIL true)))::l))
(multi_log adt)}, (NULL, 1))
else Some (adt {multi_log: ZMap.set
abid (MultiDef ((TEVENT cpuid (TTICKET (CAS_TAIL false)))::l))
(multi_log adt)}, (la, 0))
| _ ⇒ None
end
| _ ⇒ None
end
else None
else None
| _ ⇒ None
end.
End MCS_ATOMIC_PRIM.
Section MCS_INTRO_LOW_LOG_PRIM.
Function mcs_GET_NEXT_log_spec (abid cpuid: Z) (adt: RData) : option RData :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 abid lock_range then
if zle_lt 0 cpuid TOTAL_CPU then
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
let l´ := (TEVENT cpuid (TTICKET (GET_NEXT))) :: l in
Some adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
| _ ⇒ None
end
else None
else None
| _ ⇒ None
end.
Function mcs_SET_NEXT_log_spec (abid cpuid prev_id: Z) (adt:RData) : option RData :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 abid lock_range then
if zle_lt 0 cpuid TOTAL_CPU then
if zle_lt 0 prev_id TOTAL_CPU then
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
let l´ := (TEVENT cpuid (TTICKET (SET_NEXT prev_id))) :: l in
Some adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
| _ ⇒ None
end
else None
else None
else None
| _ ⇒ None
end.
Function mcs_GET_BUSY_log_spec (abid cpuid: Z) (adt: RData) : option RData :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 abid lock_range then
if zle_lt 0 cpuid TOTAL_CPU then
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
match CalMCSLock l with
| Some (MCSLOCK _ np _) ⇒
match ZMap.get cpuid np with
(is_busy, _) ⇒
let l´ := (TEVENT cpuid (TTICKET (GET_BUSY is_busy))) :: l in
Some adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
end
| _ ⇒ None
end
| _ ⇒ None
end
else None
else None
| _ ⇒ None
end.
Function mcs_SET_BUSY_log_spec (abid cpuid: Z) (adt: RData) : option RData :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 abid lock_range then
if zle_lt 0 cpuid TOTAL_CPU then
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
match CalMCSLock l with
| Some (MCSLOCK _ np _) ⇒
match ZMap.get cpuid np with
(_, next) ⇒
if zle_lt 0 next TOTAL_CPU
then let l´ := (TEVENT cpuid (TTICKET (SET_BUSY))) :: l in
Some adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
else None
end
| _ ⇒ None
end
| _ ⇒ None
end
else None
else None
| _ ⇒ None
end.
End MCS_INTRO_LOW_LOG_PRIM.
Section MCS_INTRO_LOW_PRIM.
Function mcs_SWAP_TAIL_spec (bound abid cpuid: Z) (adt: RData) : option (RData × Z) :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 abid lock_range then
if zle_lt 0 cpuid TOTAL_CPU then
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
match CalMCSLock l with
| Some (MCSLOCK prev_last _ _) ⇒
if zle_le 0 prev_last TOTAL_CPU
then if zeq prev_last NULL
then let l´ := (TEVENT cpuid (TTICKET (SWAP_TAIL (nat_of_Z bound) true))) :: l in
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}, prev_last)
else let l´ := (TEVENT cpuid (TTICKET (SWAP_TAIL (nat_of_Z bound) false))) :: l in
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}, prev_last)
else None
| None ⇒ None
end
| _ ⇒ None
end
else None
else None
| _ ⇒ None
end.
Function mcs_CAS_TAIL_spec (abid cpuid: Z) (adt: RData) : option (RData × Z) :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 abid lock_range then
if zle_lt 0 cpuid TOTAL_CPU then
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
match CalMCSLock l with
| Some (MCSLOCK la _ _) ⇒
if (zeq la cpuid)
then Some (adt {multi_log: ZMap.set abid (MultiDef ((TEVENT cpuid (TTICKET (CAS_TAIL true)))::l))
(multi_log adt)}, 1)
else Some (adt {multi_log: ZMap.set abid (MultiDef ((TEVENT cpuid (TTICKET (CAS_TAIL false)))::l))
(multi_log adt)}, 0)
| _ ⇒ None
end
| _ ⇒ None
end
else None
else None
| _ ⇒ None
end.
Function mcs_GET_NEXT_spec (abid cpuid: Z) (adt: RData) : option (RData × Z) :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 abid lock_range then
if zle_lt 0 cpuid TOTAL_CPU then
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
let l´ := (TEVENT cpuid (TTICKET (GET_NEXT))) :: l in
match CalMCSLock l´ with
| Some (MCSLOCK _ node_pool _) ⇒
match (ZMap.get cpuid node_pool) with
| (_, next_id) ⇒ Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}, next_id)
end
| _ ⇒ None
end
| _ ⇒ None
end
else None
else None
| _ ⇒ None
end.
Function mcs_SET_NEXT_spec (abid cpuid prev_id: Z) (adt:RData) : option RData :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 abid lock_range then
if zle_lt 0 cpuid TOTAL_CPU then
if zle_lt 0 prev_id TOTAL_CPU then
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
let l´ := (TEVENT cpuid (TTICKET (SET_NEXT prev_id))) :: l in
Some adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
| _ ⇒ None
end
else None
else None
else None
| _ ⇒ None
end.
Function mcs_GET_BUSY_spec (abid cpuid: Z) (adt: RData) : option (RData × Z) :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 abid lock_range then
if zle_lt 0 cpuid TOTAL_CPU then
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
match CalMCSLock l with
| Some (MCSLOCK _ node_pool _) ⇒
match (ZMap.get cpuid node_pool) with
(is_busy, _) ⇒
if is_busy then
let l´ := (TEVENT cpuid (TTICKET (GET_BUSY is_busy))) :: l in
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}, 1)
else
let l´ := (TEVENT cpuid (TTICKET (GET_BUSY is_busy))) :: l in
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}, 0)
end
| _ ⇒ None
end
| _ ⇒ None
end
else None
else None
| _ ⇒ None
end.
Function mcs_SET_BUSY_spec (abid cpuid: Z) (adt: RData) : option RData :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 abid lock_range then
if zle_lt 0 cpuid TOTAL_CPU then
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
match CalMCSLock l with
| Some (MCSLOCK _ np _) ⇒
match ZMap.get cpuid np with
(_, next) ⇒
if zle_lt 0 next TOTAL_CPU
then let l´ := (TEVENT cpuid (TTICKET (SET_BUSY))) :: l in
Some adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
else None
end
| _ ⇒ None
end
| _ ⇒ None
end
else None
else None
| _ ⇒ None
end.
End MCS_INTRO_LOW_PRIM.
Section MCS_LOG_UPDATE_PRIM.
Definition mcs_log_spec (abid cpuid: Z) (adt: RData) : option RData :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 abid lock_range then
if zle_lt 0 cpuid TOTAL_CPU then
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
let to := ZMap.get abid (multi_oracle adt) in
let l´ := (to cpuid l) ++ l in
match CalMCSLock l´ with
| Some _ ⇒ Some adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
| _ ⇒ None
end
| _ ⇒ None
end
else None
else None
| _ ⇒ None
end.
End MCS_LOG_UPDATE_PRIM.
Section MCS_INTRO_HIGH_PRIM.
Function mcs_swap_tail_spec (bound : Z) (abid cpuid: Z) (adt: RData) : option (RData × Z) :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 abid lock_range then
if zle_lt 0 cpuid TOTAL_CPU then
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
let to := ZMap.get abid (multi_oracle adt) in
let l1 := (to cpuid l) ++ l in
match CalMCSLock l1 with
| Some (MCSLOCK prev_last _ _) ⇒
if zle_le 0 prev_last TOTAL_CPU
then if zeq prev_last NULL
then let l´ := (TEVENT cpuid (TTICKET (SWAP_TAIL (nat_of_Z bound) true))) :: l1 in
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}, prev_last)
else let l´ := (TEVENT cpuid (TTICKET (SWAP_TAIL (nat_of_Z bound) false))) :: l1 in
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}, prev_last)
else None
| None ⇒ None
end
| _ ⇒ None
end
else None
else None
| _ ⇒ None
end.
Function mcs_cas_tail_spec (abid cpuid: Z) (adt: RData) : option (RData × Z) :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 abid lock_range then
if zle_lt 0 cpuid TOTAL_CPU then
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
let to := ZMap.get abid (multi_oracle adt) in
let l1 := (to cpuid l) ++ l in
match CalMCSLock l1 with
| Some (MCSLOCK la _ _) ⇒
if (zeq la cpuid)
then Some (adt {multi_log: ZMap.set abid (MultiDef ((TEVENT cpuid (TTICKET (CAS_TAIL true)))::l1))
(multi_log adt)}, 1)
else Some (adt {multi_log: ZMap.set abid (MultiDef ((TEVENT cpuid (TTICKET (CAS_TAIL false)))::l1))
(multi_log adt)}, 0)
| None ⇒ None
end
| _ ⇒ None
end
else None
else None
| _ ⇒ None
end.
Function mcs_get_next_spec (abid cpuid: Z) (adt: RData) : option (RData × Z) :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 abid lock_range then
if zle_lt 0 cpuid TOTAL_CPU then
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
let to := ZMap.get abid (multi_oracle adt) in
let l1 := (to cpuid l) ++ l in
let l´ := (TEVENT cpuid (TTICKET (GET_NEXT))) :: l1 in
match CalMCSLock l´ with
| Some (MCSLOCK _ node_pool _) ⇒
match (ZMap.get cpuid node_pool) with
| (_, next_id) ⇒ Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}, next_id)
end
| _ ⇒ None
end
| _ ⇒ None
end
else None
else None
| _ ⇒ None
end.
Function mcs_set_next_spec (abid cpuid prev_id: Z) (adt:RData) : option RData :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 abid lock_range then
if zle_lt 0 cpuid TOTAL_CPU then
if zle_lt 0 prev_id TOTAL_CPU then
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
let to := ZMap.get abid (multi_oracle adt) in
let l1 := (to cpuid l) ++ l in
match CalMCSLock l1 with
| Some _ ⇒ let l´ := (TEVENT cpuid (TTICKET (SET_NEXT prev_id))) :: l1 in
Some adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
| _ ⇒ None
end
| _ ⇒ None
end
else None
else None
else None
| _ ⇒ None
end.
Function mcs_get_busy_spec (abid cpuid: Z) (adt: RData) : option (RData × Z) :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 abid lock_range then
if zle_lt 0 cpuid TOTAL_CPU then
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
let to := ZMap.get abid (multi_oracle adt) in
let l1 := (to cpuid l) ++ l in
match CalMCSLock l1 with
| Some (MCSLOCK _ node_pool _) ⇒
match (ZMap.get cpuid node_pool) with
(is_busy, _) ⇒
if is_busy
then let l´ := (TEVENT cpuid (TTICKET (GET_BUSY true)))::l1 in
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}, 1)
else let l´ := (TEVENT cpuid (TTICKET (GET_BUSY false)))::l1 in
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}, 0)
end
| _ ⇒ None
end
| _ ⇒ None
end
else None
else None
| _ ⇒ None
end.
Function mcs_set_busy_spec (abid cpuid: Z) (adt: RData) : option RData :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 abid lock_range then
if zle_lt 0 cpuid TOTAL_CPU then
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
let to := ZMap.get abid (multi_oracle adt) in
let l1 := (to cpuid l) ++ l in
match CalMCSLock l1 with
| Some (MCSLOCK _ np _) ⇒
match ZMap.get cpuid np with
(_, next) ⇒
if zle_lt 0 next TOTAL_CPU
then let l´ := (TEVENT cpuid (TTICKET (SET_BUSY))) :: l1 in
Some adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
else None
end
| _ ⇒ None
end
| _ ⇒ None
end
else None
else None
| _ ⇒ None
end.
Function mcs_lock_get_index_spec (index ofs: Z) (adt: RData) : option (RData × Z) :=
match (ikern adt, ihost adt, index2Z index ofs) with
| (true, true, Some abid) ⇒ Some (adt, abid)
| _ ⇒ None
end.
End MCS_INTRO_HIGH_PRIM.
Section MCS_LOCK_OP_PRIM.
Section WITHWAITTIME.
Context `{waittime: WaitTime}.
Definition mcs_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
match CalMCSLock l1 with
| Some (MCSLOCK prev_tail la tq) ⇒
if zeq prev_tail NULL
then let l2 := (TEVENT cpu (TTICKET (SWAP_TAIL (nat_of_Z bound) true))) :: l1 in
Some adt {multi_log: ZMap.set abid (MultiDef l2) (multi_log adt)}
else
let l2 := (TEVENT cpu (TTICKET (SWAP_TAIL (nat_of_Z bound) false))) :: l1 in
let l3 := (to cpu l2) ++ l2 in
let l4 := (TEVENT cpu (TTICKET (SET_NEXT prev_tail)))::l3 in
match CalMCS_AcqWait (CalWaitLockTime tq) cpu l4 to with
| Some l5 ⇒ Some adt {multi_log: ZMap.set abid (MultiDef l5) (multi_log adt)}
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
Definition mcs_pass_lock_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
let to := ZMap.get abid (multi_oracle adt) in
let l1 := (to cpu l) ++ l in
match CalMCSLock l1 with
| Some (MCSLOCK old_tail _ tq) ⇒
if zeq old_tail cpu
then
let l´ := (TEVENT cpu (TTICKET (CAS_TAIL true))) :: l1 in
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)})
else
let l2 := (TEVENT cpu (TTICKET (CAS_TAIL false))) :: l1 in
match CalMCS_RelWait CalPassLockLoopTime cpu l2 to with
| Some l3 ⇒
match CalMCSLock l3 with
| Some _ ⇒ Some (adt {multi_log: ZMap.set abid (MultiDef l3) (multi_log adt)})
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
End WITHWAITTIME.
End MCS_LOCK_OP_PRIM.
Section Q_MCS_LOCK_OP_PRIM.
Context `{waittime: WaitTime}.
Function wait_qslock_spec (bound : Z) (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), ZMap.get abid (lock adt) with
| MultiDef l, LockFalse ⇒
let cpu := CPU_ID adt in
let to := ZMap.get abid (multi_oracle adt) in
let l1 := (to cpu l) ++ l in
match QS_CalLock l1 with
| Some (_, _, nil, _,_) ⇒
let l2 := ((TEVENT cpu (TTICKET (SWAP_TAIL (nat_of_Z bound) true))) :: l1) in
Some (adt {multi_log: ZMap.set abid (MultiDef l2) (multi_log adt)}
{lock: ZMap.set abid (LockOwn false) (lock adt)})
| Some (_, _, _, q, _, tq) ⇒
let l2 := (TEVENT cpu (TTICKET (SWAP_TAIL (nat_of_Z bound) false))) :: l1 in
let l3 := (to cpu l2 ++ l2) in
let l4 := (TEVENT cpu (TTICKET (SET_NEXT (last q NULL)))) :: l3 in
match QS_CalWaitGet (CalWaitLockTime tq) cpu l4 to with
| Some l5 ⇒
Some (adt {multi_log: ZMap.set abid (MultiDef l5) (multi_log adt)}
{lock: ZMap.set abid (LockOwn false) (lock adt)})
| _ ⇒ None
end
| _ ⇒ None
end
| _,_ ⇒ None
end
| _ ⇒ None
end.
Function pass_qslock_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), ZMap.get abid (lock adt) with
| MultiDef l, LockOwn false ⇒
let cpu := CPU_ID adt in
let to := ZMap.get abid (multi_oracle adt) in
let l1 := (to cpu l) ++ l in
match QS_CalLock l1 with
| Some (self_c, S rel_c, b, q, slow,tq) ⇒
match q with
| me::nil ⇒
let l´ := (TEVENT cpu (TTICKET (CAS_TAIL true))) :: l1 in
Some (adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
{lock: ZMap.set abid LockFalse (lock adt)})
| me::j::q´ ⇒
let l2 := (TEVENT cpu (TTICKET (CAS_TAIL false))) :: l1 in
match QS_CalWaitRel CalPassLockLoopTime cpu j l2 to with
| Some l3 ⇒
let l4 := (TEVENT cpu (TTICKET GET_NEXT)) :: l3 in
let l5 := (to cpu l4) ++ l4 in
match QS_CalLock l5 with
| Some (_, _, _, nil, _, _) ⇒ None
| Some (_, _, _, q, _, _) ⇒
let l6 := (TEVENT cpu (TTICKET SET_BUSY)) :: l5 in
Some (adt {multi_log: ZMap.set abid (MultiDef l6) (multi_log adt)}
{lock: ZMap.set abid LockFalse (lock adt)})
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _,_ ⇒ None
end
| _ ⇒ None
end.
End Q_MCS_LOCK_OP_PRIM.
End MCS_SPECS.
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}.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_multi_log}.
Context {re3: relate_impl_multi_oracle}.
Context {mt1: match_impl_iflags}.
Context {mt2: match_impl_multi_log}.
Context {mt3: match_impl_multi_oracle}.
Section MCS_INIT_NODE_LOG_SIM.
Lemma mcs_init_node_log_exist:
∀ s lock_index habd habd´ labd f,
mcs_init_node_log_spec lock_index habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, mcs_init_node_log_spec lock_index labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold mcs_init_node_log_spec; intros.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_multi_log_eq; eauto; intros.
revert H; subrewrite.
subdestruct; inv HQ; refine_split´; trivial.
eapply relate_impl_multi_log_update; trivial.
Qed.
Lemma mcs_init_node_log_match:
∀ s lock_index d d´ m f,
mcs_init_node_log_spec lock_index d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold mcs_init_node_log_spec; intros.
subdestruct; inv H.
eapply match_impl_multi_log_update; assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) mcs_init_node_log_spec}.
Context {inv0: PreservesInvariants (HD:= data0) mcs_init_node_log_spec}.
Lemma mcs_init_node_log_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem mcs_init_node_log_spec)
(id ↦ gensem mcs_init_node_log_spec).
Proof.
intros.
layer_sim_simpl.
compatsim_simpl (@match_AbData).
intros.
exploit mcs_init_node_log_exist; eauto 1.
intros [labd´ [HP HM]].
match_external_states_simpl.
eapply mcs_init_node_log_match; eauto.
Qed.
End MCS_INIT_NODE_LOG_SIM.
Section MCS_INIT_NODE_SIM.
Lemma mcs_init_node_exist:
∀ s lock_index habd habd´ labd f,
mcs_init_node_spec lock_index habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, mcs_init_node_spec lock_index labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold mcs_init_node_spec; intros.
exploit relate_impl_iflags_eq; eauto; inversion 1.
exploit relate_impl_multi_log_eq; eauto; intros.
revert H; subrewrite.
subdestruct; inv HQ; refine_split´; trivial.
eapply relate_impl_multi_log_update; trivial.
Qed.
Lemma mcs_init_node_match:
∀ s lock_index d d´ m f,
mcs_init_node_spec lock_index d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold mcs_init_node_spec; intros.
subdestruct; inv H.
eapply match_impl_multi_log_update; assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) mcs_init_node_spec}.
Context {inv0: PreservesInvariants (HD:= data0) mcs_init_node_spec}.
Lemma mcs_init_node_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem mcs_init_node_spec)
(id ↦ gensem mcs_init_node_spec).
Proof.
intros.
layer_sim_simpl.
compatsim_simpl (@match_AbData).
intros.
exploit mcs_init_node_exist; eauto 1.
intros [labd´ [HP HM]].
match_external_states_simpl.
eapply mcs_init_node_match; eauto.
Qed.
End MCS_INIT_NODE_SIM.
End OBJ_SIM.