The aim of this milestone is to design and implement simple frame-based memory management as a precursor to providing page-based virtual memory to sos applications.
The design differs from a native design as you must understand the initial state of the system when SOS gets control as the inital seL4 task, and you must work with the mechanisms provided by seL4 to achieve frame management.
You should review Chapter 6 in the seL4 reference manual to gain some exposure to the seL4 memory management model before proceeding further.
The image below approximates the initial state of the system.
While the mapping is approximate, you can see that part of physical memory is used by seL4 and the initial root task. The remaining memory is available to you as untyped memory.The initial virtual address space layout for SOS is also shown. The precise mapping between SOS's virtual address space and physical memory is not important. Your task involves using these untyped memory regions (i.e. the remaining free physical memory) to provide basic frame allocation and deallocation for later milestones that implement virtual memory for SOS's applications.
We provide an untyped memory allocator that is reponsible for
allocating physical address ranges for specific seL4 object
sizes within the available untyped memory. You can then use
these physical addresses (in conjunction
with ut_translate) to retype this memory
into seL4_ARM_SmallPageObject frames that can
subsequently be mapped into the virtual address space of a SOS
application (or SOS
itself). See apps/sos/src/ut_manager/ for details
of the interface (ut_alloc()/ut_free()).
You could map frames only into applications that SOS runs. However choosing to map frames directly into SOS on allocation will make copy in/out easier. We suggest mapping all frames objects into a free virtual memory range within SOS in order to create a 1:1 mapping between a virtual address range within SOS and physical memory used by a frame. This approach is illustrated in the diagram as a window onto physical memory at a fixed offset in the virtual address space. Note: only frames that are mapped will be accessible through the window.
For this milestone, you will need to create the bookkeeping
(i.e. a frame table) that can keep track of the system's
frames and the capabilities you have to those frames (cptrs
to seL4_ARM_SmallPageObject objects).
Recall that a virtual memory subsystem in general needs to:
With seL4, you need to also keep track of the frame capability for each mapping between a virtual page and a physical frame. You don't need to build an entire VM subsystem for this milestone, but you should be aware that eventually you will need to store the cptr to frames somewhere in your VM subsystem. Tutors will ask you how you will provide the above mappings for m3. It is a requirement for assessment that your frame table can take an index (possibly the physical address) and look-up the corresponding capability in constant time.
You should create a new file
(apps/sos/src/frametable.c) and populate this file
with your implementation of your frame allocation and
deallocation routines. This will need to consider the following
in the design of the routines:
seL4_ARM_SmallPageObject) and
subsequently mapped into sos for the frames to be accessible as
memory to SOS.ut_alloc when needed. If you allocate all
your memory initially as frames, you will have no memory
remaining for TCBs, page tables, etc....ut_manager;While you are free to implement your routines as you choose, we suggest the following approximate semantics:
Note: the design space (and potential optimisation of it) is large, so the above semantics is really just a guide to start you thinking, and not a specification of minimum requirements.
Some things you should think of are what information you need to store in the frame table. You may want to take into account the fact that you will later be using this frame table to support virtual memory, swapping and multiple processes. You should take this into account when designing your data structures.
You should also take into account which operations you want to perform on the frame table, and the required algorithms to fulfill these. For example, you don't want an order n-square O(n^2) search to find the next free frame.
Of course it is easy to change these data structures later as you gain a better understanding of the issues involved, so don't spend too much time designing the perfect structure now. Avoid prematurely optimising.
Your design should take into account the space and time complexity and bounds of your data structures.
The demonstration of this solution should show the execution of some example code using the allocation routine. For example:
/* Allocate 10 pages and make sure you can touch them all */
for (i = 0; i < 10; i++) {
/* Allocate a page */
seL4_Word vaddr;
frame_alloc(&vaddr);
assert(vaddr);
/* Test you can touch the page */
*vaddr = 0x37;
assert(*vaddr == 0x37);
printf("Page #%d allocated at %p\n", i, (void *) vaddr);
}
/* Test that you eventually run out of memory gracefully,
and doesn't crash */
for (;;) {
/* Allocate a page */
seL4_Word vaddr;
frame_alloc(&vaddr);
if (!vaddr) {
printf("Out of memory!\n");
break;
}
/* Test you can touch the page */
*vaddr = 0x37;
assert(*vaddr == 0x37);
}
/* Test that you never run out of memory if you always free frames.
This loop should never finish */
for (int i = 0;; i++) {
/* Allocate a page */
seL4_Word vaddr;
page = frame_alloc(&vaddr);
assert(vaddr != 0);
/* Test you can touch the page */
*vaddr = 0x37;
assert(*vaddr == 0x37);
printf("Page #%d allocated at %p\n", i, vaddr);
frame_free(page);
}
You should also be able to explain to the tutor the structure of your frame table, how your code works and any design decisions you took.