[CSE]  Advanced Operating Systems 
COMP9242 2012/S2 
UNSW
CRICOS Provider
Number: 00098G

PRINTER Printer-Friendly Version

M2: Memory manager

The aim of this milestone is to design and implement simple frame-based memory management. You will need to set up a frame table so that you can keep track of the system's physical memory and the capabilities you have to that memory (cptrs to seL4_ARM_SmallPageObject objects).

Recall in your basic operating systems knowledge that the virtual memory subsystem has to keep track of the address space (or process), virtual address, and physical address of each mapping. It has to translate (process, virtual address) to physical address for virtual address translation, and physical address to (process, virtual address) to invalidate translations for page replacement.

With seL4, for each virtual memory mapping between a virtual page and a physical frame, you must keep track of an additional cptr, i.e. a reference to a seL4_ARM_SmallPageObject capability used to establish the mapping, and to unmap it. 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 cptrs somewhere in your VM subsystem, of which the frametable is part of.

You should review Chapter 6 in the seL4 reference manual to gain some exposure to the seL4 memory management model before proceeding further.

You should create a new file in apps/sos/src/frametable.c. This will need to consider the following in its design:

  • SOS (i.e. the first process) does not have direct access to physical memory, only authority to manage untyped memory.
  • You need to interface to the existing untyped memory allocator that we provide you in order to reserve untype memory for frames. See apps/sos/src/ut_manager/ for details of the interface (ut_alloc()/ut_free()).
  • Reserving untyped memory for frames is not the same as reserving physical memory. Untyped memory needs to be retyped into frames (seL4_ARM_SmallPageObject) 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 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 frame. Or another way of thinking about it is that 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.

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.

Your design should take into account the space and time complexity and bounds of your data structures.

Assessment

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.


Last modified: 24 Jul 2012.