August 2023 - Devel - lists.sel4.systems

Changing the cspace of a TCB while it is listening on a EP
by Sid Agrawal 08 Aug '23

08 Aug '23

Hi, I have a scenario and would like to understand how the kernel is expected to behave when I change the CSpace of a TCB when it is blocked on an EP. 1. A TCB (say TCB_1) is blocked on seL4_reply() on an endpoint (say EP_1). 2. Now, another PD, which has the capability to TCB_1, changes the CSpace of TCB_1 by using seL4_TCB_SetSpace(). Let's assume that the VSpace is identical. This new CSpace can be different from the old CSpace in 4 ways: A. It doesn't have the endpoint EP_1 B. It has the endpoint EP_1 but at a different CSlot. C. It has the endpoint EP_1 at the same CSlot. But since it is a different CSpace(so CNodes shared), it is a minted copy of the EP_1. Let's call it EP_1-prime. D. It has the endpoint EP_1 at the same CSlot, and it is the same EP as I have shared the CNode containing the EP_1 from the original CSpace. New and old CSpaces share the CNode containing that EP_1 like two trees sharing a sub-tree. I think scenario D should work as if nothing happened, but I do not know what to expect in scenarios A, B, and C. I will try these out soon, but I wanted your input as I did not find a clear answer in the manual. Best, Sid

2 2

Reminder seL4 developer hangout
by Birgit Brecknell 07 Aug '23

07 Aug '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Aug 9, 8am For your time zone, please see the calendar: https://sel4.systems/contact/ 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 2pm-5pm Fri 9am-5pm

1 0

Ultra96V2 in sel4cp_VMM is cautiously here - initial support
by Nataliya Korovkina 06 Aug '23

06 Aug '23

Highlights, briefly... 1. Project "ultra96v2-sel4cpvmm" The project introduces changes to the three components: seL4, sel4CP, sel4cp_VMM. * Xilinx Linux booting requires SMC calls support in seL4. The project uses the SMC cap impelementation offered by DornerWorks (approved but not merged). * Changes in sel4CP relate to the new capability in seL4. * As for sel4cp_VMM, a policy of VM's SMC calls handling will be different from one VMM-PD to another. The project introduces registration of a custom handler by PD application as well as it provides the default handler - the simplest "pipe" passing calls and responses through. The project published as sets of patches to the components. More the details are in the README.md and Issue #1 - https://github.com/malus-brandywine/ultra96v2_sel4cpvmm/issues/1 of the project: https://github.com/malus-brandywine/ultra96v2_sel4cpvmm 2. Project "petalinux-ultra96v2-sel4cpvmm" The project enables generation of linux image and minimal rootfs to run VM with sel4cp_VMM. More details are in README.md of the project: https://github.com/malus-brandywine/petalinux-ultra96v2-sel4cpvmm Status: Linux VM loads to login prompt

1 0

2 weeks left to get the early-bird registration at the seL4 summit
by Birgit Brecknell 04 Aug '23

04 Aug '23

2 weeks left to get the early-bird registration at the seL4 summit! A friendly reminder that the early bird cut-off date is 18 August 2023. Tickets include: - Participation in the 3-day conference, including talks, keynotes, seL4 updates & discussions - Networking with other seL4 experts and enthusiasts - Reception and Dinner Registrations: https://events.linuxfoundation.org/sel4-summit/register/ seL4 summit 2023: https://sel4.systems/Foundation/Summit/2023/<https://sel4.systems/Foundation/Summit/2023/> --- 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 2pm-5pm Fri 9am-5pm

1 0