Hi all,

I was going through the tutorials, unfortunately I've been finding very challenging to follow the instructions as I keep encountering issues after issue.

First, the repo command seems to be incorrect. In document: https://docs.sel4.systems/Tutorials/

it says:

repo init -u https://github.com/SEL4PROJ/sel4-tutorials-manifest -m sel4-tutorials.xml

but the manifest file 'sel4-tutorials.xml' does not exist on the git repository (of the sel4-tutorial-manifest).

What is the correct manifest file to use? There are two manifests (in any branch and tag): master.xml and default.xml. default.xml seems to use the 'new' format of identifying the individual versions of the libraries (through the hash).

Let's assume the correct manifest to use is the 'default.xml' from the 'sel4-tutorials' branch and initialize the workspace with:

repo init -u https://github.com/SEL4PROJ/sel4-tutorials-manifest -b sel4-tutorials
repo sync

So, now: first tutorial, ok (but this tutorial does very little). Second tutorial (hello-2), not so good... to avoid mistake, I am copying directly the solution into the app area:

cp projects/sel4-tutorials/solutions/hello-2/src/main.c apps/hello-2/src/main.c
make pc99_hello-2_defconfig
make

... and the build fails with:

[...]/workspaces/sel4-tutorials-2/stage/x86/pc99/lib/libsel4allocman.a(virtual_pool.o): In function `_add_page':
[...]/workspaces/sel4-tutorials-2/libs/libsel4allocman/src/mspace/virtual_pool.c:52: undefined reference to `vspace_get_map_obj'

The missing function appears to be part of libsel4vspace, that is missing from the library dependency list. Let's add it to add it to the apps/hello-2/Makefile:

diff --git a/exercises/hello-2/Makefile b/exercises/hello-2/Makefile

index 25c0b35..97a4fc6 100644

--- a/exercises/hello-2/Makefile

+++ b/exercises/hello-2/Makefile

@@ -28,6 +28,7 @@ ASMFILES += $(patsubst $(SOURCE_DIR)/%,%,$(wildcard $(SOURCE_DIR)/src/plat/${PLA

# Libraries required to build the target

LIBS = c sel4 sel4muslcsys \

sel4simple sel4vka sel4allocman \

+ sel4vspace \

sel4platsupport platsupport \

utils sel4simple-default sel4utils sel4debug

Now it builds successfully, unfortunately when running, the child thread doesn't appear to run at all. This is the output of qemu running 'make simulate':

Booting all finished, dropped to user space
4 untypeds of size 12
5 untypeds of size 13
5 untypeds of size 14
4 untypeds of size 15
4 untypeds of size 16
4 untypeds of size 17
4 untypeds of size 18
5 untypeds of size 19
5 untypeds of size 20
2 untypeds of size 21
4 untypeds of size 22
4 untypeds of size 23
2 untypeds of size 24
3 untypeds of size 25
3 untypeds of size 26
3 untypeds of size 27
1 untypeds of size 28
6 untypeds of size 29
main: hello world

I would have expected seeing on the output the string 'thread_2: hallo wereld' somewhere...

Why the thread 2 does not run? This code was working last time I checked (version 5.2).

I tried then to continue testing the tutorials, and I went to the hello-3. Hello-3 is based on the Hello-2 but adds an endpoint for IPC between the main thread and the child thread.

Surprisingly, this app not only builds out of the box without errors (apparently libsel4vspace was already added to its Makefile), but even running it, works as expected:

Booting all finished, dropped to user space
3 untypeds of size 12
5 untypeds of size 13
5 untypeds of size 14
4 untypeds of size 15
4 untypeds of size 16
4 untypeds of size 17
4 untypeds of size 18
5 untypeds of size 19
5 untypeds of size 20
2 untypeds of size 21
4 untypeds of size 22
4 untypeds of size 23
2 untypeds of size 24
3 untypeds of size 25
3 untypeds of size 26
3 untypeds of size 27
1 untypeds of size 28
6 untypeds of size 29
main: hello world
thread_2: hallo wereld
thread_2: got a message 0x6161 from 0x61
main: got a reply: 0xffff9e9e

Right now I suspect that seL4_TCB_Configure() does not work correctly if we don't provide an endpoint (because that's essentially the main difference between the two tests).

Can somebody try to run the tutorials and perhaps confirm the problem?

Regards,

Fabrizio Bertocci

Real-Time Innovations, Inc.

Sunnyvale, CA