Hi Rod, I'm newbie too but Iin my case what I get is a long list of tests and then: (...) Starting test 120: VSPACE0006 Starting test 122: Test all tests ran Test suite passed. 122 tests passed. 54 tests disabled. *All is well in the universe* Your output is a crash. Below you can see my full output (as it looks like attachments are stripped...): ------ SeaBIOS (version 1.13.0-1ubuntu1.1) iPXE (http://ipxe.org) 00:03.0 CA00 PCI2.10 PnP PMM+BFF8C8B0+BFECC8B0 CA00 Booting from ROM..Node 0 of 1 IOPT levels: 4294967295 IPC buffer: 0x608000 Empty slots: [632 --> 8192) sharedFrames: [0 --> 0) userImageFrames: [19 --> 539) userImagePaging: [14 --> 18) untypeds: [539 --> 632) Initial thread domain: 0 Initial thread cnode size: 13 List of untypeds ------------------ Paddr | Size | Device 0 | 20 | 1 0xbffe0000 | 17 | 1 0xc0000000 | 29 | 1 0xe0000000 | 28 | 1 0xf0000000 | 27 | 1 0xf8000000 | 26 | 1 0xfc000000 | 25 | 1 0xfe000000 | 23 | 1 0xfe800000 | 22 | 1 0xfec01000 | 12 | 1 0xfec02000 | 13 | 1 0xfec04000 | 14 | 1 0xfec08000 | 15 | 1 0xfec10000 | 16 | 1 0xfec20000 | 17 | 1 0xfec40000 | 18 | 1 0xfec80000 | 19 | 1 0xfed00000 | 20 | 1 0xfee01000 | 12 | 1 0xfee02000 | 13 | 1 0xfee04000 | 14 | 1 0xfee08000 | 15 | 1 0xfee10000 | 16 | 1 0xfee20000 | 17 | 1 0xfee40000 | 18 | 1 0xfee80000 | 19 | 1 0xfef00000 | 20 | 1 0xff000000 | 23 | 1 0xff800000 | 22 | 1 0xffc00000 | 21 | 1 0xffe00000 | 20 | 1 0xfff00000 | 19 | 1 0xfff80000 | 18 | 1 0xfffc0000 | 17 | 1 0xfffe0000 | 16 | 1 0xffff0000 | 15 | 1 0xffff8000 | 14 | 1 0xffffc000 | 13 | 1 0xffffe000 | 12 | 1 0xfffff000 | 11 | 1 0xfffff800 | 10 | 1 0xfffffc00 | 9 | 1 0xfffffe00 | 8 | 1 0xffffff00 | 7 | 1 0xffffff80 | 6 | 1 0xffffffc0 | 5 | 1 0xffffffe0 | 4 | 1 0x100000000 | 32 | 1 0x200000000 | 33 | 1 0x400000000 | 34 | 1 0x800000000 | 35 | 1 0x1000000000 | 36 | 1 0x2000000000 | 37 | 1 0x4000000000 | 38 | 1 0x8000000000 | 46 | 1 0x408000000000 | 45 | 1 0x608000000000 | 44 | 1 0x708000000000 | 43 | 1 0x788000000000 | 42 | 1 0x7c8000000000 | 41 | 1 0x7e8000000000 | 40 | 1 0x7f8000000000 | 39 | 1 0x100000 | 20 | 0 0x200000 | 21 | 0 0x400000 | 22 | 0 0xc1e000 | 13 | 0 0xc20000 | 17 | 0 0xc40000 | 18 | 0 0xc80000 | 19 | 0 0xd00000 | 20 | 0 0xe00000 | 21 | 0 0x1000000 | 24 | 0 0x2000000 | 25 | 0 0x4000000 | 26 | 0 0x8000000 | 27 | 0 0x10000000 | 28 | 0 0x20000000 | 29 | 0 0x40000000 | 30 | 0 0x80000000 | 29 | 0 0xa0000000 | 28 | 0 0xb0000000 | 27 | 0 0xb8000000 | 26 | 0 0xbc000000 | 25 | 0 0xbe000000 | 24 | 0 0xbf000000 | 23 | 0 0xbf800000 | 22 | 0 0xbfc00000 | 21 | 0 0xbfe00000 | 20 | 0 0xbff00000 | 19 | 0 0xbffc9800 | 11 | 0 0xbffca000 | 13 | 0 0xbffcc000 | 14 | 0 0xbffd0000 | 16 | 0 Untyped summary 1 untypeds of size 4 1 untypeds of size 5 1 untypeds of size 6 1 untypeds of size 7 1 untypeds of size 8 1 untypeds of size 9 1 untypeds of size 10 2 untypeds of size 11 3 untypeds of size 12 5 untypeds of size 13 4 untypeds of size 14 3 untypeds of size 15 4 untypeds of size 16 5 untypeds of size 17 4 untypeds of size 18 5 untypeds of size 19 7 untypeds of size 20 4 untypeds of size 21 4 untypeds of size 22 3 untypeds of size 23 2 untypeds of size 24 3 untypeds of size 25 3 untypeds of size 26 3 untypeds of size 27 3 untypeds of size 28 3 untypeds of size 29 1 untypeds of size 30 1 untypeds of size 32 1 untypeds of size 33 1 untypeds of size 34 1 untypeds of size 35 1 untypeds of size 36 1 untypeds of size 37 1 untypeds of size 38 1 untypeds of size 39 1 untypeds of size 40 1 untypeds of size 41 1 untypeds of size 42 1 untypeds of size 43 1 untypeds of size 44 1 untypeds of size 45 1 untypeds of size 46 Switching to a safer, bigger stack... seL4 Test ========= Failed to allocate object of size 2147483648, error 1 Failed to allocate object of size 1073741824, error 1 Failed to allocate object of size 536870912, error 1 Failed to allocate object of size 268435456, error 1 Failed to allocate object of size 134217728, error 1 Failed to allocate object of size 67108864, error 1 Failed to allocate object of size 33554432, error 1 Failed to allocate object of size 16777216, error 1 Failed to allocate object of size 8388608, error 1 Failed to allocate object of size 4194304, error 1 Failed to allocate object of size 2097152, error 1 Failed to allocate object of size 1048576, error 1 Failed to allocate object of size 524288, error 1 Failed to allocate object of size 262144, error 1 Failed to allocate object of size 131072, error 1 Failed to allocate object of size 65536, error 1 Failed to allocate object of size 32768, error 1 Failed to allocate object of size 16384, error 1 Failed to allocate object of size 8192, error 1 vspace is NULL Failed to make reservation: 0x400000, 4096 Failed to create reservations Failed to reserve regions Starting test suite sel4test Starting test 0: Test that there are tests Starting test 1: SYSCALL0000 Starting test 2: SYSCALL0001 Starting test 3: SYSCALL0002 Starting test 4: SYSCALL0003 Starting test 5: SYSCALL0004 Starting test 6: SYSCALL0005 Starting test 7: SYSCALL0006 Starting test 8: SYSCALL0010 Starting test 9: SYSCALL0011 Starting test 10: SYSCALL0012 Starting test 11: SYSCALL0013 Starting test 12: SYSCALL0014 Starting test 13: SYSCALL0015 Starting test 14: SYSCALL0016 Starting test 15: SYSCALL0017 Starting test 16: TIMER0001 Starting test 17: TIMER0002 Starting test 18: BIND0001 Starting test 19: BIND0002 Starting test 20: BIND0003 Starting test 21: BIND0004 Starting test 22: CANCEL_BADGED_SENDS_0001 Starting test 23: CANCEL_BADGED_SENDS_0002 Starting test 24: CNODEOP0001 Starting test 25: CNODEOP0002 Starting test 26: CNODEOP0003 Starting test 27: CNODEOP0004 Starting test 28: CNODEOP0005 Starting test 29: CNODEOP0006 Starting test 30: CNODEOP0007 Starting test 31: CNODEOP0008 Starting test 32: CNODEOP0009 Starting test 33: CSPACE0001 Starting test 34: DOMAINS0001 Starting test 35: DOMAINS0002 Starting test 36: DOMAINS0003 Starting test 37: DOMAINS0004 Starting test 38: FPU0000 Starting test 39: FPU0001 Starting test 40: FRAMEDIPC0001 Starting test 41: FRAMEDIPC0002 Starting test 42: FRAMEDIPC0003 Starting test 43: FRAMEEXPORTS0001 Starting test 44: IOPORTS1000 Starting test 45: IPC0001 Starting test 46: IPC0002 Starting test 47: IPC0003 Starting test 48: IPC0004 Starting test 49: IPC0010 Starting test 50: IPC1001 Starting test 51: IPC1002 Starting test 52: IPC1003 Starting test 53: IPC1004 Starting test 54: IPCRIGHTS0001 Starting test 55: IPCRIGHTS0002 Starting test 56: IPCRIGHTS0003 Starting test 57: IPCRIGHTS0004 Starting test 58: IPCRIGHTS0005 Starting test 59: NBWAIT0001 Starting test 60: PAGEFAULT0001 Starting test 61: PAGEFAULT0002 Starting test 62: PAGEFAULT0003 Starting test 63: PAGEFAULT0004 Starting test 64: PAGEFAULT0005 Starting test 65: PAGEFAULT1001 Starting test 66: PAGEFAULT1002 Starting test 67: PAGEFAULT1003 Starting test 68: PAGEFAULT1004 Starting test 69: PREEMPT_REVOKE Starting test 70: REGRESSIONS0001 Starting test 71: RETYPE0000 Starting test 72: RETYPE0001 Starting test 73: RETYPE0002 Starting test 74: SCHED0000 Starting test 75: SCHED0002 Starting test 76: SCHED0003 Starting test 77: SCHED0004 Starting test 78: SCHED0005 Starting test 79: SCHED0006 Starting test 80: SCHED0020 Starting test 81: SCHED0021 Starting test 82: SERSERV_CLIENT_001 Test SERSERV_CLIENT_001 passed Starting test 83: SERSERV_CLIENT_002 Hello, world! Test SERSERV_CLIENT_002 passed Starting test 84: SERSERV_CLIENT_003 Hello, world! Test SERSERV_CLIENT_003 passed Starting test 85: SERSERV_CLIENT_004 Hello, world! Hello, world! Hello, world! Hello, world! Test SERSERV_CLIENT_004 passed Starting test 86: SERSERV_CLIENT_005 Test SERSERV_CLIENT_005 passed Starting test 87: SERSERV_CLI_PROC_001 Test SERSERV_CLI_PROC_001 passed Starting test 88: SERSERV_CLI_PROC_002 Hello, world! Test SERSERV_CLI_PROC_002 passed Starting test 89: SERSERV_CLI_PROC_003 Hello, world! Test SERSERV_CLI_PROC_003 passed Starting test 90: SERSERV_CLI_PROC_004 Hello, world! Hello, world! Hello, world! Hello, world! Test SERSERV_CLI_PROC_004 passed Starting test 91: SERSERV_CLI_PROC_005 Test SERSERV_CLI_PROC_005 passed Starting test 92: SERSERV_PARENT_001 Test SERSERV_PARENT_001 passed Starting test 93: SERSERV_PARENT_002 Test SERSERV_PARENT_002 passed Starting test 94: SERSERV_PARENT_003 Hello, world! Test SERSERV_PARENT_003 passed Starting test 95: SERSERV_PARENT_004 Hello, world! Test SERSERV_PARENT_004 passed Starting test 96: SERSERV_PARENT_005 Hello, world! Hello, world! Hello, world! Hello, world! Test SERSERV_PARENT_005 passed Starting test 97: SERSERV_PARENT_006 Test SERSERV_PARENT_006 passed Starting test 98: SERSERV_PARENT_007 Starting test 99: SERSERV_PARENT_008 Test SERSERV_PARENT_008 passed Starting test 100: SERSERV_PARENT_009 Serserv Client: printf: NULL passed for required arguments. Is connection handle valid? Serserv Client: printf: NULL passed for required arguments. Is connection handle valid? Test SERSERV_PARENT_009 passed Starting test 101: SERSERV_PARENT_010 Serserv Client: printf: NULL passed for required arguments. Is connection handle valid? Serserv Client: printf: NULL passed for required arguments. Is connection handle valid? Test SERSERV_PARENT_010 passed Starting test 102: STACK_ALIGNMENT_001 Starting test 103: SYNC001 Starting test 104: SYNC002 Starting test 105: SYNC003 Starting test 106: SYNC004 Starting test 107: THREADS0004 Starting test 108: THREADS0005 Starting test 109: TLS0001 Starting test 110: TLS0002 Starting test 111: TLS0006 Starting test 112: TRIVIAL0000 Starting test 113: TRIVIAL0001 Starting test 114: TRIVIAL0002 Starting test 115: VSPACE0000 Starting test 116: VSPACE0002 Starting test 117: VSPACE0003 Starting test 118: VSPACE0004 Starting test 119: VSPACE0005 Starting test 120: VSPACE0006 Starting test 122: Test all tests ran Test suite passed. 122 tests passed. 54 tests disabled. All is well in the universe El jue, 27 may 2021 a las 15:09, escribió:

OK... I got hello-world running in QEMU, but after printing "Hello World!", QEMU seems to crash and I have to "kill -9" it from another shell. Is that expected?

e.g.

Booting all finished, dropped to user space Hello, World! Second Hello Caught cap fault in send phase at address 0 while trying to handle: vm fault on data at address 0 with status 0x4 in thread 0xffffff801fe08400 "rootserver" at address 0 With stack: 0x41ce98: 0x401755 0x41cea0: 0x41cf10 0x41cea8: 0x0 0x41ceb0: 0x41cef0 0x41ceb8: 0x401230 0x41cec0: 0x0 0x41cec8: 0x41cf30 0x41ced0: 0x41cf20 0x41ced8: 0x41cf10 0x41cee0: 0x1 0x41cee8: 0x4010f2 0x41cef0: 0x41cff0 0x41cef8: 0x4013a9 0x41cf00: 0x0 0x41cf08: 0x525000 0x41cf10: 0x412028 _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems

On May 27, 2021, at 08:17, Roderick Chapman wrote:

On 27/05/2021 15:49, Hugo V.C. wrote:

...

Starting test 120: VSPACE0006 Starting test 122: Test all tests ran Test suite passed. 122 tests passed. 54 tests disabled. *All is well in the universe*

That's the output of the "seL4test" program, and I get the same.

My problem is with the first "hello-world" tutorial.

The hello-world example looks like it does not do anything fancy on exit, so I believe you’re looking at the (expected) cap fault when it runs out of code and has no fault handler. You can do things like suspend your own TCB to exit more “cleanly” but I suspect this complexity is deliberately not included in hello-world. As for why you can’t exit Qemu, this is the expected behavior when you run Qemu in non-GUI mode. Hit Ctrl-A,x to exit.

Easier than having to remember esoteric keys combinations: just kill the Qemu process from another terminal. Dirty but it works. El jue, 27 may 2021 a las 17:59, Roderick Chapman () escribió:

On 27/05/2021 16:29, Matthew Fernandez wrote:

...

As for why you can’t exit Qemu, this is the expected behavior when you run Qemu in non-GUI mode. Hit Ctrl-A,x to exit.

Got it - that works. It would be good if this were documented. What is the correct procedure to request changes to the documentation?

- Rod

_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems

On 28/05/2021 03:38, Matthew Fernandez wrote:

I would guess click the “Edit page on GitHub” link at the bottom of the tutorial page.

Yes... but I'm a clueless newbie, so I wouldn't presume to make such changes correctly. Who's in charge of quality assurance for the documentation?  - Rod

On 29/05/2021 06:08, Gerwin Klein wrote:

If you edit on GitHub, this will ultimately raise a pull request on the markdown file that backs that particular change, and will be reviewed by someone with (hopefully ;-)) more knowledge. So there is no danger of breaking anything by accident. OK... sounds good.

For tutorials, there tend to be two "edit" links, because text gets included from multiple sources. One link is for the main page, and one for the included text, linking to the repository it comes from (it should say something like "Tutorial included from [github repo]. [edit]")

I'm happy to do the edit, though. Just to double check, you mean the pagehttps://docs.sel4.systems/Tutorials/hello-world.html ? Yes.. that one.

What would make sense to add at the bottom to be less confusing?

It would be good to tell the reader to expect the run to end with a capability violation and a stack dump, and then "Ctrl-A, X" is needed to terminate QEMU.  - Rod

On 29 May 2021, at 17:10, Hugo V.C. mailto:skydivebcn@gmail.com> wrote: Or, change de default "main.c" so the system executes some very simple endless task (i.e. just printing "Hello World" in an endless loop) that may be more "beatiful" than a system crash due to cap violation. pull requests welcome ;-)

On 29 May 2021, at 16:47, Roderick Chapman wrote:

...

What would make sense to add at the bottom to be less confusing?

It would be good to tell the reader to expect the run to end with a capability violation and a stack dump, and then "Ctrl-A, X" is needed to terminate QEMU.

Now up here: https://github.com/seL4/sel4-tutorials/pull/55 Comments welcome. Cheers, Gerwin

On 29 May 2021, at 16:57, Hugo V.C. wrote:

just a question; is it possible to make questions in this list that are not 100% seL4's source code related? I mean, seL4 will be build and deployed on a variety of platforms, configurations, environments, etc. The tutorials themselves deal with several platforms. So, is it welcome/appropiate to make more generic questions or this is not the right list?

it’s the developer mailing list, so anything relevant to developers is fair game. That definitely includes platforms/environments/configs etc. Gernot

...

...

...

...

"Hugo" == Hugo V C writes:

Hugo> just a question; is it possible to make questions in this list Hugo> that are not 100% seL4's source code related? I mean, seL4 will Hugo> be build and deployed on a variety of platforms, configurations, Hugo> environments, etc. The tutorials themselves deal with several Hugo> platforms. So, is it welcome/appropiate to make more generic Hugo> questions or this is not the right list? As one of the list admins, I can say that anything related to developing on seL4 is fair game. That includes documentation, news of interesting deployments, virtualisation and tooling, how to contribute, newbie help, and so on. We want this to be a friendly mailing list where people fell they can ask anything about seL4 development, development process, how best to use, etc. Blatant advertising is out; but interesting news is not. If it becomes too unweildy, we'll split the list. But right now the community is small enough, and well behaved enough, that we can use just the one. Peter C -- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW