- Devel - lists.sel4.systems

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

07 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 07 Apr '22

07 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 06 Apr '22

06 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

Overlapping pointer returned by memalign
by WILLIAMS Stephen 01 Apr '22

01 Apr '22

Hi, I’m currently working on a project porting drivers from U-Boot to seL4 and have run into an unexpected problem seemingly triggered by use of the memalign within the U-Boot drivers. What I am seeing is that calls to memalign from within my CAmkES component can return pointers to regions which overlap with those previously returned by malloc. Obviously this leads to the two allocated regions trampling over each other and resulting corruption of data. I’m at a complete loss to explain this behaviour and would be very grateful to receive any suggestions or pointers. Thanks for your help, Stephen 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.

3 9

Re: How to switch virtual machines linux in vm_multi from camkes-vm-example?
by Peter Chubb 31 Mar '22

31 Mar '22

>>>>> "yjy" == yjy <yjy7894(a)126.com> writes: yjy> `screen /dev/ttyUSB0 115200`. I have a shell terminal that can yjy> see the output from VM0. I input @1 to shell, which is useless. It only works at the start of a line. Peter C yjy> At 2022-03-31 14:12:16, peter(a)chubb.wattle.id.au wrote: >>>>>>> "yjy" == yjy <yjy7894(a)126.com> writes: >> yjy> Hi, I have already run the camkes-vm-example vm_multi on my yjy> board, but i don't know how to switch linux vm shell from another yjy> linux vm, Can anyone help me solve this? >> >> If you're talking about controlling the serial console to talk to >> different VMs, the instructions are >> https://github.com/seL4/camkes-vm in the README.md under 'Serial' >> >> >> In brief, output from different VMs is colour coded. Switch >> between them for input with @0, @1, @2 etc. >> >> Peter C _______________________________________________ Devel >> mailing list -- devel(a)sel4.systems To unsubscribe send an email to >> devel-leave(a)sel4.systems yjy> [2 <text/html; GBK (base64)>] -- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW Core hours: Mon 8am-3pm; Wed: 8am-5pm; Fri 8am-12pm.

1 0

How to switch virtual machines linux in vm_multi from camkes-vm-example?
by yjy 31 Mar '22

31 Mar '22

Hi, I have already run the camkes-vm-example vm_multi on my board, but i don't know how to switch linux vm shell from another linux vm, Can anyone help me solve this? Best, Comet

2 1

Question for student research
by Seth Nielson 31 Mar '22

31 Mar '22

Hi. I am mentoring a student group trying to do some work on SEL4. We are trying to setup basic TCP/IP networking and are really struggling to find documentation or up-to-date guides. We found a project that has networking (it even has some filesystem and a small webserver as part of the project). We thought we just about had the networking component working for QEMU but there seems to be issues with QEMU and networking, at least the way we did it. Does anyone have any how-to guides for getting basic networking up and running? If QEMU is not great for networking, please suggest a development board. Thanks much.

2 2