• Home
  • About
    • Organization Structure
    • Organizing Committee
    • Privacy Policy
  • Membership
    • Apply for Membership
    • Membership Info
    • Our Members
  • Summits
    • 2024 Summit
    • 2022 Summit
    • 2020 Summit
    • 2019 Summit
    • 2018 Summit
  • Resources
    • About seL4®
    • seL4® Foundation
    • TCCoE Repository
    • Existing Platforms and Capabilities
  • Training
  • Contact
⟵ Exercise-6
table of contents
Exercise-8 ⟶

seL4 Level-1 Tutorials - Exercise #7: I/O Timer

Objective
Use I/O APIs to allocate and initialize a timer object.
Background
Talking to I/O devices is very dependent on the target platform of the system largely because different platforms use different DMAs and I/O ports for their devices. Some I/O devices have standardized I/O ports which makes them easier to access than others.
seL4 projects provide platform support libraries which define an interface to handle I/O devices in a generic way. The interface can be specialized to create device drivers when needed. The timer is an example of such device.
The platsupport library provides a very important C structure:
struct ps_io_ops { ps_io_mapper_t io_mapper; ps_io_port_ops_t io_port_ops; ps_dma_man_t dma_manager; ps_io_fdt_t io_fdt; #ifdef CONFIG_ARCH_ARM clock_sys_t clock_sys; mux_sys_t mux_sys; #endif ps_interface_registration_ops_t interface_registration_ops; ps_malloc_ops_t malloc_ops; ps_irq_ops_t irq_ops; };
This structure provides a generic interface to any I/O device. In other words, it allows you to define drivers for different I/O devices all in the userland environment. For this exercise, we will use this structure to initialize an ltimer. The driver is already provided by the utilities library.
Steps
1. Initialize build environment:
$ cd /home/$USER/sel4-files $ container # if using our environment setup $ cd level-1-tutorials $ ./init-build exercise-7 x86 $ cd application/build/exercise-7-x86 $ ninja $ ./simulate use Ctrl + A ⟶ X to quit qemu
The output should be:
2. Create I/O memory allocation operations structure (TODO #1 in main.c). This corresponds to the malloc_ops member shown in the background section. We initialize it using the driver framework provided by seL4:
sel4platsupport_new_malloc_ops(ps_malloc_ops_t *ops) - ops: target malloc ops (see ps_io_ops) - RETURNS: error code (0 on success)
Recompile and simulate. The output should be:
3. Create a new I/O mapper (TODO #2 in main.c). The mapper will allow the driver to communicate with the necessary IO and ports. It can be initialized using:
sel4platsupport_new_io_mapper(vspace_t *vspace, vka_t *vka, ps_io_mapper_t *io_mapper) - vspace: vspace to use for the new io mapper - vka: virtual kernel allocator used to allocate the mapper - io_mapper: the target io mapper (see ps_io_ops) - RETURNS: error code (0 on success)
Recompile and simulate. The output should be:
4. Create new FDT operations (TODO #3 in main.c). This step is crucial and it can be customized if needed. The FDT operations structure is part of the seL4 driver framework and it uses a default cookie structure that is defined by the specific driver. For default usage, you do not customize it. Anyway, the initialization can be done using:
sel4platsupport_new_fdt_ops(ps_io_fdt_t *io_fdt, simple_t *simple, ps_malloc_ops_t *malloc_ops) - io_fdt: target io fdt structure (see ps_io_ops) - simple: initialized simple object allocator structure - malloc_ops: initialized malloc ops structure - RETURNS: error code (0 on success)
Recompile and simulate. The output should be:
5. Initialize architecture specific operations (TODO #4 in main.c). This is the last step in the process to initialize the driver properly. Everything we’ve done until now did not target a specific architecture or platform. This step will look for the code corresponding to the current target build environment – if there is an available implementation, it will be used. If there is not, it will throw a build error. The call can be done using:
sel4platsupport_new_arch_ops(ps_io_ops_t *ops, simple_t *simple, vka_t *vka) - ops: io_ops structure which receives the architecture specific IO operations - simple: initialized simple object allocator structure - vka: initialized virtual kernel allocator structure - RETURNS: error code (0 on success)
Recompile and simulate. The output should be:
6. Destroy the timer (TODO #5 in main.c). After using the timer, make sure to destroy it when it is unnecessary:
ltimer_destroy(ltimer_t *timer) - timer: initialized ltimer object
Recompile and simulate. The output should be:
Learned APIs
  • sel4platsupport_new_malloc_ops
  • sel4platsupport_new_io_mapper
  • sel4platsupport_new_fdt_ops
  • sel4platsupport_new_arch_ops
⟵ Exercise-6
table of contents
Exercise-8 ⟶
seL4 is a trademark of LF Projects, LLC. Trusted Computing Center of Excellence™ is a tradename of The Computing Center of Excellence, Inc. Copyright © 2022 The Computing Center of Excellence, Inc.

We use cookies to enable essential functionality on our website, and analyze website traffic. By clicking Accept you consent to our use of cookies. Read about how we use cookies.

Your Cookie Settings

We use cookies to enable essential functionality on our website, and analyze website traffic. Read about how we use cookies.

Cookie Categories
Essential

These cookies are strictly necessary to provide you with services available through our websites. You cannot refuse these cookies without impacting how our websites function. You can block or delete them by changing your browser settings, as described under the heading "Managing cookies" in the Privacy and Cookies Policy.

Analytics

These cookies collect information that is used in aggregate form to help us understand how our websites are being used or how effective our marketing campaigns are.