Redesign frame allocation for easier formal verification (theseus-os#1004)

* A single type `Frames` is now used to represent all physical memory frames.
  * Each `Frames` object is globally unique, and ownership of one represents
    the exclusive capability to access those frames, e.g., map pages to them.

* The `Frames` struct is parameterized with a const generic enum that
  determines which state it is in, one of four `memory_structs::MemoryState`s:
  1. Free: the range of frames is free and is owned by the frame allocator.
     * `Frames<{MemoryState::Free}>` is type aliased to `FreeFrames`.
  2. Allocated: the range of frames has been allocated, and is owned by
     another entity outside of the frame allocator.
     * `Frames<{MemoryState::Allocated}>` is type aliased to `AllocatedFrames`,
       which replaces the previous struct of the same name.
  3. Mapped: the range of frames has been mapped by a range of virtual pages.
     * `Frames<{MemoryState::Mapped}>` is type aliased to `MappedFrames`,
       which is not yet used in the Theseus codebase.
  4. Unmapped: the range of frames has just been unmapped by a range
     of virtual pages, but has yet to be returned to the frame allocator.
     * `Frames<{MemoryState::Unmapped}>` is type aliased to `UnmappedFrames`,
       which is used as an intermediary step before transitioning back into 
       `AllocatedFrames`.
  * See the documentation of `Frames` for more info on state transitions:
    (Free) <---> (Allocated) --> (Mapped) --> (Unmapped) --> (Allocated) <---> (Free)

* `FreeFrames` is used in favor of `Chunk`. Note that the term "chunk" still
  appears in the code in order to minimize the sheer volume of tiny changes.

* Added a few new APIs to frame-related types, mostly for convenience:
  `split_at`, `split_range`, `contains_range`.

* Combined the `PhysicalMemoryRegion` and `Region` into a single type
  used across the entire frame allocator. 

* The core logic of the frame allocator has been changed to accommodate
  the new `Frames` type, which is a verified "true linear" type that cannot be 
  cloned or have its inner fields mutated.
  * The entire point of this redesigns is to make the frame allocator
    amenable to formal verification based on typestate analysis combined
    with Prusti-verifiable pre- and post-conditions for key functions.
  * Actual verification code and proofs of frame allocation correctness
    are coming soon in future PRs.

Co-authored-by: Kevin Boos <[email protected]>

Author: 2 people

kernel/frame_allocator/src/lib.rs

@@ -42,6 +42,11 @@ impl <T: Ord> Wrapper<T> {
             inner: value,
         })
     }
+
+	/// Returns the inner value, consuming this wrapper.
+	pub(crate) fn into_inner(self) -> T {
+		self.inner
+	}
 }
 
 

kernel/frame_allocator/src/static_array_rb_tree.rs

@@ -1,24 +1,19 @@
-//! Tests for the AllocatedFrames type, mainly the `split` method.
+//! Tests for the `Frames` type, mainly the `split` method.
 
 extern crate std;
 
 use self::std::dbg;
 
 use super::*;
 
-impl PartialEq for AllocatedFrames {
-    fn eq(&self, other: &Self) -> bool {
-        self.frames == other.frames
-    }
-}
-
-fn from_addr(start_addr: usize, end_addr: usize) -> AllocatedFrames {
-    AllocatedFrames {
-        frames: FrameRange::new(
+fn from_addr(start_addr: usize, end_addr: usize) -> FreeFrames {
+    FreeFrames::new(
+        MemoryRegionType::Free,
+        FrameRange::new(
             Frame::containing_address(PhysicalAddress::new_canonical(start_addr)),
             Frame::containing_address(PhysicalAddress::new_canonical(end_addr)),
         )
-    }
+    )
 }
 
 fn frame_addr(addr: usize) -> Frame {
@@ -30,7 +25,7 @@ fn split_before_beginning() {
     let original = from_addr( 0x4275000, 0x4285000);
     let split_at = frame_addr(0x4274000);
 
-    let result = original.split(split_at);
+    let result = original.split_at(split_at);
     dbg!(&result);
     assert!(result.is_err());
 }
@@ -42,11 +37,13 @@ fn split_at_beginning() {
     let first    = AllocatedFrames::empty();
     let second   = from_addr( 0x4275000, 0x4285000);
 
-    let result = original.split(split_at);
+    let result = original.split_at(split_at);
     dbg!(&result);
     let (result1, result2) = result.unwrap();
-    assert_eq!(result1, first);
-    assert_eq!(result2, second);
+    assert_eq!(result1.start(), first.start());
+    assert_eq!(result1.end(), first.end());
+    assert_eq!(result2.start(), second.start());
+    assert_eq!(result2.end(), second.end());
 }
 
 
@@ -57,11 +54,13 @@ fn split_at_middle() {
     let first    = from_addr( 0x4275000, 0x427C000);
     let second   = from_addr( 0x427D000, 0x4285000);
 
-    let result = original.split(split_at);
+    let result = original.split_at(split_at);
     dbg!(&result);
     let (result1, result2) = result.unwrap();
-    assert_eq!(result1, first);
-    assert_eq!(result2, second);
+    assert_eq!(result1.start(), first.start());
+    assert_eq!(result1.end(), first.end());
+    assert_eq!(result2.start(), second.start());
+    assert_eq!(result2.end(), second.end());
 }
 
 #[test]
@@ -71,11 +70,13 @@ fn split_at_end() {
     let first    = from_addr( 0x4275000, 0x4284000);
     let second   = from_addr( 0x4285000, 0x4285000);
 
-    let result = original.split(split_at);
+    let result = original.split_at(split_at);
     dbg!(&result);
     let (result1, result2) = result.unwrap();
-    assert_eq!(result1, first);
-    assert_eq!(result2, second);
+    assert_eq!(result1.start(), first.start());
+    assert_eq!(result1.end(), first.end());
+    assert_eq!(result2.start(), second.start());
+    assert_eq!(result2.end(), second.end());
 }
 
 
@@ -86,11 +87,13 @@ fn split_after_end() {
     let first    = from_addr( 0x4275000, 0x4285000);
     let second   = AllocatedFrames::empty();
 
-    let result = original.split(split_at);
+    let result = original.split_at(split_at);
     dbg!(&result);
     let (result1, result2) = result.unwrap();
-    assert_eq!(result1, first);
-    assert_eq!(result2, second);
+    assert_eq!(result1.start(), first.start());
+    assert_eq!(result1.end(), first.end());
+    assert_eq!(result2.start(), second.start());
+    assert_eq!(result2.end(), second.end());
 }
 
 
@@ -99,7 +102,7 @@ fn split_empty_at_zero() {
     let original = AllocatedFrames::empty();
     let split_at = frame_addr(0x0000);
 
-    let result = original.split(split_at);
+    let result = original.split_at(split_at);
     dbg!(&result);
     assert!(result.is_err());
 }
@@ -109,7 +112,7 @@ fn split_empty_at_one() {
     let original = AllocatedFrames::empty();
     let split_at = frame_addr(0x1000);
 
-    let result = original.split(split_at);
+    let result = original.split_at(split_at);
     dbg!(&result);
     assert!(result.is_err());
 }
@@ -119,7 +122,7 @@ fn split_empty_at_two() {
     let original = AllocatedFrames::empty();
     let split_at = frame_addr(0x2000);
 
-    let result = original.split(split_at);
+    let result = original.split_at(split_at);
     dbg!(&result);
     assert!(result.is_err());
 }
@@ -133,11 +136,13 @@ fn split_at_beginning_zero() {
     let first  = AllocatedFrames::empty();
     let second = from_addr(0x0, 0x5000);
 
-    let result = original.split(split_at);
+    let result = original.split_at(split_at);
     dbg!(&result);
     let (result1, result2) = result.unwrap();
-    assert_eq!(result1, first);
-    assert_eq!(result2, second);
+    assert_eq!(result1.start(), first.start());
+    assert_eq!(result1.end(), first.end());
+    assert_eq!(result2.start(), second.start());
+    assert_eq!(result2.end(), second.end());
 }
 
 #[test]
@@ -147,11 +152,13 @@ fn split_at_beginning_one() {
     let first    = from_addr( 0x0000, 0x0000);
     let second   = from_addr( 0x1000, 0x5000);
 
-    let result = original.split(split_at);
+    let result = original.split_at(split_at);
     dbg!(&result);
     let (result1, result2) = result.unwrap();
-    assert_eq!(result1, first);
-    assert_eq!(result2, second);
+    assert_eq!(result1.start(), first.start());
+    assert_eq!(result1.end(), first.end());
+    assert_eq!(result2.start(), second.start());
+    assert_eq!(result2.end(), second.end());
 }
 
 #[test]
@@ -161,11 +168,13 @@ fn split_at_beginning_max_length_one() {
     let first    = AllocatedFrames::empty();
     let second   = from_addr(0xFFFF_FFFF_FFFF_F000, 0xFFFF_FFFF_FFFF_F000);
 
-    let result = original.split(split_at);
+    let result = original.split_at(split_at);
     dbg!(&result);
     let (result1, result2) = result.unwrap();
-    assert_eq!(result1, first);
-    assert_eq!(result2, second);
+    assert_eq!(result1.start(), first.start());
+    assert_eq!(result1.end(), first.end());
+    assert_eq!(result2.start(), second.start());
+    assert_eq!(result2.end(), second.end());
 }
 
 #[test]
@@ -175,11 +184,13 @@ fn split_at_end_max_length_two() {
     let first    = from_addr( 0xFFFF_FFFF_FFFF_E000, 0xFFFF_FFFF_FFFF_E000);
     let second   = from_addr( 0xFFFF_FFFF_FFFF_F000, 0xFFFF_FFFF_FFFF_F000);
 
-    let result = original.split(split_at);
+    let result = original.split_at(split_at);
     dbg!(&result);
     let (result1, result2) = result.unwrap();
-    assert_eq!(result1, first);
-    assert_eq!(result2, second);
+    assert_eq!(result1.start(), first.start());
+    assert_eq!(result1.end(), first.end());
+    assert_eq!(result2.start(), second.start());
+    assert_eq!(result2.end(), second.end());
 }
 
 
@@ -190,11 +201,13 @@ fn split_after_end_max() {
     let first  =   from_addr( 0xFFFF_FFFF_FFFF_E000, 0xFFFF_FFFF_FFFF_E000);
     let second =   AllocatedFrames::empty();
 
-    let result = original.split(split_at);
+    let result = original.split_at(split_at);
     dbg!(&result);
     let (result1, result2) = result.unwrap();
-    assert_eq!(result1, first);
-    assert_eq!(result2, second);
+    assert_eq!(result1.start(), first.start());
+    assert_eq!(result1.end(), first.end());
+    assert_eq!(result2.start(), second.start());
+    assert_eq!(result2.end(), second.end());
 }
 
 #[test]
@@ -204,9 +217,11 @@ fn split_at_beginning_max() {
     let first    = AllocatedFrames::empty();
     let second   = from_addr(0xFFFF_FFFF_FFFF_E000, 0xFFFF_FFFF_FFFF_E000);
 
-    let result = original.split(split_at);
+    let result = original.split_at(split_at);
     dbg!(&result);
     let (result1, result2) = result.unwrap();
-    assert_eq!(result1, first);
-    assert_eq!(result2, second);
+    assert_eq!(result1.start(), first.start());
+    assert_eq!(result1.end(), first.end());
+    assert_eq!(result2.start(), second.start());
+    assert_eq!(result2.end(), second.end());
 }

kernel/frame_allocator/src/test.rs

@@ -36,6 +36,7 @@ pub use page_allocator::{
 };
 pub use frame_allocator::{
     AllocatedFrames,
+    UnmappedFrames,
     allocate_frames,
     allocate_frames_at,
     allocate_frames_by_bytes,

kernel/memory/src/lib.rs

@@ -18,7 +18,7 @@ use core::{
     slice,
 };
 use log::{error, warn, debug, trace};
-use crate::{BROADCAST_TLB_SHOOTDOWN_FUNC, VirtualAddress, PhysicalAddress, Page, Frame, FrameRange, AllocatedPages, AllocatedFrames}; 
+use crate::{BROADCAST_TLB_SHOOTDOWN_FUNC, VirtualAddress, PhysicalAddress, Page, Frame, FrameRange, AllocatedPages, AllocatedFrames, UnmappedFrames}; 
 use crate::paging::{
     get_current_p4,
     table::{P4, UPCOMING_P4, Table, Level4},
@@ -34,23 +34,23 @@ use owned_borrowed_trait::{OwnedOrBorrowed, Owned, Borrowed};
 #[cfg(target_arch = "x86_64")]
 use kernel_config::memory::ENTRIES_PER_PAGE_TABLE;
 
-/// This is a private callback used to convert `UnmappedFrames` into `AllocatedFrames`.
+/// This is a private callback used to convert `UnmappedFrameRange` into `UnmappedFrames`.
 /// 
 /// This exists to break the cyclic dependency cycle between `page_table_entry` and
 /// `frame_allocator`, which depend on each other as such:
-/// * `frame_allocator` needs to `impl Into<AllocatedPages> for UnmappedFrames`
+/// * `frame_allocator` needs to `impl Into<Frames> for UnmappedFrameRange`
 ///    in order to allow unmapped exclusive frames to be safely deallocated
 /// * `page_table_entry` needs to use the `AllocatedFrames` type in order to allow
 ///   page table entry values to be set safely to a real physical frame that is owned and exists.
 /// 
 /// To get around that, the `frame_allocator::init()` function returns a callback
-/// to its function that allows converting a range of unmapped frames back into `AllocatedFrames`,
+/// to its function that allows converting a range of unmapped frames back into `UnmappedFrames`,
 /// which then allows them to be dropped and thus deallocated.
 /// 
 /// This is safe because the frame allocator can only be initialized once, and also because
 /// only this crate has access to that function callback and can thus guarantee
-/// that it is only invoked for `UnmappedFrames`.
-pub(super) static INTO_ALLOCATED_FRAMES_FUNC: Once<fn(FrameRange) -> AllocatedFrames> = Once::new();
+/// that it is only invoked for `UnmappedFrameRange`.
+pub(super) static INTO_UNMAPPED_FRAMES_FUNC: Once<fn(FrameRange) -> UnmappedFrames> = Once::new();
 
 /// A convenience function to translate the given virtual address into a
 /// physical address using the currently-active page table.
@@ -610,8 +610,8 @@ impl MappedPages {
             );
         }   
 
-        let mut first_frame_range: Option<AllocatedFrames> = None; // this is what we'll return
-        let mut current_frame_range: Option<AllocatedFrames> = None;
+        let mut first_frame_range: Option<UnmappedFrames> = None; // this is what we'll return
+        let mut current_frame_range: Option<UnmappedFrames> = None;
 
         for page in self.pages.range().clone() {            
             let p1 = active_table_mapper.p4_mut()
@@ -631,8 +631,8 @@ impl MappedPages {
             // freed from the newly-unmapped P1 PTE entry above.
             match unmapped_frames {
                 UnmapResult::Exclusive(newly_unmapped_frames) => {
-                    let newly_unmapped_frames = INTO_ALLOCATED_FRAMES_FUNC.get()
-                        .ok_or("BUG: Mapper::unmap(): the `INTO_ALLOCATED_FRAMES_FUNC` callback was not initialized")
+                    let newly_unmapped_frames = INTO_UNMAPPED_FRAMES_FUNC.get()
+                        .ok_or("BUG: Mapper::unmap(): the `INTO_UNMAPPED_FRAMES_FUNC` callback was not initialized")
                         .map(|into_func| into_func(newly_unmapped_frames.deref().clone()))?;
 
                     if let Some(mut curr_frames) = current_frame_range.take() {
@@ -681,7 +681,8 @@ impl MappedPages {
         }
 
         // Ensure that we return at least some frame range, even if we broke out of the above loop early.
-        Ok(first_frame_range.or(current_frame_range))
+        Ok(first_frame_range.map(|f| f.into_allocated_frames())
+            .or(current_frame_range.map(|f| f.into_allocated_frames())))
     }
 
 

kernel/memory/src/paging/mapper.rs

@@ -30,7 +30,7 @@ use core::{
 use log::debug;
 use super::{
     Frame, FrameRange, PageRange, VirtualAddress, PhysicalAddress,
-    AllocatedPages, allocate_pages, AllocatedFrames, PteFlags,
+    AllocatedPages, allocate_pages, AllocatedFrames, UnmappedFrames, PteFlags,
     InitialMemoryMappings, tlb_flush_all, tlb_flush_virt_addr,
     get_p4, find_section_memory_bounds,
 };
@@ -223,11 +223,11 @@ pub fn get_current_p4() -> Frame {
 pub fn init(
     boot_info: &impl BootInformation,
     stack_start_virt: VirtualAddress,
-    into_alloc_frames_fn: fn(FrameRange) -> AllocatedFrames,
+    into_unmapped_frames_fn: fn(FrameRange) -> UnmappedFrames,
 ) -> Result<InitialMemoryMappings, &'static str> {
     // Store the callback from `frame_allocator::init()` that allows the `Mapper` to convert
-    // `page_table_entry::UnmappedFrames` back into `AllocatedFrames`.
-    mapper::INTO_ALLOCATED_FRAMES_FUNC.call_once(|| into_alloc_frames_fn);
+    // `page_table_entry::UnmappedFrameRange` back into `UnmappedFrames`.
+    mapper::INTO_UNMAPPED_FRAMES_FUNC.call_once(|| into_unmapped_frames_fn);
 
     // bootstrap a PageTable from the currently-loaded page table
     let mut page_table = PageTable::from_current()

kernel/memory/src/paging/mod.rs

@@ -7,19 +7,35 @@
 
 #![no_std]
 #![feature(step_trait)]
+#![allow(incomplete_features)]
+#![feature(adt_const_params)]
 
 use core::{
     cmp::{min, max},
     fmt,
     iter::Step,
-    ops::{Add, AddAssign, Deref, DerefMut, Sub, SubAssign}
+    marker::ConstParamTy,
+    ops::{Add, AddAssign, Deref, DerefMut, Sub, SubAssign},
 };
 use kernel_config::memory::{MAX_PAGE_NUMBER, PAGE_SIZE};
 use zerocopy::FromBytes;
 use paste::paste;
 use derive_more::*;
 use range_inclusive::{RangeInclusive, RangeInclusiveIterator};
 
+/// The possible states that a range of exclusively-owned pages or frames can be in.
+#[derive(PartialEq, Eq, ConstParamTy)]
+pub enum MemoryState {
+    /// Memory is free and owned by the allocator
+    Free,
+    /// Memory is allocated and can be used for a mapping
+    Allocated,
+    /// Memory is mapped (PTE has been set)
+    Mapped,
+    /// Memory has been unmapped (PTE has been cleared)
+    Unmapped
+}
+
 /// A macro for defining `VirtualAddress` and `PhysicalAddress` structs
 /// and implementing their common traits, which are generally identical.
 macro_rules! implement_address {
@@ -470,6 +486,13 @@ macro_rules! implement_page_frame_range {
                         None
                     }
                 }
+
+                #[doc = "Returns `true` if the `other` `" $TypeName "` is fully contained within this `" $TypeName "`."]
+                pub fn contains_range(&self, other: &$TypeName) -> bool {
+                    !other.is_empty()
+                    && (other.start() >= self.start())
+                    && (other.end() <= self.end())
+                }
             }
             impl fmt::Debug for $TypeName {
                 fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {