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