- Devel - lists.sel4.systems

sel4test:nested timeout fault test flaky?
by Sam Leffler 25 Jan '23

25 Jan '23

We run sel4test regularly for a 64-bit raspi target under qemu and occasionally see failures like this: Starting test 129: TIMEOUTFAULT0003 > Running test TIMEOUTFAULT0003 (Nested timeout fault) > Error: Check badge(3) == expected_badge(2) failed. at line 9 This is a stock sel4test <https://github.com/AmbiML/sparrow-sel4test> + dep libs but an older kernel <https://github.com/AmbiML/sparrow-kernel>. Anyone know if this is an old (presumably fixed) bug or known issue? -Sam

3 5

Reminder seL4 developer hangout
by Birgit Brecknell 25 Jan '23

25 Jan '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Tue, Jan 24, 9pm (UTC), Topics: (open) * Sydney: Wed, Jan 25, 8am * Central Europe: Tue, Jan 24, 10pm * US Pacific Time: Tue, Jan 24, 1pm Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

3 2

Sel4 on RISC-V AllwinnerD1 MangoPi MQ1PH boot problem
by alex＠nixd.org 19 Jan '23

19 Jan '23

Hello, I just have a small question because I found the documentation about booting the Sel4 on RISC-V systems a bit confusing and not answering my questions. 1) I have ported all necessary code and I have successful compiled the `sel4test`. 2) I have flashed a SPL and U-Boot to 'mmc' which was built including OpenSBI fw_dynamic.bin but against most recent version (Sel4 was also compiled against most recent version OpenSBI v1.2 U-Boot SPL 2022.10-38338-g528ae9bc6c-dirty (Jan 11 2023 - 01:07:54 +0100)). 3) SPL and U-boot runs perfectly. 4) Sel4 does not want to boot. Why? So, in the DTS which I extracted from SDK it is said: ` /memreserve/ 0x40000000 0x200000; /* opensbi */ /memreserve/ 0x42000000 0x100000; /* dsp used 1MB */ memory@40000000 { device_type = "memory"; reg = <0x0 0x40000000 0x0 0x8000000>; }; ` For the elfloader objdump reports the `_start at 0x40a21000` so I hardcoded it into the following #define CONFIG_BOOTCOMMAND \ "if mmc rescan; then " \ "echo SD/MMC found on device ${mmc_dev};" \ "fatload mmc 0 0x40a21000 elfloader;" \ "fatload mmc 0 0x40a27940 archive.archive.o.cpio;" \ "bootelf 0x40a21000;" \ "fi;" \ And it reported an error: "Unhandled exception: Load access fault EPC: 000000007ffbd308 RA: 000000007ffbd33a TVAL: 00000005c66db5aa EPC: 0000000042e50308 RA: 0000000042e5033a reloc adjusted Code: 69a2 6145 8082 7480 1793 0069 9426 943e (641c) resetting ..." It seems that it relocates itself to 42e5033a (or not?) what actually I was trying to do manually. U-boot reports (for the domain0) the next address which is 0x0000000042e00000. And when I am loading elfloader there, it exists back to uboot shell without any errors and nothing happens. I can not understand what I am doing wrong, because FreeBSD and Linux starts normally. The #define seL4_UserTop is generated from DTS file if I understood correctly. But it seems it is incorrect. I will be happy for any hint. Thank you.

3 2

Can I launch two rumprun instances at the same time?
by mincheol＠vt.edu 06 Jan '23

06 Jan '23

Hi, I am trying to run two rumprun instances on seL4. I called launch_process(bin_name, CONFIG_RUMPRUN_COMMAND_LINE, 1); launch_process(bin_name, CONFIG_RUMPRUN_COMMAND_LINE, 2); in run_rr() of rumprun-sel4-demoapps/roottask/src/main.c. Then I got below: <<seL4(CPU 0) [decodeCNodeInvocation/107 T0xffffff801fe14400 "roottask" @4166c1]: CNode Copy/Mint/Move/Mutate: Source slot invalid o> sel4utils_move_cap_to_process@process.c:157 Failed to move cap <<seL4(CPU 0) [decodeX86PortControlInvocation/147 T0xffffff801fe14400 "roottask" @451efa]: IOPortControl: Some ports in range alread> arch_copy_IOPort_cap@arch.c:25 Failed to get IO port cap for range cf8 to cff I don't understand why I got these errors. launch_process() gets rump_process_t *process from process_from_id(id) so I should get a different slot with the different process id.

1 0

Question about non-blocking notification
by mincheol＠vt.edu 31 Dec '22

31 Dec '22

Hi, Do I need to use seL4-NBSend() for sending a non-blocking signal (cause seL4_Signal() is blocking)?

3 5

Question about sel4-tutorial dynamic-2 and dynamic-3
by mincheol＠vt.edu 29 Dec '22

29 Dec '22

Hi, I have two questions regarding dynamic-2 and dynamic-3 tutorials. 1. In dynamic-2 TASK 4, 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. 2. In dynamic-3, it uses sel4utils_configure_process_custom() to create a new thread. I looked into the function and found that it created a vspace for the new thread. However, the tutorial's learning outcomes section says "this time the two threads will only share the same vspace", so I am confused. Does this tutorial create a new vspace for the new thread? Mincheol

2 2

Any reliable way to determine if a thread is suspended?
by Andrew Warkentin 28 Dec '22

28 Dec '22

Is there any reliable way to determine if a thread is suspended? seL4_TCB_Suspend() succeeds even if the thread was already suspended. I can force all calls to seL4_TCB_Suspend() and seL4_TCB_Resume() to go through a wrapper that updates a user-level flag (since my OS manages pretty much all capabilities in the root server and will only expose TCBs to regular user processes through a special filesystem); however, this leaves a race when a thread is suspended due to a fault instead of an API call (since the thread will already be suspended before the fault handler updates the "thread running" flag). My initial use for checking if a thread is running is to allow easy atomic updates of some metadata (shared between the root server and the non-root thread, and optionally shared between threads) for my IPC transport layer that implements Unix-like file descriptors on top of seL4 endpoints (and eventually notifications). To add an FD to a thread's list, the root server allocates a copy of the endpoint (and reply if the FD is server-side) into the thread's CSpace, suspends the thread, updates the metadata (which includes the underlying capabilities), and then resumes the thread if it was running. Obviously, I don't want to resume threads that weren't running in the first place. I don't want to use locks here since the root server can't trust regular user processes. Another use is to allow cancelling any in-progress transfers on FDs when they get closed and returning a status to the waiting threads, which I am planning to do by replacing the endpoint with a copy of a global "clunk endpoint" associated with a thread that repeatedly sends a "file descriptor closed" message (actually there will be two such threads - one for clients, and one for servers) and then resuming the thread.

1 0

problem Ethdriver 82574 on Qemu X86_64
by reza yazdanparast 25 Dec '22

25 Dec '22

Hi. I'm working on a new camkes-based project. This project is simulated by using Qemu, on a Q35 machine for X86_64 arch and e1000e eth. I am using an intel controller driver (82574 controller) for network communication. My project has been built successfully and the intel network driver has been initialized. But when using the network in my application in Qemu, no network packet is sent and received! Qemu command: ``` sudo qemu-system-x86_64 -machine q35,accel=kvm,kernel-irqchip=split -cpu host, -netdev tap,id=netdev0,ifname=tap0,script=no,downscript=no -device e1000e,id=nic0,netdev=netdev0,mac=52:55:00:d1:55:01 -nographic -serial mon:stdio -m size=4G -device intel-iommu -kernel ./target/debug/images/kernel-x86_64-pc99 -initrd ./target/debug/images/capdl-loader-image-x86_64-pc99 ``` . Appendix: Create tap0 command: ``` export TAP_DEV=tap0 sudo ip tuntap add dev $TAP_DEV mode tap sudo ip addr flush dev $TAP_DEV sudo ip addr add 10.10.100.1/24 brd 10.10.100.255 dev $TAP_DEV sudo ip link set dev $TAP_DEV addr 02:00:ca:fe:01 sudo ip link set dev $TAP_DEV up ``` . how to fix this problem? Thank you.

1 0

any fun holiday hacks with sel4?
by ember arlynx 25 Dec '22

25 Dec '22

merry christmas :) i've been thinking about reviving some rusty robigalia-ish things. how are you all doing, this stormy sunday? -- ember

1 0

next seL4 TSC meeting on Fri 16 Dec (15 Dec in US and Europe)
by Gerwin Klein 16 Dec '22

16 Dec '22

The Technical Steering Committee (TSC) of the seL4 Foundation will hold its next public meting on: - Sydney: Fri, 16 Dec, 8am - Central Europe: Tue, 15 Dec, 10pm - US West Coast: Tue, 15 Dec, 1pm See also the seL4 calendar feed available from here: https://sel4.systems/contact/home.pml The meeting is by Zoom, and you can join from here: https://unsw.zoom.us/j/5510249963 Anyone interested can join the meeting and listen to the discussion and request to speak, which will be granted if time permits. Only TSC members can vote. The seL4 code of conduct applies to the meeting [1]. The agenda for the meeting so far is: - election (or re-election) of TSC chair - split C-Parser/AutoCorres out from l4v repository - RFCs: - SMC https://sel4.atlassian.net/browse/RFC-9 - MCS: Improve constraints on grant via reply https://sel4.atlassian.net/browse/RFC-13 - MCS: set fault and timeout handler parameters while configuring TCBs https://sel4.atlassian.net/browse/RFC-11 - The seL4 Core Platform https://sel4.atlassian.net/browse/RFC-5 - The seL4 Device Driver Framework https://sel4.atlassian.net/browse/RFC-12 - Ability to build additional bootloaders inside the seL4 build system https://sel4.atlassian.net/browse/RFC-4 - SIG chair nominations - discuss process for establishing SIGs If there are other items that I missed or you think should be on the agenda, please let me know. If we can't get to an item this time, we can still schedule another meeting. Cheers, Gerwin (TSC chair) [1]: https://docs.sel4.systems/processes/conduct.html

1 1