seL4 Level-1 Tutorials - Exercise #9: I/O Display

Objective

Configure the ported VGA driver to work under seL4 by mapping physical memory and providing input for I/O port functions. 

Background

VGA Standard uses specific physical memory region: 0xA0000 - 0xBFFFF. Therefore, we need to map the physical memory into virtual address space where we can directly write to it. However, the memory is not all in use at any given time. Instead, it is reserved in partitions for different modes. 

VGA Standard uses BIOS interrupts, by default, to configure its I/O port registers. This is not an option and it should not be attempted because it is both extremely slow and presents security risks. Instead, we need a way to configure the registers at runtime to change the mode safely.

Luckily, as shown in exercise-8, we can configure I/O ports using the platform support libraries. And this is exactly what we’re doing here as well. A major benefit is that we do not have to rely on VGA to be configured during boot, but instead do it at runtime AND while in userspace!

The driver was incorporated from VGA test code for MS-DOS and modified to work under the seL4 environment. Since the code was developed for another environment, it relied on several functions only available there, so we redefined these functions to use a platform support library to talk to I/O ports. The result is a functioning VGA driver. 

For the sake of simplicity, the exercise focuses on mapping the physical memory onto a virtual address space which allows us to read/write from it, then we override the function outportb (inherited from MS-DOS implementation) to manually trigger an seL4 framework I/O port request. 

Steps

    1.  Initialize build environment:

         The output should be: 

    2.  Map a specific physical address range to virtual memory (TODO #1 in display.c). For this task, we need an IO mapper to be initialized, and this can be done using the allocation objects we learned in Exercise-3. We have already completed this portion, and the task is to use that IO mapper to map the physical address range into a virtual one. The range starts from 0xA0000 and is 0x20000 in length (0xA0000-0xBFFFF). We defined the address start in VGA_MEMORY_ADDR and the size in VGA_MEMORY_SIZE.

ps_io_map(ps_io_mapper_t *io_map,
                      uintptr_t paddr,
                      size_t size,
                      int cached,
                      ps_mem_flags_t flags)

- io map:             the mapper we use (already initialized)
- paddr:               physical address start
- size:                   size of map with respect to paddr (end address is calculated using paddr+size)
- cached:             allow caching - not necessary
- flags:                 access to the memory flags (hint PS_MEM_NORMAL)
- RETURNS:        virtual address mapping to physical address (void*) you will have direct access to write in the physical memory with this! if the returned value is 0 then an error occured

         Recompile and simulate. The output should be: 

    3.  Reimplement the outportb function (TODO #2 in display.c). The driver we ported from the MS-DOS implementation uses outportb function all over the place to write to different I/O ports. Our task is to provide the proper seL4 implementation for this function instead of the MS-DOS original implementation. The function is already declared in display.c, but it is empty. We need to use the IO operations to manually call the I/O port out function

         Recompile and simulate. The output should be: 

⟵ Exercise-8

table of contents

Exercise-10 ⟶