From 203c81011ea2d2d85ca50a708ca512688a2be0d7 Mon Sep 17 00:00:00 2001 From: Birgit Brecknell Date: Mon, 27 May 2024 12:40:04 +1000 Subject: [PATCH] fix errors in hello-camkes-timer Signed-off-by: Birgit Brecknell --- .../hello-camkes-timer/hello-camkes-timer.md | 219 ++++++++++++------ 1 file changed, 147 insertions(+), 72 deletions(-) diff --git a/tutorials/hello-camkes-timer/hello-camkes-timer.md b/tutorials/hello-camkes-timer/hello-camkes-timer.md index 6f41e11b..cc8e2306 100644 --- a/tutorials/hello-camkes-timer/hello-camkes-timer.md +++ b/tutorials/hello-camkes-timer/hello-camkes-timer.md @@ -20,6 +20,26 @@ The solutions to this tutorial primarily uses the method of manually defining hardware details. The solutions to the second part are also included, albeit commented out. +## CapDL Loader + +This tutorial uses the *capDL loader*, a root task which allocates statically + configured objects and capabilities. + +
+Get CapDL +The capDL loader parses +a static description of the system and the relevant ELF binaries. +It is primarily used in [Camkes](https://docs.sel4.systems/CAmkES/) projects +but we also use it in the tutorials to reduce redundant code. +The program that you construct will end up with its own CSpace and VSpace, which are separate +from the root task, meaning CSlots like `seL4_CapInitThreadVSpace` have no meaning +in applications loaded by the capDL loader. +
+More information about CapDL projects can be found [here](https://docs.sel4.systems/CapDL.html). +
+For this tutorial clone the [CapDL repo](https://github.com/sel4/capdl). This can be added in a directory that is adjacent to the tutorials-manifest directory. +
+ ## Initialising /*? macros.tutorial_init("hello-camkes-timer") ?*/ @@ -60,15 +80,18 @@ timer.hello);` and `timer.sem_value = 0;` in the `hello-camkes-timer.camkes` file. They assume that the name of the timer ''driver'' will be `timer`. If you wish to call your driver something else, you'll have to change these lines. -
-Quick solution - ``` /* Part 1, TASK 1: component instances */ /* hint 1: one hardware component and one driver component * hint 2: look at * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application */ +``` + +
+Quick solution + +``` component Timerbase timerbase; component Timer timer; ``` @@ -83,9 +106,6 @@ Connect the timer driver component (`Timer`) to the timer hardware component be connected to the timer driver. One of these represents memory-mapped registers. The other represents an interrupt. -
-Quick solution - ``` /* Part 1, TASK 2: connections */ /* hint 1: use seL4HardwareMMIO to connect device memory @@ -93,6 +113,12 @@ registers. The other represents an interrupt. * hint 3: look at * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application */ +``` + +
+Quick solution + +``` connection seL4HardwareMMIO timer_mem(from timer.reg, to timerbase.reg); connection seL4HardwareInterrupt timer_irq(from timerbase.irq, to timer.irq); ``` @@ -105,9 +131,6 @@ Configure the timer hardware component instance with device-specific info. The physical address of the timer's memory-mapped registers, and its IRQ number must both be configured. -
-Quick solution - ``` /* Part 1, TASK 3: hardware resources */ /* Timer and Timerbase: @@ -115,6 +138,12 @@ must both be configured. * hint 2: look at * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#hardware-components */ +``` + +
+Quick solution + +``` timerbase.reg_paddr = 0xF8001000; // paddr of mmio registers timerbase.reg_size = 0x1000; // size of mmio registers timerbase.irq_irq_number = 42; // timer irq number @@ -141,13 +170,15 @@ where the initial `repo init` command was executed. This task is to call the `timer_handle_irq` function from the supply driver to inform the driver that an interrupt has occurred. -
-Quick solution - ```c /* Part 1, TASK 4: call into the supplied driver to handle the interrupt. */ /* hint: timer_handle_irq */ +``` + +
+Quick solution +```c timer_handle_irq(&timer_drv); ```
@@ -157,13 +188,16 @@ TASK 5 Stop the timer from running. The `timer_stop` function will be helpful here. -
-Quick solution - ```c /* Part 1, TASK 5: stop the timer. */ /* hint: timer_stop */ +``` + +
+Quick solution + +```c timer_stop(&timer_drv); ```
@@ -177,13 +211,16 @@ CAmkES generates the seL4-specific code for ack-ing an interrupt and provides a function `_acknowldege` for IRQ interfaces (specifically those connected with `seL4HardwareInterrupt`). -
-Quick solution - ```c /* Part 1, TASK 6: acknowledge the interrupt */ /* hint 1: use the function _acknowledge() */ +``` + +
+Quick solution + +```c error = irq_acknowledge(); ZF_LOGF_IF(error != 0, "failed to acknowledge interrupt"); ``` @@ -198,15 +235,18 @@ before the component's interfaces start running. We need to initialise a handle to the timer driver for this device, and store a handle to the driver in the global variable `timer_drv`. -
-Quick solution - ```c /* Part 1, TASK 7: call into the supplied driver to get the timer handler */ /* hint1: timer_init * hint2: The timer ID is supplied as a #define in this file * hint3: The register's variable name is the same name as the dataport in the Timer component */ +``` + +
+Quick solution + +```c int error = timer_init(&timer_drv, DEFAULT_TIMER_ID, reg); assert(error == 0); ``` @@ -218,13 +258,16 @@ TASK 8 After initialising the timer, we now need to start the timer. Do so by calling `timer_start` and passing the handle to the driver. -
-Quick solution - ```c /* Part 1, TASK 8: start the timer * hint: timer_start */ +``` + +
+Quick solution + +```c error = timer_start(&timer_drv); assert(error == 0); ``` @@ -243,9 +286,6 @@ should return after a given number of seconds. in exposed by the `Timer` component is called `hello`. Thus, the function we need to implement is called `hello_sleep`. -
-Quick solution - ```c /* part 1, TASK 9: implement the rpc function. */ /* hint 1: the name of the function to implement is a composition of an interface name and a function name: @@ -257,20 +297,27 @@ need to implement is called `hello_sleep`. * hint 6: invoke a function in supplied driver the to set up the timer * hint 7: look at https://github.com/sel4/camkes-tool/blob/master/docs/index.md#creating-an-application */ +``` +
+Quick solution + +```c void hello_sleep(int sec) { - int error = 0; - /* Part 1, TASK 10: invoke a function in the supplied driver to set a timeout */ - /* hint1: timer_set_timeout - * hint2: periodic should be set to false - */ - error = timer_set_timeout(&timer_drv, sec * NS_IN_SECOND, false); - assert(error == 0); - error = sem_wait(); - ZF_LOGF_IF(error != 0, "failed to wait on semaphore"); - } + int error = 0; + + /* Part 1, TASK 10: invoke a function in the supplied driver to set a timeout */ + /* hint1: timer_set_timeout + * hint2: periodic should be set to false + */ + + error = sem_wait(); + ZF_LOGF_IF(error != 0, "failed to wait on semaphore"); +} ```
+ + ### Set a timer interrupt TASK 10 @@ -278,6 +325,27 @@ Tell the timer to interrupt after the given number of seconds. The `timer_set_timeout` function from the included driver will help. Note that it expects its time argument to be given in nanoseconds. +```c + * Part 1, TASK 10: invoke a function in the supplied driver to set a timeout */ + /* hint1: timer_set_timeout + * hint2: periodic should be set to false + */ + + error = sem_wait(); + ZF_LOGF_IF(error != 0, "failed to wait on semaphore"); +``` + +
+Quick solution + +```c + error = timer_set_timeout(&timer_drv, sec * NS_IN_SECOND, false); + assert(error == 0); + +``` +
+ + Note the existing code in `hello_sleep`. It waits on a binary semaphore. `irq_handle` will be called on another thread when the timer interrupt occurs, and that function will post to the binary semaphore, unblocking us and allowing @@ -291,19 +359,6 @@ Starting the client After the client: wakeup ``` -
-Quick solution - -```c - * Part 1, TASK 10: invoke a function in the supplied driver to set a timeout */ - /* hint1: timer_set_timeout - * hint2: periodic should be set to false - */ - error = timer_set_timeout(&timer_drv, sec * NS_IN_SECOND, false); - assert(error == 0); -``` -
- ## Exercises - Part 2 Now that you've learnt how to manually define the hardware details of a @@ -328,15 +383,18 @@ Remove the `Timerbase` and `Timer` component instantiations and instantiate a hello_timer(from client.hello, to timer.hello);` and `timer.sem_value = 0;` lines if necessary. -
-Quick solution - ``` /* Part 2, TASK 1: component instances */ /* hint 1: a single TimerDTB component * hint 2: look at * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application */ +``` + +
+Quick solution + +``` component TimerDTB timer; ```
@@ -348,9 +406,6 @@ Remove the `seL4HardwareMMIO` and `seL4HardwareInterrupt` connections. Connect the two interfaces inside the `TimerDTB` component with the `seL4DTBHardware` connector. -
-Quick solution - ``` /* Part 2, TASK 2: connections */ /* hint 1: connect the dummy_source and timer interfaces @@ -358,6 +413,11 @@ connector. * hint 3: look at * https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application */ +``` + +
+Quick solution +``` connection seL4DTBHardware timer_dtb(from timer.dummy_source, to timer.tmr); ```
@@ -375,9 +435,6 @@ and grab the necessary data to initialise hardware resources. More specifically, it reads the registers field and optionally the interrupts field to allocate memory and interrupts. -
-Quick solution - ``` /* Part 2, TASK 3: hardware resources */ /* TimerDTB: @@ -386,12 +443,19 @@ to allocate memory and interrupts. * e.g. foo.dtb = dtb({"path" : "/bar"}); * hint 3: set the 'generate_interrupts' setting to 1 */ +``` + +
+Quick solution + +``` tmr.dtb = dtb({"path" : "/amba/timer@f8001000"}); // path of the timer in the DTB tmr.generate_interrupts = 1; // tell seL4DTBHardware to init interrupts ```
-### TASK 4 +### Handle the interrupt +TASK 4 Move to `components/TimerDTB/src/timerdtb.c`. @@ -413,33 +477,41 @@ Likewise with part one, the implementation of the timer driver is in the included driver in `timer_driver` and the task here is to call `timer_handle_irq`. -
-Quick solution - ```c /* Part 2, TASK 4: call into the supplied driver to handle the interrupt. */ /* hint: timer_handle_irq */ +``` + +
+Quick solution + +```c timer_handle_irq(&timer_drv); ```
-### TASK 5 +### Stop the timer +TASK 5 The timer needs to be stopped, the task here is the same as part one's task 5. -
-Quick solution - ```c /* Part 2, TASK 5: stop the timer. */ /* hint: timer_stop */ +``` + +
+Quick solution + +```c timer_stop(&timer_drv); ```
-### TASK 6 +### Get the timer handler +TASK 6 Again, the interrupt now has to be acknowledged. @@ -450,10 +522,7 @@ takes in a `ps_irq_t *` argument. Similarly, the `ps_irq_t *` argument helps CAmkES to differentiate between the possibly many interrupts of a device that you wish to acknowledge. -
-Quick solution - -``` +```c /* Part 2, TASK 7: call into the supplied driver to get the timer handler */ /* hint1: timer_init * hint2: The timer ID is supplied as a #define in this file @@ -463,6 +532,12 @@ you wish to acknowledge. * and "register number" is the index of the register block in the device * node in the devicetree blob */ +``` + +
+Quick solution + +```c int error = timer_init(&timer_drv, DEFAULT_TIMER_ID, tmr_0); assert(error == 0); ```