Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Redesign frame allocation for easier formal verification (#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 <kevinaboos@gmail.com> 0dd9dc6- Loading branch information
1 parent
b222fcc
commit 03507c3