Library mcertikos.multithread.flatmem.HostAccessPHB
This file defines the load and store semantics for primitives at all layers
Require Import Coqlib.
Require Import Maps.
Require Import Globalenvs.
Require Import ASTExtra.
Require Import AsmX.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import LAsm.
Require Import AuxStateDataType.
Require Import Constant.
Require Import FlatMemory.
Require Import GlobIdent.
Require Import Integers.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import AsmImplLemma.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compcertx.ClightModules.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatClightSem.
Require Import liblayers.compcertx.MemWithData.
Require Import GlobalOracleProp.
Require Import AuxSingleAbstractDataType.
Require Import SingleAbstractDataType.
Require Export PageFaultPHB.
Require Export FlatLoadStoreSemPHB.
Require Import LoadStoreDefPHB.
Section Load_Store.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context `{HD: CompatData PData}.
Notation HDATAOps := (cdata (cdata_ops := data_ops) PData).
Section GE.
Context {F V} (ge: Genv.t F V).
Section Load_StorePHB.
Definition single_exec_host_load (adr: int) (chunk: memory_chunk) (m: mwd HDATAOps) (rs: regset) (rd: preg) :=
let adt:= (snd m) in
let ofs := (Int.unsigned adr) in
if zeq (proc_id (fst adt)) (PT (snd adt)) then
match ZMap.get (PDX ofs) (ZMap.get (PT (snd adt)) (ptpool (snd adt))) with
| PDEValid _ pte ⇒
if (zle (ofs mod PgSize) (PgSize - size_chunk chunk)) then
if (Zdivide_dec (align_chunk chunk) (ofs mod PgSize) (align_chunk_pos chunk)) then
match ZMap.get (PTX ofs) pte with
| PTEValid v p ⇒
match p with
| PTK _ ⇒ Stuck
| _ ⇒ match ZMap.get (PageI (PTADDR v ofs)) (pperm (snd adt)) with
| PGAlloc ⇒
single_exec_flatmem_load chunk m (PTADDR v ofs) rs rd
| _ ⇒ Stuck
end
end
| PTEUnPresent ⇒ single_exec_pagefault ge m adr rs
|_ ⇒ Stuck
end
else Stuck
else Stuck
| _ ⇒ Stuck
end
else Stuck.
Context `{single_trap_inv: Single_TrapinfoSetInvariant (oracle_ops := oracle_ops) (big_ops := big_ops) (data_ops := data_ops)}.
Lemma single_exec_host_load_high_level_invariant:
∀ adr chunk m rs rd rs´ m´,
single_exec_host_load adr chunk m rs rd = Next rs´ m´ →
high_level_invariant (snd m) →
high_level_invariant (snd m´).
Proof.
unfold single_exec_host_load.
intros until m´.
destruct (zeq (proc_id (fst (snd m))) (PT (snd (snd m)))); try discriminate.
destruct (ZMap.get (PDX (Int.unsigned adr)) (ZMap.get (PT (snd (snd m))) (ptpool (snd (snd m))))); try discriminate.
destruct (zle (Int.unsigned adr mod 4096) (4096 - size_chunk chunk)); contra_inv.
destruct (Zdivide_dec (align_chunk chunk) (Int.unsigned adr mod 4096) (align_chunk_pos chunk)); contra_inv.
destruct (ZMap.get (PTX (Int.unsigned adr)) pte); try discriminate.
destruct p; try discriminate.
× destruct (ZMap.get (PageI (PTADDR v (Int.unsigned adr))) (pperm (snd (snd m)))); try discriminate.
intros; exploit single_exec_flatmem_load_mem; eauto; intros; subst; congruence.
× destruct (ZMap.get (PageI (PTADDR v (Int.unsigned adr))) (pperm (snd (snd m)))); try discriminate.
intros; exploit single_exec_flatmem_load_mem; eauto; intros; subst; congruence.
× intros.
eapply single_exec_pagefault_high_level_invariant in H; eauto.
Qed.
Lemma single_exec_host_load_asm_invariant:
∀ chunk rd,
∀ TYP: subtype (type_of_chunk chunk) (typ_of_preg rd) = true,
∀ adr m rs rs´ m´,
single_exec_host_load adr chunk m rs rd = Next rs´ m´ →
AsmX.asm_invariant ge rs m →
AsmX.asm_invariant ge rs´ m´.
Proof.
unfold single_exec_host_load.
intros until m´.
destruct (zeq (proc_id (fst (snd m))) (PT (snd (snd m)))); try discriminate.
destruct (ZMap.get (PDX (Int.unsigned adr)) (ZMap.get (PT (snd (snd m))) (ptpool (snd (snd m))))); try discriminate.
destruct (zle (Int.unsigned adr mod 4096) (4096 - size_chunk chunk)); contra_inv.
destruct (Zdivide_dec (align_chunk chunk) (Int.unsigned adr mod 4096) (align_chunk_pos chunk)); contra_inv.
destruct (ZMap.get (PTX (Int.unsigned adr)) pte); try discriminate.
destruct p; try discriminate.
× destruct (ZMap.get (PageI (PTADDR v (Int.unsigned adr))) (pperm (snd (snd m)))); try discriminate.
intros; eapply single_exec_flatmem_load_asm_invariant; eauto.
× destruct (ZMap.get (PageI (PTADDR v (Int.unsigned adr))) (pperm (snd (snd m)))); try discriminate.
intros; eapply single_exec_flatmem_load_asm_invariant; eauto.
× intros; eapply single_exec_pagefault_asm_invariant; eauto.
Qed.
Lemma single_exec_host_load_low_level_invariant:
∀ adr chunk m rs rd rs´ m´,
single_exec_host_load adr chunk m rs rd = Next rs´ m´ →
AsmX.asm_invariant ge rs m →
CompatData.low_level_invariant (Mem.nextblock m) (snd m) →
CompatData.low_level_invariant (Mem.nextblock m´) (snd m´).
Proof.
unfold single_exec_host_load.
intros until m´.
destruct (zeq (proc_id (fst (snd m))) (PT (snd (snd m)))); try discriminate.
destruct (ZMap.get (PDX (Int.unsigned adr)) (ZMap.get (PT (snd (snd m))) (ptpool (snd (snd m))))); try discriminate.
destruct (zle (Int.unsigned adr mod 4096) (4096 - size_chunk chunk)); contra_inv.
destruct (Zdivide_dec (align_chunk chunk) (Int.unsigned adr mod 4096) (align_chunk_pos chunk)); contra_inv.
destruct (ZMap.get (PTX (Int.unsigned adr)) pte); try discriminate.
destruct p; try discriminate.
× destruct (ZMap.get (PageI (PTADDR v (Int.unsigned adr))) (pperm (snd (snd m)))); try discriminate.
intros; exploit single_exec_flatmem_load_mem; eauto; intro; subst; congruence.
× destruct (ZMap.get (PageI (PTADDR v (Int.unsigned adr))) (pperm (snd (snd m)))); try discriminate.
intros; exploit single_exec_flatmem_load_mem; eauto; intro; subst; congruence.
× eapply single_exec_pagefault_low_level_invariant; eauto.
Qed.
Context `{single_flatmem_store: PData → memory_chunk → Z → val → option (cdata PData)}.
Definition single_exec_host_store (adr: int) (chunk: memory_chunk) (m: mwd HDATAOps)
(rs: regset) (rd: preg) (destroyed: list preg) :=
let adt:= (snd m) in
let ofs := (Int.unsigned adr) in
if zeq (proc_id (fst adt)) (PT (snd adt)) then
match ZMap.get (PDX ofs) (ZMap.get (PT (snd adt)) (ptpool (snd adt))) with
| PDEValid _ pte ⇒
if (zle (ofs mod PgSize) (PgSize - size_chunk chunk)) then
if (Zdivide_dec (align_chunk chunk) (ofs mod PgSize) (align_chunk_pos chunk)) then
match ZMap.get (PTX ofs) pte with
| PTEValid v p ⇒
match p with
| PTK _ ⇒ Stuck
| _ ⇒ single_exec_flatmem_store
(single_flatmem_store:= single_flatmem_store) chunk m (PTADDR v ofs) rs rd destroyed
end
| PTEUnPresent ⇒ single_exec_pagefault ge m adr rs
|_ ⇒ Stuck
end
else Stuck
else Stuck
| _ ⇒ Stuck
end
else Stuck.
Context {single_flat_inv: Single_FlatmemStoreInvariant
(data_ops := data_ops)
(single_flatmem_store:= single_flatmem_store)}.
Lemma single_exec_host_store_high_level_invariant:
∀ adr chunk m rs rd rs´ ds m´,
single_exec_host_store adr chunk m rs rd ds = Next rs´ m´ →
high_level_invariant (snd m) →
high_level_invariant (snd m´).
Proof.
unfold single_exec_host_store.
intros until m´.
destruct (zeq (proc_id (fst (snd m))) (PT (snd (snd m)))); try discriminate.
destruct (ZMap.get (PDX (Int.unsigned adr)) (ZMap.get (PT (snd (snd m))) (ptpool (snd (snd m))))); try discriminate.
destruct (zle (Int.unsigned adr mod 4096) (4096 - size_chunk chunk)); contra_inv.
destruct (Zdivide_dec (align_chunk chunk) (Int.unsigned adr mod 4096) (align_chunk_pos chunk)); contra_inv.
destruct (ZMap.get (PTX (Int.unsigned adr)) pte); try discriminate.
destruct p; try discriminate.
× intros; eapply single_exec_flatmem_store_high_level_invariant; eauto.
eapply single_PTADDR_mod_lt; assumption.
× intros; eapply single_exec_flatmem_store_high_level_invariant; eauto.
eapply single_PTADDR_mod_lt; assumption.
× eapply single_exec_pagefault_high_level_invariant; eauto.
Qed.
Lemma single_exec_host_store_asm_invariant:
∀ chunk rd,
∀ adr m rs rs´ ds m´,
single_exec_host_store adr chunk m rs rd ds = Next rs´ m´ →
AsmX.asm_invariant ge rs m →
AsmX.asm_invariant ge rs´ m´.
Proof.
unfold single_exec_host_store.
intros until m´.
destruct (zeq (proc_id (fst (snd m))) (PT (snd (snd m)))); try discriminate.
destruct (ZMap.get (PDX (Int.unsigned adr)) (ZMap.get (PT (snd (snd m))) (ptpool (snd (snd m))))); try discriminate.
destruct (zle (Int.unsigned adr mod 4096) (4096 - size_chunk chunk)); contra_inv.
destruct (Zdivide_dec (align_chunk chunk) (Int.unsigned adr mod 4096) (align_chunk_pos chunk)); contra_inv.
destruct (ZMap.get (PTX (Int.unsigned adr)) pte); try discriminate.
destruct p; try discriminate.
× intros; eapply single_exec_flatmem_store_asm_invariant; eauto.
× intros; eapply single_exec_flatmem_store_asm_invariant; eauto.
× intros; eapply single_exec_pagefault_asm_invariant; eauto.
Qed.
Lemma single_exec_host_store_low_level_invariant:
∀ adr chunk m rs rd rs´ ds m´,
single_exec_host_store adr chunk m rs rd ds = Next rs´ m´ →
AsmX.asm_invariant ge rs m →
CompatData.low_level_invariant (Mem.nextblock m) (snd m) →
CompatData.low_level_invariant (Mem.nextblock m´) (snd m´).
Proof.
unfold single_exec_host_store.
intros until m´.
destruct (zeq (proc_id (fst (snd m))) (PT (snd (snd m)))); try discriminate.
destruct (ZMap.get (PDX (Int.unsigned adr)) (ZMap.get (PT (snd (snd m))) (ptpool (snd (snd m))))); try discriminate.
destruct (zle (Int.unsigned adr mod 4096) (4096 - size_chunk chunk)); contra_inv.
destruct (Zdivide_dec (align_chunk chunk) (Int.unsigned adr mod 4096) (align_chunk_pos chunk)); contra_inv.
destruct (ZMap.get (PTX (Int.unsigned adr)) pte); try discriminate.
destruct p; try discriminate.
× intros; eapply single_exec_flatmem_store_low_level_invariant; eauto.
× intros; eapply single_exec_flatmem_store_low_level_invariant; eauto.
× eapply single_exec_pagefault_low_level_invariant; eauto.
Qed.
End Load_StorePHB.
End GE.
End Load_Store.