sel4 / sel4-tutorials Goto Github PK

View Code? Open in Web Editor NEW

51.0 27.0 55.0 27.82 MB

Tutorials for working with seL4 and/or CAmkES.

Home Page: https://docs.sel4.systems/Tutorials

C 11.52% CMake 34.45% Python 53.73% Makefile 0.30%

sel4-tutorials's Introduction

seL4 Tutorials

Various tutorials for using seL4, its libraries, and CAmkES.

Prerequisites

Follow the instructions for setting up your host environment on the seL4 docsite.

Starting a tutorial

This tutorial repository is part of a larger collection of repositories, which are required to run the tutorial and are coordinated in a manifest file. See this guide on how to check out a consistent set.

Once you have that, a tutorial is started through the use of the init script that is provided in the root directory. Using this script you can specify a tutorial and target machine and it will create a copy of the tutorial for you to work on.

Example:

mkdir build_hello_world
cd build_hello_world
../init --plat pc99 --tut hello-world

The init script will initialize a build directory in the current directory and at the end it will print out a list of files that need to be modified to complete the tutorial. Building is performed simply be invoking ninja, and once the tutorial compiles it can be tested in Qemu by using the provided simulation script through ./simulate

Tutorials and targets

The -h switch to the init script provides a list of different tutorials and targets that can be provided to --plat and --tut respectively.

Most tutorials support any target platform, with the exception of hello-camkes-timer, which only supports the zynq7000 platform.

Virtual Machine Image

You can also download a VirtualBox virtual machine appliance(md5) (3GB, based on Lubuntu 16.04.1 with all the seL4 tutorial prerequisites installed).

This appliance is based on VirtualBox 5.1.2. You may also need to install the appropriate VirtualBox extensions available from the same page.

Solutions

To view the solutions for a tutorial instead of performing the tutorial pass the --solution flag to the init script

Example:

mkdir build_hello_world
cd build_hello_world
../init --plat pc99 --tut hello-world --solution

After which it will tell you where the solution files are that you can look at. You can then do ninja && ./simulate to build and run the solution.

Reporting issues or bugs in the tutorials:

Please report any issues you find in the tutorials (bugs, outdated API calls, etc) by filing an issue on the public github repository: https://github.com/seL4/sel4-tutorials/issues/

Build system tutorial

Due to custom written additions to the build system specifically for the tutorials they are not appropriate for learning how to create and structure new applications/systems. Future tutorials for this will be forthcoming. For now it is suggested to look at other existing applications for ideas.

Documentation

Developer wiki

A walkthrough of each tutorial is available on the docs site

Tutorial Slides

The slides used for the tutorial are available in docs.

seL4 Manual

The seL4 manual lives in the kernel source in the manual directory. To generate a PDF go into that directory and type make. You will need to have LaTeX installed to build it.

A pre-generated PDF version can be found here.

CAmkES Documentation

CAmkES documentation lives in the camkes-tool repository in docs/index.md.

sel4-tutorials's People

Contributors

Stargazers

Watchers

sel4-tutorials's Issues

The notification tutorial solution seems to have a race condition

Every once in a while we're getting a failure in the CI simulation run. Since it's simulation, we can exclude hardware glitches and since it is working most of the time it's likely that there is a race condition somewhere that gets triggered rarely.

Example log output:

2023-03-27T10:30:10.0851519Z simulate: qemu-system-x86_64  -cpu Nehalem,-vme,+pdpe1gb,-xsave,-xsaveopt,-xsavec,-fsgsbase,-invpcid,+syscall,+lm,enforce -nographic -serial mon:stdio -m size=512M  -kernel images/kernel-x86_64-pc99 -initrd images/capdl-loader-image-x86_64-pc99 �c�[?7l�[2J�[0mSeaBIOS (version 1.14.0-2)
2023-03-27T10:30:10.0852108Z 
2023-03-27T10:30:10.0852114Z 
2023-03-27T10:30:10.0852120Z 
2023-03-27T10:30:10.0852416Z iPXE (http://ipxe.org) 00:03.0 CA00 PCI2.10 PnP PMM+1FF8F360+1FECF360 CA00
2023-03-27T10:30:10.0852666Z 
2023-03-27T10:30:10.0852886Z Press Ctrl-B to configure iPXE (PCI 00:03.0)...
2023-03-27T10:30:10.0853085Z 
2023-03-27T10:30:10.0853095Z 
2023-03-27T10:30:10.0853101Z 
2023-03-27T10:30:10.0853106Z 
2023-03-27T10:30:10.0853268Z Booting from ROM..Boot config: debug_port = 0x3f8
2023-03-27T10:30:10.0853423Z 
2023-03-27T10:30:10.0853560Z Boot config: disable_iommu = false
2023-03-27T10:30:10.0853766Z 
2023-03-27T10:30:10.0853892Z Detected 1 boot module(s):
2023-03-27T10:30:10.0854079Z 
2023-03-27T10:30:10.0854406Z   module #0: start=0xa14000 end=0xbac6d0 size=0x1986d0 name='images/capdl-loader-image-x86_64-pc99'
2023-03-27T10:30:10.0854661Z 
2023-03-27T10:30:10.0854759Z Parsing GRUB physical memory map
2023-03-27T10:30:10.0854948Z 
2023-03-27T10:30:10.0855106Z 	Physical Memory Region from 0 size 9fc00 type 1
2023-03-27T10:30:10.0855301Z 
2023-03-27T10:30:10.0855490Z 	Physical Memory Region from 9fc00 size 400 type 2
2023-03-27T10:30:10.0855694Z 
2023-03-27T10:30:10.0855871Z 	Physical Memory Region from f0000 size 10000 type 2
2023-03-27T10:30:10.0856066Z 
2023-03-27T10:30:10.0856193Z 	Physical Memory Region from 100000 size 1fee0000 type 1
2023-03-27T10:30:10.0856390Z 
2023-03-27T10:30:10.0856614Z Adding physical memory region 0x100000-0x1ffe0000
2023-03-27T10:30:10.0856814Z 
2023-03-27T10:30:10.0856977Z 	Physical Memory Region from 1ffe0000 size 20000 type 2
2023-03-27T10:30:10.0857200Z 
2023-03-27T10:30:10.0857379Z 	Physical Memory Region from fffc0000 size 40000 type 2
2023-03-27T10:30:10.0857527Z 
2023-03-27T10:30:10.0857672Z Multiboot gave us no video information
2023-03-27T10:30:10.0857862Z 
2023-03-27T10:30:10.0857990Z ACPI: RSDP paddr=0xf5b20
2023-03-27T10:30:10.0858159Z 
2023-03-27T10:30:10.0858284Z ACPI: RSDP vaddr=0xf5b20
2023-03-27T10:30:10.0858452Z 
2023-03-27T10:30:10.0858537Z ACPI: RSDT paddr=0x1ffe1550
2023-03-27T10:30:10.0858735Z 
2023-03-27T10:30:10.0858875Z ACPI: RSDT vaddr=0x1ffe1550
2023-03-27T10:30:10.0859044Z 
2023-03-27T10:30:10.0859236Z Kernel loaded to: start=0x100000 end=0xa13000 size=0x913000 entry=0x1002ea
2023-03-27T10:30:10.0859449Z 
2023-03-27T10:30:10.0859569Z ACPI: RSDT paddr=0x1ffe1550
2023-03-27T10:30:10.0859827Z 
2023-03-27T10:30:10.0859906Z ACPI: RSDT vaddr=0x1ffe1550
2023-03-27T10:30:10.0860082Z 
2023-03-27T10:30:10.0860234Z ACPI: FADT paddr=0x1ffe1404
2023-03-27T10:30:10.0860401Z 
2023-03-27T10:30:10.0860519Z ACPI: FADT vaddr=0x1ffe1404
2023-03-27T10:30:10.0860680Z 
2023-03-27T10:30:10.0860800Z ACPI: FADT flags=0x80a5
2023-03-27T10:30:10.0860921Z 
2023-03-27T10:30:10.0861043Z ACPI: MADT paddr=0x1ffe1478
2023-03-27T10:30:10.0861200Z 
2023-03-27T10:30:10.0861334Z ACPI: MADT vaddr=0x1ffe1478
2023-03-27T10:30:10.0861526Z 
2023-03-27T10:30:10.0861657Z ACPI: MADT apic_addr=0xfee00000
2023-03-27T10:30:10.0861837Z 
2023-03-27T10:30:10.0861911Z ACPI: MADT flags=0x1
2023-03-27T10:30:10.0862070Z 
2023-03-27T10:30:10.0862193Z ACPI: MADT_APIC apic_id=0x0
2023-03-27T10:30:10.0862359Z 
2023-03-27T10:30:10.0862548Z ACPI: MADT_IOAPIC ioapic_id=0 ioapic_addr=0xfec00000 gsib=0
2023-03-27T10:30:10.0862755Z 
2023-03-27T10:30:10.0862929Z ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0
2023-03-27T10:30:10.0863073Z 
2023-03-27T10:30:10.0863313Z ACPI: MADT_ISO bus=0 source=5 gsi=5 flags=0xd
2023-03-27T10:30:10.0863582Z 
2023-03-27T10:30:10.0863731Z ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xd
2023-03-27T10:30:10.0863925Z 
2023-03-27T10:30:10.0864077Z ACPI: MADT_ISO bus=0 source=10 gsi=10 flags=0xd
2023-03-27T10:30:10.0864279Z 
2023-03-27T10:30:10.0864384Z ACPI: MADT_ISO bus=0 source=11 gsi=11 flags=0xd
2023-03-27T10:30:10.0864580Z 
2023-03-27T10:30:10.0864730Z ACPI: 1 CPU(s) detected
2023-03-27T10:30:10.0864895Z 
2023-03-27T10:30:10.0865116Z ELF-loading userland images from boot modules:
2023-03-27T10:30:10.0865319Z 
2023-03-27T10:30:10.0865522Z size=0x30c000 v_entry=0x408477 v_start=0x400000 v_end=0x70c000 p_start=0xbad000 p_end=0xeb9000
2023-03-27T10:30:10.0865760Z 
2023-03-27T10:30:10.0865924Z Moving loaded userland images to final location: from=0xbad000 to=0xa13000 size=0x30c000
2023-03-27T10:30:10.0866267Z 
2023-03-27T10:30:10.0866399Z Starting node #0 with APIC ID 0
2023-03-27T10:30:10.0866609Z 
2023-03-27T10:30:10.0866749Z Mapping kernel window is done
2023-03-27T10:30:10.0866927Z 
2023-03-27T10:30:10.0867064Z available phys memory regions: 1
2023-03-27T10:30:10.0867200Z 
2023-03-27T10:30:10.0867327Z   [100000..1ffe0000]
2023-03-27T10:30:10.0867480Z 
2023-03-27T10:30:10.0867624Z reserved virt address space regions: 1
2023-03-27T10:30:10.0867822Z 
2023-03-27T10:30:10.0867992Z   [ffffff8000100000..ffffff8000d1f000]
2023-03-27T10:30:10.0868173Z 
2023-03-27T10:30:10.0868332Z Booting all finished, dropped to user space
2023-03-27T10:30:10.0868481Z 
2023-03-27T10:30:10.0868611Z Waiting for producer
2023-03-27T10:30:10.0868776Z 
2023-03-27T10:30:10.0868887Z 2: produce
2023-03-27T10:30:10.0869034Z 
2023-03-27T10:30:10.0869139Z 1: produce
2023-03-27T10:30:10.0869308Z 
2023-03-27T10:30:10.0869376Z Got badge: 2
2023-03-27T10:30:10.0869527Z 
2023-03-27T10:30:10.0869638Z Got badge: 1
2023-03-27T10:30:10.0869799Z 
2023-03-27T10:30:10.0869902Z 2: produce
2023-03-27T10:30:10.0870044Z 
2023-03-27T10:30:10.0870103Z 1: produce
2023-03-27T10:30:10.0870249Z 
2023-03-27T10:30:10.0870352Z Got badge: 2
2023-03-27T10:30:10.0870526Z 
2023-03-27T10:30:10.0870633Z Got badge: 1
2023-03-27T10:30:10.0870790Z 
2023-03-27T10:30:10.0870899Z 2: produce
2023-03-27T10:30:10.0870997Z 
2023-03-27T10:30:10.0871099Z 1: produce
2023-03-27T10:30:10.0871237Z 
2023-03-27T10:30:10.0871342Z Got badge: 2
2023-03-27T10:30:10.0871488Z 
2023-03-27T10:30:10.0871616Z Got badge: 1
2023-03-27T10:30:10.0871759Z 
2023-03-27T10:30:10.0871820Z 2: produce
2023-03-27T10:30:10.0871970Z 
2023-03-27T10:30:10.0872070Z 1: produce
2023-03-27T10:30:10.0872211Z 
2023-03-27T10:30:10.0872318Z Got badge: 2
2023-03-27T10:30:10.0872462Z 
2023-03-27T10:30:10.0872567Z Got badge: 1
2023-03-27T10:30:10.0872667Z 
2023-03-27T10:30:10.0872793Z 2: produce
2023-03-27T10:30:10.0872944Z 
2023-03-27T10:30:10.0873052Z 1: produce
2023-03-27T10:30:10.0873191Z 
2023-03-27T10:30:10.0873297Z Got badge: 2
2023-03-27T10:30:10.0873397Z 
2023-03-27T10:30:10.0873504Z Got badge: 1
2023-03-27T10:30:10.0873648Z 
2023-03-27T10:30:10.0873849Z Succes2: produce
2023-03-27T10:30:10.0874048Z 
2023-03-27T10:30:10.0874150Z 1: produce
2023-03-27T10:30:10.0874291Z 
2023-03-27T10:30:10.0874349Z s!
2023-03-27T10:30:10.0874485Z 
2023-03-27T10:30:10.0874640Z Caught cap fault in send phase at address 0
2023-03-27T10:30:10.0874832Z 
2023-03-27T10:30:10.0874951Z while trying to handle:
2023-03-27T10:30:10.0875126Z 
2023-03-27T10:30:10.0875305Z vm fault on data at address 0 with status 0x4
2023-03-27T10:30:10.0875453Z 
2023-03-27T10:30:10.0875623Z in thread 0xffffff80083a4400 "tcb_consumer" at address 0
2023-03-27T10:30:10.0875827Z 
2023-03-27T10:30:10.0875935Z With stack:
2023-03-27T10:30:10.0876088Z 
2023-03-27T10:30:10.0876198Z 0x41bee8: 0x407f8e
2023-03-27T10:30:10.0876351Z 
2023-03-27T10:30:10.0876418Z 0x41bef0: 0x419000
2023-03-27T10:30:10.0876584Z 
2023-03-27T10:30:10.0876714Z 0x41bef8: 0x0
2023-03-27T10:30:10.0876865Z 
2023-03-27T10:30:10.0876974Z 0x41bf00: 0x41bf40
2023-03-27T10:30:10.0877120Z 
2023-03-27T10:30:10.0877228Z 0x41bf08: 0x407bdf
2023-03-27T10:30:10.0877331Z 
2023-03-27T10:30:10.0877436Z 0x41bf10: 0x0
2023-03-27T10:30:10.0877591Z 
2023-03-27T10:30:10.0877701Z 0x41bf18: 0x41bfd8
2023-03-27T10:30:10.0877866Z 
2023-03-27T10:30:10.0877978Z 0x41bf20: 0x41bfd0
2023-03-27T10:30:10.0878128Z 
2023-03-27T10:30:10.0878190Z 0x41bf28: 0x41bfb8
2023-03-27T10:30:10.0878339Z 
2023-03-27T10:30:10.0878443Z 0x41bf30: 0x2
2023-03-27T10:30:10.0878587Z 
2023-03-27T10:30:10.0878704Z 0x41bf38: 0x4019f9
2023-03-27T10:30:10.0878849Z 
2023-03-27T10:30:10.0878980Z 0x41bf40: 0x41bf90
2023-03-27T10:30:10.0879082Z 
2023-03-27T10:30:10.0879192Z 0x41bf48: 0x407b81
2023-03-27T10:30:10.0879335Z 
2023-03-27T10:30:10.0879443Z 0x41bf50: 0x0
2023-03-27T10:30:10.0879595Z 
2023-03-27T10:30:10.0879713Z 0x41bf58: 0x41bfb0
2023-03-27T10:30:10.0879862Z 
2023-03-27T10:30:10.0880013Z 0x41bf60: 0x0
2023-03-27T10:30:10.0880162Z 
2023-03-27T10:30:10.0880427Z Failure! <class 'pexpect.exceptions.TIMEOUT'>
2023-03-27T10:30:10.0880982Z   File "/github/workspace/build/../projects/sel4-tutorials/test.py", line 144, in <module>
2023-03-27T10:30:10.0881365Z     sys.exit(main())
2023-03-27T10:30:10.0881760Z   File "/github/workspace/build/../projects/sel4-tutorials/test.py", line 139, in main
2023-03-27T10:30:10.0882105Z     run_tests(tests)
2023-03-27T10:30:10.0882576Z   File "/github/workspace/build/../projects/sel4-tutorials/test.py", line 107, in run_tests
2023-03-27T10:30:10.0883055Z     run_single_test(config, app, temp_file)
2023-03-27T10:30:10.0883542Z   File "/github/workspace/build/../projects/sel4-tutorials/test.py", line 87, in run_single_test
2023-03-27T10:30:10.0883979Z     if run_single_test_iteration(build_dir, solution, temp_file):
2023-03-27T10:30:10.0884511Z   File "/github/workspace/build/../projects/sel4-tutorials/test.py", line 50, in run_single_test_iteration
2023-03-27T10:30:10.0884899Z     result = check(_out=logfile, _cwd=build_dir)
2023-03-27T10:30:10.0885356Z   File "/usr/local/lib/python3.9/dist-packages/sh.py", line 1524, in __call__
2023-03-27T10:30:10.0885779Z     return RunningCommand(cmd, call_args, stdin, stdout, stderr)
2023-03-27T10:30:10.0886230Z   File "/usr/local/lib/python3.9/dist-packages/sh.py", line 788, in __init__
2023-03-27T10:30:10.0886575Z     self.wait()
2023-03-27T10:30:10.0886975Z   File "/usr/local/lib/python3.9/dist-packages/sh.py", line 845, in wait
2023-03-27T10:30:10.0887351Z     self.handle_command_exit_code(exit_code)
2023-03-27T10:30:10.0887780Z   File "/usr/local/lib/python3.9/dist-packages/sh.py", line 869, in handle_command_exit_code
2023-03-27T10:30:10.0888148Z     raise exc
2023-03-27T10:30:10.0888438Z sh.ErrorReturnCode_2: 
2023-03-27T10:30:10.0888567Z 
2023-03-27T10:30:10.0888750Z   RAN: /github/workspace/notificationsg3wja63r_build/check
2023-03-27T10:30:10.0888964Z 
2023-03-27T10:30:10.0889071Z   STDOUT:
2023-03-27T10:30:10.0889224Z 
2023-03-27T10:30:10.0889230Z 
2023-03-27T10:30:10.0889357Z   STDERR:
2023-03-27T10:30:10.0889513Z

Include File Path Error in hello-camkes-2 Tutorial

I was having trouble with compiling the hello-camkes-2 tutorial, so I downloaded the solution source files for the hello-camkes-2 tutorial and inserted them on top of the initial file set, to ensure they were located in the right place. I received compiler errors on all instances of

include "str_buf.h".

This affected about 8-10 files. I took the easy way of changing these instances to point to an absolute path of "/home/sel4/sel4-tutorials-camkes/projects/sel4-tutorials/solutions/hello-camkes-2/include/str_buf.h", which enabled the example to compile and run correctly. Since there are multiple tutorials and multiple instances of the str_buf.h file, I wasn't sure of the most elegant way to fix the path issue.

Caught cap fault in send phase at address 0x0 while trying to handle:

Hi,
I configure my environment according to https://docs.sel4.systems/HostDependencies, and I get the code following "repo init -u https://github.com/SEL4PROJ/sel4-tutorials-manifest -b refs/tags/sel4-tutorials-9.0.1
repo sync". After "make pc99_hello-1_defcongfig" and "make", I run it by "qemu-system-i386 -nographic -m 512 -kernel images/kernel-ia32-pc99 -initrd images/hello-1-image-ia32-pc99". It successfully print "hello world". But when I do hello-2 like this, there is an exception :
"Caught cap fault in send phase at address 0x0
while trying to handle:
user exception 0x6 code 0x0
in thread 0xffaf7400 "rootserver" at address 0x80571eb
With stack:
0x807b2b0: 0x0
0x807b2b4: 0x0
0x807b2b8: 0x0
0x807b2bc: 0x0
0x807b2c0: 0x0
0x807b2c4: 0x0
0x807b2c8: 0x0
0x807b2cc: 0x0
0x807b2d0: 0x0
0x807b2d4: 0x0
0x807b2d8: 0x0
0x807b2dc: 0x0
0x807b2e0: 0x0
0x807b2e4: 0x0
0x807b2e8: 0x0
0x807b2ec: 0x0
"
I don't know what's wrong, and do you have any ideas? Thank you!

Bug in the hello-camkes-timer tutorial

As far as I can see there is a bug with the hello-camkes-timer tutorial. The expected output after running the tutorial should be:

"------Sleep for X seconds------" and with a delay of 2 seconds (by default) a second message "After the client: wakeup"

Real behavior: the program prints out the 2 messages without a delay.

I suspect that the cause for this is that:

ttc_start() starts the timer and it immediately generates an interrupt
in the irq_handle() we release the semaphore and stop the timer
the timer will not generate interrupts anymore and the semaphore is not locked so the delay in the hello sleep will not occur (hello_sleep() is executed after the hello_init() and irq_handle())

Shared Folder Warning during VirtualBox Startup

Note: This is only a warning and doesn't seem to prevent the tutorials from working correctly, at least that I've found so far.

When I start VirtualBox with your provided virtual machine image (Version 4.3.18 -- I know 5.0.0 is recommended, but I cannot get that through my corporate repository yet), I get the following warning:

"The virtual machine execution may run into an error condition as described below. We suggest that you take an appropriate action to avert the error.The shared folder 'Shared' could not be set up: Shared folder path '/Users/ikuz/VirtualBox VMs/Shared' is not absolute. The shared folder setup will not be complete. It is recommended to power down the virtual machine and fix the shared folder settings while the machine is not running.
Error ID: BrokenSharedFolder
Severity: Warning"

When the CAmkES tutorials can be supported.

Hi, now it only support the native seL4 tutorials, when we can try the CAmkES tutorials? Thanks!
Sincerely!

hello-2: Deprecated API

seL4_GetBootInfo and simple_default_init_bootinfo are deprecated. hello-2 app won't compile.

Edit: The problem is that I used repo tool with sel4-tutorials.xml in sel4-tutorials-manifest. The manifest file configure the project for version seL4 version 3.2, not the current version.

Question about seL4_ARCH_PageTable_Map() in the dynamic-2 TASK 4

Hi,

Why is the ipc_buffer_vaddr put in seL4_ARCH_PageTable_Map()?
ipc_buffer_vaddr is the virtual address of the new physical frame allocated for the IPC buffer.
I think seL4_ARCH_PageTable_Map's 3rd parameter is the virtual address of the page table frame.

Mincheol

Discussion starter: Possible improvements to hello-camkes-2 tutorial.

Regarding this tutorial, I believe there is a chance to make some changes to improve the goals of having the tutorial around.

Following through the hello-camkes-2 tutorial, it asked for a lot of steps, without being explicit about how to confirm that you are progressing correctly. Being unfamiliar with a workflow that works well, it was unclear to me how and when to stop and validate work done up to a given point.

When I started over again, from the beginning of hello-camkes-2, I took a modified approach. In this approach I accomplished smaller things in smaller steps, validating each along the way. I would not move on to the next step until I was satisfied with the current

Understand setting up producer/consumer events each side

confirmed through successful build

Setup shared memory buffer

confirmed by printing it client-side

Bring server into the equation

confirmed with a log message in the handler

print the shared buffer
modify shared buffer

confirmed by repeating the print

signal the client

confirmed with a log message after the wait()

print the same buffer again

Expect to see changes propagated from server

I did a similar work flow for the typed dataport.

Generate clean CMake project

Currently, the generate CMake project is incomplete.
simulate.py is located in the build directory, but it is necessary to build the project.

I worked around the issue by appending the following to hello-world/CMakeLists.txt.

set(SEL4_TUTORIALS_DIR ../projects/sel4-tutorials)
set(TUT_BOARD pc)
set(TUT_ARCH x86_64)
set(TUTORIAL_DIR hello-world)

Problem on linux vm tutorial

I have been trying to make (ninja) the solution of camkes-linux-vm works for a week now and I can't seem to do so. I have limited experience on everything related with sel4 and compiler stuff.

Also, first of all I am aware of this: #80
and this: https://github.com/seL4/sel4-tutorials/pull/81/files/445c6319bab65c4d0b4e7c063ac065800322bfda

However, even with the changes, I see the following:

Performing configure step for 'poke-module'
FAILED: poke-module-stamp/poke-module-configure /home/admin2/seL4_tutorial/camkes-vm-linuxvfpqy831_build/poke-module-stamp/poke-module-configure
cd /home/admin2/seL4_tutorial/camkes-vm-linuxvfpqy831_build/poke-module && /usr/bin/cmake -DCMAKE_BUILD_TYPE=Debug -DCMAKE_TOOLCHAIN_FILE=/home/admin2/seL4_tutorial/tools/seL4/cmake-tool/polly_toolchains/linux-gcc-32bit-pic.cmake -DLINUX_KERNEL_DIR=/home/admin2/seL4_tutorial/camkes-vm-linuxvfpqy831_build/out/linux-4.8.16 -DMODULE_HELPERS_FILE=/home/admin2/seL4_tutorial/projects/camkes-vm-linux/linux-module-helpers.cmake -GNinja /home/admin2/seL4_tutorial/camkes-vm-linuxvfpqy831/modules && /usr/bin/cmake -E touch /home/admin2/seL4_tutorial/camkes-vm-linuxvfpqy831_build/poke-module-stamp/poke-module-configure
CMake Warning (dev) in CMakeLists.txt:
No project() command is present. The top-level CMakeLists.txt file must
contain a literal, direct call to the project() command. Add a line of
code such as
project(ProjectName)
near the top of the file, but after cmake_minimum_required().
CMake is pretending there is a "project(Project)" command on the first
line.
This warning is for project developers. Use -Wno-dev to suppress it.
-- [polly] Used toolchain: Linux / gcc / PIC / c++11 support / 32 bit
-- The CXX compiler identification is GNU 11.3.0
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - failed
-- Check for working CXX compiler: /usr/bin/g++
-- Check for working CXX compiler: /usr/bin/g++ - broken
CMake Error at /usr/share/cmake-3.22/Modules/CMakeTestCXXCompiler.cmake:62 (message):
The C++ compiler
"/usr/bin/g++"
is not able to compile a simple test program.
It fails with the following output:
Change Dir: /home/admin2/seL4_tutorial/camkes-vm-linuxvfpqy831_build/poke-module/CMakeFiles/CMakeTmp
Run Build Command(s):/usr/bin/ninja cmTC_a7cf9 && [1/2] Building CXX object CMakeFiles/cmTC_a7cf9.dir/testCXXCompiler.cxx.o
[2/2] Linking CXX executable cmTC_a7cf9
FAILED: cmTC_a7cf9
: && /usr/bin/g++ -m32 -fPIC -std=c++11 CMakeFiles/cmTC_a7cf9.dir/testCXXCompiler.cxx.o -o cmTC_a7cf9 && :
/usr/bin/ld: skipping incompatible /usr/lib/gcc/x86_64-linux-gnu/11/libstdc++.so when searching for -lstdc++
/usr/bin/ld: skipping incompatible /usr/lib/gcc/x86_64-linux-gnu/11/libstdc++.a when searching for -lstdc++
/usr/bin/ld: cannot find -lstdc++: No such file or directory
/usr/bin/ld: skipping incompatible /usr/lib/gcc/x86_64-linux-gnu/11/libstdc++.so when searching for -lstdc++
collect2: error: ld returned 1 exit status
ninja: build stopped: subcommand failed.
CMake will not be able to correctly generate this project.
Call Stack (most recent call first):
CMakeLists.txt
-- Configuring incomplete, errors occurred!
See also "/home/admin2/seL4_tutorial/camkes-vm-linuxvfpqy831_build/poke-module/CMakeFiles/CMakeOutput.log".
See also "/home/admin2/seL4_tutorial/camkes-vm-linuxvfpqy831_build/poke-module/CMakeFiles/CMakeError.log".
ninja: build stopped: subcommand failed.

It seem that I don't have libstdc++11, however I tried
apt-get build-essential and sudo apt-get install libstdc++-11-dev-i386-cross. The latter one is me trying to compile it to a 32-bit thing, which as you can tell I don't even know what I am talking about.

In summary am I missing something? If it helps the ninja is sucessful when I init the tutorial without the solution.
Any input is appreciated.

Just so when I am here, the tutorial "camkes-vm-crossvm" just simply does not init, saying
CMake Error at CMakeLists.txt:20 (message): This application is only supported on x86_64 Call Stack (most recent call first): /home/admin2/seL4_tutorial/projects/sel4-tutorials/Findsel4-tutorials.cmake:23 (include) CMakeLists.txt:3 (sel4_tutorials_regenerate_tutorial)
But I am on 64 bit?
Thanks!

Mistake in capabilities tutorial

Not sure if this is the correct place to post this.

Lines 162-163 of capabilities.md, which are lines 4-5 of the main.c file:

size_t initial_cnode_object_size = BIT(info->initThreadCNodeSizeBits);
printf("Initial CNode is %zu bytes in size\n", initial_cnode_object_size);

However, BIT(n) is 1ul<<n, so this is not in fact reporting the CNode size is bytes.

If I understand correctly, BIT(info->initThreadCNodeSizeBits) would be the number of CSlots the CNode can hold, so the printf should perhaps read:

printf("Initial CNode is %zu slots in size\n", initial_cnode_object_size);

Of course this is inconsequential to what the tutorial is teaching, but it seemed worth pointing out.

Solution code not hidden in --tut hello-camkes-1 gen

In hello-camkes-1/interfaces/HelloSimple.idl4 Reading the hint, it seems that the following is expected

/* Simple RPC interface */
procedure HelloSimple {
    /* TODO define RPC functions */
    /* hint 1: define at least one function that takes a string as input parameter. call it say_hello. no return value
     * hint 2: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application
     */
};

got:

/* Simple RPC interface */
procedure HelloSimple {
    /* TODO define RPC functions */
    /* hint 1: define at least one function that takes a string as input parameter. call it say_hello. no return value
     * hint 2: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application
     */
    void say_hello(in string str);
};

If you go to tutorials/hello-camkes-1.md, line 177, you can see the filter-block with the line in question.

/*- filter File("interfaces/HelloSimple.idl4") --*/
/* Simple RPC interface */
procedure HelloSimple {
/*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="interface") -*/
    /* TODO define RPC functions */
    /* hint 1: define at least one function that takes a string as input parameter. call it say_hello. no return value
     * hint 2: look at https://github.com/seL4/camkes-tool/blob/master/docs/index.md#creating-an-application
     */
/*-- endfilter -*/
/*-- filter TaskContent("hello", TaskContentType.COMPLETED, subtask="interface") -*/
    void say_hello(in string str);
/*-- endfilter -*/
};
/*-- endfilter -*/

This approach to filtering and generation is new to me. Not sure about what sort of changes might be needed, assuming this isn't working as intended.

mcs tutorial: Simplify passive server initialization protocol example

Once seL4/seL4#523 is merged, setting up a passive server becomes simpler and doesn't need a special init protocol anymore. The mcs tutorial should take advantage of this when showing how to configure a passive server: https://github.com/seL4/sel4-tutorials/blob/master/tutorials/mcs/mcs.md#passive-servers-1

Running CAmkES Solution

I tried running the CAmkES solutions and, while everything seems to compile I am having an issue running them:

I started from the begining:

cd ~
mkdir -p camkes-fresh/camkes-solutions; cd camkes-fresh/camkes-solutions
repo init -u https://github.com/SEL4PROJ/sel4-tutorials-manifest -m camkes-solutions.xml
repo sync

I then did a make menuconfig and chose the CapDL Loader and Simple CAmkES Hello World Application. I also made note that it is being built for the x86 PC99 platform.

Then I did a make clean and then a make, it ended with a:

[GEN] /home/jesse/camkes-fresh/camkes-solutions/Makefile
[KERNEL]
 [MKDIR] arch/object
 [PBF_GEN] arch/object/structures.pbf
 [PBF_GEN] plat/machine/hardware.pbf
 [PBF_GEN] 32/mode/api/shared_types.pbf
 [BF_GEN] arch/object/structures_gen.h
 [BF_GEN] plat/machine/hardware_gen.h
 [BF_GEN] 32/mode/api/shared_types_gen.h
 [CPP] src/arch/x86/32/machine_asm.s_pp
 [AS] src/arch/x86/32/machine_asm.o
 [CPP] src/arch/x86/32/traps.s_pp
 [AS] src/arch/x86/32/traps.o
 [CPP] src/arch/x86/32/head.s_pp
 [AS] src/arch/x86/32/head.o
 [TOUCH] sources_list_updated
 [CPP_GEN] kernel_all.c
 [CPP] kernel_all.c_pp
 [Circular includes] kernel_all.c_pp
 [CP] kernel_final.c
 [CC] kernel_final.s
 [AS] kernel.o
l [CPP] linker.lds_pp
 [LD] kernel.elf
 [STRIP] kernel.elf.strip
 [STAGE] kernel.elf
[KERNEL] done.
[libs/libsel4] building...
 [GEN] include/interfaces/sel4_client.h
 [PBF_GEN] include/sel4/types_32.pbf
 [GEN] include/sel4/types_gen.h
 [GEN] include/sel4/syscall.h
 [GEN] include/sel4/invocation.h
 [GEN] arch_include/x86/sel4/arch/invocation.h
 [PBF_GEN] include/sel4/shared_types_32.pbf
 [GEN] include/sel4/shared_types_gen.h
 [GEN] sel4_arch_include/ia32/sel4/sel4_arch/invocation.h
 [PBF_GEN] include/sel4/sel4_arch/types.pbf
 [GEN] sel4_arch_include/ia32/sel4/sel4_arch/types_gen.h
 [HEADERS]
 [STAGE] sel4/*
 [STAGE] api/*
 [STAGE] interfaces/*
 [STAGE] sel4/*
 [STAGE] interfaces/*
 [STAGE] sel4/*
 [STAGE] interfaces/*
 [STAGE] sel4/*
 [STAGE] sel4/*
 [STAGE] interfaces/*
 [STAGE] sel4/*
 [STAGE] autoconf.h
 [CC] src/sel4_bootinfo.o
 [AR] libsel4.a objs: src/sel4_bootinfo.o   
 [STAGE] libsel4.a
[libs/libsel4] done.
[libs/libmuslc] building...
[libs/libmuslc] done.
[libs/libcpio] building...
 [HEADERS]
 [STAGE] cpio/*
 [STAGE] autoconf.h
 [CC] src/cpio.o
 [AR] libcpio.a objs: src/cpio.o   
 [STAGE] libcpio.a
[libs/libcpio] done.
[libs/libelf] building...
 [HEADERS]
 [STAGE] elf/*
 [STAGE] autoconf.h
 [CC] src/elf.o
 [CC] src/elf32.o
 [CC] src/elf64.o
 [AR] libelf.a objs: src/elf.o src/elf32.o src/elf64.o   
 [STAGE] libelf.a
[libs/libelf] done.
[libs/libutils] building...
 [HEADERS]
 [STAGE] utils/*
 [STAGE] utils/*
 [STAGE] autoconf.h
 [CC] src/zf_log.o
 [CC] src/xml.o
 [CC] src/list.o
 [CC] src/debug.o
 [CC] src/arch/x86/stack.o
 [AR] libutils.a objs: src/zf_log.o src/xml.o src/list.o src/debug.o src/arch/x86/stack.o   
 [STAGE] libutils.a
[libs/libutils] done.
[libs/libsel4vka] building...
 [HEADERS]
 [STAGE] vka/*
 [STAGE] vka/*
 [STAGE] vka/*
 [STAGE] autoconf.h
 [CC] src/debug-vka.o
 [CC] src/null-vka.o
 [AR] libsel4vka.a objs: src/debug-vka.o src/null-vka.o   
 [STAGE] libsel4vka.a
[libs/libsel4vka] done.
[libs/libsel4vspace] building...
 [HEADERS]
 [STAGE] vspace/*
 [STAGE] vspace/*
 [STAGE] autoconf.h
 [CC] src/vspace.o
 [AR] libsel4vspace.a objs: src/vspace.o   
 [STAGE] libsel4vspace.a
[libs/libsel4vspace] done.
[libs/libplatsupport] building...
 [HEADERS]
 [STAGE] platsupport/*
 [STAGE] platsupport/*
 [STAGE] platsupport/*
 [STAGE] autoconf.h
 [CC] src/plat/pc99/pit.o
 [CC] src/plat/pc99/keyboard_chardev.o
 [CC] src/plat/pc99/keyboard_ps2.o
 [CC] src/plat/pc99/keyboard_vkey.o
 [CC] src/plat/pc99/tsc_timer.o
 [CC] src/plat/pc99/ega.o
 [CC] src/plat/pc99/serial.o
 [CC] src/plat/pc99/rtc.o
 [CC] src/plat/pc99/hpet.o
 [CC] src/plat/pc99/chardev.o
 [CC] src/arch/x86/tsc.o
 [CC] src/plat/pc99/acpi/acpi.o
 [CC] src/plat/pc99/acpi/walker.o
 [CC] src/plat/pc99/acpi/browser.o
 [CC] src/plat/pc99/acpi/printer.o
 [CC] src/plat/pc99/acpi/regions.o
 [CC] src/serial.o
 [AR] libplatsupport.a objs: src/plat/pc99/pit.o src/plat/pc99/keyboard_chardev.o src/plat/pc99/keyboard_ps2.o src/plat/pc99/keyboard_vkey.o src/plat/pc99/tsc_timer.o src/plat/pc99/ega.o src/plat/pc99/serial.o src/plat/pc99/rtc.o src/plat/pc99/hpet.o src/plat/pc99/chardev.o src/arch/x86/tsc.o src/plat/pc99/acpi/acpi.o src/plat/pc99/acpi/walker.o src/plat/pc99/acpi/browser.o src/plat/pc99/acpi/printer.o src/plat/pc99/acpi/regions.o src/serial.o   
 [STAGE] libplatsupport.a
[libs/libplatsupport] done.
[libs/libsel4simple] building...
 [HEADERS]
 [STAGE] simple/*
 [STAGE] simple/*
 [STAGE] autoconf.h
 [CC] src/simple.o
 [AR] libsel4simple.a objs: src/simple.o   
 [STAGE] libsel4simple.a
[libs/libsel4simple] done.
[libs/libsel4debug] building...
 [HEADERS]
 [STAGE] sel4debug/*
 [STAGE] sel4debug/*
 [STAGE] sel4debug/*
 [STAGE] autoconf.h
 [CC] src/register_dump.o
 [CC] src/caps.o
 [CC] src/stack.o
 [CC] src/trace.o
 [CC] src/backtrace.o
 [CC] src/identity.o
 [CC] src/alloc.o
 [CC] src/faulthandler.o
 [CC] src/bootinfo.o
 [AR] libsel4debug.a objs: src/register_dump.o src/caps.o src/stack.o src/trace.o src/backtrace.o src/identity.o src/alloc.o src/faulthandler.o src/bootinfo.o   
 [STAGE] libsel4debug.a
[libs/libsel4debug] done.
[libs/libsel4simple-default] building...
 [HEADERS]
 [STAGE] simple-default/*
 [STAGE] autoconf.h
 [CC] src/libsel4simple-default.o
 [CC] src/arch/x86/default.o
 [AR] libsel4simple-default.a objs: src/libsel4simple-default.o src/arch/x86/default.o   
 [STAGE] libsel4simple-default.a
[libs/libsel4simple-default] done.
[libs/libsel4platsupport] building...
 [HEADERS]
 [STAGE] sel4platsupport/*
 [STAGE] sel4platsupport/*
 [STAGE] sel4platsupport/*
 [STAGE] autoconf.h
 [ASM] src/sel4_arch/ia32/sel4_crt0.o
 [ASM] src/sel4_arch/ia32/crt0.o
 [CC] src/timer_common.o
 [CC] src/common.o
 [CC] src/init.o
 [CC] src/io.o
 [CC] src/device.o
 [CC] src/serial.o
 [CC] src/arch/x86/io_port_ops.o
 [CC] src/plat/pc99/pit.o
 [CC] src/plat/pc99/device.o
 [CC] src/plat/pc99/hpet.o
 [CC] src/plat/pc99/timer.o
 [AR] libsel4platsupport.a objs:src/sel4_arch/ia32/sel4_crt0.o src/sel4_arch/ia32/crt0.o src/timer_common.o src/common.o src/init.o src/io.o src/device.o src/serial.o src/arch/x86/io_port_ops.o src/plat/pc99/pit.o src/plat/pc99/device.o src/plat/pc99/hpet.o src/plat/pc99/timer.o   
 [STAGE] libsel4platsupport.a
[libs/libsel4platsupport] done.
[libs/libsel4utils] building...
 [HEADERS]
 [STAGE] sel4utils/*
 [STAGE] sel4utils/*
 [STAGE] sel4utils/*
 [STAGE] autoconf.h
 [CC] src/mapping.o
 [CC] src/elf.o
 [CC] src/stack.o
 [CC] src/page_dma.o
 [CC] src/profile.o
 [CC] src/iommu_dma.o
 [CC] src/strerror.o
 [CC] src/process.o
 [CC] src/thread.o
 [CC] src/vspace/client_server_vspace.o
 [CC] src/vspace/vspace.o
 [CC] src/vspace/bootstrap.o
 [CC] src/irq_server/irq_server.o
 [CC] src/serial_server/parentapi.o
 [CC] src/serial_server/clientapi.o
 [CC] src/serial_server/server.o
 [CC] src/sel4_arch/ia32/arch.o
 [AR] libsel4utils.a objs: src/mapping.o src/elf.o src/stack.o src/page_dma.o src/profile.o src/iommu_dma.o src/strerror.o src/process.o src/thread.o src/vspace/client_server_vspace.o src/vspace/vspace.o src/vspace/bootstrap.o src/irq_server/irq_server.o src/serial_server/parentapi.o src/serial_server/clientapi.o src/serial_server/server.o src/sel4_arch/ia32/arch.o   
 [STAGE] libsel4utils.a
[libs/libsel4utils] done.
[libs/libsel4muslcsys] building...
 [HEADERS]
 [STAGE] arch_stdio.h
 [STAGE] autoconf.h
 [CC] src/sys_yield.o
 [CC] src/sys_thread.o
 [CC] src/sys_morecore.o
 [CC] src/vsyscall.o
 [CC] src/sys_stubs.o
 [CC] src/sys_io.o
 [CC] src/sys_exit.o
 [AR] libsel4muslcsys.a objs: src/sys_yield.o src/sys_thread.o src/sys_morecore.o src/vsyscall.o src/sys_stubs.o src/sys_io.o src/sys_exit.o   
 [STAGE] libsel4muslcsys.a
[libs/libsel4muslcsys] done.
[libs/libsel4camkes] building...
 [HEADERS]
 [STAGE] camkes/*
 [STAGE] autoconf.h
 [ASM] src/arch/x86/crt0.o
 [CC] src/error.o
 [CC] src/io.o
 [CC] src/main.o
 [CC] src/dma.o
 [CC] src/allocator.o
 [AR] libsel4camkes.a objs:src/arch/x86/crt0.o src/error.o src/io.o src/main.o src/dma.o src/allocator.o   
 [STAGE] libsel4camkes.a
[libs/libsel4camkes] done.
[libs/libsel4muslccamkes] building...
 [HEADERS]
 [STAGE] arch_stdio.h
 [STAGE] autoconf.h
 [CC] src/sys_yield.o
 [CC] src/sys_socket.o
 [CC] src/sys_signal.o
 [CC] src/sys_epoll.o
 [CC] src/sys_select.o
 [CC] src/sys_thread.o
 [CC] src/sys_morecore.o
 [CC] src/vsyscall.o
 [CC] src/sys_stubs.o
 [CC] src/sys_io.o
 [CC] src/sys_exit.o
 [CC] src/sys_clock.o
 [CC] src/sys_pause.o
 [AR] libsel4muslccamkes.a objs: src/sys_yield.o src/sys_socket.o src/sys_signal.o src/sys_epoll.o src/sys_select.o src/sys_thread.o src/sys_morecore.o src/vsyscall.o src/sys_stubs.o src/sys_io.o src/sys_exit.o src/sys_clock.o src/sys_pause.o   
 [STAGE] libsel4muslccamkes.a
[libs/libsel4muslccamkes] done.
[libs/libsel4sync] building...
 [HEADERS]
 [STAGE] sync/*
 [STAGE] autoconf.h
 [CC] src/recursive_mutex.o
 [AR] libsel4sync.a objs: src/recursive_mutex.o   
 [STAGE] libsel4sync.a
[libs/libsel4sync] done.
[apps/hello-camkes-1] building...
/home/jesse/camkes-fresh/camkes-solutions/tools/camkes/camkes.mk:126: /home/jesse/camkes-fresh/camkes-solutions/build/x86/pc99/hello-camkes-1/camkes-gen.mk: No such file or directory
 [GEN] camkes-gen.mk
 [HEADERS]
 [STAGE] autoconf.h
 [CP] echo.c
 [GEN] Echo.h
 [GEN] camkes.h
 [GEN] Echo.c
 [GEN] hello_seL4RPCCall.c
 [CC] echo.o
 [CC] Echo.o
 [CC] hello_seL4RPCCall.o
 [GEN] linker.lds
 [LD] echo.instance.bin
 [CP] client.c
 [GEN] Client.h
 [GEN] camkes.h
 [GEN] Client.c
 [GEN] hello_seL4RPCCall.c
 [CC] client.o
 [CC] Client.o
 [CC] hello_seL4RPCCall.o
 [GEN] linker.lds
 [LD] client.instance.bin
 [OBJCOPY] echo.instance-copy.bin
 [CP] echo_group_bin
 [STAGE] echo_group_bin
 [OBJCOPY] client.instance-copy.bin
 [CP] client_group_bin
 [STAGE] client_group_bin
 [GEN] hello-camkes-1.cdl
[apps/hello-camkes-1] done.
[parse-capDL] building...
make: Entering directory '/home/jesse/camkes-fresh/camkes-solutions/projects/capdl/capDL-tool'
stack setup
stack will use a sandboxed GHC it installed
For more information on paths, see 'stack path' and 'stack exec env'
To use this GHC and packages outside of a project, consider using:
stack ghc, stack ghci, stack runghc, or stack exec
stack build --only-dependencies
make: Leaving directory '/home/jesse/camkes-fresh/camkes-solutions/projects/capdl/capDL-tool'
make: Entering directory '/home/jesse/camkes-fresh/camkes-solutions/projects/capdl/capDL-tool'
make: Nothing to be done for 'all'.
make: Leaving directory '/home/jesse/camkes-fresh/camkes-solutions/projects/capdl/capDL-tool'
make: Entering directory '/home/jesse/camkes-fresh/camkes-solutions/projects/capdl/capDL-tool'
stack install
Copying from /home/jesse/camkes-fresh/camkes-solutions/projects/capdl/capDL-tool/.stack-work/install/x86_64-linux/lts-7.10/8.0.1/bin/parse-capDL to /home/jesse/camkes-fresh/camkes-solutions/projects/capdl/capDL-tool/parse-capDL

Copied executables to /home/jesse/camkes-fresh/camkes-solutions/projects/capdl/capDL-tool:
- parse-capDL

WARNING: Installation path /home/jesse/camkes-fresh/camkes-solutions/projects/capdl/capDL-tool not found on the PATH environment variable
make: Leaving directory '/home/jesse/camkes-fresh/camkes-solutions/projects/capdl/capDL-tool'
[parse-capDL] done.
[cpio-strip] building...
 [CC] cpio-strip
[cpio-strip] done.
[apps/capdl-loader-experimental] building...
 [HEADERS]
 [STAGE] debug.h
 [STAGE] capdl_spec.h
 [STAGE] capdl.h
 [STAGE] autoconf.h
 [GEN] capdl_spec.c
 [CPIO] archive.o
  [CPIO] client_group_bin
  [CPIO] echo_group_bin
 [CC] src/main.o
 [CC] /home/jesse/camkes-fresh/camkes-solutions/build/x86/pc99/capdl-loader-experimental/src/capdl_spec.o
 [LINK] capdl-loader-experimental.elf
 [STAGE] capdl-loader-experimental.bin
 [STAGE] capdl-loader-experimental
[apps/capdl-loader-experimental] done.
[GEN_IMAGE] capdl-loader-experimental-image

Then to run it I ran:

qemu-system-i386 -m 512 -nographic -kernel images/kernel-ia32-pc99 -initrd images/capdl-loader-experimental-image-ia32-pc99

It printed out:

Boot config: parsing cmdline 'images/kernel-ia32-pc99 '
Boot config: console_port = 0x3f8
Boot config: debug_port = 0x3f8
Boot config: disable_iommu = false
Warning: Your kernel was not compiled for the current microarchitecture.
Parsing GRUB physical memory map
	Physical Memory Region from 0 size 9fc00 type 1
	Physical Memory Region from 9fc00 size 400 type 2
	Physical Memory Region from f0000 size 10000 type 2
	Physical Memory Region from 100000 size 1fee0000 type 1
Adding physical memory region 0x100000-0x1fc00000
	Physical Memory Region from 1ffe0000 size 20000 type 2
	Physical Memory Region from fffc0000 size 40000 type 2
Kernel loaded to: start=0x100000 end=0x13d000 size=0x3d000 entry=0x10003a
ACPI: RSDP paddr=0xf6460
ACPI: RSDP vaddr=0xdfcf6460
ACPI: RSDT paddr=0x1ffe16ee
ACPI: RSDT vaddr=0xdffe16ee
ACPI: FADT paddr=0x1ffe0c14
ACPI: FADT vaddr=0xdffe0c14
ACPI: FADT flags=0x80a5
ACPI: 0 IOMMUs detected
ACPI: MADT paddr=0x1ffe163e
ACPI: MADT vaddr=0xdffe163e
ACPI: MADT apic_addr=0xfee00000
ACPI: MADT flags=0x1
ACPI: MADT_APIC apic_id=0x0
ACPI: MADT_IOAPIC ioapic_id=0 ioapic_addr=0xfec00000 gsib=0
ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0
ACPI: MADT_ISO bus=0 source=5 gsi=5 flags=0xd
ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xd
ACPI: MADT_ISO bus=0 source=10 gsi=10 flags=0xd
ACPI: MADT_ISO bus=0 source=11 gsi=11 flags=0xd
ACPI: 1 CPU(s) detected
Detected 1 IOAPICs, but configured to use PIC instead
Detected 1 boot module(s):
  module #0: start=0x13e000 end=0x259794 size=0x11b794 name='images/capdl-loader-experimental-image-ia32-pc99'
ELF-loading userland images from boot modules:
size=0x1d1000 v_entry=0x804ef04 v_start=0x8048000 v_end=0x8219000 p_start=0x25a000 p_end=0x42b000
Moving loaded userland images to final location: from=0x25a000 to=0x13d000 size=0x1d1000
Starting node #0 with APIC ID 0
Booting all finished, dropped to user space
Assertion failed: free_slot_end - free_slot_start >= CONFIG_CAPDL_LOADER_MAX_OBJECTS (/home/jesse/camkes-fresh/camkes-solutions/apps/capdl-loader-experimental/src/main.c: parse_bootinfo: 574)
Ignoring call to sys_rt_sigprocmask
Ignoring call to sys_gettid
sys_tkill assuming self kill

This doesn't seem to be working. I looked at the apps/hello-camkes-1/ files and it seems that there should be at least something printing. The line about the "Assertion failed" seems concerning.

Is this not the proper way to build the solutions?

I just finished the sel4-tutorials and that is how it was handled there it seems.

Thanks

`capdl_linker.py` is not executable

capDL is introduced in the threads tutorial but it appears that the logic for running the capdl_linker.py script via cmake may be broken. AFAICT a clean checkout of the tutorials and capdl repositories, and a clean ../init --tut threads results in a build error when we try to execute the script with its #! rather than explicitly via python.

[1/12] cd /path/to/sel4-tutorials/threads_build && /usr/bin/cmake -E env PYTHONPATH=/path/to/sel4-tutorials/projects/capdl/python-capdl-tool /path/to/sel4-tutorials/projects/capdl/cdl_utils/capdl_linker.py --arch=x86_64 --object-sizes /path/to/sel4-tutorials/threads_build/capdl/object_sizes/object_sizes.yaml build_cnode --manifest-in=/path/to/sel4-tutorials/threads/.manifest.obj --elffile threads --ccspace /path/to/sel4-tutorials/threads_build/cspace_threads.c
FAILED: cspace_threads.c
cd /path/to/sel4-tutorials/threads_build && /usr/bin/cmake -E env PYTHONPATH=/path/to/sel4-tutorials/projects/capdl/python-capdl-tool /path/to/sel4-tutorials/projects/capdl/cdl_utils/capdl_linker.py --arch=x86_64 --object-sizes /path/to/sel4-tutorials/threads_build/capdl/object_sizes/object_sizes.yaml build_cnode --manifest-in=/path/to/sel4-tutorials/threads/.manifest.obj --elffile threads --ccspace /path/to/sel4-tutorials/threads_build/cspace_threads.c
Permission denied
ninja: build stopped: subcommand failed.

chmod u+x .../capdl_linker.py fixes the build. It's unclear to me if this is the the tutorial's cmake logic's fault or if the capdl repo should be changed to make the script executable.

Tutorials using CAmkES / capDL fail an assertion

Using the Docker image, I started with a fresh copy of the tutorial repo:

mkdir test && cd test
repo init -u https://github.com/SEL4PROJ/sel4-tutorials-manifest
repo sync

(I did have to change .repo/manifest.xml from <project name="polly" to <project name="polly.git" to get the sync to work, not sure if this is related or a networking issue on my end).

From here, I'm able to build the tutorials, and Capabilities, Untyped, Mapping, and the Dynamic Libraries tutorials build and run fine. For any tutorials using CAmkES / capDL (Threads, IPC, Notifications, Interrupts, Faults, Camkes, Camkes 1-3 (Camkes VM Linux had an unrelated build error)), I run into some issues.

Towards the end of the build there is a warning:

Warning: Installation path /host/test/hello-camkes-timer_build/hello-camkes-timer/capDL-tool not found on the PATH environment variable.

Adding the directory to the path does not make a difference with this issue.

If I try to run any of the CAmkES / capDL tutorials with ./simulate I get the initial QEMU output then see:

Assertion failed: free_slot_end - free_slot_start >= CONFIG_CAPDL_LOADER_MAX_OBJECTS (../projects/camkes/capdl/capdl-l)

This seems to be the same error as in #12, but I'm not sure if the resolution there is applicable since it used the older build system. I also noticed that ../projects/camkes/capdl/capdl-l does not exist.

apps/hello-3 some confusing steps

/* TODO 12: make sure it is what we expected */
Already has the code in place.

/* TODO 7: make a badged copy of it in our cspace. This copy will be used to send
* an IPC message to the original cap */
The TODO is described using vka_mint_object however the Error text below it mentions seL4_Mint

The manual it links to describes seL4_CNode_Mint, I did not see a seL4_Mint described.
perhaps a link to the header where cspacepath_t is declared?

Cap fault in dynamic-3 tutorial

The dynamic-3 tutorial involves spawning a new process which sends data to the root thread. I am hitting a weird error during the spawning process.

    /* TASK 5: spawn the process */
    /* hint 1: sel4utils_spawn_process_v()
     * int sel4utils_spawn_process_v(sel4utils_process_t *process, vka_t *vka, vspace_t *vspace, int argc, char *argv[], int resume)
     * @param process Initialised sel4utils process struct.
     * @param vka Vka interface to use for allocation of frames.
     * @param vspace The current vspace.
     * @param argc The number of arguments.
     * @param argv A pointer to an array of strings in the current vspace.
     * @param resume 1 to start the process, 0 to leave suspended.
     * @return 0 on success, -1 on error.
     */
    char *argv[] = { (char*)new_ep_cap };
    error = sel4utils_spawn_process_v(&new_process, &vka, &vspace, 1,  argv, 1);
    ZF_LOGF_IFERR(error, "Failed to spawn and start the new thread.\n"
                  "\tVerify: the new thread is being executed in the root thread's VSpace.\n"
                  "\tIn this case, the CSpaces are different, but the VSpaces are the same.\n"
                  "\tDouble check your vspace_t argument.\n");

new_ep_cap is a badged endpoint capability returned from a call to sel4utils_mint_cap_to_process. The spawn process in app.c provides the following hint and code:

    /* TASK 8: send and wait for a reply */
    /* hint 1: seL4_Call()
     * seL4_MessageInfo_t seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
     * @param dest The capability to be invoked.
     * @param msgInfo The messageinfo structure for the IPC.  This specifies information about the message to send (such as the number of message registers to send).
     * @return A seL4_MessageInfo_t structure.  This is information about the repy message.
     *
     * hint 2: send the endpoint cap using argv (see TASK 6 in the other main.c)
     */
    ZF_LOGF_IF(argc < 1,
               "Missing arguments.\n");
    seL4_CPtr ep = (seL4_CPtr) atol(argv[0]);

However, sending the endpoint capability in this way results in a cap fault:

Caught cap fault in send phase at address (nil)
while trying to handle:
vm fault on data at address 0x8 with status 0x4
in thread 0xffffff801fe08400 "dynamic-3" at address 0x43b9c9
With stack:
0x4a9c48: 0x40becd
0x4a9c50: 0x4a9cc0
0x4a9c58: 0x4a9ef8
0x4a9c60: 0x1004a9f80
0x4a9c68: 0x4af120
0x4a9c70: 0x4a9f80
0x4a9c78: 0x4af080
0x4a9c80: 0x6ca
0x4a9c88: 0x1c0
0x4a9c90: 0x1c0
0x4a9c98: 0x1c8
0x4a9ca0: 0x4a9ed0
0x4a9ca8: 0x40c4f1
0x4a9cb0: 0x4a9e40
0x4a9cb8: 0x0
0x4a9cc0: 0x4a9ed0

This error occurs even in cases where I do not use the endpoint capability in the spawned thread, i.e. commenting out the ep assignment.

Confusingly, there are also some (I think erroneous) hints in the root thread about using the badged endpoint capability which appears to conflict with the root thread's role as receiver:

seL4_Word sender_badge = 0;
    seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 0, 0);
    seL4_Word msg;

    /* TASK 6: wait for a message */
    /* hint 1: seL4_Recv()
     * seL4_MessageInfo_t seL4_Recv(seL4_CPtr src, seL4_Word* sender)
     * @param src The capability to be invoked.
     * @param sender The badge of the endpoint capability that was invoked by the sender is written to this address.
     * @return A seL4_MessageInfo_t structure
     *
     * hint 2: seL4_MessageInfo_t is generated during build.
     * hint 3: use the badged endpoint cap that you minted above
     */```

hello-4 recommends using badged cap for receiving

The hello-4 example recommends that the receiver use the badged cap for receiving. I would expect it to recommend just using the original (unbadged) cap.

https://github.com/SEL4PROJ/sel4-tutorials/blob/master/apps/hello-4/src/main.c#L238

https://github.com/SEL4PROJ/sel4-tutorials/blob/master/apps/hello-4/src/main.c#L272

unable to install prerequisites

I am trying to install the prerequisites from https://github.com/SEL4PROJ/sel4-tutorials/blob/master/Prerequisites.md on ubuntu 16.04

When trying to install MissingH I have the following problem:

$ cabal install MissingH-1.3.0.2
Resolving dependencies...
cabal Could not resolve dependencies:
next goal: MissingH (user goal)
rejecting: MissingH-1.4.0.1, 1.4.0.0 (global constraint)
trying: MissingH-1.3.0.2
next goal: hslogger (dependency of MissingH-1.3.0.2)
Dependency tree exhaustively searched.

Incorrect/outdated instructions for repo

The repo manifest contains a distinction between seL4 and camkes tutorials. It appears to me that, at some point, this was done using differently named XML manifest files, but it is now done by putting the different manifests into separate branches.
However, at several points in the documentation, learners are instructed to select the manifest they want to check out by filename (which will no longer work and produce a fatal error).

The old instructions ask the user to execute the following command:

repo init -u http://github.com/sel4proj/sel4-tutorials-manifest -m sel4-tutorials.xml

I believe that the correct command should be either:

repo init -u http://github.com/sel4proj/sel4-tutorials-manifest -b sel4-tutorials

or:

repo init -u http://github.com/sel4proj/sel4-tutorials-manifest

The first option seems more likely to me, but from looking at the manifest repository on GitHub, I am not sure which one is correct.

This includes, at least:

The README of this repository
The Wiki (pages "Getting Started", "Tutorials" and "seL4 Tutorial 1")
The file "docs/seL4-APILib-details.pdf" in this repository

I am neither experienced in nor committed to this project enough to do this myself, but does somebody want to update this?

How can I use another image?

I want to use a image build by buildroot not the file under projects/camkes-vm-linux/images/rootfs/64/default_buildroot_rootfs-bare.cpio.I want build another file system,including my own packages,How can I get it?

dynamic-2 is misrendered on sel4.systems

https://docs.sel4.systems/Tutorials/dynamic-2.html

It looks like the renderer has gotten confused about where code block fences start and end. It seems like it could be the fault of line 232 which has a closing fence with a leading space, but if not that then I have no idea.

Not able to input in buildroot camkes-vm-linux

I am trying to boot the camkes-vm-linux but am not able to input anything after Buildroot login
In the general display im getting Loading Rootserver OK, Loading sel4kernel OK and
VM.Linux.Logs.txt
thats it
This is the output as follows in the serial monitor

Starting network[ 0.810972] ip (679) used greatest stack depth: 6732 bytes left
: OK

Failed to locate device consumes_event.
Failed to locate device emits_event.

Welcome to Buildroot

buildroot login: [ 1.431752] clocksource: tsc: mask: 0xffffffffffffffff max_cycles: 0x31015f85297, max_idle_ns: 440795334135 ns

[ 1.442241] clocksource: Switched to clocksource tsc

[ 2.811817] random: fast init done

[ 134.023597] random: crng init done

What changes should i do to make it work
Thanks

failed to init with cmake 3.16.0

I have no issue with cmake 3.15.5 on Ubuntu 18.04, but it failed to init when I update to the newest cmake version.

Small prototype issue with hello_2 tutorial in Task 9

Hi,

The tutorials are really helpful, thank you.

In the hello_2 tutorial at Task 9, the function prototype in the comments for seL4_TCB_Configure() contains a "seL4_Uint8 priority" argument which is also mentioned in Hint 5. Neither the solution nor the seL4 reference manual seem to agree that there is such a parameter.

Best,
Geoff

clarify what "retype" creates

#65 raises that the description of what the retype operation does is not clear enough.

mention the different kinds of caps in the capabilities tutorial
reference that in the untyped tutorial
expand the description of retype a little

Outdated installation instructions

It appears as though the bash commands for git repo init and sync are outdated, and reference old repositories that no longer exist/no longer host the correct manifest and xml files. The tutorial page on the seL4 wiki has the correct instructions (or rather instructions that worked on my machine), which can be found here: https://wiki.sel4.systems/Tutorials

Update VM to provide something with 20.4 at least

https://github.com/seL4/sel4-tutorials/blob/master/README.md points to a Ubuntu 16.4 VM at https://trustworthy.systems/Downloads/sel4_tut_v3_lubuntu_16_041-v2.ova
This should be updated to Ubuntu 20.4 to avoid running into more and more issues

Cross-VM connector issue

Hi,

I am trying to follow below guide to test the cross-vm connector and understand how communication works between guest and component. However, the build always fail due to this

CMake Error at CMakeLists.txt:9 (add_subdirectory):
add_subdirectory given source
"/host/projects/camkes-vm-linux/camkes-linux-artifacts/camkes-linux-apps/camkes-connector-apps/libs/camkes"
which is not an existing directory.

which is relate to the repo "camkes-vm-linux". Lib is removed in this commit.
seL4/camkes-vm-linux@bab3e9c#diff-8f4a0b5dd424b723d6c6c7c82fb67274d18d98385239823d1fafabb3c3756123

Would you please update the tutorial to reflect the new communication interfaces? I am a newbie of SEL4 so I am still trying to figure out how to apply the new way to fix this issue...

Many thanks!

sel4 tutorials build error

I'm having trouble running sel4-tutorials. All prerequisites were installed and tested with sel4test which successfully compiled and returned "All is well in the universe". However, when I try to run sel4-tutorials hello-1, the final make fails with the following error:

*** SEL4_ARCH invalid or undefined, should be one of [aarch32 ia32]

With make SEL4_ARCH="ia32" the Kernel part does get compiled but then it fails on libsel4

/sel4-tutorials/libs/libsel4/Makefile:21: *** Cannot determine TYPE_SUFFIX. Stop.
Tools/common/project.mk:286: recipe for target ‘libsel4’ failed
make: *** [libsel4] Error 2

Please advise.

hello-1 app won't run under QEMU

Error running app "hello-1" with QEMU.

I've tried to follow the tutorial documentation, but things go wrong when
I get to running qemu with the image I built.

In particular, when I run

qemu-system-i386 -nographic -m 512 -kernel images/kernel-ia32-pc99 -initrd images/hello-1-image-ia32-pc99

I get the following error:

qemu: fatal: Trying to execute code outside RAM or ROM at 0xe01207a0

Along with a dump of register state.

Have I done something wrong, or is the tutorial project broken? How should I
fix it?

Below are all the commands I used to build the project.

Steps to reproduce

Get repositories

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

From this point on, I've run all commands within the sel4-tutorials-manifest directory.

Open the "howto" slides

I tried to open the tutorial PDF, but it doesn't seem to exist in the repository:

xpdf $(realpath projects/sel4-tutorials/docs/seL4-APILib-details.pdf)

I instead am using the version on the master branch of sel4-tutorials:

https://github.com/SEL4PROJ/sel4-tutorials/blob/master/docs/seL4-APILib-details.pdf

From the sel4-tutorials-manifest root directory, I run:

make ia32_hello-1_defconfig

Output looks fine:

[GEN] /my/home/dir/sel4-tutorials-manifest/Makefile
make -f tools/kbuild/Makefile.build obj=tools/kbuild/basic
#
# configuration written to .config
#

Now I run

make

This fails (as expected) with the error:

`undefined reference to 'main'`

So I fix this by adding a main function:

int main(void) {
  printf("Hello, World\n");
  return 0;
}

(I later copied this from the solution to make sure it was exactly correct and
I didn't have any subtle problem)

Running make again seems to work fine. The last lines of output are:

[STAGE] hello-1
[apps/hello-1] done.
[GEN_IMAGE] hello-1-image

Running QEMU

Now I run QEMU to test my image:

qemu-system-i386 -nographic -m 512 -kernel images/kernel-ia32-pc99 -initrd images/hello-1-image-ia32-pc99

I get the following error:

qemu: fatal: Trying to execute code outside RAM or ROM at 0xe01207a0

EAX=2badb002 EBX=00009500 ECX=0010003e EDX=00000511
ESI=00009500 EDI=2badb002 EBP=00000000 ESP=00100ff0
EIP=e01207a0 EFL=00000002 [-------] CPL=0 II=0 A20=1 SMM=0 HLT=0
ES =0010 00000000 ffffffff 00cf9300 DPL=0 DS   [-WA]
CS =0008 00000000 ffffffff 00cf9a00 DPL=0 CS32 [-R-]
SS =0010 00000000 ffffffff 00cf9300 DPL=0 DS   [-WA]
DS =0010 00000000 ffffffff 00cf9300 DPL=0 DS   [-WA]
FS =0010 00000000 ffffffff 00cf9300 DPL=0 DS   [-WA]
GS =0010 00000000 ffffffff 00cf9300 DPL=0 DS   [-WA]
LDT=0000 00000000 0000ffff 00008200 DPL=0 LDT
TR =0000 00000000 0000ffff 00008b00 DPL=0 TSS32-busy
GDT=     000caa68 00000027
IDT=     00000000 000003ff
CR0=00000011 CR2=00000000 CR3=00000000 CR4=00000000
DR0=00000000 DR1=00000000 DR2=00000000 DR3=00000000 
DR6=ffff0ff0 DR7=00000400
CCS=00000000 CCD=00950000 CCO=EFLAGS  
EFER=0000000000000000
FCW=037f FSW=0000 [ST=0] FTW=00 MXCSR=00001f80
FPR0=0000000000000000 0000 FPR1=0000000000000000 0000
FPR2=0000000000000000 0000 FPR3=0000000000000000 0000
FPR4=0000000000000000 0000 FPR5=0000000000000000 0000
FPR6=0000000000000000 0000 FPR7=0000000000000000 0000
XMM00=00000000000000000000000000000000 XMM01=00000000000000000000000000000000
XMM02=00000000000000000000000000000000 XMM03=00000000000000000000000000000000
XMM04=00000000000000000000000000000000 XMM05=00000000000000000000000000000000
XMM06=00000000000000000000000000000000 XMM07=00000000000000000000000000000000
zsh: abort (core dumped)  qemu-system-i386 -nographic -m 512 -kernel images/kernel-ia32-pc99 -initrd

explain seL4 "bit" sizes more prominently

2 queries for the untyped tutorial makes this a frequently asked question (see e.g. #71 ).

We should explain more prominently that those sizes are the exponent n in 2^n bytes. Ideally in the tutorial solution as a comment and in the text.

add solution comment
check if untyped is the right tutorial or if this should come earlier and have a reference in untyped
add text to tutorial itself
check if this is explained in the reference manual

Following Tutorials, unable to dollow CAmkESTutorial.pdf

I realize that there is a VM that is provided and works great but I wanted to be able to set up an environment myself. So I followed the prerequisites instructions and then tried the steps which are outlined in the docs/CAmkESTutorial.pdf file:

mkdir camkes-tutorials
cd camkes-tutorials
repo init -u http://github.com/sel4-projects/sel4-tutorials-manifest -m camkes-tutorials.xml
repo sync 
make arm_hello-camkes-0_defconfig
make

when I run make there was an issue with the capdl-tool building. It seemed there was an issue with cabal not finding the correct packages. The prerequisite instructions outline installing stack and the makefile in the master branch of the capDL tool uses stack to get the correct version of ghc and other packages. The capdl tool that is downloaded with the camkes-tutorials.xml manifest is an older version that uses cabal.

Changing the revision field in the capdl project line in the manifest file and doing another repo sync got me past the making of the capdl tool. Then there were more issues after that though. So I changed all of the revision fields from 3.0.x=compatible to 4.0.x-compatible and the kernel revision from 3.0.0 to 4.0.0 and the camkes tool from refx/tags/camkes-2.1.0 to refs/tags/camkes-2-3.0 (not sure if that was needed)

After those changes, doing a repo sync, make clean, make arm_hello-camkes-0_defonfig, and make I was able to successfully make the hello camkes project and use qemu to simulate it.

I am on Ubuntu 16.04 and did try installing cabal and installing the packages needed for the capdl tool that is originally downloaded by the camkes-tutorials.xml manifest but I could not figure out how to download the correct version of ghc for capdl

Camkes-VM-Linux Ninja Failed

I am a newbie to SeL4 and followed the step by step process to build camkes-vm-linux project
but it fails while running ninja and the output is as follows

ubuntu@ubuntu1804:~/sel4-tutorials-manifest/b11_build$ ninja
[5/427] Performing configure step for 'hello-app'
FAILED: hello-app-stamp/hello-app-configure 
cd /home/ubuntu/sel4-tutorials-manifest/b11_build/hello-app && /usr/local/bin/cmake -DCMAKE_BUILD_TYPE=Debug -DCMAKE_TOOLCHAIN_FILE=/home/ubuntu/sel4-tutorials-manifest/tools/seL4/cmake-tool/polly_toolchains/linux-gcc-32bit-pic.cmake -GNinja /home/ubuntu/sel4-tutorials-manifest/b11/pkg/hello && /usr/local/bin/cmake -E touch /home/ubuntu/sel4-tutorials-manifest/b11_build/hello-app-stamp/hello-app-configure
-- [polly] Used toolchain: Linux / gcc / PIC / c++11 support / 32 bit
-- The C compiler identification is GNU 7.5.0
-- Check for working C compiler: /usr/bin/gcc
-- Check for working C compiler: /usr/bin/gcc -- broken
CMake Error at /usr/local/share/cmake-3.13/Modules/CMakeTestCCompiler.cmake:52 (message):
  The C compiler
    "/usr/bin/gcc"
  is not able to compile a simple test program.
  It fails with the following output:
    Change Dir: /home/ubuntu/sel4-tutorials-manifest/b11_build/hello-app/CMakeFiles/CMakeTmp
    
    Run Build Command:"/usr/bin/ninja-build" "cmTC_ac0a4"
    [1/2] Building C object CMakeFiles/cmTC_ac0a4.dir/testCCompiler.c.o
    [2/2] Linking C executable cmTC_ac0a4
    FAILED: cmTC_ac0a4 
    : && /usr/bin/gcc -m32 -fPIC   CMakeFiles/cmTC_ac0a4.dir/testCCompiler.c.o  -o cmTC_ac0a4   && :
    /usr/bin/ld: cannot find Scrt1.o: No such file or directory
    /usr/bin/ld: cannot find crti.o: No such file or directory
    /usr/bin/ld: skipping incompatible /usr/lib/gcc/x86_64-linux-gnu/7/libgcc.a when searching for -lgcc
    /usr/bin/ld: cannot find -lgcc
    /usr/bin/ld: skipping incompatible /usr/lib/gcc/x86_64-linux-gnu/7/libgcc.a when searching for -lgcc
    /usr/bin/ld: cannot find -lgcc
    collect2: error: ld returned 1 exit status
    ninja: build stopped: subcommand failed.
    
  CMake will not be able to correctly generate this project.
Call Stack (most recent call first):
  CMakeLists.txt:5 (project)

-- Configuring incomplete, errors occurred!
See also "/home/ubuntu/sel4-tutorials-manifest/b11_build/hello-app/CMakeFiles/CMakeOutput.log".
See also "/home/ubuntu/sel4-tutorials-manifest/b11_build/hello-app/CMakeFiles/CMakeError.log".

What changes are to be made and How do I solve this

Improved instructions for Debian

The provided quick start instructions do not quite work on Debian. Notably:

Debian doesn't have the universe repository. It has contrib instead.
It's necessary to specify the distro version explicitly when adding a PPA, that is: add-apt-repository 'deb http://ppa.launchpad.net/hvr/ghc/ubuntu trusty main'.
Debian does not provide gcc-arm-linux-gnueabi (it does provide gcc-arm-none-eabi). You'd need to figure some other way (I already had it installed locally so I wouldn't know which.)
Debian does not provide phablet-tools but it appears that the only thing needed from there is repo, which it does provide.

I have built and ran both ARM and x86 versions.

Permission Denied when ninja

The tutorials ahead of threads had no problems，however，when I ran threads/IPC，the error occured.
"rm -rf threads_build" makes no sense.

camkes-vm-linux solution, out-of-the-box: module "poke" is not loading

In out-of-the-box camkes-vm-linux solution, "poke" module is not loading because of vermagic mismatch between the pre-built kernel and the module.

insmod /lib/modules/4.8.16/kernel/drivers/vmm/poke.ko
[ 30.023396] poke: version magic '4.8.16 SMP mod_unload 686 ' should be '4.8.16 mod_unload 686 '

The fast solution (until the issue has been solved) is to use config.backup-singlecore to build the module. To do it one needs just replace

set(linux_config "${CAMKES_VM_LINUX_DIR}/linux_configs/${linux_major}.${linux_minor}/32/config")

with

set(linux_config "${CAMKES_VM_LINUX_DIR}/linux_configs/${linux_major}.${linux_minor}/32/config.backup-singlecore")

in file CMakeList.txt (directory camkes-vm-linuxyyy).

All I can do is just report this. Its up to maintainers to either re-build the kernel or patch the tutorial.md, because I don't know reasoning behind keeping 2 configs and pre-built non-SMP kernel image.

Thanks!

dynamic-[2,3] comments refer to deprecated function.

Hi,

dynamic-2 and dynamic-3 both have the old function signature for vka_mint_object referring to the departed seL4_CapData_t and contain the "hint" for the badge use seL4_CapData_Badge_new(), which is no longer necessary. Probably removing that hint and correctly settling the type of badge to seL4_Word should make things clear enough

Update mapping tutorial due to API changes for AArch64 VSpaces

The mapping tutorial (https://docs.sel4.systems/Tutorials/mapping.html) refers to levels of paging objects that no longer exist due to RFC-10 (https://sel4.atlassian.net/jira/software/c/projects/RFC/issues/RFC-10) and hence should be updated.

Not able to run camkes-vm-linux on the AMD platform

According to tutorials, how can I simulate on the AMD platform?

Error During seL4 Tutorial Build

I am receiving an error during the the x86 make tutorial. I have executed all the steps on this page:
https://github.com/seL4-projects/sel4-tutorials/blob/master/Prerequisites.md
Everything works including make ia32_simple_defconfig; make silentoldconfig. When I execute the final make, lots of build activity occurs, then the make stops with the following error: "make: *** No rule to make target 'libsel4camkes', needed by 'libsel4muslccamkes'. Stop."

I have a co-worker who has built this example before, and they tried with the latest repository and receive the same error.

Please advise. Thank you,
John

Solution `hello-camkes-1` won't build with RPC

In the apps/hello-camkes-1/hello-camkes-1 it says

/* TODO 2: connections */
                /* hint 1: use seL4RPCCall as the connector (or you could use seL4RPC if you prefer)
                 * hint 2: look at
		 * https://github.com/seL4/camkes-tool/blob/2.1.0/docs/index.md#creating-an-application
                 */
                // connection seL4RPC hello_con(from client.hello, to echo.hello);
                connection seL4RPCCall hello_con(from client.hello, to echo.hello);

If the connection seL4RPCCall line is commented out and the one above it is uncommented the solution fails to build. The build got this far:

[apps/hello-camkes-1] building...
/home/jesse/camkes-Learning/camkes-solutions/tools/camkes/camkes.mk:126: /home/jesse/camkes-Learning/camkes-solutions/build/arm/imx31/hello-camkes-1/camkes-gen.mk: No such file or directory
 [GEN] camkes-gen.mk
 [HEADERS]
 [STAGE] autoconf.h
 [CP] echo.c
 [GEN] Echo.h
 [GEN] camkes.h
 [GEN] Echo.c
 [GEN] hello_seL4RPC.c
 [CC] echo.o
 [CC] Echo.o
 [CC] hello_seL4RPC.o
 [GEN] linker.lds
 [LD] echo.instance.bin
 [CP] client.c
 [GEN] Client.h
 [GEN] camkes.h
 [GEN] Client.c
 [GEN] hello_seL4RPC.c
 [CC] client.o
 [CC] Client.o
 [CC] hello_seL4RPC.o
In file included from /home/jesse/camkes-Learning/camkes-solutions/build/arm/imx31/hello-camkes-1/src/client/generated/hello_seL4RPC.c:12:0:
/home/jesse/camkes-Learning/camkes-solutions/stage/arm/imx31/include/camkes/timing.h:16:33: fatal error: sel4bench/sel4bench.h: No such file or directory
 #include <sel4bench/sel4bench.h>
                                 ^
compilation terminated.
/home/jesse/camkes-Learning/camkes-solutions/tools/camkes/camkes.mk:77: recipe for target '/home/jesse/camkes-Learning/camkes-solutions/build/arm/imx31/hello-camkes-1/src/client/generated/hello_seL4RPC.o' failed
make[1]: *** [/home/jesse/camkes-Learning/camkes-solutions/build/arm/imx31/hello-camkes-1/src/client/generated/hello_seL4RPC.o] Error 1
tools/common/project.mk:320: recipe for target 'hello-camkes-1' failed

sel4-tutorials building error, CMake Error: The source directory "xxxxx/projects/sel4-tutorials/settings.cmake" is a file, not a directory.

seL4 Tutorial 1 won't build the code

OS: Ubuntu 16.04 x86_64

I have installed all prerequisites

    apt-get install git repo cmake ninja-build clang gcc-multilib gcc-arm-none-eabi binutils-arm-none-eabi \
    libncurses-dev libxml2-utils libssl-dev libsqlite3-dev libcunit1-dev expect python-pip

    pip install camkes-deps

    # Required for CAmkES only
    curl -sSL https://get.haskellstack.org/ | sh

I have also got the code

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

From the root directory of sel4-tutorials-manifest I have tried running the following from https://wiki.sel4.systems/seL4%20Tutorial%201.

make ia32_hello-1_defconfig

Although am getting the error:

$ make ia32_hello-1_defconfig
/home/andrew/work/projects/os/sel4/tutorials/projects/sel4-tutorials/build-config//Makefile-common:24: Unsupport or undefined platform, did you run make <defconfig>?
/home/andrew/work/projects/os/sel4/tutorials/projects/sel4-tutorials/build-config//Makefile-common:42: Unsupported or undefined architecture, did you run make <defconfig>?
[GEN] /home/andrew/work/projects/os/sel4/tutorials/Makefile
make -f tools/kbuild/Makefile.build obj=tools/kbuild/basic
make[1]: Entering directory '/home/andrew/work/projects/os/sel4/tutorials'
   gcc -Wp,-MD,tools/kbuild/basic/.fixdep.d -Itools/kbuild/basic -Wall -o tools/kbuild/basic/fixdep tools/kbuild/basic/fixdep.c  
   gcc -Wp,-MD,tools/kbuild/basic/.docproc.d -Itools/kbuild/basic -Wall -o tools/kbuild/basic/docproc tools/kbuild/basic/docproc.c  
make[1]: Leaving directory '/home/andrew/work/projects/os/sel4/tutorials'
   gcc -Wp,-MD,tools/kbuild/kconfig/.conf.o.d -Itools/kbuild/kconfig -Wall -DCURSES_LOC="<ncurses.h>" -DLOCALE -c -o tools/kbuild/kconfig/conf.o tools/kbuild/kconfig/conf.c
   gcc -Wp,-MD,tools/kbuild/kconfig/.zconf.tab.o.d -Itools/kbuild/kconfig -Wall -DCURSES_LOC="<ncurses.h>" -DLOCALE  -I/home/andrew/work/projects/os/sel4/tutorials/tools/kbuild/kconfig -Itools/kbuild/kconfig -c -o tools/kbuild/kconfig/zconf.tab.o tools/kbuild/kconfig/zconf.tab.c
   gcc  -o tools/kbuild/kconfig/conf tools/kbuild/kconfig/conf.o tools/kbuild/kconfig/zconf.tab.o  
Kconfig:26: can't open file "apps/hello-1/Kconfig"
/home/andrew/work/projects/os/sel4/tutorials/tools/kbuild/kconfig/Makefile:33: recipe for target 'ia32_hello-1_defconfig' failed
make[1]: *** [ia32_hello-1_defconfig] Error 1
tools/common/project.mk:212: recipe for target 'ia32_hello-1_defconfig' failed
make: *** [ia32_hello-1_defconfig] Error 2

Tutorial VM S3 link down

In sel4-tutorials/README.md, the S3 link to the VirtualBox virtual machine appliance is down.

https://s3-us-west-1.amazonaws.com/sel4-developer-day/sel4-tutorial-lubuntu-15.04-v4.ova
NoSuchBucket

January Commit to camkes-vm-linux breaks camkes-vm-crossvm Tutorial

This commit appears to remove the libraries necessary to complete the crossvm tutorial: seL4/camkes-vm-linux@bab3e9c.

Doing a git hard reset also does not solve the problem as camkes_mutex.h and a few others are also missing. Is there an updated tutorial somewhere since the point of this commit appears to depreciate the old crossvm connector modules?