Exam starts at 14:00 Tue Nov 26 and ends at 14:00 Wed Nov 27.
Milestone 0: Familiarisation

This is a simple exercise designed to get you started on seL4 and set up your environment. It contains very detailed instructions, together with the existing source code and the seL4 manual you should have no problem doing it.

Your Environment

If you haven't already you may want to take a look at Odroid C2 Lab, which provides details on the hardware and how to communicate with it remotely.

The required tools can be set up on a CSE lab machine by running 9242, as follows: 

weill% 9242
newclass starting new subshell for class COMP9242...
weill% aarch64-linux-gnu-ld
aarch64-linux-gnu-ld: no input files

The above updates your path to include the cross compilers and other tools located in the cs9242 home directory, and python packages that the seL4 build depends on for your local user account. You will need to run 9242 each time you start a new shell on a lab machine in order to build the project successfully.

Get the source

The sources to the project are also available at https://github.com/SEL4PROJ/AOS-manifest for anybody outside UNSW who wishes to take a look at the project. Using the projects from this repository will require the use of the repo tool. Read the README.md for more details on setting up the project from that repository.

Clone your copy of the milestone 0 starting code.

We use git for revision control for this project, and it will be simplest if you do also. You will be submitting via a provided git repository for each milestone in the project. You will need to support yourself if you use any other tools.

You can find some pointers on using git on our git page. 

git clone https://nw-syd-gitlab.cseunsw.tech/COMP9242/24T3/{your-zID}-m0.git aos-2024-m0

You will need to provide your username and password when cloning. If you set up your ssh-keys on our gitlab server you can use the following command instead: 

git clone git@nw-syd-gitlab.cseunsw.tech:COMP9242/24T3/{your-zID}-m0.git aos-2024-m0

Note: you will only be using this repository for milestone 0. Once you have selected your group members for the remainder of semester you will be using a different group respository to submit.

Building SOS

Dependencies

The CSE lab machines and login servers have already been configured with all dependencies. To set up another machine, follow the seL4 build dependencies (you only need to install the Base Build Dependencies and the Python Dependencies) instructions on the seL4 docsite. Note: that you only require the aarch64 cross-compilers.

Once this stage is completed successfully, you should be able to compile the AOS project.

Build the project

We use Cmake and ninja as our build system, which you can read more about on the seL4 docsite. Importantly, this build system does not build in the source tree: you create another directory to build code in, and develop in the source directories.

Follow these instructions to build SOS: 

cd aos-2024-m0 # change to the project directory
mkdir build # create a build directory
cd build # change to the build directory
../init-build.sh # initialise the build directory
ninja # build

By default ninja builds in parallel. If you have a lot of build errors, this can cause confusing output. use ninja -j1 to build with only one thread, which will make the build slower but also serialise the output.

Getting it Going

Booting your Odroid-C2 for the first time is easy:

  1. From a CSE lab machine run 9242 odroid serial

  2. Reset the ODroid-C2 by running 9242 odroid reset in a different terminal.

    The first time you run this you may be prompted to enter your zID and zPass. 

    --- UART initialized after reboot ---
[Reset cause: unknown]
[Image: unknown, amlogic_v1.1.3046-00db630-dirty 2016-08-31 09:24:14 tao.zeng@droid04]
bl30: check_permit, count is 1
bl30: check_permit: ok!
chipid: ef Load bl33 from eMMC, src: 0x00034200, des: 0x01000000, size: 0x00074ae0
be ad de d f0 ad ba ef be ad de not ES chip
[0.275944 Inits done]
secure task start!
high task start!
low task start!
NOTICE:  BL3-1: v1.0(debug):4d2e34d
NOTICE:  BL3-1: Built : 17:08:35, Oct 29 2015
INFO:    BL3-1: Initializing runtime services
INFO:    BL3-1: Preparing for EL3 exit to normal world
INFO:    BL3-1: Next image address = 0x1000000
INFO:    BL3-1: Next image spsr = 0x3c9


U-Boot 2015.01 (Sep 26 2017 - 00:56:33)

DRAM:  2 GiB
Relocation Offset is: 76f31000
-------------------------------------------------
* Welcome to Hardkernel's ODROID-C2
-------------------------------------------------
CPU : AMLogic S905
S/N : HKC213254DFFB152
MAC : 00:1e:06:35:fd:d2
BID : HKC2211804
-------------------------------------------------
register usb cfg[1][0] = 0000000077f95190
register usb cfg[0][1] = 0000000077f951b0
vpu detect type: 5
vpu clk_level = 7
set vpu clk: 666667000Hz, readback: 666660000Hz(0x300)
MMC:   aml_priv->desc_buf = 0x0000000073f29d30
aml_priv->desc_buf = 0x0000000073f2bec0
SDIO Port C: 0, SDIO Port B: 1
[mmc_init] mmc init success
In:    serial
Out:   serial
Err:   serial
----------------------------------
MMC Size : 8 GB
----------------------------------
reading boot-logo.bmp.gz
** Unable to read file boot-logo.bmp.gz **
reading boot-logo.bmp
** Unable to read file boot-logo.bmp **
movi: the partiton 'logo' is reading...

MMC read: dev # 0, block # 61024, count 2048 ... 2048 blocks read: OK
hpd_state=1
[CANVAS]addr=0x3f800000 width=3840, height=1440

set hdmitx VIC = 16
hdmitx phy setting done
set hdmitx VIC = 16
hdmitx phy setting done
Error: Bad gzipped data
There is no valid bmp file at the given address
Net:   Meson_Ethernet
Hit [Enter] key twice to stop autoboot:  0

Development cycle

We have developed a few tools to speed the development cycle along. The provided scripts will copy the sos operating system, known as a bootimage to your tftp directory and reset the OdroidC2. Below is a typical development cycle, assuming the path changes to your login script:

  1. In a terminal on a CSE machine, run 9242 odroid serial.
  2. In another terminal on a CSE machine, run 9242 odroid netcon.
  3. Make your changes in the source directory, (hint: learn cscope or see our guide to VS Code).
  4. Build with ninja, in the build dir.
  5. Test your changes (from the build dir ../reset.sh).
  6. Repeat from step 3 above until satisfied, or you fall over for lack of sleep.

The Milestone

The example skeleton operating system includes an application console_test which starts up, prints out its name, and then blocks itself forever. The framework page describes the provided code structure.

The example application makes a system call to write to stdout. The libsosapi contains system call skeletons that you will gradually implement over the term. Currently, sos_write uses the seL4 debug API seL4_DebugPutChar to output data to seL4's debug console. This function should only be used for internal SOS debugging, not as a console for applications, so, your task is to modify the sos_write function to send data through the operating system and across the network to your netcon (odroid netcon) console.

Note: your sos_write implementation must support buffers larger than the IPC buffer.

The second part of milestone zero is to find a partner for the rest of the project. The project is to be completed, in pairs, unless prior permission has been obtained from the LiC.

Before you complete this milestone, be sure to spend time becoming familiar with the seL4 Debugging Guide. It will save you a lot of debugging effort throughout the project.

Recommended procedure

  1. Read (and understand) the code in projects/aos/sos/src/main.c and the code in the projects/aos/apps/console_test application directory.
  2. Read the documentation on libnetworkconsole.
  3. Initialise network console during SOS startup. Note that you need to initialise the network console after network_init is called.
  4. Design a simple IPC protocol to transfer data from the user program to your operating system (Recommended reading: seL4 Reference Manual, Chapter 4 (all) and Chapter 10 (Section 10.1, 10.2 (not 10.2.1), 10.2.2). Note that we are using the MCS version of the kernel. Note also that an endpoint has already been set up between the console_test application and sos.)
  5. Write the client side implementation in sos_write in libsosapi/src/sos.c.
  6. Change the syscall_loop in main.c to recognise your new protocol, and print out a debug message when you receive one of these messages.
  7. Change the server side so that it now passes the data to the network console, which will send it onto the network and be available via 9242 odroid netcon on a CSE terminal.
  8. Test that all of console_test's output now goes to the odroid netcon console, not the console debugger.

Assessment

Milestone submission

See the milestone submission guidelines for instructions on submitting your milestone solution.

Milestone Demonstration

You will need to demonstrate user applications printing to the 2nd console via libnetworkconsole to the tutor during the demonstration period. You should be prepared to show your tutor which files you modified in your solution, and explain any design decisions you made.

Note that since you do not have consistent virtual memory management yet, your protocol will be fairly simple for now. However, it should be upgraded as more parts of the system are completed. Your tutor will be particularly interested in the details of your IPC interface with different sized blocks of data etc, and how you plan to improve it in future.

Examining the IPC Buffer:

Note: For m0, sending data byte-by-byte via IPC is fine.

You will let the tutor know who your partner is so that group accounts can be created for you.