April 2020 - Devel - lists.sel4.systems

Failed to find device frame in new verion on my environment
by yadong.li 16 Apr '20

16 Apr '20

Hi， I recently move my wrok to a new seL4 version (I checkout default.xml in project camkes-arm-vm on 2020.02.25), I have below error print: “create_object@main.c:659 [Cond failed: err != seL4_NoError] Failed to find device frame/untyped at paddr = 0x90006000” 1、 I debug code, /**/ is my environment run parameter BOOT_CODE bool_t create_device_untypeds(cap_t root_cnode_cap, seL4_SlotPos slot_pos_before) { paddr_t start = 0; /*---------------------add region, start = 0x1800000, end = 0x2080000 *---------------------add region, start = 0x20ff000, end = 0x2100000 *---------------------add region, start = 0x80000000, end = 0x90001000 *---------------------add region, start = 0x90003000, end = 0x90004000 */ for (word_t i = 0; i < ndks_boot.resv_count; i++) { if (start < ndks_boot.reserved[i].start) { region_t reg = paddr_to_pptr_reg((p_region_t) { start, ndks_boot.reserved[i].start }); if (!create_untypeds_for_region(root_cnode_cap, true, reg, slot_pos_before)) { return false; } } start = ndks_boot.reserved[i].end; } /*---------------------add region, start = 0x90005000, CONFIG_PADDR_USER_DEVICE_TOP = 0xff, PPTR_TOP = 0xffffc0000000*/ if (start < CONFIG_PADDR_USER_DEVICE_TOP) { region_t reg = paddr_to_pptr_reg((p_region_t) { start, CONFIG_PADDR_USER_DEVICE_TOP }); /* * The auto-generated bitfield code will get upset if the * end pptr is larger than the maximum pointer size for this architecture. */ if (reg.end > PPTR_TOP) { reg.end = PPTR_TOP; } if (!create_untypeds_for_region(root_cnode_cap, true, reg, slot_pos_before)) { return false; } } return true; } 2、 CONFIG_PADDR_USER_DEVICE_TOP = 0xff, I found print the value must use 0x%x, can’t use 0x%lx, it is wrong 3、My platform is cortexA53 kernel/src/plat/j2/config.cmake:28: set(KernelArmCortexA53 ON) 4、and I change follow KernelArmCortexA53： a) ‘math(EXPR KernelPaddrUserTop "(1 << 40) - 1")’ to ‘set(KernelPaddrUserTop "1099511627775")’ ----------the print is “Failed to find device frame” disappear 5、my pc tools install，follow the seL4 wiki， cmakes version is 3.12.2 (> 3.7.2) 6、I did not find error or warning when I ../init-build.sh -DAARCH64=TRUE …… ---------------is it need to install new tools? Or other problem Thank you very much.

2 1

RPi4: DTS memory device and vm_minimal
by Turner, Ben 16 Apr '20

16 Apr '20

Hi, I have been attempting to get the vm_minimal application running on the Raspberry Pi 4 platform, and I have managed to get to the point where I need to define the memory regions for the kernel and virtual machine. The issue is that I do not know what the correct values (if any) would be needed in the overlay-rpi4.dts that I have created. From what I have found to this point, the Pi platform implements a memory system that means it is not possible to define memory regions in a DTS file. These memory regions are user-defined and are not known until runtime. I think I know what the answer will be to this; is there a way to overcome the oddities of the RPi4 memory setup when attempting to create a seL4 CAmkES VM linux image? Thanks, Ben Turner Senior Engineer Roke Manor Research Ltd Tel: +44 (0)1794 833721 ben.turner(a)roke.co.uk<mailto:ben.turner@roke.co.uk> ________________________________________ Roke Manor Research Limited, Romsey, Hampshire, SO51 0ZN, United Kingdom.Part of the Chemring Group. Registered in England & Wales. Registered No: 00267550 http://www.roke.co.uk _______________________________________ The information contained in this e-mail and any attachments is proprietary to Roke Manor Research Limited and must not be passed to any third party without permission. This communication is for information only and shall not create or change any contractual relationship. ________________________________________

2 3

Trouble booting default cmakes-vm-arm project under QEMU
by Travis Wheatley 16 Apr '20

16 Apr '20

Sel4 Developers, Still learning to crawl here. I have built the cmakes-vm-arm project for the qemu-arm-virt target. I have QEMU version 3.1.0 installed on my host. When I run the simulation by executing the command “./simulate”. it appears as though Sel4 is booting and successfully downloading the kernel, dtb, and loader. However, I am running into problems when it starts booting the kernel. It looks to me like it might be booting the kernel OK with the exception of a warning about GIC interrupts and subsequently drops to user space. Following that I see errors about insufficient memory and invalid num_vcpus. Not quite sure how to correct this. Hoping one of y’all can point me in the right direction. Here is a copy of the output — Begin included text — $ ./simulate ./simulate: qemu-system-aarch64 -machine virt,virtualization=on,highmem=off,secure=off -cpu cortex-a53 -nographic -m size=2048 -kernel images/capdl-loader-image-arm-qemu-arm-virt ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 paddr=[61b01000..62edd947] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 61bf7400. Loaded DTB from 61bf7400. paddr=[60239000..6023afff] ELF-loading image 'kernel' paddr=[60000000..60238fff] vaddr=[ff8060000000..ff8060238fff] (my_virtual_env) trickdev@trickvm ~/cmakes-arm-vm/vm-build $ ./simulate ./simulate: qemu-system-aarch64 -machine virt,virtualization=on,highmem=off,secure=off -cpu cortex-a53 -nographic -m size=2048 -kernel images/capdl-loader-image-arm-qemu-arm-virt ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 paddr=[61b01000..62edd947] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 61bf7400. Loaded DTB from 61bf7400. paddr=[60239000..6023afff] ELF-loading image 'kernel' paddr=[60000000..60238fff] vaddr=[ff8060000000..ff8060238fff] virt_entry=ff8060000000 ELF-loading image 'capdl-loader' paddr=[6023b000..61703fff] vaddr=[400000..18c8fff] virt_entry=407fe8 Enabling hypervisor MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Warning: Could not infer GIC interrupt target ID, assuming 0. Booting all finished, dropped to user space <<seL4(CPU 0) [decodeUntypedInvocation/216 T0xff80bf815400 "rootserver" @400704]: Untyped Retype: Insufficient memory (1 * 2097152 bytes needed, 0 bytes available).>> run(a)main.c<mailto:run@main.c>:1095 Invalid 'num_vcpus' attribute setting: Exceeds maximum number of supported nodes. Capping value to CONFIG_MAX_NUM_NODES (1) sel4platsupport_copy_irq_cap(a)device.c<mailto:sel4platsupport_copy_irq_cap@device.c>:41 Failed to get cap for irq irq_register_common(a)irq.c<mailto:irq_register_common@irq.c>:316 Failed to register an IRQ Assertion failed: (cspace->bitmap[index / BITS_PER_WORD] & BIT(index % BITS_PER_WORD)) == 0 (/home/trickdev/cmakes-arm-vm/projects/seL4_libs/libsel4allocman/src/cspace/single_level.c: _cspace_single_level_free: 100)

2 1

Best starting point for running VM Linux on a raspberry pi?
by Travis Wheatley 16 Apr '20

16 Apr '20

Greetings sel4 developers. Thus far I have successfully built and run the camkes-arm-vm on a TK1 platform as described here:https://docs.sel4.systems/projects/camkes-arm-vm/ I have also been able to boot to a u-boot prompt and run some sel4 test code as described here:https://docs.sel4.systems/Hardware/Rpi3.html My goal is to run a custom linux kernel under sel4 on the raspberry pi and am wondering what would be the best starting point. There is a tutorial about running a linux kernel under sel4 located here:https://docs.sel4.systems/Tutorials/camkes-vm-linux.html However, it only supports x86. There is also the camkes-arm-vm mentioned above but the raspberry pi is not among the supported platforms. Before reinventing the wheel I am hoping there might be some existing project or a better starting point for running a linux guest under sel4 on a raspberry pi that I can use. — Travis

2 1

Re: [seL4] Cross-core thread migration
by Millar, Curtis (Data61, Kensington NSW) 13 Apr '20

13 Apr '20

Hi Demi, > If I have a manycore machine, what is the best way to migrate a thread from > one core to another? Similarly, how can I send a capability (such as to > memory)? Cryptography is an option for the second one, but seems inelegant > and inefficient. When configured with SMP (which is not currently available in any verified config urations) a thread can be migrated to another core within a single kernel image cluster by changing its affinity. The MCS API will change this slightly; each scheduling context is associated with a core of the kernel image cluster so the scheduling context can be reconfigured to run on a different core (using that core's ScheduleControl capability) or a scheduling context already associated with that core can be bound to the thread to move it to that core. > Alternatively, are future versions of seL4 expected to > scale to manycore systems without needing a multikernel? That would > presumably make the answer trivial. IPC between cores in a single kernel image provides all of the necessary mechanisms for transferring data and capabilities between threads. In larger multicore machines, the cores would be split up into clusters where each cluster would essentially map to a single shared L2 cache (more generally, the clusters would be split to keep accesses to shared data structures in the kernel in the higher-level caches). I'm not sure how we would approach transferring kernel objects and capabilities between kernel images on different clusters whilst preserving the particular design goals that seL4 aims to implement. Cheers, Curtis

3 4

Support for 64-bit virtual machines on x86-64
by J Call 12 Apr '20

12 Apr '20

Hi all, I’m trying to use seL4 as a hypervisor on an embedded system. This particular SBC has 32 Gb of RAM and I’d like to install a couple of CentOS 8 64bit VMs side by side, but would like the vm’s to take advantage of more than 4Gb of RAM. Is there any word on seL4 supporting 64-bit virtual machines on the x86-64 architecture one day? Sincerely, Jonathan

2 1

Scheduler discussion on LWN
by Zach Lym 12 Apr '20

12 Apr '20

Red Hat's lead real-time scheduling engineer (who has a solid background in formal methods) posted an interested comment on an LWN article about seL4's scheduler research (https://lwn.net/Articles/745946/) While I disagree with the tone of the comment, I rarely see informed critiques of seL4 and context switching performance is core to microkernel viability. My apologies if this is an inappropriate venue for this discussion. --- "With the current scheduler, that driver must be given a high priority and trusted to not hog the CPU." So, they need to implement either RT throttling or the CBS, like Linux. "Another problem is data structures that are shared between criticalities....se of the priority-ceiling protocol can help." Nice, then they will see that the priority ceiling will add release jitter to the highest priority task, and then will notice that they will have to use other protocol, like, mutexes with priority inheritance? Where did I hear about it already... ah! On Linux! It is widely known that if you use priority ceiling, you will have scheduling "latency." But it really helps to reduce the response time... so, what do you prefer Response Time or Scheduling latency (release jitter or any scheduling delay, scheduler overhead... or any other name people do for it)? "Any process that exceeds its CPU budget during a given period can be throttled. Processes that have shorter periods are given a higher priority by the scheduler." Ok! here they have something like CBS, but they are using the fixed-priority rate monotonic scheduling approach! Nice! that is a technology from... 1969? But wait, if they already implemented this, why is the "network driver" a problem? - answer: because they cannot estimate the period of the packets arriving - RM is not flexible enough to all real-world cases! But that does not mean that this is the only solution. So my question is: Is there a sufficient & necessary schedulability test for their scheduler? "what happens if the client's budget runs out while the server is running?" Welcome to our world, check the "dl_boosted" variable on sched_deadline. "This new scheduler solves the problem, but it does not come for free: interrupt latency increases by 11% and scheduling itself is 19% more expensive. In both cases, the need to reprogram hardware timers is the source of most of the slowdown. But, he noted, scheduling in seL4 is "still an order of magnitude faster than Linux"" Welcome to our world again! And let me guess when you will start to have our numbers... When you finish implementing "some memory-management unit operations, and multicore operation"? Because on PREEMPT_RT we do this in microseconds, will they implementation continue working on ns (i.e., an order of magnitude faster than Linux) with such features? And I wonder, where is the mixed-criticality part of the schedulers...? Running Linux as a guest? I read the papers, and the work is very nice! Seriously! Very nice! But please, stop the comparison of orange and apples. It is not possible to compare this OS with Linux. Moreover, there are other OSs with such features running on real systems. Verified or not, they are certified for it.

2 1

答复: Devel Digest, Vol 71, Issue 10
by yadong.li 10 Apr '20

10 Apr '20

Subject: [seL4] TimeServer "IRQ already mapped" error Maybe the irq of Time exist in vm and TimeServer meanwhile. Try delete the tree node of time in your devices.camkes of you platform, like this: assembly { vm0.dtb = dtb([{}]); /*vm0.dtb = dtb([{"path": "/soc/serial@0xA5000000"}]);*/ -----only delete the conflict part } -----邮件原件----- 发件人: Devel [mailto:devel-bounces@sel4.systems] 代表 devel-request(a)sel4.systems 发送时间: 2020年4月10日 10:00 收件人: devel(a)sel4.systems 主题: Devel Digest, Vol 71, Issue 10 Send Devel mailing list submissions to devel(a)sel4.systems To subscribe or unsubscribe via the World Wide Web, visit https://sel4.systems/lists/listinfo/devel or, via email, send a message with subject or body 'help' to devel-request(a)sel4.systems You can reach the person managing the list at devel-owner(a)sel4.systems When replying, please edit your Subject line so it is more specific than "Re: Contents of Devel digest..." Today's Topics: 1. Re: setConsumed() in seL4_SchedContext_YieldTo (=?utf-8?B?bGFva3o=?=) 2. TimeServer "IRQ already mapped" error (Grant Jurgensen) ---------------------------------------------------------------------- Message: 1 Date: Thu, 9 Apr 2020 19:11:14 +0800 From: "=?utf-8?B?bGFva3o=?=" <laokz(a)foxmail.com> To: "=?utf-8?B?QW5uYSBMeW9ucw==?=" <anna(a)gh.st>, "=?utf-8?B?ZGV2ZWw=?=" <devel(a)sel4.systems> Subject: Re: [seL4] setConsumed() in seL4_SchedContext_YieldTo Message-ID: <tencent_C27271A3F0A40CF84A7FDBB4F299EB059A09(a)qq.com> Content-Type: text/plain; charset="utf-8" Hello Anna, With your point, I am cleared - activateThread() does the completeYieldTo assurance before A yield to B again. Can I conclude that YieldTo() method is limited to 1:1 relationship? Thanks, laokz ------------------ Original ------------------ From: "Anna Lyons"<anna(a)gh.st>; Date: Thu, Apr 9, 2020 07:12 AM To: "laokz"<laokz(a)foxmail.com>;"devel"<devel(a)sel4.systems>; Subject: Re: [seL4] setConsumed() in seL4_SchedContext_YieldTo P {margin-top:0;margin-bottom:0;} Hi laokz, Yes, that scenario cannot happen. If B runs to block, and A is scheduled, the kernel will complete A's initial yieldTo call and clear the appropriate values before resuming A. Cheers Anna. From: laokz <laokz(a)foxmail.com> Sent: Wednesday, 8 April 2020 11:32 PM To: Anna Lyons <anna(a)gh.st>; devel <devel(a)sel4.systems> Subject: Re: [seL4] setConsumed() in seL4_SchedContext_YieldTo Hello Anna, Thanks for the reply. Maybe I'v imagined an impractical scenario: 1. A yield to B. B->sc->scYieldFrom=A 2. B run then block. 3. A run then yield to B again. 4. Now at the beginning, setConsumed() called; because B is not runnable, so return_now=true and setConsumed() called again at the end. For cooperative threads, this indeed shouldn't happen but it depends. For example if B can block, then great care should be taken to forbid this edge case. Regards, laokz ------------------ Original ------------------ From: "Anna Lyons"<anna(a)gh.st>; Date: Mon, Apr 6, 2020 12:16 PM To: "laokz"<laokz(a)foxmail.com>;"devel"<devel(a)sel4.systems>; Subject: Re: [seL4] setConsumed() in seL4_SchedContext_YieldTo P {margin-top:0;margin-bottom:0;} Hi, Thanks for the observation! It's true that setConsumed should only be called once per kernel entry, and it's not obvious just from the code snippets to observe that this is true. However, the semantics of YieldTo mean that both of these code paths cannot be executed in the same kernel entry. If return_now is true, this means that the current thread will be switched to and sc->scYieldFrom should be NULL (as the YieldTo call has completed). This is usually the case if the calling thread YieldTo a lower priority thread, or a thread that is not runnable. On the other hand if return_now is false, the YieldTo resulted in the thread being YieldedTo being switched to, so we return the result of the YieldTo on a different kernel entry (when we run the thread that called YieldTo again). With this context, take a look at the if block here: https://github.com/seL4/seL4/blob/master/src/object/schedcontext.c#L191 Where you can see that we only set sc->scYieldFrom when we also set return_now to false. Glad to see someone looking at the MCS kernel. Anna. ------------------------------ Message: 2 Date: Thu, 9 Apr 2020 09:48:49 -0500 From: Grant Jurgensen <gajurgensen(a)gmail.com> To: devel(a)sel4.systems Subject: [seL4] TimeServer "IRQ already mapped" error Message-ID: <CAGJ6_3Cdhk9BrMD0roaCZvi7QZr1M7U3GA1jQ3=m0tMHaThSew(a)mail.gmail.com> Content-Type: text/plain; charset="UTF-8" Hi all, I'm trying to add a timer to my CAmkES component (all I need is a timestamp). I've been using this example component as a reference: https://github.com/seL4/camkes/tree/master/apps/timeserver My problem is that when I declare an instance of the global TimeServer component in my ".camkes" file, I get an error at build-time: "parse-capDL: IRQ already mapped: 68". I'm not sure what to make of this error. The only major difference between my project and the reference above is that I am building atop the camkes-arm-vm project. Could the VM be interfering here? Thanks, Grant Jurgensen ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel ------------------------------ End of Devel Digest, Vol 71, Issue 10 *************************************

1 0

Re: [seL4] setConsumed() in seL4_SchedContext_YieldTo
by laokz 09 Apr '20

09 Apr '20

Hello Anna, With your point, I am cleared - activateThread() does the completeYieldTo assurance before A yield to B again. Can I conclude that YieldTo() method is limited to 1:1 relationship? Thanks, laokz ------------------ Original ------------------ From: "Anna Lyons"<anna(a)gh.st>; Date: Thu, Apr 9, 2020 07:12 AM To: "laokz"<laokz(a)foxmail.com>;"devel"<devel(a)sel4.systems>; Subject: Re: [seL4] setConsumed() in seL4_SchedContext_YieldTo P {margin-top:0;margin-bottom:0;} Hi laokz, Yes, that scenario cannot happen. If B runs to block, and A is scheduled, the kernel will complete A's initial yieldTo call and clear the appropriate values before resuming A. Cheers Anna. From: laokz <laokz(a)foxmail.com> Sent: Wednesday, 8 April 2020 11:32 PM To: Anna Lyons <anna(a)gh.st>; devel <devel(a)sel4.systems> Subject: Re: [seL4] setConsumed() in seL4_SchedContext_YieldTo Hello Anna, Thanks for the reply. Maybe I'v imagined an impractical scenario: 1. A yield to B. B->sc->scYieldFrom=A 2. B run then block. 3. A run then yield to B again. 4. Now at the beginning, setConsumed() called; because B is not runnable, so return_now=true and setConsumed() called again at the end. For cooperative threads, this indeed shouldn't happen but it depends. For example if B can block, then great care should be taken to forbid this edge case. Regards, laokz ------------------ Original ------------------ From: "Anna Lyons"<anna(a)gh.st>; Date: Mon, Apr 6, 2020 12:16 PM To: "laokz"<laokz(a)foxmail.com>;"devel"<devel(a)sel4.systems>; Subject: Re: [seL4] setConsumed() in seL4_SchedContext_YieldTo P {margin-top:0;margin-bottom:0;} Hi, Thanks for the observation! It's true that setConsumed should only be called once per kernel entry, and it's not obvious just from the code snippets to observe that this is true. However, the semantics of YieldTo mean that both of these code paths cannot be executed in the same kernel entry. If return_now is true, this means that the current thread will be switched to and sc->scYieldFrom should be NULL (as the YieldTo call has completed). This is usually the case if the calling thread YieldTo a lower priority thread, or a thread that is not runnable. On the other hand if return_now is false, the YieldTo resulted in the thread being YieldedTo being switched to, so we return the result of the YieldTo on a different kernel entry (when we run the thread that called YieldTo again). With this context, take a look at the if block here: https://github.com/seL4/seL4/blob/master/src/object/schedcontext.c#L191 Where you can see that we only set sc->scYieldFrom when we also set return_now to false. Glad to see someone looking at the MCS kernel. Anna.

1 0

Re: [seL4] Cross-core thread migration
by Millar, Curtis (Data61, Kensington NSW) 09 Apr '20

09 Apr '20

On Tue, 2020-04-07 at 12:00 +1000, devel-request(a)sel4.systems wrote: > Send Devel mailing list submissions to > devel(a)sel4.systems > > To subscribe or unsubscribe via the World Wide Web, visit > https://sel4.systems/lists/listinfo/devel > or, via email, send a message with subject or body 'help' to > devel-request(a)sel4.systems > > You can reach the person managing the list at > devel-owner(a)sel4.systems > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Devel digest..." > > > Today's Topics: > > 1. Re: setConsumed() in seL4_SchedContext_YieldTo (Anna Lyons) > 2. Cross-core thread migration (Demi Obenour) > > > ------------------------------------------------------------------- > --- > > Message: 1 > Date: Mon, 6 Apr 2020 04:16:00 +0000 > From: Anna Lyons <anna(a)gh.st> > To: laokz <laokz(a)foxmail.com>, devel <devel(a)sel4.systems> > Subject: Re: [seL4] setConsumed() in seL4_SchedContext_YieldTo > Message-ID: > < > BYAPR13MB22292529DC4150329B0C44E6DCC20(a)BYAPR13MB2229.namprd13.prod.outlook.com > > > > Content-Type: text/plain; charset="iso-8859-1" > > Hi, > > Thanks for the observation! It's true that setConsumed should only be > called once per kernel entry, and it's not obvious just from the code > snippets to observe that this is true. > > However, the semantics of YieldTo mean that both of these code paths > cannot be executed in the same kernel entry. > > If return_now is true, this means that the current thread will be > switched to and sc->scYieldFrom should be NULL (as the YieldTo call > has completed). This is usually the case if the calling thread > YieldTo a lower priority thread, or a thread that is not runnable. On > the other hand if return_now is false, the YieldTo resulted in the > thread being YieldedTo being switched to, so we return the result of > the YieldTo on a different kernel entry (when we run the thread that > called YieldTo again). > > With this context, take a look at the if block here: > https://github.com/seL4/seL4/blob/master/src/object/schedcontext.c#L191 > Where you can see that we only set sc->scYieldFrom when we also set > return_now to false. > > Glad to see someone looking at the MCS kernel. > Anna. > > > > Confidentiality Note:This email is intended only for the person or > entity to which it is addressed and may contain information that is > privileged, confidential or otherwise protected from disclosure. > Unauthorized use, dissemination, distribution or copying of this > email or the information herein by anyone other than the intended > recipient is strictly prohibited. If you have received this email in > error, please notify the sender immediately and destroy the original > message, any attachments thereto and all copies. > > > ------------------------------ > > Message: 2 > Date: Mon, 6 Apr 2020 02:23:08 -0400 > From: Demi Obenour <demiobenour(a)gmail.com> > To: devel(a)sel4.systems > Subject: [seL4] Cross-core thread migration > Message-ID: > < > CAJEMUN_it3Uf4Bhs3dVvfLRPeQvznJ8BCJ+Rq2wLbqcLDDHyCw(a)mail.gmail.com> > Content-Type: text/plain; charset="UTF-8" > > If I have a manycore machine, what is the best way to migrate a > thread from > one core to another? Similarly, how can I send a capability (such as > to > memory)? Cryptography is an option for the second one, but seems > inelegant > and inefficient. Alternatively, are future versions of seL4 expected > to > scale to manycore systems without needing a multikernel? That would > presumably make the answer trivial. > > Sincerely, > > Demi > > > ------------------------------ > > Subject: Digest Footer > > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel > > > ------------------------------ > > End of Devel Digest, Vol 71, Issue 6 > ************************************ Hi Demi, > If I have a manycore machine, what is the best way to migrate a thread from > one core to another? Similarly, how can I send a capability (such as to > memory)? Cryptography is an option for the second one, but seems inelegant > and inefficient. When configured with SMP (which is not currently available in any verified config urations) a thread can be migrated to another core within a single kernel image cluster by changing its affinity. The MCS API will change this slightly; each scheduling context is associated with a core of the kernel image cluster so the scheduling context can be reconfigured to run on a different core (using that core's ScheduleControl capability) or a scheduling context already associated with that core can be bound to the thread to move it to that core. > Alternatively, are future versions of seL4 expected to > scale to manycore systems without needing a multikernel? That would > presumably make the answer trivial. IPC between cores in a single kernel image provides all of the necessary mechanisms for transferring data and capabilities between threads. In larger multicore machines, the cores would be split up into clusters where each cluster would essentially map to a single shared L2 cache (more generally, the clusters would be split to keep accesses to shared data structures in the kernel in the higher-level caches). I'm not sure how we would approach transferring kernel objects and capabilities between kernel images on different clusters whilst preserving the particular design goals that seL4 aims to implement. Cheers, Curtis

1 0