Require an `AllocatedFrame` in order to set the frame value of a `PageTableEntry`

[kevinaboos]

[kevinaboos]

Not yet finished. Posting for @Ramla-I to review and brainstorm a solution to the need for an AllocatedFrame to set up a new recursive P4 mapping when creating a new PageTable

[Ramla-I]

The simplest solution I could think of was to separate TemporaryPage (TP) from MappedPages (MP) so that TP stores both the AP and AF after the mapping (this can be done because a TP always uses 1 frame). Then add a TP method which casts it into a page table and updates the 510th entry with the stored AF. We could add a runtime check that the current P4 is not equal to the TP frame. The drawback is having repetitive code for TP and MP, but:

• the TP code is specialized to only one type (PageTable) so we could probably remove all of the checks found in as_type_mut.
• map_allocated_pages_to can be split up into two functions, the first one is private and returns both the mapped AllocatedPages and AllocatedFrames which can also be used by TP.

The problem at the end of the day is trying to add a mapping for the same frame to two page tables. That doesn't break a MP invariant, but any generic solution I could think of was very complicated. Since we don't intend for Theseus to become a MAS OS, it doesn't seem worth it to implement a generic solution where we keep track of the Page Tables that each frame has already been added to.

[kevinaboos]

Yep, I was hesitant to reach a similar conclusion, but at this point I can't see a different way around it.

The problem at the end of the day is trying to add a mapping for the same frame to two page tables. That doesn't break a MP invariant

Hmm, doesn't it? That breaks the most fundamental invariant, bijectiveness, right?

any generic solution I could think of was very complicated

Can you share them to see if any are worth entertaining?

[Ramla-I]

yes, actually I agree. I was thinking the invariant is bijective mapping per page table, but that could violate many type and memory safety guarantees. So cross that.

For the second point, there was no full-fledged design. Just various thoughts.

• If we wanted to use APs in multiple page tables, we would have to store the page table information in each AP. Then compile time-checks would become runtime checks to make sure pages aren't used more than once per page table.
• AFs would have to be transformed to a type that prevents writable mappings to make sure they could be shared among multiple page tables.
• None of this solves the temporary page problem because that requires two writable mappings for the same frame, which is inherently not allowed.