adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

aarch64 haskell+design: record PT types in ghost state 

For making the state relation functional in refine/ADH_H we need to
know to which type of page table each PTE belongs. Record this
information in ghost state, similar to what we do for CNode size and
user page size.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2023-05-24 18:03:49 +10:00
parent a4f944d094
commit e0ae44a577
No known key found for this signature in database
GPG Key ID: 20A847CE6AB7F5F3
11 changed files with 132 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
spec/design/skel/AARCH64/ArchIntermediate_H.thy
View File

@ -25,10 +25,14 @@ private abbreviation (input)
od)"
private abbreviation (input)
"createNewTableCaps regionBase numObjects tableBits objectProto cap initialiseMappings \<equiv> (do
"createNewTableCaps regionBase numObjects ptType objectProto cap initialiseMappings \<equiv> (do
tableBits \<leftarrow> return (ptBits ptType);
tableSize \<leftarrow> return (tableBits - objBits objectProto);
addrs \<leftarrow> createObjects regionBase numObjects (injectKO objectProto) tableSize;
pts \<leftarrow> return (map (PPtr \<circ> fromPPtr) addrs);
modify (\<lambda>ks. ks \<lparr>ksArchState :=
ksArchState ks \<lparr>gsPTTypes :=
gsPTTypes (ksArchState ks) (regionBase \<mapsto> ptType)\<rparr>\<rparr>);
initialiseMappings pts;
return $ map (\<lambda>pt. cap pt Nothing) pts
od)"
@ -45,11 +49,11 @@ defs Arch_createNewCaps_def:
| HugePageObject \<Rightarrow>
createNewFrameCaps regionBase numObjects dev (2 * ptTranslationBits NormalPT_T) ARMHugePage
| VSpaceObject \<Rightarrow>
createNewTableCaps regionBase numObjects (ptBits VSRootPT_T) (makeObject::pte)
createNewTableCaps regionBase numObjects VSRootPT_T (makeObject::pte)
(\<lambda>base addr. PageTableCap base VSRootPT_T addr)
(\<lambda>pts. return ())
| PageTableObject \<Rightarrow>
createNewTableCaps regionBase numObjects (ptBits NormalPT_T) (makeObject::pte)
createNewTableCaps regionBase numObjects NormalPT_T (makeObject::pte)
(\<lambda>base addr. PageTableCap base NormalPT_T addr)
(\<lambda>pts. return ())
| VCPUObject \<Rightarrow> (do

20
spec/design/skel/AARCH64/ArchPSpace_H.thy Normal file
View File

@ -0,0 +1,20 @@
(*
* Copyright 2023, Proofcraft Pty Ltd
*
* SPDX-License-Identifier: GPL-2.0-only
*)
(* Arch-specific ghost update functions for physical memory *)
theory ArchPSpace_H
imports
ObjectInstances_H
begin
context Arch begin global_naming AARCH64_H
#INCLUDE_HASKELL SEL4/Model/PSpace/AARCH64.hs
end (* context Arch *)
end

4
spec/design/skel/PSpaceFuns_H.thy
View File

@ -10,6 +10,7 @@ theory PSpaceFuns_H
imports
ObjectInstances_H
FaultMonad_H
ArchPSpace_H
"Lib.DataMap"
begin
@ -22,6 +23,9 @@ requalify_consts
loadWord
end
requalify_consts (in Arch)
deleteGhost
definition deleteRange :: "( machine_word , 'a ) DataMap.map \<Rightarrow> machine_word \<Rightarrow> nat \<Rightarrow> ( machine_word , 'a ) DataMap.map"
where "deleteRange m ptr bits \<equiv>
let inRange = (\<lambda> x. x && ((- mask bits) - 1) = fromPPtr ptr) in

5
spec/haskell/SEL4.cabal
View File

@ -124,6 +124,7 @@ Library
SEL4.Object.Instances.ARM
SEL4.Object.TCB.ARM
SEL4.Model.StateData.ARM
SEL4.Model.PSpace.ARM
SEL4.Machine.RegisterSet.ARM
SEL4.Machine.Hardware.ARM
@ -147,6 +148,7 @@ Library
SEL4.Object.VCPU.ARM
SEL4.Object.TCB.ARM
SEL4.Model.StateData.ARM
SEL4.Model.PSpace.ARM
SEL4.Machine.RegisterSet.ARM
SEL4.Machine.Hardware.ARM
@ -168,6 +170,7 @@ Library
SEL4.Object.IOPort.X64
SEL4.Object.TCB.X64
SEL4.Model.StateData.X64
SEL4.Model.PSpace.X64
SEL4.Machine.RegisterSet.X64
SEL4.Machine.Hardware.X64
@ -189,6 +192,7 @@ Library
SEL4.Object.Instances.RISCV64
SEL4.Object.TCB.RISCV64
SEL4.Model.StateData.RISCV64
SEL4.Model.PSpace.RISCV64
SEL4.Machine.RegisterSet.RISCV64
SEL4.Machine.Hardware.RISCV64
@ -211,6 +215,7 @@ Library
SEL4.Object.VCPU.AARCH64
SEL4.Object.TCB.AARCH64
SEL4.Model.StateData.AARCH64
SEL4.Model.PSpace.AARCH64
SEL4.Machine.RegisterSet.AARCH64
SEL4.Machine.Hardware.AARCH64

13
spec/haskell/src/SEL4/Model/PSpace.lhs
View File

@ -6,6 +6,14 @@
This module contains the data structure and operations for the physical memory model.
\begin{impdetails}
This module uses the C preprocessor to select a target architecture.
> {-# LANGUAGE CPP #-}
\end{impdetails}
> module SEL4.Model.PSpace (
> PSpace, newPSpace, initPSpace,
> PSpaceStorable,
@ -21,6 +29,8 @@ This module contains the data structure and operations for the physical memory m
% {-# BOOT-EXPORTS: PSpace #PRegion newPSpace #-}
> import Prelude hiding (Word)
> import qualified SEL4.Model.PSpace.TARGET as Arch
> import SEL4.Model.StateData
> import SEL4.Object.Structures
@ -241,7 +251,7 @@ No type checks are performed when deleting objects; "deleteObjects" simply delet
> let ps' = ps { psMap = map' }
> modify (\ks -> ks { ksPSpace = ps'})
Clear the ghost state for user pages and cnodes within the deleted range.
Clear the ghost state for user pages, cnodes, and arch-specific objects within the deleted range.
> modify (\ks -> ks { gsUserPages = (\x -> if inRange x
> then Nothing else gsUserPages ks x) })
@ -249,6 +259,7 @@ Clear the ghost state for user pages and cnodes within the deleted range.
> "Object deletion would split CNodes."
> modify (\ks -> ks { gsCNodes = (\x -> if inRange x
> then Nothing else gsCNodes ks x) })
> Arch.deleteGhost ptr bits
> stateAssert ksASIDMapSafe "Object deletion would leave dangling PD pointers"
In "deleteObjects" above, we assert "deletionIsSafe"; that is, that there are no pointers to these objects remaining elsewhere in the kernel state. Since we cannot easily check this in the Haskell model, we assume that it is always true; the assertion is strengthened during translation into Isabelle.

21
spec/haskell/src/SEL4/Model/PSpace/AARCH64.hs Normal file
View File

@ -0,0 +1,21 @@
--
-- Copyright 2023, Proofcraft Pty Ltd
--
-- SPDX-License-Identifier: GPL-2.0-only
--
-- This module contains architecture-specific code for PSpace, in particular
-- for potential ghost state updates when deleting objects.
module SEL4.Model.PSpace.AARCH64(deleteGhost) where
import Prelude hiding (Word)
import SEL4.Model.StateData
import SEL4.Machine.RegisterSet
deleteGhost :: PPtr a -> Int -> Kernel ()
deleteGhost ptr bits = do
let inRange = (\x -> x .&. ((- mask bits) - 1) == fromPPtr ptr)
ptTypes <- gets (gsPTTypes . ksArchState)
let ptTypes' = (\x -> if inRange x then Nothing else ptTypes x)
modify (\ks -> ks { ksArchState = (ksArchState ks) { gsPTTypes = ptTypes' } })

17
spec/haskell/src/SEL4/Model/PSpace/ARM.hs Normal file
View File

@ -0,0 +1,17 @@
--
-- Copyright 2023, Proofcraft Pty Ltd
--
-- SPDX-License-Identifier: GPL-2.0-only
--
-- This module contains architecture-specific code for PSpace, in particular
-- for potential ghost state updates when deleting objects.
module SEL4.Model.PSpace.ARM(deleteGhost) where
import Prelude hiding (Word)
import SEL4.Model.StateData
import SEL4.Machine.RegisterSet
deleteGhost :: PPtr a -> Int -> Kernel ()
deleteGhost ptr bits = return ()

17
spec/haskell/src/SEL4/Model/PSpace/RISCV64.hs Normal file
View File

@ -0,0 +1,17 @@
--
-- Copyright 2023, Proofcraft Pty Ltd
--
-- SPDX-License-Identifier: GPL-2.0-only
--
-- This module contains architecture-specific code for PSpace, in particular
-- for potential ghost state updates when deleting objects.
module SEL4.Model.PSpace.RISCV64(deleteGhost) where
import Prelude hiding (Word)
import SEL4.Model.StateData
import SEL4.Machine.RegisterSet
deleteGhost :: PPtr a -> Int -> Kernel ()
deleteGhost ptr bits = return ()

17
spec/haskell/src/SEL4/Model/PSpace/X64.hs Normal file
View File

@ -0,0 +1,17 @@
--
-- Copyright 2023, Proofcraft Pty Ltd
--
-- SPDX-License-Identifier: GPL-2.0-only
--
-- This module contains architecture-specific code for PSpace, in particular
-- for potential ghost state updates when deleting objects.
module SEL4.Model.PSpace.X64(deleteGhost) where
import Prelude hiding (Word)
import SEL4.Model.StateData
import SEL4.Machine.RegisterSet
deleteGhost :: PPtr a -> Int -> Kernel ()
deleteGhost ptr bits = return ()

5
spec/haskell/src/SEL4/Model/StateData/AARCH64.hs
View File

@ -12,7 +12,7 @@ module SEL4.Model.StateData.AARCH64 where
import Prelude hiding (Word)
import SEL4.Machine
import SEL4.Machine.Hardware.AARCH64 (PTE(..), config_ARM_PA_SIZE_BITS_40)
import SEL4.Machine.Hardware.AARCH64 (PTE(..), PT_Type, config_ARM_PA_SIZE_BITS_40)
import SEL4.Object.Structures.AARCH64
import Data.Array
@ -40,7 +40,8 @@ data KernelState = ARMKernelState {
-- used e.g. for user threads with missing or invalid VSpace root
armKSGlobalUserVSpace :: PPtr PTE,
armHSCurVCPU :: Maybe (PPtr VCPU, Bool),
armKSGICVCPUNumListRegs :: Int
armKSGICVCPUNumListRegs :: Int,
gsPTTypes :: Word -> Maybe PT_Type
}
-- counting from 0 at bottom, i.e. number of levels = maxPTLevel + 1;

9
spec/haskell/src/SEL4/Object/ObjectType/AARCH64.hs
View File

@ -158,6 +158,13 @@ placeNewDataObject regionBase sz isDevice = if isDevice
then placeNewObject regionBase UserDataDevice sz
else placeNewObject regionBase UserData sz
updatePTType :: PPtr () -> PT_Type -> Kernel ()
updatePTType p pt_t = do
ptTypes <- gets (gsPTTypes . ksArchState)
let funupd = (\f x v y -> if y == x then v else f y)
let ptTypes' = funupd ptTypes (fromPPtr p) (Just pt_t)
modify (\ks -> ks { ksArchState = (ksArchState ks) { gsPTTypes = ptTypes' } })
createObject :: ObjectType -> PPtr () -> Int -> Bool -> Kernel ArchCapability
createObject t regionBase _ isDevice =
let funupd = (\f x v y -> if y == x then v else f y) in
@ -189,10 +196,12 @@ createObject t regionBase _ isDevice =
Arch.Types.PageTableObject -> do
let ptSize = ptBits NormalPT_T - objBits (makeObject :: PTE)
placeNewObject regionBase (makeObject :: PTE) ptSize
updatePTType regionBase NormalPT_T
return $ PageTableCap (pointerCast regionBase) NormalPT_T Nothing
Arch.Types.VSpaceObject -> do
let ptSize = ptBits VSRootPT_T - objBits (makeObject :: PTE)
placeNewObject regionBase (makeObject :: PTE) ptSize
updatePTType regionBase VSRootPT_T
return $ PageTableCap (pointerCast regionBase) VSRootPT_T Nothing
Arch.Types.VCPUObject -> do
placeNewObject regionBase (makeObject :: VCPU) 0