Require Import Coqlib.
Require Import Maps.
Require Import Integers.
Require Import Values.
Require Import GenSem.
Require Import Maps.
Require Import Integers.
Require Import Values.
Require Import RealParams.
Require Import GenSem.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import PrimSemantics.
Require Import CompatClightSem.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import RData.
Require Import CalLock.
Require Import Constants.
Require Import HypsecCommLib.
Require Import LockOpsH.Spec.
Require Import LockOpsH.Layer.
Require Import AbstractMachine.Spec.
Local Open Scope Z_scope.
Section LocksSpec.
Definition acquire_lock_spec (lk: Z) (adt: RData): option RData :=
if adt.(shared).(halt) then Some adt else
match ZMap.get lk adt.(log), ZMap.get lk adt.(lock) with
| Some l, LockFalse =>
let wl := WAIT_LOCK (Z.to_nat lock_bound) in
let to := ZMap.get lk adt.(oracle) in
let l' := TEVENT adt.(curid) (TSHARED (OPULL lk)) ::
TEVENT adt.(curid) (TTICKET wl) ::
to adt.(curid) l ++ l in
match H_CalLock l', CalState lk l' adt.(shared) with
| Some _, sdt' => Some adt {log: ZMap.set lk (Some l') adt.(log)}
{lock: ZMap.set lk (LockOwn true) adt.(lock)}
{tstate: 0}
{shared: sdt'}
| _, _ => None
end
| _, _ => None
end
.
Definition release_lock_spec (e: SharedMemEvent) (lk: Z) (adt: RData): option RData :=
if adt.(shared).(halt) then Some adt else
match ZMap.get lk adt.(log), ZMap.get lk adt.(lock) with
| Some l, LockOwn true =>
let l' := TEVENT adt.(curid) (TTICKET REL_LOCK) ::
TEVENT adt.(curid) (TSHARED e) ::
l in
match H_CalLock l' with
| Some _ => Some adt {log: ZMap.set lk (Some l') adt.(log)}
{lock: ZMap.set lk LockFalse adt.(lock)}
{tstate: 1}
| _ => None
end
| _, _ => None
end
.
Definition acquire_lock_pt_spec (vmid: Z) (adt: RData) : option RData :=
rely is_vmid vmid;
acquire_lock_spec (lock_idx_pt vmid) adt.
Definition acquire_lock_spt_spec (adt: RData): option RData :=
acquire_lock_spec lock_idx_spt adt.
Definition acquire_lock_s2page_spec (adt: RData): option RData :=
acquire_lock_spec lock_idx_s2page adt.
Definition acquire_lock_core_spec (adt: RData): option RData :=
acquire_lock_spec lock_idx_core adt.
Definition acquire_lock_vm_spec (vmid: Z) (adt: RData) : option RData :=
rely is_vm vmid;
acquire_lock_spec (lock_idx_vm vmid) adt.
Definition acquire_lock_smmu_spec (adt: RData): option RData :=
acquire_lock_spec lock_idx_smmu adt.
Definition release_lock_pt_spec (vmid: Z) (adt: RData) : option RData :=
let e := ONPT (ZMap.get vmid adt.(shared).(npts)) in
rely is_vmid vmid;
release_lock_spec e (lock_idx_pt vmid) adt.
Definition release_lock_spt_spec (adt: RData): option RData :=
let e := OSPT adt.(shared).(spts) in
release_lock_spec e lock_idx_spt adt.
Definition release_lock_s2page_spec (adt: RData): option RData :=
let e := OS2_PAGE adt.(shared).(s2page) in
release_lock_spec e lock_idx_s2page adt.
Definition release_lock_core_spec (adt: RData): option RData :=
let e := OCORE_DATA adt.(shared).(core_data) in
release_lock_spec e lock_idx_core adt.
Definition release_lock_vm_spec (vmid: Z) (adt: RData) : option RData :=
let e := OVMINFO (ZMap.get vmid adt.(shared).(vminfos)) in
rely is_vm vmid;
release_lock_spec e (lock_idx_vm vmid) adt.
Definition release_lock_smmu_spec (adt: RData): option RData :=
let e := OSMMU adt.(shared).(smmu_vmid) in
release_lock_spec e lock_idx_smmu adt.
End LocksSpec.
Section LocksSpecLow.
Context `{real_params: RealParams}.
Notation LDATA := RData.
Notation LDATAOps := (cdata (cdata_ops := LockOpsH_ops) LDATA).
Definition acquire_lock_spec0 (lk: Z) (adt: RData): option RData :=
match wait_hlock_spec lk adt with
| Some adt' => acquire_shared_spec lk adt'
| _ => None
end.
Definition release_lock_spec0 (e: SharedMemEvent) (lk: Z) (adt: RData): option RData :=
match release_shared_spec e lk adt with
| Some adt' => pass_hlock_spec lk adt'
| _ => None
end.
Definition acquire_lock_pt_spec0 (vmid: Z) (adt: RData) : option RData :=
acquire_lock_spec0 (lock_idx_pt vmid) adt.
Definition acquire_lock_spt_spec0 (adt: RData) : option RData :=
acquire_lock_spec0 lock_idx_spt adt.
Definition acquire_lock_s2page_spec0 (adt: RData) : option RData :=
acquire_lock_spec0 lock_idx_s2page adt.
Definition acquire_lock_core_spec0 (adt: RData) : option RData :=
acquire_lock_spec0 lock_idx_core adt.
Definition acquire_lock_vm_spec0 (vmid: Z) (adt: RData) : option RData :=
acquire_lock_spec0 (lock_idx_vm vmid) adt.
Definition acquire_lock_smmu_spec0 (adt: RData) : option RData :=
acquire_lock_spec0 lock_idx_smmu adt.
Definition release_lock_pt_spec0 (vmid: Z) (adt: RData) : option RData :=
let lk := lock_idx_pt vmid in
match release_shared_pt_spec vmid adt with
| Some adt' => pass_hlock_spec lk adt'
| _ => None
end.
Definition release_lock_spt_spec0 (adt: RData) : option RData :=
let lk := lock_idx_spt in
match release_shared_spt_spec adt with
| Some adt' => pass_hlock_spec lk adt'
| _ => None
end.
Definition release_lock_s2page_spec0 (adt: RData) : option RData :=
let lk := lock_idx_s2page in
match release_shared_s2page_spec adt with
| Some adt' => pass_hlock_spec lk adt'
| _ => None
end.
Definition release_lock_core_spec0 (adt: RData) : option RData :=
let lk := lock_idx_core in
match release_shared_core_spec adt with
| Some adt' => pass_hlock_spec lk adt'
| _ => None
end.
Definition release_lock_vm_spec0 (vmid: Z) (adt: RData) : option RData :=
let lk := lock_idx_vm vmid in
match release_shared_vm_spec vmid adt with
| Some adt' => pass_hlock_spec lk adt'
| _ => None
end.
Definition release_lock_smmu_spec0 (adt: RData) : option RData :=
let lk := lock_idx_smmu in
match release_shared_smmu_spec adt with
| Some adt' => pass_hlock_spec lk adt'
| _ => None
end.
Inductive acquire_lock_pt_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
| acquire_lock_pt_spec_low_intro s (WB: _ -> Prop) m'0 labd labd' vmid
(Hinv: high_level_invariant labd)
(Hspec: acquire_lock_pt_spec0 (Int.unsigned vmid) labd = Some labd'):
acquire_lock_pt_spec_low_step s WB ((Vint vmid)::nil) (m'0, labd) Vundef (m'0, labd').
Inductive acquire_lock_spt_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
| acquire_lock_spt_spec_low_intro s (WB: _ -> Prop) m'0 labd labd'
(Hinv: high_level_invariant labd)
(Hspec: acquire_lock_spt_spec0 labd = Some labd'):
acquire_lock_spt_spec_low_step s WB nil (m'0, labd) Vundef (m'0, labd').
Inductive acquire_lock_s2page_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
| acquire_lock_s2page_spec_low_intro s (WB: _ -> Prop) m'0 labd labd'
(Hinv: high_level_invariant labd)
(Hspec: acquire_lock_s2page_spec0 labd = Some labd'):
acquire_lock_s2page_spec_low_step s WB nil (m'0, labd) Vundef (m'0, labd').
Inductive acquire_lock_core_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
| acquire_lock_core_spec_low_intro s (WB: _ -> Prop) m'0 labd labd'
(Hinv: high_level_invariant labd)
(Hspec: acquire_lock_core_spec0 labd = Some labd'):
acquire_lock_core_spec_low_step s WB nil (m'0, labd) Vundef (m'0, labd').
Inductive acquire_lock_vm_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
| acquire_lock_vm_spec_low_intro s (WB: _ -> Prop) m'0 labd labd' vmid
(Hinv: high_level_invariant labd)
(Hspec: acquire_lock_vm_spec0 (Int.unsigned vmid) labd = Some labd'):
acquire_lock_vm_spec_low_step s WB ((Vint vmid)::nil) (m'0, labd) Vundef (m'0, labd').
Inductive acquire_lock_smmu_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
| acquire_lock_smmu_spec_low_intro s (WB: _ -> Prop) m'0 labd labd'
(Hinv: high_level_invariant labd)
(Hspec: acquire_lock_smmu_spec0 labd = Some labd'):
acquire_lock_smmu_spec_low_step s WB nil (m'0, labd) Vundef (m'0, labd').
Inductive release_lock_pt_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
| release_lock_pt_spec_low_intro s (WB: _ -> Prop) m'0 labd labd' vmid
(Hinv: high_level_invariant labd)
(Hspec: release_lock_pt_spec0 (Int.unsigned vmid) labd = Some labd'):
release_lock_pt_spec_low_step s WB ((Vint vmid)::nil) (m'0, labd) Vundef (m'0, labd').
Inductive release_lock_spt_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
| release_lock_spt_spec_low_intro s (WB: _ -> Prop) m'0 labd labd'
(Hinv: high_level_invariant labd)
(Hspec: release_lock_spt_spec0 labd = Some labd'):
release_lock_spt_spec_low_step s WB nil (m'0, labd) Vundef (m'0, labd').
Inductive release_lock_s2page_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
| release_lock_s2page_spec_low_intro s (WB: _ -> Prop) m'0 labd labd'
(Hinv: high_level_invariant labd)
(Hspec: release_lock_s2page_spec0 labd = Some labd'):
release_lock_s2page_spec_low_step s WB nil (m'0, labd) Vundef (m'0, labd').
Inductive release_lock_core_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
| release_lock_core_spec_low_intro s (WB: _ -> Prop) m'0 labd labd'
(Hinv: high_level_invariant labd)
(Hspec: release_lock_core_spec0 labd = Some labd'):
release_lock_core_spec_low_step s WB nil (m'0, labd) Vundef (m'0, labd').
Inductive release_lock_vm_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
| release_lock_vm_spec_low_intro s (WB: _ -> Prop) m'0 labd labd' vmid
(Hinv: high_level_invariant labd)
(Hspec: release_lock_vm_spec0 (Int.unsigned vmid) labd = Some labd'):
release_lock_vm_spec_low_step s WB ((Vint vmid)::nil) (m'0, labd) Vundef (m'0, labd').
Inductive release_lock_smmu_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
sextcall_sem (mem := mwd LDATAOps) :=
| release_lock_smmu_spec_low_intro s (WB: _ -> Prop) m'0 labd labd'
(Hinv: high_level_invariant labd)
(Hspec: release_lock_smmu_spec0 labd = Some labd'):
release_lock_smmu_spec_low_step s WB nil (m'0, labd) Vundef (m'0, labd').
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Definition acquire_lock_pt_spec_low: compatsem LDATAOps :=
csem acquire_lock_pt_spec_low_step (type_of_list_type (Tint32::nil)) Tvoid.
Definition acquire_lock_spt_spec_low: compatsem LDATAOps :=
csem acquire_lock_spt_spec_low_step (type_of_list_type nil) Tvoid.
Definition acquire_lock_s2page_spec_low: compatsem LDATAOps :=
csem acquire_lock_s2page_spec_low_step (type_of_list_type nil) Tvoid.
Definition acquire_lock_core_spec_low: compatsem LDATAOps :=
csem acquire_lock_core_spec_low_step (type_of_list_type nil) Tvoid.
Definition acquire_lock_vm_spec_low: compatsem LDATAOps :=
csem acquire_lock_vm_spec_low_step (type_of_list_type (Tint32::nil)) Tvoid.
Definition acquire_lock_smmu_spec_low: compatsem LDATAOps :=
csem acquire_lock_smmu_spec_low_step (type_of_list_type nil) Tvoid.
Definition release_lock_pt_spec_low: compatsem LDATAOps :=
csem release_lock_pt_spec_low_step (type_of_list_type (Tint32::nil)) Tvoid.
Definition release_lock_spt_spec_low: compatsem LDATAOps :=
csem release_lock_spt_spec_low_step (type_of_list_type nil) Tvoid.
Definition release_lock_s2page_spec_low: compatsem LDATAOps :=
csem release_lock_s2page_spec_low_step (type_of_list_type nil) Tvoid.
Definition release_lock_core_spec_low: compatsem LDATAOps :=
csem release_lock_core_spec_low_step (type_of_list_type nil) Tvoid.
Definition release_lock_vm_spec_low: compatsem LDATAOps :=
csem release_lock_vm_spec_low_step (type_of_list_type (Tint32::nil)) Tvoid.
Definition release_lock_smmu_spec_low: compatsem LDATAOps :=
csem release_lock_smmu_spec_low_step (type_of_list_type nil) Tvoid.
End WITHMEM.
End LocksSpecLow.