Frame allocator changes #1004

Ramla-I · 2023-07-06T19:07:25Z

Merged Chunk and AllocatedFrames into a single type Frames with two states: Unmapped and Mapped. The frame allocator is responsible for make sure a Frames object has no overlap.
Created a Region type used just for bookkeeping.
Changed the core allocation functions to remove Frames objects from the free list before allocating from it (since we can no longer clone a Frames).
For code local to the frame allocator, I changed all references to AllocatedFrames to UnmappedFrames, but for all public functions I kept the AllocatedFrames terminology.
I also kept the word "chunk" in comments and function definitions rather than changing it everywhere to "frames" to keep the changes minimal.

Questions:

Can we combine PhysicalMemoryRegion and Region? They contain the same information, but Region has additional trait implementations.
I've added comments in the code for a few specific questions.

kernel/frame_allocator/src/lib.rs

kevinaboos

This is just a partial review so you can get started addressing some of my comments without having to wait too long for more feedback.

My main concern is that the term UnmappedFrames or Frames<{FrameState::Unmapped}> is misleading, or at the very least, quite easy for readers to misunderstand. It makes it sound like those frames were previously mapped and we just unmapped them; in fact, that's how the term has been used thus far, e.g., in the page_table_entry crate. I'd be interested to hear your thoughts on this; perhaps we can brainstorm another term.

Similarly, there isn't a FrameState variant that differentiates between "free" (un-allocated) and "unmapped" (allocated). I find that to be confusing, as one would expect there to be a series of changes in state when going from Mapped --> Unmapped --> Free.

Another minor concern is that Frames<{FrameState::Unmapped}> is ugly to read and definitely hard for newcomers to understand, especially considering that that const enum variant syntax isn't even stable. Let's define typedef aliases for these states and use them everywhere, including within the frame allocator itself.

Merged Chunk and AllocatedFrames into a single type Frames with two states: Unmapped and Mapped. The frame allocator is responsible for make sure a Frames object has no overlap.

This is generally fine. It's a bit weird that "chunk" is still used prolifically throughout the frame allocator, but I see that you did that on purpose to minimize changes. We can always refactor that later.

Created a Region type used just for bookkeeping.

Nice, I like this.

Changed the core allocation functions to remove Frames objects from the free list before allocating from it (since we can no longer clone a Frames).

This is inefficient, right? In my mind we should be able to avoid this, since we only need to split it rather than clone it... right?

For code local to the frame allocator, I changed all references to AllocatedFrames to UnmappedFrames, but for all public functions I kept the AllocatedFrames terminology.

Sure, fine for now I guess. I'd still like to decide on one term or typedef alias that we can use everywhere, as I said above.

Questions:

Can we combine PhysicalMemoryRegion and Region? They contain the same information, but Region has additional trait implementations.

Yep, good idea! Let's use the term PhysicalMemoryRegion since it's much more descriptive than Region.

I've added comments in the code for a few specific questions.

Thanks, I responded to them.

kernel/frame_allocator/src/lib.rs

Ramla-I · 2023-07-07T17:44:02Z

Changed the core allocation functions to remove Frames objects from the free list before allocating from it (since we can no longer clone a Frames).

This is inefficient, right? In my mind we should be able to avoid this, since we only need to split it rather than clone it... right?

In the original design, a clone of the chosen Chunk and the reference to the Chunk in the rb-tree would be passed to the allocate_from_chosen_chunk function, where the cloned Chunk would be split and then the Chunk in the rb-tree would be removed.
The way I see it, I'm simply reversing the steps: removing the Frames object first and then splitting it, with additional steps to extract the Frames from its wrapper.

Also, I did consider the design where we split/ merged the chunk while it's still stored in the tree as that could be useful when merging contiguous Frames objects, but I don't think we can gain mutable access to an element in the tree. The CursorMut only has a get() method, no get_mut() method. I assume that's because changing the element can mess up the ordering of the rb-tree.

Though, rb-tree already has functions like replace_with, insert_after, etc, that rely on the user to maintain ordering, so we could add our own get_mut function.

kevinaboos · 2023-07-07T20:34:44Z

ah, oops -- i made a change to the page allocator to use replace_with() for that purpose, as in 99% of cases, we can just add on the deallocated page range to an existing chunk.

I just didn't apply that to the frame allocator yet, so I was mis-remembering what the Drop impl of AllocatedFrames did. Sorry!

Anyway, take a look at the Drop implementation for AllocatedPages, you'll see what I did there and how it can be much more efficient. Do let me know if that approach isn't compatible with the new Frames type due to trait limitations or linear typing restrictions.

kevinaboos · 2023-07-19T21:59:54Z

Can we move the various new functions from Frames into a "lower-level" type, perhaps FrameRange or maybe even RangeInclusive (assuming you can still get Prusti to work therein)? The functions I'm referring to are things like merge, split, split_at, split_range, contains_range, etc.

kernel/frame_allocator/Cargo.toml

Ramla-I · 2023-07-21T19:16:38Z

New Changes:

4 typestates (Free, Allocated, Mapped, Unmapped)
added get_mut to the rbtree implementation, which allows use to merge frames in the drop handler... we could use replace_with but then we'd have to replace with an empty frames, merge, and then replace the merged chunk back in.
changed the name of page_table_entry::UnmappedFrames to page_table_entry::UnmappedFramesInfo since UnmappedFrames is now a typestate. Now the call back creates an UnmappedFrames from UnmappedFramesInfo

kevinaboos

Based on our slack discussion, let's revert back to using replace_with() until we have confirmation from intrusive-rs maintainers that adding a get_mut() cursor API is okay/sound.

I love the new naming conventions in the frame allocator, they're much clearer! Nice. (I'm referring to things like UnmappedFrames, FreeFrames instead of Chunk, PhysicalMemoryRegion, etc.

PhysicalMemoryRegion and its docs are perfectly done, very nice!

One thing about your comment:

changed the name of page_table_entry::UnmappedFrames to page_table_entry::UnmappedFramesInfo since UnmappedFrames is now a typestate. Now the call back creates an UnmappedFrames from UnmappedFramesInfo

Agreed on the need for this name change; however, let's go with something like UnmappedFrameRange instead of "info" because "info" implies it's some kind of contextual metadata or something, not the actual frames that were unmapped.

Note that I haven't yet deeply reviewed the changes to the internal frame allocator logic itself, i.e., find_specific_chunk(), find_any_chunk(), allocate_from_chosen_chunk(), etc.

I'm still not a huge fan of the redesign regarding allocate_from_chosen_chunk() in which you always remove a chunk from the list and then re-add it.... I know we previously discussed this briefly during a meeting, but I can't remember what the resolution was.
We can re-discuss this again once your changes to remove get_mut() usage are in. At that point, I will do a deep review of the actual logic changes in frame allocation, and hopefully we can go through them together in person to speed up my understanding of the changes.

kernel/frame_allocator/src/lib.rs

kernel/memory_structs/src/lib.rs

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

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

kevinaboos · 2023-07-24T22:04:48Z

Thanks, looks good. I can confirm that everything except the changes to the internal frame allocation logic are approved now. I'll review the inner details of the frame allocation logic changes soon.

kevinaboos · 2023-07-24T22:05:24Z

(Also i made a few minor changes here and there, make sure to pull those down before you push any other changes)

Ramla-I · 2023-07-24T22:12:20Z

Thanks, looks good. I can confirm that everything except the changes to the internal frame allocation logic are approved now. I'll review the inner details of the frame allocation logic changes soon.

Thanks for the review. lmk if you would like to go through those changes together over zoom.

kevinaboos

Full review of internal logic is complete. I left some comments.

There are still some more efficiency improvements that can be made, but I didn't want to overburden you with too many nitpicky comments. I don't think we should bother addressing them until after the verification-related changes are merged in, since that will likely change the code structure even further.

kernel/frame_allocator/src/lib.rs

…mes methods

kernel/frame_allocator/src/lib.rs

kevinaboos

woot, finally made it! The first step to pushing verified code up to the mainline!

Thanks very much! 🎉

kevinaboos · 2023-07-27T23:46:22Z

kernel/frame_allocator/src/lib.rs

-                    frames: self.frames.clone(),
-                };
+                let frames = core::mem::replace(&mut self.frames, FrameRange::empty());  
+                let free_frames: FreeFrames = Frames { typ: self.typ, frames };

                let mut list = if free_frames.typ == MemoryRegionType::Reserved {


this is fine for now, but in a future PR we should log an error and return early if we encounter an Unknown type here.

* 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]> 0dd9dc6

…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]> 0dd9dc6

…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]>

Ramla-I added 8 commits July 6, 2023 12:40

added frames typestate, just finalizing chunk finding functions

3d4d28e

runs

34c2d8e

runs and tests pass

b78dc4e

moved frames to lib.rs

14fea3e

removed frames file

bd0a7a5

comments

dbcf462

comments

52ce8c3

comments and clippy errors

e5ec8f5

Ramla-I commented Jul 6, 2023

View reviewed changes

kernel/frame_allocator/src/lib.rs Outdated Show resolved Hide resolved

Ramla-I commented Jul 6, 2023

View reviewed changes

kernel/frame_allocator/src/lib.rs Outdated Show resolved Hide resolved

Ramla-I commented Jul 6, 2023

View reviewed changes

kernel/frame_allocator/src/lib.rs Outdated Show resolved Hide resolved

Ramla-I requested a review from kevinaboos July 6, 2023 19:30

kevinaboos requested changes Jul 6, 2023

View reviewed changes

Ramla-I added 5 commits July 17, 2023 16:09

pr changes

2c0e482

PR issues

c57aa16

tests

69943bb

moved frame state to memory structs

21f2b38

added unmapped frames

69d246d

PR changes

0dfbc98

Ramla-I commented Jul 21, 2023

View reviewed changes

kernel/frame_allocator/Cargo.toml Outdated Show resolved Hide resolved

Ramla-I added 2 commits July 21, 2023 15:02

comments

45e3a30

comments and cleanup

4c8d2ed

kevinaboos requested changes Jul 22, 2023

View reviewed changes

Ramla-I and others added 3 commits July 24, 2023 11:38

Update kernel/frame_allocator/src/lib.rs

906a7b3

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

Update kernel/frame_allocator/src/lib.rs

2d4987e

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

Update kernel/frame_allocator/src/lib.rs

6abc6aa

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

Ramla-I and others added 14 commits July 24, 2023 11:41

Update kernel/memory_structs/src/lib.rs

c6ce7ce

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

Update kernel/frame_allocator/src/lib.rs

dc40d1f

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

Update kernel/memory_structs/src/lib.rs

01fd398

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

Update kernel/frame_allocator/src/lib.rs

b786c22

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

Update kernel/frame_allocator/src/lib.rs

ea87a4a

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

Update kernel/frame_allocator/src/lib.rs

cc822c6

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

Update kernel/frame_allocator/src/lib.rs

58d25aa

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

small changes

66c0b26

changed UnmappedFramesInfo to UnmappedFrameRange

a9ac710

drop handler log statements

8639f12

pr comments

7a6e458

spacing

53a14b3

improve formatting

6f75236

clarify Frames docs

a77b8b9

kevinaboos mentioned this pull request Jul 24, 2023

Attempt to remove runtime match statement for Frames const generic state #1017

Closed

improve clarity of docs / drop handler

00cc97f

fix formatting, use proper early return pattern

42f7d84

kevinaboos requested changes Jul 25, 2023

View reviewed changes

Ramla-I added 3 commits July 25, 2023 16:20

comments

43ecf9f

make sure two frames objects never have the same range within the Fra…

0d8ede6

…mes methods

drop handler uses remove rather than replace_with

cb1ec40

Ramla-I commented Jul 27, 2023

View reviewed changes

kernel/frame_allocator/src/lib.rs Show resolved Hide resolved

kevinaboos approved these changes Jul 27, 2023

View reviewed changes

kevinaboos merged commit 0dd9dc6 into theseus-os:theseus_main Jul 28, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Frame allocator changes #1004

Frame allocator changes #1004

Ramla-I commented Jul 6, 2023 •

edited

Loading

kevinaboos left a comment

Ramla-I commented Jul 7, 2023 •

edited

Loading

kevinaboos commented Jul 7, 2023

kevinaboos commented Jul 19, 2023

Ramla-I commented Jul 21, 2023

kevinaboos left a comment

kevinaboos commented Jul 24, 2023

kevinaboos commented Jul 24, 2023

Ramla-I commented Jul 24, 2023

kevinaboos left a comment

kevinaboos left a comment

kevinaboos Jul 27, 2023

Frame allocator changes #1004

Frame allocator changes #1004

Conversation

Ramla-I commented Jul 6, 2023 • edited Loading

kevinaboos left a comment

Choose a reason for hiding this comment

Ramla-I commented Jul 7, 2023 • edited Loading

kevinaboos commented Jul 7, 2023

kevinaboos commented Jul 19, 2023

Ramla-I commented Jul 21, 2023

kevinaboos left a comment

Choose a reason for hiding this comment

kevinaboos commented Jul 24, 2023

kevinaboos commented Jul 24, 2023

Ramla-I commented Jul 24, 2023

kevinaboos left a comment

Choose a reason for hiding this comment

kevinaboos left a comment

Choose a reason for hiding this comment

kevinaboos Jul 27, 2023

Choose a reason for hiding this comment

Ramla-I commented Jul 6, 2023 •

edited

Loading

Ramla-I commented Jul 7, 2023 •

edited

Loading