x64: spec: update machine functions, invocations, set_vm_root for new
kernel version
This commit is contained in:
Joel Beeren
parent
3504b119a4
commit
b35c50c481
|
|
@ -324,7 +324,7 @@ where
|
|||
(attribs_from_word attr) vspace;
|
||||
ensure_safe_mapping entries;
|
||||
returnOk $ InvokePage $ PageMap
|
||||
(ArchObjectCap $ PageCap dev p R map_type pgsz (Some (asid,vaddr))) cte entries
|
||||
(ArchObjectCap $ PageCap dev p R map_type pgsz (Some (asid,vaddr))) cte entries vspace
|
||||
odE
|
||||
else throwError TruncatedMessage
|
||||
else if invocation_type label = ArchInvocationLabel X64PageRemap then
|
||||
|
|
@ -347,7 +347,7 @@ where
|
|||
check_vp_alignment pgsz vaddr;
|
||||
entries \<leftarrow> create_mapping_entries (addrFromPPtr p) vaddr pgsz vm_rights
|
||||
(attribs_from_word attr) vspace;
|
||||
returnOk $ InvokePage $ PageRemap entries
|
||||
returnOk $ InvokePage $ PageRemap entries asid vspace
|
||||
odE
|
||||
else throwError TruncatedMessage
|
||||
else if invocation_type label = ArchInvocationLabel X64PageUnmap then
|
||||
|
|
@ -395,7 +395,7 @@ where
|
|||
unlessE (old_pdpte = InvalidPDPTE) $ throwError DeleteFirst;
|
||||
pdpte \<leftarrow> returnOk (PageDirectoryPDPTE (addrFromPPtr p)
|
||||
(filter_frame_attrs $ attribs_from_word attr) vm_read_write);
|
||||
returnOk $ InvokePageDirectory $ PageDirectoryMap cap' cte pdpte pdpt_slot
|
||||
returnOk $ InvokePageDirectory $ PageDirectoryMap cap' cte pdpte pdpt_slot pml
|
||||
odE
|
||||
else throwError TruncatedMessage
|
||||
else if invocation_type label = ArchInvocationLabel X64PageDirectoryUnmap then doE
|
||||
|
|
@ -430,7 +430,7 @@ where
|
|||
returnOk $ InvokePageTable $
|
||||
PageTableMap
|
||||
(ArchObjectCap $ PageTableCap p (Some (asid,vaddr')))
|
||||
cte pde pd_slot
|
||||
cte pde pd_slot pml
|
||||
odE
|
||||
else throwError TruncatedMessage
|
||||
else if invocation_type label = ArchInvocationLabel X64PageTableUnmap then doE
|
||||
|
|
@ -454,18 +454,18 @@ where
|
|||
+ ptTranslationBits + ptTranslationBits;
|
||||
vaddr' \<leftarrow> returnOk $ vaddr && ~~ mask shift_bits;
|
||||
whenE (vaddr' \<ge> kernel_base) $ throwError IllegalOperation;
|
||||
(pml,asid) \<leftarrow> (case vspace_cap of
|
||||
(vspace,asid) \<leftarrow> (case vspace_cap of
|
||||
ArchObjectCap (PML4Cap pml (Some asid)) \<Rightarrow> returnOk (pml,asid)
|
||||
| _ \<Rightarrow> throwError $ InvalidCapability 0);
|
||||
pml' \<leftarrow> lookup_error_on_failure False $ find_vspace_for_asid (asid);
|
||||
whenE (pml \<noteq> pml) $ throwError $ InvalidCapability 0;
|
||||
pml_slot \<leftarrow> returnOk $ lookup_pml4_slot pml vaddr;
|
||||
vspace' \<leftarrow> lookup_error_on_failure False $ find_vspace_for_asid (asid);
|
||||
whenE (vspace' \<noteq> vspace) $ throwError $ InvalidCapability 0;
|
||||
pml_slot \<leftarrow> returnOk $ lookup_pml4_slot vspace vaddr;
|
||||
old_pml4e \<leftarrow> liftE $ get_pml4e pml_slot;
|
||||
cap' <- returnOk $ ArchObjectCap $ PDPointerTableCap p $ Some (asid,vaddr');
|
||||
unlessE (old_pml4e = InvalidPML4E) $ throwError DeleteFirst;
|
||||
pml4e \<leftarrow> returnOk (PDPointerTablePML4E (addrFromPPtr p)
|
||||
(filter_frame_attrs $ attribs_from_word attr) vm_read_write);
|
||||
returnOk $ InvokePDPT $ PDPTMap cap' cte pml4e pml_slot
|
||||
returnOk $ InvokePDPT $ PDPTMap cap' cte pml4e pml_slot vspace
|
||||
odE
|
||||
else throwError TruncatedMessage
|
||||
else if invocation_type label = ArchInvocationLabel X64PDPTUnmap then doE
|
||||
|
|
|
|||
|
|
@ -45,15 +45,15 @@ x64-specific system calls. Selectors are defined for various fields
|
|||
for convenience elsewhere. *}
|
||||
|
||||
datatype pdpt_invocation =
|
||||
PDPTMap cap cslot_ptr pml4e obj_ref
|
||||
PDPTMap cap cslot_ptr pml4e obj_ref obj_ref
|
||||
| PDPTUnmap cap cslot_ptr
|
||||
|
||||
datatype page_directory_invocation =
|
||||
PageDirectoryMap cap cslot_ptr pdpte obj_ref
|
||||
PageDirectoryMap cap cslot_ptr pdpte obj_ref obj_ref
|
||||
| PageDirectoryUnmap cap cslot_ptr
|
||||
|
||||
datatype page_table_invocation =
|
||||
PageTableMap cap cslot_ptr pde obj_ref
|
||||
PageTableMap cap cslot_ptr pde obj_ref obj_ref
|
||||
| PageTableUnmap cap cslot_ptr
|
||||
|
||||
datatype asid_control_invocation =
|
||||
|
|
@ -67,8 +67,11 @@ datatype page_invocation
|
|||
(page_map_cap: cap)
|
||||
(page_map_ct_slot: cslot_ptr)
|
||||
(page_map_entries: "vm_page_entry \<times> obj_ref")
|
||||
(page_map_vspace: obj_ref)
|
||||
| PageRemap
|
||||
(page_remap_entries: "vm_page_entry \<times> obj_ref")
|
||||
(page_remap_asid: asid)
|
||||
(page_remap_vspace: obj_ref)
|
||||
| PageUnmap
|
||||
(page_unmap_cap: arch_cap)
|
||||
(page_unmap_cap_slot: cslot_ptr)
|
||||
|
|
|
|||
|
|
@ -148,14 +148,42 @@ where
|
|||
| X64InstructionFault \<Rightarrow> throwError $ ArchFault $ VMFault addr [1, fault && mask 5]
|
||||
odE"
|
||||
|
||||
|
||||
(* FIXME x64: should be a machine interface op/imported from Haskell *)
|
||||
consts'
|
||||
setCurrentVSpaceRoot_impl :: "machine_word \<Rightarrow> asid \<Rightarrow> unit machine_rest_monad"
|
||||
definition
|
||||
setCurrentVSpaceRoot :: "machine_word \<Rightarrow> asid \<Rightarrow> unit machine_monad" where
|
||||
"setCurrentVSpaceRoot pml4 asid = machine_op_lift (setCurrentVSpaceRoot_impl pml4 asid)"
|
||||
getCurrentCR3 :: "(CR3, 'z::state_ext) s_monad"
|
||||
where
|
||||
"getCurrentCR3 \<equiv> gets (x64_current_cr3 \<circ> arch_state)"
|
||||
|
||||
definition
|
||||
setCurrentCR3 :: "CR3 \<Rightarrow> (unit,'z::state_ext) s_monad"
|
||||
where
|
||||
"setCurrentCR3 cr3 \<equiv> do
|
||||
modify (\<lambda>s. s \<lparr>arch_state := (arch_state s) \<lparr>x64_current_cr3 := cr3\<rparr>\<rparr>);
|
||||
do_machine_op $ writeCR3 (CR3BaseAddress cr3) (CR3pcid cr3)
|
||||
od"
|
||||
|
||||
definition
|
||||
invalidateLocalPageStructureCacheASID :: "obj_ref \<Rightarrow> asid \<Rightarrow> (unit, 'z::state_ext) s_monad"
|
||||
where
|
||||
"invalidateLocalPageStructureCacheASID vspace asid \<equiv> do
|
||||
curCR3 \<leftarrow> getCurrentCR3;
|
||||
setCurrentCR3 (CR3 vspace asid);
|
||||
setCurrentCR3 curCR3
|
||||
od"
|
||||
|
||||
abbreviation "invalidatePageStructureCacheASID \<equiv> invalidateLocalPageStructureCacheASID"
|
||||
|
||||
definition
|
||||
getCurrentVSpaceRoot :: "(obj_ref, 'z::state_ext) s_monad"
|
||||
where
|
||||
"getCurrentVSpaceRoot \<equiv> do
|
||||
cur \<leftarrow> getCurrentCR3;
|
||||
return $ CR3BaseAddress cur
|
||||
od"
|
||||
|
||||
definition
|
||||
setCurrentVSpaceRoot :: "obj_ref \<Rightarrow> asid \<Rightarrow> (unit, 'z::state_ext) s_monad"
|
||||
where
|
||||
"setCurrentVSpaceRoot vspace asid \<equiv> setCurrentCR3 $ CR3 vspace asid"
|
||||
|
||||
text {* Switch into the address space of a given thread or the global address
|
||||
space if none is correctly configured. *}
|
||||
|
|
@ -168,12 +196,14 @@ definition
|
|||
ArchObjectCap (PML4Cap pml4 (Some asid)) \<Rightarrow> doE
|
||||
pml4' \<leftarrow> find_vspace_for_asid asid;
|
||||
whenE (pml4 \<noteq> pml4') $ throwError InvalidRoot;
|
||||
liftE $ do_machine_op $ setCurrentVSpaceRoot (addrFromPPtr pml4) asid
|
||||
curCR3 \<leftarrow> liftE $ getCurrentCR3;
|
||||
whenE (CR3BaseAddress curCR3 \<noteq> pml4 \<and> CR3pcid curCR3 \<noteq> asid) $
|
||||
liftE $ setCurrentCR3 $ CR3 (addrFromPPtr pml4) asid
|
||||
odE
|
||||
| _ \<Rightarrow> throwError InvalidRoot) <catch>
|
||||
(\<lambda>_. do
|
||||
global_pml4 \<leftarrow> gets (x64_global_pml4 \<circ> arch_state);
|
||||
do_machine_op $ setCurrentVSpaceRoot (addrFromKPPtr global_pml4) 0
|
||||
setCurrentVSpaceRoot (addrFromKPPtr global_pml4) 0
|
||||
od)
|
||||
od"
|
||||
|
||||
|
|
@ -196,7 +226,7 @@ definition
|
|||
delete_asid :: "asid \<Rightarrow> obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where
|
||||
"delete_asid asid pml4 \<equiv> do
|
||||
asid_table \<leftarrow> gets (x64_asid_table \<circ> arch_state);
|
||||
do_machine_op $ hwASIDInvalidate asid;
|
||||
do_machine_op $ hwASIDInvalidate asid pml4;
|
||||
case asid_table (asid_high_bits_of asid) of
|
||||
None \<Rightarrow> return ()
|
||||
| Some pool_ptr \<Rightarrow> do
|
||||
|
|
@ -211,42 +241,32 @@ delete_asid :: "asid \<Rightarrow> obj_ref \<Rightarrow> (unit,'z::state_ext) s_
|
|||
od"
|
||||
|
||||
definition
|
||||
flush_all :: "(unit,'z::state_ext) s_monad" where
|
||||
"flush_all = do_machine_op resetCR3"
|
||||
flush_all :: "obj_ref \<Rightarrow> asid \<Rightarrow> (unit,'z::state_ext) s_monad" where
|
||||
"flush_all vspace asid \<equiv> do_machine_op $ invalidateASID vspace asid "
|
||||
|
||||
abbreviation
|
||||
flush_pdpt :: "(unit,'z::state_ext) s_monad" where
|
||||
flush_pdpt :: "obj_ref \<Rightarrow> asid \<Rightarrow> (unit,'z::state_ext) s_monad" where
|
||||
"flush_pdpt \<equiv> flush_all"
|
||||
|
||||
abbreviation
|
||||
flush_pd :: "(unit,'z::state_ext) s_monad" where
|
||||
flush_pd :: "obj_ref \<Rightarrow> asid \<Rightarrow> (unit,'z::state_ext) s_monad" where
|
||||
"flush_pd \<equiv> flush_all"
|
||||
|
||||
text {* Flush mappings associated with a page table. *}
|
||||
definition
|
||||
flush_table :: "obj_ref \<Rightarrow> vspace_ref \<Rightarrow> obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where
|
||||
"flush_table pml4_ref vptr pt_ref \<equiv> do
|
||||
flush_table :: "obj_ref \<Rightarrow> vspace_ref \<Rightarrow> obj_ref \<Rightarrow> asid \<Rightarrow> (unit,'z::state_ext) s_monad" where
|
||||
"flush_table pml4_ref vptr pt_ref asid \<equiv> do
|
||||
assert (vptr && mask (ptTranslationBits + pageBits) = 0);
|
||||
tcb \<leftarrow> gets cur_thread;
|
||||
thread_root_slot \<leftarrow> return (tcb, tcb_cnode_index 1);
|
||||
thread_root \<leftarrow> get_cap thread_root_slot;
|
||||
case thread_root of
|
||||
ArchObjectCap (PML4Cap pml4_ref' (Some _)) \<Rightarrow>
|
||||
when (pml4_ref = pml4_ref') $ do
|
||||
pt \<leftarrow> get_pt pt_ref;
|
||||
forM_x [0 .e. (-1::9 word)] (\<lambda>index. do
|
||||
pte \<leftarrow> return $ pt index;
|
||||
case pte of
|
||||
InvalidPTE \<Rightarrow> return ()
|
||||
| _ \<Rightarrow> do_machine_op $ invalidateTLBEntry (vptr + (ucast index << pageBits))
|
||||
| _ \<Rightarrow> do_machine_op $ invalidateTranslationSingleASID (vptr + (ucast index << pageBits)) asid
|
||||
od)
|
||||
od
|
||||
| _ \<Rightarrow> return ()
|
||||
od"
|
||||
|
||||
|
||||
|
||||
|
||||
text {* Unmap a Page Directory Pointer Table from a PML4. *}
|
||||
definition
|
||||
unmap_pdpt :: "asid \<Rightarrow> vspace_ref \<Rightarrow> obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where
|
||||
|
|
@ -255,11 +275,11 @@ unmap_pdpt :: "asid \<Rightarrow> vspace_ref \<Rightarrow> obj_ref \<Rightarrow>
|
|||
pm_slot \<leftarrow> returnOk $ lookup_pml4_slot vspace vaddr;
|
||||
pml4e \<leftarrow> liftE $ get_pml4e pm_slot;
|
||||
case pml4e of
|
||||
PDPointerTablePML4E pt' _ _ \<Rightarrow>
|
||||
PDPointerTablePML4E pt' _ _ \<Rightarrow>
|
||||
if pt' = addrFromPPtr pdpt then returnOk () else throwError InvalidRoot
|
||||
| _ \<Rightarrow> throwError InvalidRoot;
|
||||
liftE $ do
|
||||
flush_pdpt;
|
||||
flush_pdpt vspace asid;
|
||||
store_pml4e pm_slot InvalidPML4E
|
||||
od
|
||||
odE <catch> (K $ return ())"
|
||||
|
|
@ -272,13 +292,13 @@ unmap_pd :: "asid \<Rightarrow> vspace_ref \<Rightarrow> obj_ref \<Rightarrow> (
|
|||
pdpt_slot \<leftarrow> lookup_pdpt_slot vspace vaddr;
|
||||
pdpte \<leftarrow> liftE $ get_pdpte pdpt_slot;
|
||||
case pdpte of
|
||||
PageDirectoryPDPTE pd' _ _ \<Rightarrow>
|
||||
PageDirectoryPDPTE pd' _ _ \<Rightarrow>
|
||||
if pd' = addrFromPPtr pd then returnOk () else throwError InvalidRoot
|
||||
| _ \<Rightarrow> throwError InvalidRoot;
|
||||
liftE $ do
|
||||
flush_pd;
|
||||
flush_pd vspace asid;
|
||||
store_pdpte pdpt_slot InvalidPDPTE;
|
||||
do_machine_op invalidatePageStructureCache
|
||||
invalidatePageStructureCacheASID (addrFromPPtr vspace) asid
|
||||
od
|
||||
odE <catch> (K $ return ())"
|
||||
|
||||
|
|
@ -290,13 +310,13 @@ unmap_page_table :: "asid \<Rightarrow> vspace_ref \<Rightarrow> obj_ref \<Right
|
|||
pd_slot \<leftarrow> lookup_pd_slot vspace vaddr;
|
||||
pde \<leftarrow> liftE $ get_pde pd_slot;
|
||||
case pde of
|
||||
PageTablePDE addr _ _ \<Rightarrow>
|
||||
PageTablePDE addr _ _ \<Rightarrow>
|
||||
if addrFromPPtr pt = addr then returnOk () else throwError InvalidRoot
|
||||
| _ \<Rightarrow> throwError InvalidRoot;
|
||||
liftE $ do
|
||||
flush_table vspace vaddr pt;
|
||||
liftE $ do
|
||||
flush_table vspace vaddr pt asid;
|
||||
store_pde pd_slot InvalidPDE;
|
||||
do_machine_op $ invalidatePageStructureCache
|
||||
invalidatePageStructureCacheASID (addrFromPPtr vspace) asid
|
||||
od
|
||||
odE <catch> (K $ return ())"
|
||||
|
||||
|
|
@ -339,16 +359,7 @@ unmap_page :: "vmpage_size \<Rightarrow> asid \<Rightarrow> vspace_ref \<Rightar
|
|||
unlessE (check_mapping_pptr pptr (VMPDPTE pdpte)) $ throwError InvalidRoot;
|
||||
liftE $ store_pdpte pdpt_slot InvalidPDPTE
|
||||
odE;
|
||||
liftE $ do
|
||||
tcb \<leftarrow> gets cur_thread;
|
||||
(* FIXME: duplication, pull this pattern out into a function; also in Haskell/C *)
|
||||
thread_root_slot \<leftarrow> return (tcb, tcb_cnode_index 1);
|
||||
thread_root \<leftarrow> get_cap thread_root_slot;
|
||||
case thread_root of
|
||||
ArchObjectCap (PML4Cap vspace' (Some _ )) \<Rightarrow>
|
||||
when (vspace' = vspace) $ do_machine_op $ invalidateTLBEntry vptr
|
||||
| _ \<Rightarrow> return ()
|
||||
od
|
||||
liftE $ do_machine_op $ invalidateTranslationSingleASID vptr asid
|
||||
odE <catch> (K $ return ())"
|
||||
|
||||
|
||||
|
|
@ -502,7 +513,7 @@ attribs_from_word :: "machine_word \<Rightarrow> frame_attrs" where
|
|||
text {* Update the mapping data saved in a page or page table capability. *}
|
||||
definition
|
||||
update_map_data :: "arch_cap \<Rightarrow> (asid \<times> vspace_ref) option \<Rightarrow> arch_cap" where
|
||||
"update_map_data cap m \<equiv> case cap of
|
||||
"update_map_data cap m \<equiv> case cap of
|
||||
PageCap dev p R mt sz _ \<Rightarrow> PageCap dev p R mt sz m
|
||||
| PageTableCap p _ \<Rightarrow> PageTableCap p m
|
||||
| PageDirectoryCap p _ \<Rightarrow> PageDirectoryCap p m
|
||||
|
|
|
|||
|
|
@ -8,7 +8,7 @@
|
|||
* @TAG(GD_GPL)
|
||||
*)
|
||||
|
||||
(*
|
||||
(*
|
||||
Entry point for architecture dependent definitions.
|
||||
*)
|
||||
|
||||
|
|
@ -91,10 +91,10 @@ text {* The ASIDPool capability confers the authority to assign a virtual ASID
|
|||
to a page directory. *}
|
||||
definition
|
||||
perform_asid_pool_invocation :: "asid_pool_invocation \<Rightarrow> (unit,'z::state_ext) s_monad" where
|
||||
"perform_asid_pool_invocation iv \<equiv> case iv of Assign asid pool_ptr ct_slot \<Rightarrow>
|
||||
"perform_asid_pool_invocation iv \<equiv> case iv of Assign asid pool_ptr ct_slot \<Rightarrow>
|
||||
do
|
||||
pml4_cap \<leftarrow> get_cap ct_slot;
|
||||
case pml4_cap of
|
||||
case pml4_cap of
|
||||
ArchObjectCap (PML4Cap pml4_base _) \<Rightarrow> do
|
||||
pool \<leftarrow> get_asid_pool pool_ptr;
|
||||
pool' \<leftarrow> return (pool (ucast asid \<mapsto> pml4_base));
|
||||
|
|
@ -128,19 +128,25 @@ in. *}
|
|||
definition
|
||||
perform_page_invocation :: "page_invocation \<Rightarrow> (unit,'z::state_ext) s_monad" where
|
||||
"perform_page_invocation iv \<equiv> (case iv of
|
||||
PageMap cap ct_slot entries \<Rightarrow> do
|
||||
PageMap cap ct_slot entries vspace \<Rightarrow> do
|
||||
set_cap cap ct_slot;
|
||||
case entries
|
||||
(case entries
|
||||
of (VMPTE pte, slot) \<Rightarrow> store_pte slot pte
|
||||
| (VMPDE pde, slot) \<Rightarrow> store_pde slot pde
|
||||
| (VMPDPTE pdpte, slot) \<Rightarrow> store_pdpte slot pdpte
|
||||
| _ \<Rightarrow> fail
|
||||
| _ \<Rightarrow> fail);
|
||||
asid <- case cap of ArchObjectCap (PageCap _ _ _ _ _ (Some (as, _))) \<Rightarrow> return as
|
||||
| _ \<Rightarrow> fail;
|
||||
invalidatePageStructureCacheASID (addrFromPPtr vspace) asid
|
||||
od
|
||||
| PageRemap entries \<Rightarrow> (case entries
|
||||
| PageRemap entries asid vspace \<Rightarrow> do
|
||||
(case entries
|
||||
of (VMPTE pte, slot) \<Rightarrow> store_pte slot pte
|
||||
| (VMPDE pde, slot) \<Rightarrow> store_pde slot pde
|
||||
| (VMPDPTE pdpte, slot) \<Rightarrow> store_pdpte slot pdpte
|
||||
| _ \<Rightarrow> fail)
|
||||
| _ \<Rightarrow> fail);
|
||||
invalidatePageStructureCacheASID (addrFromPPtr vspace) asid
|
||||
od
|
||||
| PageUnmap cap ct_slot \<Rightarrow>
|
||||
(case cap
|
||||
of PageCap dev base rights map_type sz mapped \<Rightarrow>
|
||||
|
|
@ -160,11 +166,13 @@ text {* PageTable capabilities confer the authority to map and unmap page
|
|||
tables. *}
|
||||
definition
|
||||
perform_page_table_invocation :: "page_table_invocation \<Rightarrow> (unit,'z::state_ext) s_monad" where
|
||||
"perform_page_table_invocation iv \<equiv>
|
||||
case iv of PageTableMap cap ct_slot pde pd_slot \<Rightarrow> do
|
||||
"perform_page_table_invocation iv \<equiv>
|
||||
case iv of PageTableMap cap ct_slot pde pd_slot vspace \<Rightarrow> do
|
||||
set_cap cap ct_slot;
|
||||
store_pde pd_slot pde;
|
||||
do_machine_op $ invalidatePageStructureCache
|
||||
asid <- case cap of ArchObjectCap (PageTableCap _ (Some (as, _))) \<Rightarrow> return as
|
||||
| _ \<Rightarrow> fail;
|
||||
invalidatePageStructureCacheASID (addrFromPPtr vspace) asid
|
||||
od
|
||||
| PageTableUnmap (ArchObjectCap (PageTableCap p mapped_address)) ct_slot \<Rightarrow> do
|
||||
case mapped_address of Some (asid, vaddr) \<Rightarrow> do
|
||||
|
|
@ -182,18 +190,20 @@ text {* PageDirectory capabilities confer the authority to map and unmap page
|
|||
tables. *}
|
||||
definition
|
||||
perform_page_directory_invocation :: "page_directory_invocation \<Rightarrow> (unit,'z::state_ext) s_monad" where
|
||||
"perform_page_directory_invocation iv \<equiv>
|
||||
case iv of PageDirectoryMap cap ct_slot pdpte pdpt_slot \<Rightarrow> do
|
||||
"perform_page_directory_invocation iv \<equiv>
|
||||
case iv of PageDirectoryMap cap ct_slot pdpte pdpt_slot vspace \<Rightarrow> do
|
||||
set_cap cap ct_slot;
|
||||
store_pdpte pdpt_slot pdpte;
|
||||
do_machine_op $ invalidatePageStructureCache
|
||||
asid <- case cap of ArchObjectCap (PageDirectoryCap _ (Some (as, _))) \<Rightarrow> return as
|
||||
| _ \<Rightarrow> fail;
|
||||
invalidatePageStructureCacheASID (addrFromPPtr vspace) asid
|
||||
od
|
||||
| PageDirectoryUnmap (ArchObjectCap (PageDirectoryCap p mapped_address)) ct_slot \<Rightarrow> do
|
||||
case mapped_address of Some (asid, vaddr) \<Rightarrow> do
|
||||
unmap_pd asid vaddr p;
|
||||
pde_bits \<leftarrow> return word_size_bits;
|
||||
slots \<leftarrow> return [p, p + (1 << pde_bits) .e. p + (1 << pd_bits) - 1];
|
||||
mapM_x (swp store_pde InvalidPDE) slots
|
||||
mapM_x (swp store_pde InvalidPDE) slots
|
||||
od | None \<Rightarrow> return ();
|
||||
cap \<leftarrow> liftM the_arch_cap $ get_cap ct_slot;
|
||||
set_cap (ArchObjectCap $ update_map_data cap None) ct_slot
|
||||
|
|
@ -204,11 +214,13 @@ text {* PageDirectory capabilities confer the authority to map and unmap page
|
|||
tables. *}
|
||||
definition
|
||||
perform_pdpt_invocation :: "pdpt_invocation \<Rightarrow> (unit,'z::state_ext) s_monad" where
|
||||
"perform_pdpt_invocation iv \<equiv>
|
||||
case iv of PDPTMap cap ct_slot pml4e pml4_slot \<Rightarrow> do
|
||||
"perform_pdpt_invocation iv \<equiv>
|
||||
case iv of PDPTMap cap ct_slot pml4e pml4_slot vspace \<Rightarrow> do
|
||||
set_cap cap ct_slot;
|
||||
store_pml4e pml4_slot pml4e;
|
||||
do_machine_op $ invalidatePageStructureCache
|
||||
asid <- case cap of ArchObjectCap (PDPointerTableCap _ (Some (as, _))) \<Rightarrow> return as
|
||||
| _ \<Rightarrow> fail;
|
||||
invalidatePageStructureCacheASID (addrFromPPtr vspace) asid
|
||||
od
|
||||
| PDPTUnmap (ArchObjectCap (PDPointerTableCap p mapped_address)) ct_slot \<Rightarrow> do
|
||||
case mapped_address of Some (asid, vaddr) \<Rightarrow> do
|
||||
|
|
|
|||
|
|
@ -32,7 +32,6 @@ type_synonym asid = "machine_word"
|
|||
type_synonym io_port = "16 word"
|
||||
type_synonym io_asid = "16 word"
|
||||
|
||||
|
||||
section {* Architecture-specific capabilities *}
|
||||
|
||||
text {* The x64 kernel supports capabilities for ASID pools and an ASID controller capability,
|
||||
|
|
@ -64,6 +63,21 @@ definition
|
|||
asid_bits :: nat where
|
||||
"asid_bits \<equiv> 12 :: nat"
|
||||
|
||||
(* CR3 Stuff *)
|
||||
datatype CR3 = CR3 obj_ref asid
|
||||
|
||||
primrec CR3BaseAddress where
|
||||
"CR3BaseAddress (CR3 v0 _) = v0"
|
||||
|
||||
primrec CR3BaseAddress_update where
|
||||
"CR3BaseAddress_update f (CR3 v0 v1) = (CR3 (f v0) v1)"
|
||||
|
||||
primrec CR3pcid where
|
||||
"CR3pcid (CR3 _ v1) = v1"
|
||||
|
||||
primrec CR3pcid_update where
|
||||
"CR3pcid_update f (CR3 v0 v1) = (CR3 v0 (f v1))"
|
||||
|
||||
section {* Architecture-specific objects *}
|
||||
|
||||
datatype table_attr = Accessed | CacheDisabled | WriteThrough | ExecuteDisable
|
||||
|
|
@ -280,6 +294,7 @@ record arch_state =
|
|||
x64_global_pdpts :: "obj_ref list"
|
||||
x64_global_pds :: "obj_ref list"
|
||||
x64_asid_map :: "X64_A.asid \<rightharpoonup> obj_ref" (* FIXME x64: do we need this? *)
|
||||
x64_current_cr3 :: "X64_A.CR3"
|
||||
|
||||
(* FIXME x64-vtd:
|
||||
x64_num_io_domain_bits :: "16 word"
|
||||
|
|
|
|||
|
|
@ -20,8 +20,8 @@ begin
|
|||
section "Wrapping and Lifting Machine Operations"
|
||||
|
||||
text {*
|
||||
Most of the machine operations below work on the underspecified
|
||||
part of the machine state @{typ machine_state_rest} and cannot fail.
|
||||
Most of the machine operations below work on the underspecified
|
||||
part of the machine state @{typ machine_state_rest} and cannot fail.
|
||||
We could express the latter by type (leaving out the failure flag),
|
||||
but if we later wanted to implement them,
|
||||
we'd have to set up a new hoare-logic
|
||||
|
|
@ -77,7 +77,7 @@ definition
|
|||
|
||||
definition
|
||||
storeWord :: "machine_word \<Rightarrow> machine_word \<Rightarrow> unit machine_monad"
|
||||
where "storeWord p w \<equiv> do
|
||||
where "storeWord p w \<equiv> do
|
||||
assert (p && mask 3 = 0);
|
||||
modify (underlying_memory_update (
|
||||
fold (\<lambda>i m. m((p + (of_int i)) := word_rsplit w ! (nat i))) [0 .. 7]))
|
||||
|
|
@ -89,7 +89,7 @@ lemma upto0_7_def:
|
|||
lemma loadWord_storeWord_is_return:
|
||||
"p && mask 3 = 0 \<Longrightarrow> (do w \<leftarrow> loadWord p; storeWord p w od) = return ()"
|
||||
apply (rule ext)
|
||||
by (simp add: loadWord_def storeWord_def bind_def assert_def return_def
|
||||
by (simp add: loadWord_def storeWord_def bind_def assert_def return_def
|
||||
modify_def gets_def get_def eval_nat_numeral put_def upto0_7_def
|
||||
word_rsplit_rcat_size word_size)
|
||||
|
||||
|
|
@ -106,7 +106,7 @@ consts'
|
|||
definition
|
||||
configureTimer :: "irq machine_monad"
|
||||
where
|
||||
"configureTimer \<equiv> do
|
||||
"configureTimer \<equiv> do
|
||||
machine_op_lift configureTimer_impl;
|
||||
gets configureTimer_val
|
||||
od"
|
||||
|
|
@ -142,10 +142,10 @@ where
|
|||
|
||||
-- "Interrupt controller operations"
|
||||
|
||||
text {*
|
||||
text {*
|
||||
@{term getActiveIRQ} is now derministic.
|
||||
It 'updates' the irq state to the reflect the passage of
|
||||
time since last the irq was gotten, then it gets the active
|
||||
time since last the irq was gotten, then it gets the active
|
||||
IRQ (if there is one).
|
||||
*}
|
||||
definition
|
||||
|
|
@ -163,7 +163,7 @@ where
|
|||
definition
|
||||
maskInterrupt :: "bool \<Rightarrow> irq \<Rightarrow> unit machine_monad"
|
||||
where
|
||||
"maskInterrupt m irq \<equiv>
|
||||
"maskInterrupt m irq \<equiv>
|
||||
modify (\<lambda>s. s \<lparr> irq_masks := (irq_masks s) (irq := m) \<rparr>)"
|
||||
|
||||
text {* Does nothing on imx31 *}
|
||||
|
|
@ -185,7 +185,7 @@ definition
|
|||
clearMemory :: "machine_word \<Rightarrow> nat \<Rightarrow> unit machine_monad"
|
||||
where
|
||||
"clearMemory ptr bytelength \<equiv> mapM_x (\<lambda>p. storeWord p 0) [ptr, ptr + word_size .e. ptr + (of_nat bytelength) - 1]"
|
||||
|
||||
|
||||
definition
|
||||
clearMemoryVM :: "machine_word \<Rightarrow> nat \<Rightarrow> unit machine_monad"
|
||||
where
|
||||
|
|
@ -221,35 +221,34 @@ type_synonym user_context = "register \<Rightarrow> machine_word"
|
|||
type_synonym 'a user_monad = "(user_context, 'a) nondet_monad"
|
||||
|
||||
definition
|
||||
getRegister :: "register \<Rightarrow> machine_word user_monad"
|
||||
getRegister :: "register \<Rightarrow> machine_word user_monad"
|
||||
where
|
||||
"getRegister r \<equiv> gets (\<lambda>uc. uc r)"
|
||||
|
||||
definition
|
||||
setRegister :: "register \<Rightarrow> machine_word \<Rightarrow> unit user_monad"
|
||||
setRegister :: "register \<Rightarrow> machine_word \<Rightarrow> unit user_monad"
|
||||
where
|
||||
"setRegister r v \<equiv> modify (\<lambda>uc. uc (r := v))"
|
||||
|
||||
definition
|
||||
"getRestartPC \<equiv> getRegister FaultInstruction"
|
||||
"getRestartPC \<equiv> getRegister FaultInstruction"
|
||||
|
||||
definition
|
||||
"setNextPC \<equiv> setRegister NextIP"
|
||||
|
||||
|
||||
consts'
|
||||
initL2Cache_impl :: "unit machine_rest_monad"
|
||||
definition
|
||||
initL2Cache :: "unit machine_monad"
|
||||
where "initL2Cache \<equiv> machine_op_lift initL2Cache_impl"
|
||||
|
||||
definition getCurrentCR3 :: "Platform.X64.cr3 machine_monad"
|
||||
|
||||
consts'
|
||||
writeCR3_impl :: "machine_word \<Rightarrow> machine_word \<Rightarrow> unit machine_rest_monad"
|
||||
|
||||
definition writeCR3 :: "machine_word \<Rightarrow> machine_word \<Rightarrow> unit machine_monad"
|
||||
where
|
||||
"getCurrentCR3 \<equiv> undefined"
|
||||
|
||||
definition setCurrentCR3 :: "Platform.X64.cr3 \<Rightarrow> unit machine_monad"
|
||||
where
|
||||
"setCurrentCR3 \<equiv> undefined"
|
||||
|
||||
"writeCR3 vspace pcid \<equiv> machine_op_lift (writeCR3_impl vspace pcid)"
|
||||
|
||||
consts'
|
||||
mfence_impl :: "unit machine_rest_monad"
|
||||
definition
|
||||
|
|
@ -266,15 +265,24 @@ where
|
|||
"invalidateTLBEntry vptr \<equiv> machine_op_lift (invalidateTLBEntry_impl vptr)"
|
||||
|
||||
consts'
|
||||
invalidatePageStructureCache_impl :: "unit machine_rest_monad"
|
||||
|
||||
invalidateTranslationSingleASID_impl :: "machine_word \<Rightarrow> machine_word \<Rightarrow> unit machine_rest_monad"
|
||||
|
||||
definition
|
||||
invalidatePageStructureCache :: "unit machine_monad" where
|
||||
"invalidatePageStructureCache \<equiv> machine_op_lift invalidatePageStructureCache_impl"
|
||||
|
||||
invalidateTranslationSingleASID :: "machine_word \<Rightarrow> machine_word \<Rightarrow> unit machine_monad"
|
||||
where
|
||||
"invalidateTranslationSingleASID vptr asid \<equiv> machine_op_lift (invalidateTranslationSingleASID_impl vptr asid)"
|
||||
|
||||
consts'
|
||||
invalidateASID_impl :: "machine_word \<Rightarrow> machine_word \<Rightarrow> unit machine_rest_monad"
|
||||
|
||||
definition
|
||||
invalidateASID :: "machine_word \<Rightarrow> machine_word \<Rightarrow> unit machine_monad"
|
||||
where
|
||||
"invalidateASID vspace asid \<equiv> machine_op_lift (invalidateASID_impl vspace asid)"
|
||||
|
||||
consts'
|
||||
resetCR3_impl :: "unit machine_rest_monad"
|
||||
|
||||
|
||||
definition
|
||||
resetCR3 :: "unit machine_monad" where
|
||||
"resetCR3 \<equiv> machine_op_lift resetCR3_impl "
|
||||
|
|
@ -291,12 +299,10 @@ where
|
|||
"numIODomainIDBits \<equiv> undefined"
|
||||
*)
|
||||
|
||||
consts'
|
||||
hwASIDInvalidate_impl :: "word64 \<Rightarrow> unit machine_rest_monad"
|
||||
definition
|
||||
hwASIDInvalidate :: "word64 \<Rightarrow> unit machine_monad"
|
||||
hwASIDInvalidate :: "word64 \<Rightarrow> machine_word \<Rightarrow> unit machine_monad"
|
||||
where
|
||||
"hwASIDInvalidate asid \<equiv> machine_op_lift (hwASIDInvalidate_impl asid)"
|
||||
"hwASIDInvalidate \<equiv> invalidateASID"
|
||||
|
||||
|
||||
consts'
|
||||
|
|
@ -346,10 +352,10 @@ ioapicMapPinToVector :: "machine_word \<Rightarrow> machine_word \<Rightarrow> m
|
|||
where
|
||||
"ioapicMapPinToVector ioapic pin level polarity vector \<equiv> machine_op_lift (ioapicMapPinToVector_impl ioapic pin level polarity vector)"
|
||||
|
||||
datatype X64IRQState =
|
||||
datatype X64IRQState =
|
||||
IRQFree
|
||||
| IRQReserved
|
||||
| IRQMSI
|
||||
| IRQMSI
|
||||
(MSIBus : machine_word)
|
||||
(MSIDev : machine_word)
|
||||
(MSIFunc : machine_word)
|
||||
|
|
@ -360,7 +366,7 @@ datatype X64IRQState =
|
|||
(IRQLevel : machine_word)
|
||||
(IRQPolarity : machine_word)
|
||||
(IRQMasked : bool)
|
||||
|
||||
|
||||
|
||||
consts'
|
||||
updateIRQState_impl :: "irq \<Rightarrow> X64IRQState \<Rightarrow> unit machine_rest_monad"
|
||||
|
|
|
|||
|
|
@ -64,7 +64,7 @@ definition
|
|||
maxIRQ :: "irq" where
|
||||
"maxIRQ \<equiv> 63"
|
||||
|
||||
datatype cr3 = X64CR3 word64 word64
|
||||
datatype cr3 = X64CR3 word64 (*pml4*) word64 (*asid*)
|
||||
|
||||
primrec CR3BaseAddress where
|
||||
"CR3BaseAddress (X64CR3 v0 _) = v0"
|
||||
|
|
|
|||
Loading…
Reference in New Issue