arm+arm-hyp+aarch64 spec: defer cache flush in retype

Defer the cache flush done in untyped_reset (inside clearMemory) to the
actual retype call, and only flush for the object types where that is
needed.

See seL4/seL4#1289 for more detailed rationale.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

spec/abstract/AARCH64/ArchRetype_A.thy

@@ -24,9 +24,34 @@ definition reserve_region :: "obj_ref \<Rightarrow> nat \<Rightarrow> bool \<Rig
 
 text \<open>Initialise architecture-specific objects.\<close>
 
+definition vs_apiobj_size where
+  "vs_apiobj_size ty \<equiv>
+     case ty of
+       ArchObject SmallPageObj \<Rightarrow> pageBitsForSize ARMSmallPage
+     | ArchObject LargePageObj \<Rightarrow> pageBitsForSize ARMLargePage
+     | ArchObject HugePageObj \<Rightarrow> pageBitsForSize ARMHugePage
+     | ArchObject PageTableObj \<Rightarrow> table_size NormalPT_T
+     | ArchObject VSpaceObj \<Rightarrow> table_size VSRootPT_T"
+
 definition init_arch_objects ::
-  "apiobject_type \<Rightarrow> obj_ref \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> obj_ref list \<Rightarrow> (unit,'z::state_ext) s_monad" where
-  "init_arch_objects new_type ptr num_objects obj_sz refs \<equiv> return ()"
+  "apiobject_type \<Rightarrow> bool \<Rightarrow> obj_ref \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> obj_ref list \<Rightarrow> (unit,'z::state_ext) s_monad"
+  where
+  "init_arch_objects new_type is_device ptr num_objects obj_sz refs \<equiv>
+     if \<not>is_device \<and>
+        new_type \<in> {ArchObject SmallPageObj, ArchObject LargePageObj, ArchObject HugePageObj}
+     then
+       mapM_x (\<lambda>ref. do_machine_op $
+                       cleanCacheRange_RAM ref (ref + mask (vs_apiobj_size new_type))
+                                           (addrFromPPtr ref))
+              refs
+     else if new_type \<in> {ArchObject PageTableObj, ArchObject VSpaceObj}
+     then
+       mapM_x (\<lambda>ref. do_machine_op $
+                       cleanCacheRange_PoU ref (ref + mask (vs_apiobj_size new_type))
+                                           (addrFromPPtr ref))
+              refs
+     else
+       return ()"
 
 definition empty_context :: user_context where
   "empty_context \<equiv> UserContext (FPUState (\<lambda>_. 0) 0 0) (\<lambda>_. 0)"

spec/abstract/ARM/ArchRetype_A.thy

@@ -26,15 +26,38 @@ definition
 
 text \<open>Initialise architecture-specific objects.\<close>
 
-definition
-  init_arch_objects :: "apiobject_type \<Rightarrow> obj_ref \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> obj_ref list \<Rightarrow> (unit,'z::state_ext) s_monad"
-where
-  "init_arch_objects new_type ptr num_objects obj_sz refs
-    \<equiv> if new_type = ArchObject PageDirectoryObj then (do
-      mapM_x copy_global_mappings refs;
-      do_machine_op $ mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + ((1::word32) << pd_bits) - 1)
-                                                      (addrFromPPtr x)) refs
-    od) else return ()"
+definition vs_apiobj_size where
+  "vs_apiobj_size ty \<equiv>
+     case ty of
+       ArchObject SmallPageObj \<Rightarrow> pageBitsForSize ARMSmallPage
+     | ArchObject LargePageObj \<Rightarrow> pageBitsForSize ARMLargePage
+     | ArchObject SectionObj \<Rightarrow> pageBitsForSize ARMSection
+     | ArchObject SuperSectionObj \<Rightarrow> pageBitsForSize ARMSuperSection
+     | ArchObject PageTableObj \<Rightarrow> pt_bits
+     | ArchObject PageDirectoryObj \<Rightarrow> pd_bits"
+
+definition init_arch_objects ::
+  "apiobject_type \<Rightarrow> bool \<Rightarrow> obj_ref \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> obj_ref list \<Rightarrow> (unit,'z::state_ext) s_monad"
+  where
+  "init_arch_objects new_type is_device ptr num_objects obj_sz refs \<equiv> do
+     when (new_type = ArchObject PageDirectoryObj) $ mapM_x copy_global_mappings refs;
+     if \<not>is_device \<and>
+        new_type \<in> {ArchObject SmallPageObj, ArchObject LargePageObj,
+                    ArchObject SectionObj, ArchObject SuperSectionObj}
+     then
+       mapM_x (\<lambda>ref. do_machine_op $
+                       cleanCacheRange_RAM ref (ref + mask (vs_apiobj_size new_type))
+                                           (addrFromPPtr ref))
+              refs
+     else if new_type \<in> {ArchObject PageTableObj, ArchObject PageDirectoryObj}
+     then
+       mapM_x (\<lambda>ref. do_machine_op $
+                       cleanCacheRange_PoU ref (ref + mask (vs_apiobj_size new_type))
+                                           (addrFromPPtr ref))
+              refs
+     else
+       return ()
+   od"
 
 definition
   empty_context :: user_context where

spec/abstract/ARM_HYP/ArchRetype_A.thy

@@ -26,15 +26,38 @@ definition
 
 text \<open>Initialise architecture-specific objects.\<close>
 
-definition
-  init_arch_objects :: "apiobject_type \<Rightarrow> obj_ref \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> obj_ref list \<Rightarrow> (unit,'z::state_ext) s_monad"
-where
-  "init_arch_objects new_type ptr num_objects obj_sz refs
-    \<equiv> if new_type = ArchObject PageDirectoryObj then (do
-      mapM_x copy_global_mappings refs;
-      do_machine_op $ mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + ((1::word32) << pd_bits) - 1)
-                                                      (addrFromPPtr x)) refs
-    od) else return ()"
+definition vs_apiobj_size where
+  "vs_apiobj_size ty \<equiv>
+     case ty of
+       ArchObject SmallPageObj \<Rightarrow> pageBitsForSize ARMSmallPage
+     | ArchObject LargePageObj \<Rightarrow> pageBitsForSize ARMLargePage
+     | ArchObject SectionObj \<Rightarrow> pageBitsForSize ARMSection
+     | ArchObject SuperSectionObj \<Rightarrow> pageBitsForSize ARMSuperSection
+     | ArchObject PageTableObj \<Rightarrow> pt_bits
+     | ArchObject PageDirectoryObj \<Rightarrow> pd_bits"
+
+definition init_arch_objects ::
+  "apiobject_type \<Rightarrow> bool \<Rightarrow> obj_ref \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> obj_ref list \<Rightarrow> (unit,'z::state_ext) s_monad"
+  where
+  "init_arch_objects new_type is_device ptr num_objects obj_sz refs \<equiv> do
+     when (new_type = ArchObject PageDirectoryObj) $ mapM_x copy_global_mappings refs;
+     if \<not>is_device \<and>
+        new_type \<in> {ArchObject SmallPageObj, ArchObject LargePageObj,
+                    ArchObject SectionObj, ArchObject SuperSectionObj}
+     then
+       mapM_x (\<lambda>ref. do_machine_op $
+                       cleanCacheRange_RAM ref (ref + mask (vs_apiobj_size new_type))
+                                           (addrFromPPtr ref))
+              refs
+     else if new_type \<in> {ArchObject PageTableObj, ArchObject PageDirectoryObj}
+     then
+       mapM_x (\<lambda>ref. do_machine_op $
+                       cleanCacheRange_PoU ref (ref + mask (vs_apiobj_size new_type))
+                                           (addrFromPPtr ref))
+              refs
+     else
+       return ()
+   od"
 
 definition
   empty_context :: user_context where

spec/abstract/Retype_A.thy

@@ -189,7 +189,7 @@ doE
 
   \<comment> \<open>Create new objects.\<close>
   orefs \<leftarrow> retype_region retype_base (length slots) obj_sz new_type is_device;
-  init_arch_objects new_type retype_base (length slots) obj_sz orefs;
+  init_arch_objects new_type is_device retype_base (length slots) obj_sz orefs;
   sequence_x (map (create_cap new_type obj_sz src_slot is_device) (zip slots orefs))
 od odE"
 

spec/design/skel/AARCH64/ArchIntermediate_H.thy

@@ -21,6 +21,11 @@ private abbreviation (input)
         modify (\<lambda>ks. ks \<lparr> gsUserPages := (\<lambda> addr.
           if addr `~elem~` map fromPPtr addrs then Just pSize
           else gsUserPages ks addr)\<rparr>);
+        when (\<not>dev) $
+          mapM_x (\<lambda>addr. doMachineOp $
+                            cleanCacheRange_RAM addr
+                                                (addr + mask (pageBitsForSize pSize))
+                                                (addrFromPPtr addr)) addrs;
         return $ map (\<lambda>n. FrameCap  (PPtr (fromPPtr n)) VMReadWrite pSize dev Nothing) addrs
      od)"
 
@@ -35,6 +40,8 @@ private abbreviation (input)
                                            if addr `~elem~` map fromPPtr addrs then Just ptType
                                            else gsPTTypes (ksArchState ks) addr)\<rparr>\<rparr>);
       initialiseMappings pts;
+      mapM_x (\<lambda>addr. doMachineOp $
+                       cleanCacheRange_PoU addr (addr + mask tableBits) (addrFromPPtr addr)) addrs;
       return $ map (\<lambda>pt. cap pt Nothing) pts
     od)"
 
@@ -59,7 +66,7 @@ defs Arch_createNewCaps_def:
               (\<lambda>pts. return ())
         | VCPUObject \<Rightarrow> (do
             addrs \<leftarrow> createObjects regionBase numObjects (injectKO (makeObject :: vcpu)) 0;
-            return $ map (\<lambda> addr. VCPUCap addr) addrs
+            return $ map (\<lambda>addr. VCPUCap addr) addrs
             od)
         )"
 

spec/design/skel/ARM/ArchIntermediate_H.thy

@@ -20,6 +20,11 @@ private abbreviation (input)
         modify (\<lambda>ks. ks \<lparr> gsUserPages := (\<lambda> addr.
           if addr `~elem~` map fromPPtr addrs then Just pSize
           else gsUserPages ks addr)\<rparr>);
+        when (\<not>dev) $
+          mapM_x (\<lambda>addr. doMachineOp $
+                            cleanCacheRange_RAM addr
+                                                (addr + mask (pageBitsForSize pSize))
+                                                (addrFromPPtr addr)) addrs;
         return $ map (\<lambda>n. PageCap dev (PPtr (fromPPtr n)) VMReadWrite pSize Nothing) addrs
      od)"
 
@@ -29,6 +34,8 @@ private abbreviation (input)
       addrs \<leftarrow> createObjects regionBase numObjects (injectKO objectProto) tableSize;
       pts \<leftarrow> return (map (PPtr \<circ> fromPPtr) addrs);
       initialiseMappings pts;
+      mapM_x (\<lambda>addr. doMachineOp $
+                       cleanCacheRange_PoU addr (addr + mask tableBits) (addrFromPPtr addr)) addrs;
       return $ map (\<lambda>pt. cap pt Nothing) pts
     od)"
 
@@ -51,10 +58,7 @@ defs Arch_createNewCaps_def:
         | PageDirectoryObject \<Rightarrow>
             createNewTableCaps regionBase numObjects pdBits (makeObject::pde) PageDirectoryCap
               (\<lambda>pds. do objSize \<leftarrow> return (((1::nat) `~shiftL~` pdBits));
-                        mapM_x copyGlobalMappings pds;
-                        doMachineOp $ mapM_x (\<lambda>x. cleanCacheRange_PoU x
-                                                    (x + (fromIntegral objSize) - 1)
-                                                    (addrFromPPtr x)) pds
+                        mapM_x copyGlobalMappings pds
                      od)
         )"
 

spec/design/skel/ARM_HYP/ArchIntermediate_H.thy

@@ -20,6 +20,11 @@ private abbreviation (input)
         modify (\<lambda>ks. ks \<lparr> gsUserPages := (\<lambda> addr.
           if addr `~elem~` map fromPPtr addrs then Just pSize
           else gsUserPages ks addr)\<rparr>);
+        when (\<not>dev) $
+          mapM_x (\<lambda>addr. doMachineOp $
+                            cleanCacheRange_RAM addr
+                                                (addr + mask (pageBitsForSize pSize))
+                                                (addrFromPPtr addr)) addrs;
         return $ map (\<lambda>n. PageCap dev (PPtr (fromPPtr n)) VMReadWrite pSize Nothing) addrs
      od)"
 
@@ -29,6 +34,8 @@ private abbreviation (input)
       addrs \<leftarrow> createObjects regionBase numObjects (injectKO objectProto) tableSize;
       pts \<leftarrow> return (map (PPtr \<circ> fromPPtr) addrs);
       initialiseMappings pts;
+      mapM_x (\<lambda>addr. doMachineOp $
+                       cleanCacheRange_PoU addr (addr + mask tableBits) (addrFromPPtr addr)) addrs;
       return $ map (\<lambda>pt. cap pt Nothing) pts
     od)"
 
@@ -51,14 +58,11 @@ defs Arch_createNewCaps_def:
         | PageDirectoryObject \<Rightarrow>
             createNewTableCaps regionBase numObjects pdBits (makeObject::pde) PageDirectoryCap
               (\<lambda>pds. do objSize \<leftarrow> return (((1::nat) `~shiftL~` pdBits));
-                        mapM_x copyGlobalMappings pds;
-                        doMachineOp $ mapM_x (\<lambda>x. cleanCacheRange_PoU x
-                                                    (x + (fromIntegral objSize) - 1)
-                                                    (addrFromPPtr x)) pds
+                        mapM_x copyGlobalMappings pds
                      od)
         | VCPUObject \<Rightarrow> (do
             addrs \<leftarrow> createObjects regionBase numObjects (injectKO (makeObject :: vcpu)) 0;
-            return $ map (\<lambda> addr. VCPUCap addr) addrs
+            return $ map (\<lambda>addr. VCPUCap addr) addrs
             od)
         )"
 

spec/haskell/src/SEL4/Object/ObjectType/AARCH64.hs

@@ -177,31 +177,51 @@ createObject t regionBase _ isDevice =
             modify (\ks -> ks { gsUserPages =
               funupd (gsUserPages ks)
                      (fromPPtr regionBase) (Just ARMSmallPage)})
+            when (not isDevice) $ doMachineOp $
+                cleanCacheRange_RAM (VPtr $ fromPPtr regionBase)
+                    (VPtr $ fromPPtr regionBase + mask (pageBitsForSize ARMSmallPage))
+                    (addrFromPPtr regionBase)
             return $ FrameCap (pointerCast regionBase)
                   VMReadWrite ARMSmallPage isDevice Nothing
         Arch.Types.LargePageObject -> do
             placeNewDataObject regionBase (ptTranslationBits NormalPT_T) isDevice
             modify (\ks -> ks { gsUserPages =
               funupd (gsUserPages ks)
                      (fromPPtr regionBase) (Just ARMLargePage)})
+            when (not isDevice) $ doMachineOp $
+                cleanCacheRange_RAM (VPtr $ fromPPtr regionBase)
+                    (VPtr $ fromPPtr regionBase + mask (pageBitsForSize ARMLargePage))
+                    (addrFromPPtr regionBase)
             return $ FrameCap (pointerCast regionBase)
                   VMReadWrite ARMLargePage isDevice Nothing
         Arch.Types.HugePageObject -> do
             placeNewDataObject regionBase (2*ptTranslationBits NormalPT_T) isDevice
             modify (\ks -> ks { gsUserPages =
               funupd (gsUserPages ks)
                      (fromPPtr regionBase) (Just ARMHugePage)})
+            when (not isDevice) $ doMachineOp $
+                cleanCacheRange_RAM (VPtr $ fromPPtr regionBase)
+                    (VPtr $ fromPPtr regionBase + mask (pageBitsForSize ARMHugePage))
+                    (addrFromPPtr regionBase)
             return $ FrameCap (pointerCast regionBase)
                   VMReadWrite ARMHugePage isDevice Nothing
         Arch.Types.PageTableObject -> do
             let ptSize = ptBits NormalPT_T - objBits (makeObject :: PTE)
             placeNewObject regionBase (makeObject :: PTE) ptSize
             updatePTType regionBase NormalPT_T
+            doMachineOp $
+                cleanCacheRange_PoU (VPtr $ fromPPtr regionBase)
+                    (VPtr $ fromPPtr regionBase + mask (ptBits NormalPT_T))
+                    (addrFromPPtr regionBase)
             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
+            doMachineOp $
+                cleanCacheRange_PoU (VPtr $ fromPPtr regionBase)
+                    (VPtr $ fromPPtr regionBase + mask (ptBits VSRootPT_T))
+                    (addrFromPPtr regionBase)
             return $ PageTableCap (pointerCast regionBase) VSRootPT_T Nothing
         Arch.Types.VCPUObject -> do
             placeNewObject regionBase (makeObject :: VCPU) 0

spec/haskell/src/SEL4/Object/ObjectType/ARM.lhs

@@ -218,12 +218,20 @@ Create an architecture-specific object.
 >             modify (\ks -> ks { gsUserPages =
 >               funupd (gsUserPages ks)
 >                      (fromPPtr regionBase) (Just ARMSmallPage)})
+>             when (not isDevice) $ doMachineOp $
+>                 cleanCacheRange_RAM (VPtr $ fromPPtr regionBase)
+>                     (VPtr $ fromPPtr regionBase + mask (pageBitsForSize ARMSmallPage))
+>                     (addrFromPPtr regionBase)
 >             return $ mkPageCap ARMSmallPage
 >         Arch.Types.LargePageObject -> do
 >             placeNewDataObject regionBase 4 isDevice
 >             modify (\ks -> ks { gsUserPages =
 >               funupd (gsUserPages ks)
 >                      (fromPPtr regionBase) (Just ARMLargePage)})
+>             when (not isDevice) $ doMachineOp $
+>                 cleanCacheRange_RAM (VPtr $ fromPPtr regionBase)
+>                     (VPtr $ fromPPtr regionBase + mask (pageBitsForSize ARMLargePage))
+>                     (addrFromPPtr regionBase)
 >             return $ mkPageCap ARMLargePage
 >         Arch.Types.SectionObject -> do
 #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
@@ -234,6 +242,10 @@ Create an architecture-specific object.
 >             modify (\ks -> ks { gsUserPages =
 >               funupd (gsUserPages ks)
 >                      (fromPPtr regionBase) (Just ARMSection)})
+>             when (not isDevice) $ doMachineOp $
+>                 cleanCacheRange_RAM (VPtr $ fromPPtr regionBase)
+>                     (VPtr $ fromPPtr regionBase + mask (pageBitsForSize ARMSection))
+>                     (addrFromPPtr regionBase)
 >             return $ mkPageCap ARMSection
 >         Arch.Types.SuperSectionObject -> do
 #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
@@ -244,19 +256,26 @@ Create an architecture-specific object.
 >             modify (\ks -> ks { gsUserPages =
 >               funupd (gsUserPages ks)
 >                      (fromPPtr regionBase) (Just ARMSuperSection)})
+>             when (not isDevice) $ doMachineOp $
+>                 cleanCacheRange_RAM (VPtr $ fromPPtr regionBase)
+>                     (VPtr $ fromPPtr regionBase + mask (pageBitsForSize ARMSuperSection))
+>                     (addrFromPPtr regionBase)
 >             return $ mkPageCap ARMSuperSection
 >         Arch.Types.PageTableObject -> do
 >             let ptSize = ptBits - objBits (makeObject :: PTE)
 >             placeNewObject regionBase (makeObject :: PTE) ptSize
+>             doMachineOp $
+>                 cleanCacheRange_PoU (VPtr $ fromPPtr regionBase)
+>                     (VPtr $ fromPPtr regionBase + mask ptBits)
+>                     (addrFromPPtr regionBase)
 >             return $ PageTableCap (pointerCast regionBase) Nothing
 >         Arch.Types.PageDirectoryObject -> do
 >             let pdSize = pdBits - objBits (makeObject :: PDE)
->             let regionSize = (1 `shiftL` pdBits)
 >             placeNewObject regionBase (makeObject :: PDE) pdSize
 >             copyGlobalMappings (pointerCast regionBase)
 >             doMachineOp $
 >                 cleanCacheRange_PoU (VPtr $ fromPPtr regionBase)
->                       (VPtr $ fromPPtr regionBase + regionSize - 1)
+>                       (VPtr $ fromPPtr regionBase + mask pdBits)
 >                       (addrFromPPtr regionBase)
 >             return $ PageDirectoryCap (pointerCast regionBase) Nothing
 #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT

spec/machine/AARCH64/MachineOps.thy

@@ -414,12 +414,10 @@ lemmas cache_machine_op_defs =
 
 subsection "Clearing Memory"
 
-text \<open>Clear memory contents to recycle it as user memory\<close>
+text \<open>Clear memory contents to recycle it as user memory. Do not yet flush the cache.\<close>
 definition clearMemory :: "machine_word \<Rightarrow> nat \<Rightarrow> unit machine_monad" where
-  "clearMemory ptr bytelength \<equiv> do
-     mapM_x (\<lambda>p. storeWord p 0) [ptr, ptr + word_size .e. ptr + (of_nat bytelength) - 1];
-     cleanCacheRange_RAM ptr (ptr + of_nat bytelength - 1) (addrFromPPtr ptr)
-   od"
+  "clearMemory ptr bytelength \<equiv>
+     mapM_x (\<lambda>p. storeWord p 0) [ptr, ptr + word_size .e. ptr + (of_nat bytelength) - 1]"
 
 text \<open>Haskell simulator interface stub.\<close>
 definition clearMemoryVM :: "machine_word \<Rightarrow> nat \<Rightarrow> unit machine_monad" where