- Devel - lists.sel4.systems

Combatting spam
by David Barrass 12 Apr '22

12 Apr '22

Hi Peter, Thank you for raising this issue - it is an annoying distraction. The general standard of the list is very high as one would expect and it is a shame to see this kind of behaviour polluting the discussions. I am very happy to have to earn a privilege to post and am happy for anything I post to be moderated. I would welcome any proposition to keep spammers off the list whilst keeping it open but I don't think any solution should impose additional burdens on the moderators. I think that this warrants a bit of thought and will give this some consideration. Your proposal sounds good and I support it. In the meantime thank you and many thanks to all the team who make this happen. I find the work on seL4 very valuable and relevant. best regards to all, David

1 0

Combatting spam on this list
by Peter Chubb 12 Apr '22

12 Apr '22

Hi Folks, We're trying hard to avoid spam coming through this list. In particular we moderate all emails coming from non-members, and only let through on-topic postings. Recently, however, we've had some people join the list, and then posting spam. I'm proposing that the first post a person makes will always be moderated; and we'll turn off the moderation after the first on-topic posting. Anyone who posts spam will have that address marked as discard immediately. This means that *all* next posts will be moderated until I or one of the other moderators lets them through, because I'll be changing the default processing. Comments? I'd rather keep things as open as possible, but spammers are making it hard. Peter C -- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW Core hours: Mon 8am-3pm; Wed: 8am-5pm; Fri 8am-12pm.

1 0

RFC 10
by Gerwin Klein 11 Apr '22

11 Apr '22

This is a last call for comments for RFC-10 before the TSC votes on it this week: https://sel4.atlassian.net/browse/RFC-10 The RFC is about consolidating AArch64 page table objects and has been uncontroversial so far, just wanted to make sure people are aware of it. Cheers, Gerwin

2 1

Does the lastest master branch support gic v3 virtulization?
by wtliang785 09 Apr '22

09 Apr '22

hello devel, We want to use Sel4 in our project, but the gic version is v3. I know sel4 kernel 12.1.0 version does not support v3 virtuliazation. My question is that what is the status for supporting the v3 virtulization in lastest sel4 kernel master branch? Does the lastest master branch support gic v3 virtulization? thank you Peter Wang

2 1

capDL-tool fix for empty CNode slots
by Sam Leffler 06 Apr '22

06 Apr '22

If you generate capdl for a CNode with empty slots, capDL-tool incorrectly calculates CDL_CapMap::num because it uses Map.size which doesn't include empty slots. The right way to calculate "num" is by taking the max of the key values +1. diff --git a/capDL-tool/CapDL/PrintC.hs b/capDL-tool/CapDL/PrintC.hs index ec0eda9..b4a2cbb 100644 --- a/capDL-tool/CapDL/PrintC.hs +++ b/capDL-tool/CapDL/PrintC.hs @@ -224,7 +224,7 @@ memberSlots objs obj_id slots irqNode cdt ms = showSlots objs obj_id (Map.toList slots) irqNode cdt ms +++ "}," where - slot_count = Map.size slots + slot_count = if Map.null slots then 0 else (fst $ Map.findMax slots) + 1 printInit :: [Word] -> String printInit argv = -Sam

2 3

Interrupt handling - General Purpose Timer
by JENKINSON Mark 06 Apr '22

06 Apr '22

Hi seL4 Devel, We are trying to use the General Purpose Timer1 for our i.MX8MQ-based board within a simple CAmkES app. GPT1 is initialising and starting OK, but the interrupt handler for handling rollover is not being triggered. Through instrumenting the code with printf's, the GPT initialisation looks reasonable, and the expected rollover interrupt is being generated and seen within handleInterrupt(); however, the interrupt handler routine that has been registered is not being called. I'm hoping that someone can give me some ideas where to investigate next please? A few more details: From gpt_init() (in util_libs/libplatsupport/src/mach/imx/gpt.c), instrumentation within allocate_irq_callback() confirms that, for: gpt->irq_id = ps_irq_register(&gpt->io_ops.irq_ops, irq, gpt_handle_irq, gpt); our values are: irq->type = 3; // PS_INTERRUPT irq->irq.number = 87 (0x57); // 55 (0x37) + 32 = 87 (0x57) which agrees with the GPT1 entry from our dts file (when combined with the offset of 32, which I've seen explained elsewhere): gpt@302d0000 {... reg = < 0x302d0000 0x10000 >; interrupts = < 0x00 0x37 0x04 >;... And gpt_handle_irq() is registered as the interrupt handler, which resets the rollover flag and manages the counter's high_bits variable. Resulting from this call to ps_irq_register(), gpt->irq_id = 27 (0x1b), although I'm not sure of the significance of this irq_id value. Our test app starts GPT1. After ~3 mins, the timer rolls over, as expected. Instrumentation in handleInterrupt(irq) is triggered with: irq = 87 (0x57); // as expected, the GPT1 rollover interrupt However, gpt_handle_irq() is never called, despite being associated with irq 87 back in the ps_irq_register() call. Instrumentation in handleInterrupt() shows that the IRQSignal case is executed and sendSignal() is called. Within sendSignal, the NtfnState_Idle case is executed, calling ntfn_set_active(ntfnPtr, badge), with badge = 1. I stop tracking the flow there, but pick up again that ackInterrupt() is visited with irq = 87 (0x57). Everything looks in order (the right interrupt is generated at the right time and is detected) except gpt_handle_irq() is not called. The timer app keeps ticking away, but without the rollover management, time ends up skipping. Thanks for your help, Mark. This message contains information that may be privileged or confidential and is the property of the Capgemini Group. It is intended only for the person to whom it is addressed. If you are not the intended recipient, you are not authorized to read, print, retain, copy, disseminate, distribute, or use this message or any part thereof. If you receive this message in error, please notify the sender immediately and delete all copies of this message.

1 0

OpenPower/PowerPC/ppc64le port: major concerns and obstacles
by Isaac Beckett 06 Apr '22

06 Apr '22

Hello seL4 devel! Recently I was on the developer hangout meeting and brought up a ppc port. Interest seemed low, and some even called ppc a “niche” architecture which seems unfair. There was also the much more concrete concerns of funding and overall maintenance. I believe an PPC port would be very valuable, and I plan to do a whole essay/write up of some sort, but I am also not the most familiar with the technical challenges, and could use more information on those. I do think there is definitely people who would want to run seL4 on PowerPC platforms. PowerPC is one of the few ISAs that has existing, modern hardware without closed-source binary blobs, which I believe pose a real threat to the trustworthiness of the hardware seL4 is currently capable of running on.

2 1

A way to reclaim initial thread resources
by Marcin Witkowski 05 Apr '22

05 Apr '22

Hey, I am currently looking for a way to reclaim resources allocated by kernel for the rootserver thread, i.e. memory for CNode, TCB, BootInfo, etc. My current approach looks like this: * in rootserver instead of calling seL4_TCB_Suspend, call custom syscall seL4_ReclaimRootserverResources. This sycall as parameters takes CNode and slot no. after which kernel should be able to freely write new caps. This CNode is main CNode of some component initialized by the rootserver. * implmenetation of this syscall then suspends initial thread, schedules new thread, revokes most of rootserver's resources, notably TCB, BootInfo, IPCBuffer, VSpace and CNode. Then for those now free memory regions new untyped capabilities are created, with the same sizes as the original objects. Lastly, new capabilities are written to subsequent slots in CNode a'la boot.c, so with null MDBNode; mdbRevocable and mdbFirstBadged set to true. This solution has couple of problems. First and foremost, it requires creating additional syscall to handle this. Secondly, even though the component _technically_ has access to this newly created capabilities, it doesn't know where they are, or how big they are. This could be partially band-aided by hardcoding this information in relevant component, but that is far from elegant. This component also recives rest of the untyped memory from rootserver, including bootinfo entries about this memory specification, so that renders solution with hardcoding spec even worse. Last but not least, before the seL4_ReclaimRootserverResources is called, all the components are resumed using seL4_TCB_Resume as part of rootserver's work, so there could be race-condition between calling reclaiming syscall, and component initialization (although I am not 100% sure about that part) Is there maybe a better way to do it, and I am doing it all round? The perfect solution would be to somehow extend bootinfo and/or remaining untypeds that were given by the kernel to the rootserver.

2 3

Reminder seL4 developer hangout/video call
by Birgit Brecknell 04 Apr '22

04 Apr '22

Hi all A friendly reminder that the seL4 developer hangout is on this week: Wed, Apr 6, 7am (UTC), Topics: (open) * Sydney: Wed, Apr 6, 5pm * Central Europe: Wed, Apr 6, 9am * US Pacific Time: Wed, Apr 6, 12 midnight (There are too many time zones in the world to cite them all :-)) 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

The Call for Presentations for the seL4 summit 2022 is out!
by June Andronick (seL4 Foundation) 01 Apr '22

01 Apr '22

We are calling for proposals to present at the seL4 Summit 2022! Share your seL4 work. Share your seL4 experience. Share your seL4 thoughts. Share your seL4 questions. Check the full Call For Presentations and topics of interest at: https://sel4.systems/Foundation/Summit/cfp <https://sel4.systems/Foundation/Summit/cfp> To propose a talk, send an abstract of one page or less by Monday 9th of May 2022 to summit(a)sel4.systems <mailto:summit@sel4.systems>. Please do spread the word and also encourage others to submit a talk if you like their work! Thanks, June

1 0