Devel June 2023

devel@sel4.systems

6 participants
5 discussions

Reminder seL4 developer hangout
by Birgit Brecknell 23 Jun '23

23 Jun '23

Hi all A friendly reminder that the seL4 developer hangout is on again next week: Wed, Jun 28, 7am (UTC), Topics: (open) * Sydney: Wed, Jun 28, 5pm * Central Europe: Wed, Jun 28, 9am * US Pacific Time: Wed, Jun 28, 12pm (midnight) 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

Bitfield generator EBNF grammar
by June Tate-Gans (ジューン) 07 Jun '23

07 Jun '23

Hey guys, I've been attempting to put together some rust bindings for the seL4 fault handling mechanisms, and I'm afraid the bitfield generator is driving me a bit up a wall at this point. I'd like to find a concise grammar for the language so I can better understand how bitfield_gen.py works, but there doesn't seem to be any explicit BNF for it anywhere. Is there a paper I should be reading or a reference guide somewhere that would help? Thanks! -- June Tate-Gans Software Engineer Techlead, Kata OS / AmbiML, Google

3 5

question about sel4 kernel preemptionPoint
by yadong.li 05 Jun '23

05 Jun '23

Hi: I have one question about sel4 kernel preemptionPoint on smp platform such as ARMv8. Take an example, when kernel takes long time to clear memory when UntypedRetype kernel object on core1, it will check preemptionPoint, when pending IRQ exists on core1, it will handle this irq, and return to userspace let other syscall or cores such as core2 have chance to run, but irq pending only check current cpu(PerCPU), no all cores of smp system, if core1 execute long seL4_Untyped_Retype syscall, core2 has a pending irq, the pending irq will not be checked in current core1, it will block until the execution of long syscall is completed if we take no account of archtimer irq, This phenomenon looks inconsistent at the system level between signal core and mutil core I want to know the current design intent about preemptionPoint of archtimer interrupt and other peripheral interrupts on SMP platform, only take current core interrupt as soon as possible or give other core and high priority task a chance to entry kernel and take big kernel lock? Thanks for your help

2 1

seL4 Rust crates doc links broken
by Hugo V.C. 01 Jun '23

01 Jun '23

Hi all, was looking around the Rust crates to check what is available to play around with seL4 from Rust and just found that most interesting ones (sel4_sys, sel4-start, ...) have documentation pointing doc.robigalia.org which is a broken link. Looks like the only communication way to Robigalia is #robigalia IRC channel... (I don't use IRC since 90s, not used to it anymore...) so I'm publishing this info here as I bet those amazing developers are in this list too and can read this message: please 🙏 fix the link at crates.io. Beside this, I will never get tired of remember the importance of taking care of the "general public" (that is, common developers not familiarized with seL4, common companies that are not security nor technical gurus, etc... that is, the average potential user of seL4 in the future) so it has an "easy/friendly" approach to seL4 as an early adopter. For that reason, checking that (healthy) Rust environment is there available for everyone will be a good starting point. seL4 topic is complex enough with documentation, so without it becomes simply not usable (for humans... 😅). Hoping Robigalia amazing guys can read this here, thank you for your work on Rust, as this is the best interface to seL4 development for people living on this planet. Best,

1 0

porting to a new platform
by steve.burke.56＠gmail.com 01 Jun '23

01 Jun '23

I'm trying to port an old sel4 code base to the latest so I decided to take the sel4test manifest & work through through the following page (https://docs.sel4.systems/projects/sel4/porting.html) The old code base does not add the new platform the same way since the new code seems to have some new CMake macros that do most of the heavy lifting. Is there a test project that does this with an arbitrary platform that I can use as a reference? My platform defines don't seem to be coming through correctly. Is working through the porting page the best way to do and does it seem current? Thanks.

3 2

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel June 2023