Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Page allocator enhancements #36

Merged
merged 13 commits into from
Feb 12, 2024
Merged

Page allocator enhancements #36

merged 13 commits into from
Feb 12, 2024

Conversation

wojciechozga
Copy link
Member

This PR aims to improve the quality of page allocator implementation. The eventual goal is to reach an implementation that can be formally verified using RefinedRust.

Current changes include:

  • Renamed memory tracker to page allocator.
  • Reimplemented page allocator internal logic to simplify the reasoning about page token division and allocation.

@wojciechozga
Renamed memory tracker to page allocator. Reimplemented page allocato…
a7f8964 
…r internal logic to simplify the reasoning.

Signed-off-by: Wojciech Ozga <woz@zurich.ibm.com>
@wojciechozga wojciechozga added the enhancement New feature or request label Feb 9, 2024
@wojciechozga
Copy link
Member Author

@lgaeher please have a look at these changes and let me know what you think. I went for another implementation of the constructor that we discussed offline, i.e., I am using a vector instead of slice. Would that be fine?

We probably should use a sorted collection that stores page tokens due to our implementation of allocation (acquire_continous_pages_of_given_size).

@wojciechozga wojciechozga changed the title Page Allocator improvements Page Allocator enhancements Feb 9, 2024
@wojciechozga wojciechozga changed the title Page Allocator enhancements Page allocator enhancements Feb 9, 2024
@wojciechozga wojciechozga marked this pull request as draft February 9, 2024 13:22
@wojciechozga wojciechozga requested a review from lgaeher February 9, 2024 13:22
lgaeher
lgaeher reviewed Feb 9, 2024
View reviewed changes
Copy link
Collaborator

@lgaeher lgaeher left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!
The iteration over the vector in the constructor actually goes via slices, but I think that should be fine to handle, probably. It's definitely easier than dealing with the direct slice we had before.
I've left some minor comments, but otherwise looks good!

@wojciechozga wojciechozga assigned wojciechozga and unassigned lgaeher Feb 9, 2024
wojciechozga and others added 11 commits February 9, 2024 14:49
@wojciechozga @lgaeher
Update security-monitor/src/core/page_allocator/page_allocator.rs
a54c157 
Co-authored-by: Lennard Gäher <33029057+lgaeher@users.noreply.github.com>
@wojciechozga @lgaeher
Update security-monitor/src/core/page_allocator/page_allocator.rs
4071f5b 
Co-authored-by: Lennard Gäher <33029057+lgaeher@users.noreply.github.com>
@wojciechozga @lgaeher
Update security-monitor/src/core/page_allocator/page_allocator.rs
57b3e73 
Co-authored-by: Lennard Gäher <33029057+lgaeher@users.noreply.github.com>
@wojciechozga @lgaeher
Update security-monitor/src/core/page_allocator/page_allocator.rs
396da46 
Co-authored-by: Lennard Gäher <33029057+lgaeher@users.noreply.github.com>
@wojciechozga @lgaeher
Update security-monitor/src/core/page_allocator/page_allocator.rs
e5f18ab 
Co-authored-by: Lennard Gäher <33029057+lgaeher@users.noreply.github.com>
@wojciechozga @lgaeher
Update security-monitor/src/core/page_allocator/page_allocator.rs
431492d 
Co-authored-by: Lennard Gäher <33029057+lgaeher@users.noreply.github.com>
@wojciechozga @lgaeher
Update security-monitor/src/core/page_allocator/page_allocator.rs
832b094 
Co-authored-by: Lennard Gäher <33029057+lgaeher@users.noreply.github.com>
@wojciechozga @lgaeher
Update security-monitor/src/core/page_allocator/page_allocator.rs
d78c410 
Co-authored-by: Lennard Gäher <33029057+lgaeher@users.noreply.github.com>
@wojciechozga @lgaeher
Update security-monitor/src/core/page_allocator/page_allocator.rs
227344e 
Co-authored-by: Lennard Gäher <33029057+lgaeher@users.noreply.github.com>
@wojciechozga @lgaeher
Update security-monitor/src/core/page_allocator/page_allocator.rs
3a18cb6 
Co-authored-by: Lennard Gäher <33029057+lgaeher@users.noreply.github.com>
@wojciechozga
Changed the algorithm of creating page tokens to make sure that pages…
1c1eab9 
… are aligned to their size as required by the riscv spec

Signed-off-by: Wojciech Ozga <woz@zurich.ibm.com>
@wojciechozga wojciechozga marked this pull request as ready for review February 12, 2024 15:25
@wojciechozga
Copy link
Member Author

@lgaeher please have a look. The latest commit introduces the new algorithm for constructing page tokens over the given memory region.

lgaeher
lgaeher approved these changes Feb 12, 2024
View reviewed changes
Copy link
Collaborator

@lgaeher lgaeher left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good to me!

@wojciechozga
minor changes in comments
97b2231 
Signed-off-by: Wojciech Ozga <woz@zurich.ibm.com>
@wojciechozga wojciechozga merged commit f1f27d5 into main Feb 12, 2024
3 of 4 checks passed
@wojciechozga wojciechozga deleted the woz/memory_tracker_fixes branch February 20, 2024 09:09
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@lgaeher lgaeher lgaeher approved these changes

Assignees

@wojciechozga wojciechozga

Labels
enhancement New feature or request
Projects
None yet
Milestone
Formal verification of the memory man...
Development

Successfully merging this pull request may close these issues.
2 participants
@wojciechozga @lgaeher