auxoncorp / ferros

A Rust-based userland which also adds compile-time assurances to seL4 development.
https://ferros.auxon.io/
Apache License 2.0
107 stars 11 forks source link

Make use of arch-specific address space granules #35

Open pittma opened 5 years ago

pittma commented 5 years ago
pittma commented 5 years ago

A thought that occurred to me when thinking about this: I think I'd like to type-alias granules.

// vspace.rs

type UnmappedPage<Kind> = UnmappedRegion<U12, Kind>;
type MappedPage<Kind> = MappedRegion<U12, Kind>;

#[cfg(target_arch = "aarch64")]
type UnmappedLargePage<Kind> = UnmappedRegion<U21, Kind>;
#[cfg(target_arch = "aarch64")]
type MappedLargePage<Kind> = MappedRegion<U21, Kind>;
// &c.

The reason for this is that I'd like to make all of arch pub(crate). When debating with myself on this, it occurrs to me that it's possible that this complicates mapping these regions in terms of what goes in the caps member of *Regions, but I like the notion of hiding arch things behind the region types. One possible solution is the use of existential types.

pittma commented 5 years ago

Actually, disregard that previous comment regarding type aliasing granules. The "I'd like to make all of arch pub(crate)" stands, though.

To hold on to the granule caps once we know how to map them, we can just use a Granule type from which we can retrieve the cptr, the vaddr, and call unmap on—that's what should go into the caps member of MappedMemoryRegion, not PageRange.

This all, of course, depends on us being able to actually map those granules which is still an open question.

pittma commented 5 years ago

I encountered a complication in the "recursive" mapping algorithm as it pertains to mapping larger memory granules. While we can ensure that mapping is possible through the recursion as an artifact of address alignment, we cannot, when unrolling that recursion, know when to stop at a specific layer and invoke the leaf-mapping syscall (seL4_<ARCH>_Page_Map). Doing so causes the Maps implementations to become more complex as they would need to discern what's being mapped, invoke the leaf mapper, and then signal to the caller that the recursion should stop.