seL4 Level-1 Tutorials - Exercise #1: Hello World!
Objectives
- Build a basic application using TCCoE seL4 repository.
- Work with cmake & ninja
- Print a debug message to console.
Steps
This exercise focuses on getting the build environment ready for use. For this exercise, we manually do what the common command section does in order to get a better understanding of the process.
- Open a terminal and change working directory to root directory of the sel4-files, and start a container.
You should get the following output:
2. Navigate to level-1-tutorials directory and link to version 1.0
You should get the following output:
3. Use cmake to initialize the build environment. cmake can be configured with different code generators. For seL4, they use ninja. Furthermore, cmake can also have a cache file which contains common configuration. In this case, it is the settings.cmake file which allows cmake to find seL4 and its libraries, as well as to properly configure the architecture/platform targets. Finally, the last argument sent to cmake is the actual directory of the project that needs to be built. This directory must include a CMakeLists.txt file which specifies exactly how the project needs to be built. Anything starting with -D is a variable that can be defined anywhere in the command line arguments. Here, we use -DARCH=x86 which tells cmake to define a variable called ARCH and set its value to x86.
4. Modify application/core/exercise-1/src/main.c, using any editor of your choice (e.g. gedit, vi, nano, ..., etc.), and add `printf` before the program returns:
Note: it is important to use \n for the output buffer to properly display the message in simulation.
5. Recompile and simulate (in application/build/exercise-1-x86)
The output should be:
