Screen Version

M2: Memory manager

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 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 seL4 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 the remaining untyped memory regions (i.e. the remaining free physical memory) to provide basic frame allocation and deallocation for later milestones for two purposes: for virtual memory required by SOS itself, and virtual memory for for SOS's applications.

You are provided with an untyped memory allocator which can allocate memory objects of size 4K and below. This is set up during the bootstrapping phase, where all free untyped memory is retyped into 4K untyped objects. You will need to allocate 4K objects and retype them into seL4_ARM_SmallPageObject that can subsequently be mapped into the the SOS virtual address space. You will need to use the following functions for this milestone: ut_size, ut_alloc_4k_untyped and ut_free.

You could map frames only into applications that SOS creates and manages. However choosing to map frames directly into SOS on allocation will make copying memory into and out of applications 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 specific frames.

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:

• Provide a quick lookup from (process, virtual address) to an index or reference to the frame (when an existing mapping needs to be remapped).
• Provide a quick lookup from an index or reference to the frame to (process, virtual address) (when a frame is swapped to disk)

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 in the next milestone, m3, 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 a frame identifier (possibly the SOS virtual address, or frame number) and look-up the corresponding capability in constant time.

Implementation Hints

The helper function map_frame is used to simplify mapping frames into the virtual address space. It is only a partial implementation in its present form as it leaks page table cptrs (SOS never free page table objects for itself, only its applications). In later milestones, you'll need to modify it (or create your own version) that is compatible with your book keeping.

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. Recall that you need to tell CMake about any new files.

You will need need to consider the following when designing your frame table:

• SOS (i.e. the first process) does not have direct access to physical memory, only authority to manage untyped memory.
• Reserving untyped memory for frames is not the same as reserving physical memory. Untyped memory needs to be retyped into frames (seL4_ARM_SmallPageObject) (see alloc_retype for an example of this) and subsequently mapped into sos for the frames to be accessible as memory to SOS.
• You should only populate your frametable on demand using ut_alloc_4k_untyped when needed. If you allocate all your memory initially as frames, you will have no memory remaining for TCBs, page tables, etc....
• Effectively, your frame table will keep track of only the untyped memory that is currently a seL4 frame object (you'll also need to track TCBs and page tables, either seperately, or using the frame table). One way to think about your design is to consider the logical states a physical frame can be in (from SOS's perspective). Each frame can be in one of at least three states:
  1. Untyped, i.e. managed by ut_manager;
  2. A free frame, i.e. allocated from untyped manager, and retyped, and appears as a free frame in the frame table similar to traditional free frames in an OS; and
  3. An allocated frame, i.e. what was a free frame in the frametable, that is now allocated and in use.

While you are free to implement your routines as you choose, we suggest the following approximate semantics:

• frame_alloc: the physical memory is reserved via the ut_alloc_4k_untyped, the memory is retyped into a frame, and the frame is mapped into the SOS window at a fixed offset of the physical address.
• frame_free: the physical memory is no longer mapped in the window, the frame object is destroyed, and the physical memory range is returned via ut_free.

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.

Design alternatives

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.

Assessment

Demonstration

The demonstration of this solution should show some unit tests which test your frame table. The following examples are the minimum required (we recommend testing extensively):

/* Allocate 10 pages and make sure you can touch them all */
for (int 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 never run out of memory if you always free frames. */
for (int i = 0; i < 10000; 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);

     /* print every 1000 iterations */
     if (i % 1000 == 0) {
         printf("Page #%d allocated at %p\n",  i, vaddr);
     }

     frame_free(page);
}

/* Test that you eventually run out of memory gracefully,
   and doesn't crash */
while (true) {
     /* 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);
}

/* finally clean up all the memory allocated above */

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.

Show Stoppers

• A frametable sized via compile time constant.
• Linear searches for allocation or lookup of status/attribute of a frame
• Any approach that just "leaks" the frame object capability.
• Crashing when running out of memory
• A Frame table or the window to physical memory overlaps with DMA or other existing regions (ipc buffer etc).

Better Solutions

• Designs that can easily be extended to support a second-chance clock replacement policy later in the semester
• The frame table is not allocated using malloc.
• Frame table entries are compact. For example, only containing a capability reference and an index or pointer used for allocation.
• Designs that avoid deleting and retyping a frame object for every frame free and frame alloc request. For example, by using a high- and low-water mark.