- Devel - lists.sel4.systems

Nvidia Tegra SoCs: Has anyone tried running seL4 on them?
by Isaac Beckett 12 Dec '21

12 Dec '21

Has anyone experimented with running seL4 on Tegra SoCs? I’m interested mainly because I own a Nintendo Switch console that is vulnerable to an exploit in the boot rom that allows for booting arbitrary payloads. Most people use it to run modified versions of the official firmware, or to run Linux or Android, so the hardware is at least decently well reverse engineered at this point, and there are even proper Linux drivers for the joy-con detachable controllers. I’m interested in attempting to run seL4 on this device, mostly to see if I can, but I figured I’d ask here first to see if anyone’s attempted similar hardware.

2 2

next seL4 TSC meeting on Fri 17 Dec (16 Dec in US and Europe)
by Gerwin Klein 11 Dec '21

11 Dec '21

The Technical Steering Committee (TSC) of the seL4 Foundation will hold its next public meting on: - Sydney: Fri, 17 Dec, 8am - Central Europe: Tue, 16 Dec, 10pm - US West Coast: Tue, 16 Dec, 1pm The meeting is by Zoom, and you can join from here: https://unsw.zoom.us/j/82827057586 Anyone interested can join the meeting and listen to the discussion and request to speak, which will be granted if time permits. Only TSC members can vote. The seL4 code of conduct applies to the meeting [1]. The agenda for the meeting so far is: - update on GitHub status, test stability, etc - release schedule - change main verification platform to imx8? - RFCs: - Core Platform https://sel4.atlassian.net/browse/RFC-5 - Removing CNode Mutate https://sel4.atlassian.net/browse/RFC-7 - SMC calls https://sel4.atlassian.net/browse/RFC-9 If there are other items that I missed or you think should be on the agenda, please let me know. If we can't get to an item this time, we can still schedule another meeting. Cheers, Gerwin (TSC chair) [1]: https://docs.sel4.systems/processes/conduct.html

1 0

two questions about cteDelete of sel4 kernel？
by yadong.li 11 Dec '21

11 Dec '21

Hi： I have two questions about cteDelete of sel4 kernel？ IF I want to delete slot that slot->cap is cnode object(I called it level 1 cnode). The finaliseSlot function will create zombie capability and call reduceZombie(), param "immediate" is ture. the reduceZombie() call cteDelete() delete the endSlot, if the endSlot->cap is cnode capability again(I call it level 2 cnode), this time param "immediate" is false. and cteDelete() will call reduceZombie again, but because param "immediate " is false ,this time reduceZombie will not call cteDelete recursively. the reduceZombie will call capSwapForDelete，it will swap zombie cap with slot 0 of level 2 cnode, if Swap cap(slot0 of level 2 cnode) is not cnode or tcb(the cnode object slot 0 must point to cnode self ? I did not find this limitation), when it return to finaliseSlot, finaliseSlot will check finaliseCap, because swap cap is not cnode or tcb, almost it call be capRemovable, and it return directly. 1. I think when call capSwapForDelete in reduceZombie, the level 2 cnode become Cyclic zombie, but when return finaliseSlot, I do not think it will deal with below branch: if (!immediate && capCyclicZombie(fc_ret.remainder, slot)) { } because this time ,slot ->cap is not cnode or tcb, it will not create zombie cap. then Who will delete level 2 cnode ? Is it lost as "Cyclic zombie", memory leak? 2. when delete cnode, it will check "preemptionPoint", if our delete is beak, even though fs_ret.success is false, but this false is not deliver to caller who will delete it again? thank you for your help

1 0

How can I port the seL4 microkernel to my unofficially verified hardware？
by yjy 10 Dec '21

10 Dec '21

Does the document provide relevant information or project? I read related articles and I can be sure that my instruction set is common. Thank you.

2 1

Troubles booting VM with large memory(e.g VM_RAM_SIZE >= 2048MB)
by Han JingLong 韩景龙 09 Dec '21

09 Dec '21

Hello all, Reference to seL4 Docs/Projects/CAmkES ARM VMM, I have successfully run a VM (a Linux guest OS and config VM_RAM_SIZE = 1024MB) on a new ARM(ArmV8a CortexA55) platform. But when I tried to increase the ram size assigned to VM, I encountered the following error: ============================================================================== ram_ut_alloc_iterator@guest_ram.c:295 Failed to allocate page map_vm_memory_reservation@guest_memory.c:470 Failed to get frame for reservation address 0xae7c0000 reservation_size:60000000 …… vm_ram_touch@guest_ram.c:160 Failed to touch ram region: Not registered RAM region 32 bit ARM insts not decoded Pagefault from [Linux]: write fault @ PC: 0xffff000008d9132c IPA: 0xaffff000, FSR: 0x92000046 Context: x0: 0xffff7dfffe639000 x1: 0x0 x2: 0xfc0 x3: 0x4 x4: 0x0 x5: 0x40 x6: 0x3f x7: 0x0 x8: 0xffff7dfffe639000 x9: 0x0 x10: 0x1000 x11: 0x6f01c3b8 x12: 0xc0000000 pc: 0xffff000008d9132c x14: 0x0 sp: 0xffff000009668d80 spsr: 0x40000085 x13: 0x60000000 x15: 0x4 x16: 0x1800 x17: 0xffff7dfffe81c3b4 x18: 0x8 x19: 0xaffff000 x20: 0xffff0000096a1fd0 x21: 0xffff7dfffe80009c x22: 0x58389df x23: 0xffff0000091ce000 x24: 0x4b78e0 x25: 0x47b87c x26: 0x0 x27: 0xa0000000047b818 x28: 0x614f0018 x29: 0xffff000009643eb0 x30: 0xffff0000094f7ad0 m-------- Assertion failed: rt >= 0 (/home/hjl/workdir/vmm_sel4_sdx_android/projects/seL4_projects_libs/libsel4vm/src/arch/arm/fault.c: fault_get_width: 623) Attach config file for reference： 1. overlay dts reserved-memory { #address-cells = < 0x02 >; #size-cells = < 0x02 >; ranges; vm-memory@60000000 { reg = < 0x00 0x60000000 0x00 0x60000000 >; no-map; }; }; 1. devices.camkes #define VM_INITRD_MAX_SIZE 0x5000000 //80 MB #define VM_RAM_BASE 0x60000000 #define VM_RAM_OFFSET 0 #define VM_RAM_SIZE 0x60000000 #define VM_DTB_ADDR 0x6F000000 #define VM_INITRD_ADDR 0x6A000000 vm0.untyped_mmios = [ “0x35436000:12”, // Interrupt Controller Virtual CPU interface (Virtual Machine view) /* The purpose of these untyped regions is to force the untyped * allocator to treat this memory region as reserved so that when we * try to ensure that the VMM is placed into this region in RAM, it * will definitely be available for placement. * * This address pertains to vm-memory@60000000 in the overlay DTS */ “0x60000000:28”, // RAM “0x70000000:28”, // RAM “0x80000000:28”, // RAM “0x90000000:28”, // RAM “0xa0000000:28”, // RAM “0xb0000000:28”, // RAM ]; 1. guest linux dts memory@60000000 { device_type = “memory”; reg = <0x00 0x60000000 0x00 0x60000000>; }; ============================================================================== In contrast, I tried to expand the VM memory based on QEMU and encountered the same problem. Attach config file for reference： 1. settings.cmake if(${PLATFORM} STREQUAL “qemu-arm-virt”) set(QEMU_MEMORY “4096”) set(KernelArmCPU cortex-a53 CACHE STRING “” FORCE) set(VmInitRdFile ON CACHE BOOL “” FORCE) endif() 1. overlay-reserve-vm-memory.dts reserved-memory { #address-cells = < 0x02 >; #size-cells = < 0x02 >; ranges; vm-memory@40000000 { reg = <0x0 0x40000000 0x0 0x50000000>; no-map; }; }; 1. devices.camkes #define VM_INITRD_MAX_SIZE 0x1900000 //25 MB #define VM_RAM_BASE 0x40000000 #define VM_RAM_SIZE 0x50000000 #define VM_RAM_OFFSET 0x00000000 #define VM_DTB_ADDR 0x4F000000 #define VM_INITRD_ADDR 0x4D700000 vm0.untyped_mmios = [ “0x8040000:12”, // Interrupt Controller Virtual CPU interface (Virtual Machine view) “0x40000000:29”, // Linux kernel memory regions “0x60000000:29”, // Linux kernel memory regions “0x80000000:28”, // Linux kernel memory regions ]; 1. guest linux dts memory@40000000 { reg = <0x0 0x40000000 0x0 0x50000000>; device_type = “memory”; }; Is there any memory limit for VM? or Configuration problem? Anyways anyone any help can provide would be awesome and thanks in advance for any help! 邮件免责申明 Email Disclaimer 本邮件仅供本邮件指定收件人使用，其所载内容可能因含有保密信息或其它原因而不得披露。除本公司及本邮件指定收件人外，任何人不得公开、传播、分发、复制、印刷或使用本邮件之任何部分或其所载之任何内容。如您误收到本邮件，请立即通知本公司，并将原始邮件、附件及其所有复本从系统中删除，切勿使用。 This email is for the use of the designated receivers only，and the content is not allowed to be disclosed due to the confidential information or other reasons. Except for the Company and the designated receivers of this email, no one shall disclose, disseminate, distribute, copy, print or use any part of this email or any content contained therein. If you receive this email by mistake, please notify the Company immediately, and delete the original email, attachments and all copies from the system. Do not use it. 网络通信可能含有计算机病毒或其它缺陷，可能无法准确和/或及时送达其它系统，亦可能受阻而不为本公司或本邮件指定收件人所知。本公司对此类错误或遗漏以及任何因使用本邮件而引致之任何损失概不承担责任。 Network communication may contain computer viruses or other defects, which may not be delivered to other systems accurately and / or in time, or may be blocked by the Company or the designated receivers of this email. The Company shall not be liable for such errors or omissions and for any loss arising from this email. 本邮件所载任何内容仅作为业务层面交流与参考，除非明确说明，本公司不对邮件所载内容之准确性、完整性或公平性等承担任何法律责任。 Any contents contained in this email are only for the purpose of business communication and reference only. Unless explicitly stated otherwise, the Company shall not assume any legal responsibility for the accuracy, completeness or fairness of the content contained in the email. 本邮件指定收件人应特别注意：本邮件所载任何内容不构成本公司对本邮件指定收件人和/或其所属商业实体的任何要约、要约邀请或承诺，任何权利义务皆以双方签字盖章的书面文件为准。除经本公司以签字盖章的书面文件确认外，收件人和/或其所属商业实体不得以本邮件所载任何内容作为其向本公司主张任何权利或利益的正式依据。 The designated receivers should pay special attention to the fact that nothing contained in this email shall constitute an offer, invitation or acceptance by the Company to the designated receivers of this email and/or its affiliated business entities, and any rights and obligations are subject to the written documents signed and sealed by both parties. Except from the written document signed ,sealed and confirmed by the Company, the receivers and / or its affiliated business entity shall not rely on anything contained in this email as the formal basis for claiming any rights or interests to the Company.

1 0

getKernelWcetUs: where does the 10us return value come from?
by Jack Chen 09 Dec '21

09 Dec '21

Hi all, Quick questions regarding the return value of getKernelWcetUs(): 1. For ARM the value is assigned during build process taking config.cmake files, where KERNEL_WCET's are all 10us (except for tk1 it's 100us, typo?) For x86 the function returns 10 directly, and for risc-v, comment suggests it's copied from x86 hoping it's an overestimate. Where does this "10us" come from? Based on static estimate done previously on Armv6 (imx31)? AOS lecture mentioned a "378us" kernel WCET estimate and 99.5us observed WCET for Armv6. 2. Is this 10us WCET value the one used as padding in the Temporal Partitioning routine? ("worst-case flushing time"?) Regards, Jack

3 5

Incorporating seL4 into your project, risc-v architecture
by so_s＠gmx.de 08 Dec '21

08 Dec '21

Dear seL4 devs and community. I try to create a simple project using the seL4 micro kernel. For setting up my environment I followed this (https://github.com/manu88/SeL4_101) and this (https://docs.sel4.systems/projects/buildsystem/incorporating.html) article. As kernel I'm using the last release of SeL4 (https://github.com/seL4/seL4/releases/tag/12.1.0) I created some kind of user application, like Manu88 did with a simple Hello World C-Program. While building with the delivered init-build.sh script I got a lot of repeating errors like this: CMake Error at tools/cmake-tool/helpers/simulation.cmake:179 (add_custom_command): Error evaluating generator expression: $<TARGET_PROPERTY:rootserver_image,KERNEL_IMAGE_NAME> Target "rootserver_image" not found. Call Stack (most recent call first): CMakeLists.txt:22 (GenerateSimulateScript) While going through Manu88s guide I saw that he also got this errors. But after adding a CMakeList.txt file inside his user code, and declaring it as rootserver inside the CMakeList.txt file (I just copied the contents from here: https://github.com/manu88/SeL4_101/blob/master/projects/Hello/CMakeLists.txt) he got rid of the errors. I still get them and searching through the internet could not find a solution for me. Bellow I added the folder structure of my project. Project/ ├── kernel/ ├── projects/ │ ├── Hello/ │ ├── musllibc/ │ ├── utils_libs/ │ ├── seL4_libs/ ├── build/ ├── tools/ │ └── cmake-tool/ │ └── elfloader-tool/ ├── init-build.sh -> tools/cmake-tool/init-build.sh ├── CMakeLists.txt ├── application_settings.cmake -> tools/cmake-tool/helpers/application_settings.cmake ├── settings.cmake So I cannot tell where the issue lies. Any pointers would be appreciated. Kind regards, Sophia

2 3

capdl-loader questions
by Sam Leffler 08 Dec '21

08 Dec '21

I've been investigating how capd-loader works and have some questions. My apologies if these were previously discussed. 1. CDL_Model is mutable. The capDL specification looks like a perfect candidate for being in .rodata but it's stored+treated as mutable. Why? I see capdl-loader uses the mutability to store mapped page frame caps and, for risc-v, VSpace roots, but both can be easily handled w/o modifying the spec. Having this immutable has many benefits. 2. All page frames are treated as shared. CAPDL_SHARED_FRAMES is #define'd in the code so every frame is treated as shared. This inflates the size of the orig_caps array and the kernel capabilities table but seems unnecessary. Why? I've verified that instead of doing the Copy op on each page you can just check the return of the seL4_Page_Map call and if necessary clone the cap. Better would be for camkes to identify shared page frames so this doesn't require 2x syscalls (which spam's the console w/ CONFIG_PRINTING enabled). 3. Why does copy_addr_with_pt exist? There are two memory regions created for mapping page frames into the rootserver address space for doing fill ops. One is 64KB and the other is 1 page (nominally 4KB). init_frame tries the 4KB region first then falls back to the 64K region if mapping into the 4KB region fails. Why (i.e. why would the 1st mapping call fail)? On my risc-v system I never use the 64K region and I'm not sure when it might be used? Even if it were used, why is 64K always allocated; seems like the region should be sized according to the target platform. Having this extra region has a cost that can be significant on small systems. 4. console output. Why is sel4_DebugPutChar (or similar) not a standard part of the kernel? This forces capdl-loader to depend on libsel4platsupport for console output which in turn affects cap space. I can't imagine an seL4 system that cannot write to the console and I think it's entirely reasonable to have a critical system service like the rootserver use that. 5. duplicate_caps. The scheme for constructing a running system from a spec is straightforward except for duplicating caps. Why are all TCB's and CNode caps dup'd? Why does init_tcbs call init_tcb on the original object but immediately configure_tcb on the dup? There are other places where the dup cap is used instead of the original cap (e.g. init_cnode_slot). None of this seems to matter on risc-v; maybe this matters on some other architectures? 6. On risc-v all pages appear to be marked executable--including ipc buffers! This seems just wrong and a potential security hole. 7. Why does seL4_TCB_WriteRegisters take a _mutable_ seL4_UserContext? I'm guessing this is a mistake in the xml spec (but haven't looked). 8. init_cspaces mystifies me. There are two loops over all CNodes; one that does "COPY" operations and one that does "MOVE" operations. I see nothing explaining what's happening. I've read this code many times and still don't get it; please explain. 9. According to comments, the use of a global static to setup the UserContext for a new TCB is done because one cannot take the address of a local variable. On what architecture is this true? On risc-v the context is copied into "registers" before calling the kernel so this doesn't appear to be an issue with crossing the user-kernel protection boundary. 10. Memory reclamation. I'm unclear what happens to the memory used by capdl-loader. The process does a TCB_Suspend call when it's done. Does this cause the CSpace & VSpace to be reclaimed? For CAmkES this doesn't matter as there's no support for allocating memory but I'm building a system where this isn't true. How do I release memory (in particular) back to the untyped pool? I have a bunch of niggly code complaints/questions but let's start with the above. -Sam

2 4

Re: some performance problem when test 4 cores SMP答复: Devel Digest, Vol 127, Issue 5
by yadong.li 07 Dec '21

07 Dec '21

Hi: > So you would expect that the reported metric would scale following Amdahl's law based on the proportion of an operation that is serialized inside the kernel lock which would potentially vary across platforms. > It cannot simply be throughput, else the doubled delay should be reflected in a significantly reduced throughput, but it has almost no effect. 1. This is what I also feel confused, I think whether it is depend on the implementation of ipc_normal_delay ipc_normal_delay will call below code: delay = OVERHEAD_FIXUP(REXP(id) * current_delay_cycle, overhead); insert a command such as 'zigset(...)'for every core, The ziggurat method for generating random variables, when double delay, the random variables coefficient will reduce the delay influence? 2. " the proportion of an operation that is serialized inside the kernel lock ", CLH lock is serialized between cores, if 4 cores will have big different performance on different ARM platform? > For 3 or 4 cores the combined latency of two IPCs is larger than the 500cy delay and you expect lock contention, resulting in reduced scaling, while it should still scale almost perfectly with the 1000cy delay. > > > Addition： > > Our seL4_Call performance is same with other platform > > XXXX IMX8MM_EVK_64 TX2_64 > > seL4_Call 367(0) 378(2) 492(16) client->server, same vspace, ipc_len is 0 > > seL4_ReplyRecv 396(0) 402(2) 513(16) server->client, same vspace, ipc_len is 0 1. the seL4_Call and seL4_ReplyRecv are measured on SMP kernel 2. or 3 or 4 cores the combined latency of two IPCs is larger than the 500cy delay and you expect lock contention ---- that's what I thought at first, But It can't be explained very well on IMX8MM_EVK_64, base on the test seL4_Call data, when run on 3 cores and 4cores, IMX8MM_EVK_64 still have a good scalability, so I think not all seL4_Call and ReplyRecv flow which cost maybe 300 or 400 is locked(like el trap), TX2 should have a good scalability as expected when run on 3 or 4 cores, but it did not show good, from data below：1497740（3core， 500cycles），1545872（4core） > > My test results below: > > ARM platform > > Test item XXX IMX8MM_EVK_64 TX2 > > mean(Stddev) > > 500 cycles, 1 core 636545(46) 625605(29) 598142(365) > > 500 cycles, 2 cores 897900(2327) 1154209(44) 994298(94) > > 500 cycles, 3 cores 1301679(2036) 1726043(65) 1497740(127) > > 500 cycles, 4 cores 1387678(549) 2172109(12674) 1545872(109) > > 1000 cycles, 1 core 636529(42) 625599(22) 597627(161) > > 1000 cycles, 2 cores 899212(3384) 1134110(34) 994437(541) > > 1000 cycles, 3 cores 1297322(5028) 1695385(45) 1497547(714) > > 1000 cycles, 4 cores 1387149(456) 2174605(81) 1545716(614) > I notice your standard deviations for 2 and 3 cores are surprisingly high (although still small in relative terms). > > Did you try running the same again? Are the numbers essentially the same or are multiple runs all over the shop? 1. Yes，I test several times，I always get the same results, have little different 2. I think the stddev is small relative to our test results, IMX8MM_EVK_64 also have a big stddev(500 cycles, 3core) from the data. -----邮件原件----- 发件人: devel-request(a)sel4.systems [mailto:devel-request@sel4.systems] 发送时间: 2021年12月7日 11:45 收件人: devel(a)sel4.systems 主题: Devel Digest, Vol 127, Issue 5 Send Devel mailing list submissions to devel(a)sel4.systems To subscribe or unsubscribe 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: Use TimeServer by Group Components Questions (Kent Mcleod) 2. Re: Incorporating seL4 into your project, risc-v architecture (Kent Mcleod) 3. Re: some performance problem when test 4 cores SMP benchmark of seL4bench project 答复: Devel Digest, Vol 127, Issue 1 (Kent Mcleod) 4. Re: Use TimeServer by Group Components Questions (15852538526(a)139.com) 5. Re: Use TimeServer by Group Components Questions (Kent Mcleod) 6. Re: some performance problem when test 4 cores SMP benchmark of seL4bench project 答复: Devel Digest, Vol 127, Issue 1 (Gernot Heiser) ---------------------------------------------------------------------- Message: 1 Date: Tue, 7 Dec 2021 13:03:00 +1100 From: Kent Mcleod <kent.mcleod72(a)gmail.com> Subject: [seL4] Re: Use TimeServer by Group Components Questions To: 15852538526(a)139.com Cc: devel <devel(a)sel4.systems> Message-ID: <CA+-ozWeJgZm3B902EKBU6dUGxy6wU3Cp92jEUYwRKNFcVS=7DA(a)mail.gmail.com> Content-Type: text/plain; charset="UTF-8" On Fri, Dec 3, 2021 at 2:51 PM <15852538526(a)139.com> wrote: > > I got an problem when I use TimeServer with Group Components. I wish more than one component in the same Group Components, that can use TimeServer. While the cdl only have one ep for all components in the Group to communicate to TimeServer with an badge value that not equal to zero. And TimeServer must to distinguish requester by the badge, so only one component can receive TimeServer's response. How can I resolve this problem? The TimeServer component cannot be used as part of a Group component. The Group component mechanism isn't designed to transparently work for any component and the Connection types that the TimeServer uses are not compatible with the Group mechanism. > _______________________________________________ > Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email > to devel-leave(a)sel4.systems ------------------------------ Message: 2 Date: Tue, 7 Dec 2021 13:14:30 +1100 From: Kent Mcleod <kent.mcleod72(a)gmail.com> Subject: [seL4] Re: Incorporating seL4 into your project, risc-v architecture To: so_s(a)gmx.de Cc: devel <devel(a)sel4.systems> Message-ID: <CA+-ozWeU7Bi-byXhsvo9jnQ_tcn90U7QRa8_hh39p2rVgUcKzA(a)mail.gmail.com> Content-Type: text/plain; charset="UTF-8" On Fri, Dec 3, 2021 at 8:14 AM <so_s(a)gmx.de> wrote: > > Dear seL4 devs and community. > > I try to create a simple project using the seL4 micro kernel. For setting up my environment I followed this (https://github.com/manu88/SeL4_101) and this (https://docs.sel4.systems/projects/buildsystem/incorporating.html) article. As kernel I'm using the last release of SeL4 (https://github.com/seL4/seL4/releases/tag/12.1.0) I created some kind of user application, like Manu88 did with a simple Hello World C-Program. While building with the delivered init-build.sh script I got a lot of repeating errors like this: > CMake Error at tools/cmake-tool/helpers/simulation.cmake:179 (add_custom_command): > Error evaluating generator expression: > > $<TARGET_PROPERTY:rootserver_image,KERNEL_IMAGE_NAME> > > Target "rootserver_image" not found. > Call Stack (most recent call first): > CMakeLists.txt:22 (GenerateSimulateScript) While going through > Manu88s guide I saw that he also got this errors. But after adding a CMakeList.txt file inside his user code, and declaring it as rootserver inside the CMakeList.txt file (I just copied the contents from here: https://github.com/manu88/SeL4_101/blob/master/projects/Hello/CMakeLists.txt) he got rid of the errors. I still get them and searching through the internet could not find a solution for me. Bellow I added the folder structure of my project. > Project/ > ├── kernel/ > ├── projects/ > │ ├── Hello/ > │ ├── musllibc/ > │ ├── utils_libs/ > │ ├── seL4_libs/ > ├── build/ > ├── tools/ > │ └── cmake-tool/ > │ └── elfloader-tool/ > ├── init-build.sh -> tools/cmake-tool/init-build.sh > ├── CMakeLists.txt > ├── application_settings.cmake -> > tools/cmake-tool/helpers/application_settings.cmake > ├── settings.cmake > > So I cannot tell where the issue lies. Any pointers would be appreciated. If you are using https://github.com/manu88/SeL4_101/blob/master/projects/Hello/CMakeLists.txt inside projects/Hello/ then you need to make sure that the top level CMakeLists inside Project/ is either a symlink to tools/cmake-tool/default-CMakeLists.txt or is similar to https://github.com/manu88/SeL4_101/blob/master/CMakeLists.txt. With this file layout, ../init-build.sh will end up calling the following CMake invocation: `cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DSEL4_CACHE_DIR=../.sel4_cache -C "../settings.cmake" "../"`. What is the contents of your settings.cmake file? > > Kind regards, > Sophia > _______________________________________________ > Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email > to devel-leave(a)sel4.systems ------------------------------ Message: 3 Date: Tue, 7 Dec 2021 13:43:48 +1100 From: Kent Mcleod <kent.mcleod72(a)gmail.com> Subject: [seL4] Re: some performance problem when test 4 cores SMP benchmark of seL4bench project 答复: Devel Digest, Vol 127, Issue 1 To: Gernot Heiser <gernot(a)unsw.edu.au> Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> Message-ID: <CA+-ozWcihN6my4WOyPbpCcfp3=rksYSnnEgZE2kc6c-BV4Kymw(a)mail.gmail.com> Content-Type: text/plain; charset="UTF-8" On Thu, Dec 2, 2021 at 9:28 PM Gernot Heiser <gernot(a)unsw.edu.au> wrote: > > > > > On 2 Dec 2021, at 16:17, yadong.li <yadong.li(a)horizon.ai> wrote: > > > > First, I got the data of IMX8MM_EVK_64 and TX2 from > > https://github.com/seL4/sel4bench/actions/runs/1469475721#artifacts, > > the sel4bench-results-imx8mm_evk file and sel4bench-results-tx2 file, unpack the file out, I find xxxx_SMP_64.json Secondly, the test is the smp benchmark form sel4bench-manifest project, the source file is sel4bench/apps/smp/src/main.c The test scenario look like below: > > A pair thread of ping-pong on the same core, the ping thread will > > wait for "ipc_normal_delay" time then send 0 len ipc message to pong > > thread, then return. I think the 500 cycles mean how long > > ipc_normal_delay will really delay > > > The above scenario will test on one core, or mutil core. If we run 4 cores, every core will have a ping thread and a pong thread run like above description, then record the sum of all cores ping-pong counts. > > ok, but what is the metric reported? [Apologies for not being on top > of the details of our benchmarking setups.] Looking at the sel4bench smp benchmark implementation, the metric is the total number of "operations" in a single second. An operation is a round trip intra address space seL4_Call + seL4_ReplyRecv between 2 threads on the same core with each thread delaying for the cycle count before performing the next operation. After 1 second of all cores performing these operations continuously and maintaining a core-local (on a separate cache line) count, the total number of operations is added together and reported as the final number. So you would expect that the reported metric would scale following Amdahl's law based on the proportion of an operation that is serialized inside the kernel lock which would potentially vary across platforms. > > It cannot simply be throughput, else the doubled delay should be reflected in a significantly reduced throughput, but it has almost no effect. > > > I think this experiment is used to illustrate in multi core, our seL4 kernel big lock will not affect mutli-core performance, am I right ? > > Not quite. As there’s only one big lock, only one core can execute the kernel at any time. If one core is in the IPC while another core is trying to IPC, even though both IPCs are core-local, the second will have to wait until the first gets out of the lock. > > As the delay is higher than the syscall latency, you’d expect perfect scalability from one core to two (with the lock essentially synchronising the threads). For 3 or 4 cores the combined latency of two IPCs is larger than the 500cy delay and you expect lock contention, resulting in reduced scaling, while it should still scale almost perfectly with the 1000cy delay. This is exactly what you see for the i.MX8 and the TX2. > > > Addition： > > Our seL4_Call performance is same with other platform > > XXXX IMX8MM_EVK_64 TX2_64 > > seL4_Call 367(0) 378(2) 492(16) client->server, same vspace, ipc_len is 0 > > seL4_ReplyRecv 396(0) 402(2) 513(16) server->client, same vspace, ipc_len is 0 > > OK, so baseline performance is good. But are these measured on a single-core or SMP kernel (i.e. is locking included)? > > > My test results below: > > ARM platform > > Test item XXX IMX8MM_EVK_64 TX2 > > mean(Stddev) > > 500 cycles, 1 core 636545(46) 625605(29) 598142(365) > > 500 cycles, 2 cores 897900(2327) 1154209(44) 994298(94) > > 500 cycles, 3 cores 1301679(2036) 1726043(65) 1497740(127) > > 500 cycles, 4 cores 1387678(549) 2172109(12674) 1545872(109) > > 1000 cycles, 1 core 636529(42) 625599(22) 597627(161) > > 1000 cycles, 2 cores 899212(3384) 1134110(34) 994437(541) > > 1000 cycles, 3 cores 1297322(5028) 1695385(45) 1497547(714) > > 1000 cycles, 4 cores 1387149(456) 2174605(81) 1545716(614) > > I notice your standard deviations for 2 and 3 cores are surprisingly high (although still small in relative terms). > > Did you try running the same again? Are the numbers essentially the same or are multiple runs all over the shop? > > There are some issues with our benchmarking methodology. Fixing up sel4bench is one of the projects I’d like to do if I got a student for it, or maybe someone from the community would want to help? > > But just from looking at the data I’m not sure that’s the issue here. > > Gernot > _______________________________________________ > Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email > to devel-leave(a)sel4.systems ------------------------------ Message: 4 Date: Tue, 07 Dec 2021 03:06:38 -0000 From: 15852538526(a)139.com Subject: [seL4] Re: Use TimeServer by Group Components Questions To: devel(a)sel4.systems Message-ID: <163884639883.1070957.2394639262660252936(a)mattermost.seL4.systems> Content-Type: text/plain; charset="utf-8" Thank you very much for answering my question. I still have a doubt about the TimeServer. I can manually modify the cdl file and then I get the the expected source file(capdl_spec.c) from using capdl-parse. I also need to change the return value of timeserver <IF>_notification API. I have try and I can run the program as I expected. Is there any way to create adapted cdl file automatic by modifying the ADL parse project? I am looking forward to getting your answer again. Thank you very much. my ADL file: import <std_connector.camkes>; import <global-connectors.camkes>; import <TimeServer/TimeServer.camkes>; component Client { control; uses Timer timeout; } assembly { composition { group grp { component Client c1; component Client c2; } component TimeServer time_server; connection seL4TimeServer ts1( from grp.c1.timeout, to time_server.the_timer); connection seL4TimeServer ts2( from grp.c2.timeout, to time_server.the_timer); } configuration { time_server.timers_per_client = 1; } } ------------------------------ Message: 5 Date: Tue, 7 Dec 2021 14:23:54 +1100 From: Kent Mcleod <kent.mcleod72(a)gmail.com> Subject: [seL4] Re: Use TimeServer by Group Components Questions To: 15852538526(a)139.com Cc: devel <devel(a)sel4.systems> Message-ID: <CA+-ozWestyqAM4wy+x359CLZLf13PzdCRBNFSfPY-3nyo9Y6wA(a)mail.gmail.com> Content-Type: text/plain; charset="UTF-8" On Tue, Dec 7, 2021 at 2:09 PM <15852538526(a)139.com> wrote: > > Thank you very much for answering my question. I still have a doubt about the TimeServer. I can manually modify the cdl file and then I get the the expected source file(capdl_spec.c) from using capdl-parse. I also need to change the return value of timeserver <IF>_notification API. I have try and I can run the program as I expected. Is there any way to create adapted cdl file automatic by modifying the ADL parse project? There isn't a supported way to modify the generated cdl file as CAmkES expects to generate a full system specification. What is your motivation for trying to make the timeserver a group component instead of a separate component? As part of a group component it will still have its own kernel objects for its threads, code, data and heap memories so you still have the costs of isolation but without the benefits because it still shares the virtual address space and capability space with other components in the same group. > I am looking forward to getting your answer again. Thank you very much. > > my ADL file: > import <std_connector.camkes>; > import <global-connectors.camkes>; > import <TimeServer/TimeServer.camkes>; > > component Client { > control; > uses Timer timeout; > } > > assembly { > composition { > group grp { > component Client c1; > component Client c2; > } > component TimeServer time_server; > > connection seL4TimeServer ts1( > from grp.c1.timeout, to time_server.the_timer); > connection seL4TimeServer ts2( > from grp.c2.timeout, to time_server.the_timer); > } > > configuration { > time_server.timers_per_client = 1; > } > } > _______________________________________________ > Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email > to devel-leave(a)sel4.systems ------------------------------ Message: 6 Date: Tue, 7 Dec 2021 03:45:09 +0000 From: Gernot Heiser <gernot(a)unsw.edu.au> Subject: [seL4] Re: some performance problem when test 4 cores SMP benchmark of seL4bench project 答复: Devel Digest, Vol 127, Issue 1 To: "devel(a)sel4.systems" <devel(a)sel4.systems> Message-ID: <17FC6BC4-3407-44AE-B7AA-4623EFF76988(a)unsw.edu.au> Content-Type: text/plain; charset="utf-8" On 7 Dec 2021, at 13:43, Kent Mcleod <kent.mcleod72(a)gmail.com> wrote: > > Looking at the sel4bench smp benchmark implementation, the metric is > the total number of "operations" in a single second. An operation is > a round trip intra address space seL4_Call + seL4_ReplyRecv between 2 > threads on the same core with each thread delaying for the cycle count > before performing the next operation. After 1 second of all cores > performing these operations continuously and maintaining a core-local > (on a separate cache line) count, the total number of operations is > added together and reported as the final number. So you would expect > that the reported metric would scale following Amdahl's law based on > the proportion of an operation that is serialized inside the kernel > lock which would potentially vary across platforms. Thanks for the explanation, Kent. Observations: 1) The metric is essentially independent of the delay. Looking at the single-core figures for the i/MX8, I get 1598.5 ns in both cases, the difference being 15ps. Doesn’t make sense to me. 2) Assuming this processor runs at the 1.8GHz it seems speced for, this corresponds to 2877 cycles, which is huge, even if the 1000cy delay is subtracted! 3) As I said before, intra-AS IPC is a meaningless metric we should never use (but that’s incidental to the particular thing we want to measure here). 4) Having to do these calculations to understand the numbers is a sure indication that the results are presented in an unsuitable form. I can’t see how these figures make sense. Gernot ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email to devel-leave(a)sel4.systems ------------------------------ End of Devel Digest, Vol 127, Issue 5 *************************************

1 0

CfP: Microkernel and Component-based OS Devroom at FOSDEM 2022
by Alexander Boettcher 07 Dec '21

07 Dec '21

Hello seL4 community, FOSDEM 2022 will be an online event (again) with the traditional Microkernel devroom as part of it. Thanks to Martin Decky & my colleague Sebastian Sumpf for engagement! The original Call for Papers follows. Best regards, Alexander. -- Alexander Boettcher Genode Labs https://www.genodians.org - https://www.genode.org ------------------------------------------------------------------------------------------------------ Microkernel and Component-based OS Devroom at FOSDEM 2022 CALL FOR PARTICIPATION On-line version of this CfP: http://fosdem.microkernel.info/ The developers and users of several free and open source microkernel-based and component-based operating systems will meet on-line as part of FOSDEM 2022 [1] and will share a developer room. The devroom is currently looking for content in the form of talks and activities related to the area of microkernel-based, unikernel-based, component-based operating systems and similar topics. The devroom has been preliminarily scheduled to Saturday February 5th 2022. The devroom will take place during European day hours. Possible topics of the devroom include, but are not limited to: * introduction of a specific OS or framework * design of subsystems and the general architecture of an OS * languages, tools and toolchains used * enabling support for hardware (architectures, device drivers) and programming languages * development processes, debugging * maintenance, testing and release engineering * safety, security and robustness * trends and challenges * research and open questions * community and governance * use cases, experiences and status updates * best practices and lessons learned * demos This is a call for your participation. We kindly ask you to submit your proposals no later than on December 28th 2021. Please use the Pentabarf web site [2] to submit your proposals. If you already have a user account in Pentabarf, please do not create a new one. Addtionally, make sure to select the Microkernel and Component-based OS Devroom as the track when submitting your talk and include at least the following information in your proposal: * title of your talk * your full name * short abstract of your talk (one or two paragraphs) * duration of your talk (at least 20 minutes and no longer than 50 minutes) * your short bio * your photo The talks will be pre-recorded in advance in January and streamed automatically during the event. This means that you will need to complete and submit your talk recording by January 15th 2022. However, each speaker should be also present on-line just after the streaming of their talk for a live Q&A. You can specify your prefered time slot of your talk. The communication language of the devroom is English. The official devroom schedule (along with the accepted talks) will be announced on December 31st 2021 on the devroom's mailing list [3] and the speakers will be notified via e-mail. The schedule will also be published on the FOSDEM web site. For any comments, questions and suggestions (e.g. suggestions for a different type of event during the devroom), please do not hesitate to use the devroom's mailing list [3]. About the Devroom Since the first Microkernel OS Devroom at FOSDEM 2012 [4], this devroom has been a part of each following FOSDEM (with slight variations of the name). The focus gradually widened to include component-based, unikernel-based and other operating systems. By now, it has become a somewhat institutionalized tradition for the open source operating systems community and it is one of the few places where microkernel enthusiasts and people with different views on how operating systems should work meet regularly. To this date, over a dozen projects have participated in one way or another. Many of the projects face similar challenges but come up with partially different solutions. Therefore, the goal of the devroom is to bring the various projects together, let them exchange ideas, cross-pollinate and socialize. Extraordinary Circumstances in 2022 (Again) Due to the extraordinary mode of organization of FOSDEM 2022 (being an on-line event again), the devroom talks will be required to be pre-recorded in January and streamed during the event (with a live Q&A). The talk videos will be published under Creative Commons license by FOSDEM. By submitting a recorded talk, the speaker agrees to have it made available publicly indefinitively. For organizational purposes, we also need contact information of the speakers of accepted talks. Please check the official CfP page [5] of the devroom regularly. We will keep updating it as technical guidelines will be set by the FOSDEM organizers. Microkernel Dinner Sadly, it will not be possible to arrange our traditional microkernel dinner and other in-person social gatherings in Brussels this time again. However, we plan a closing event of the devroom as a loose approximation of the microkernel dinner. The details will be announced later. We encourage the on-line participats to bring their own food and beverages. About FOSDEM FOSDEM [6] is a two-day event organized by volunteers to promote the widespread use of free and open source software. FOSDEM is widely recognized as one of the best such conferences worldwide. FOSDEM covers a wide spectrum of free and open source software and hardware projects and offers a platform for people to collaborate. To this end, FOSDEM has set up developer rooms (devrooms) where teams can meet and showcase their projects. Devrooms are a place for teams to discuss, hack and publicly present latest directions, lightning talks, news and proposals. Besides developer rooms, FOSDEM also offers main tracks, lightning talks, certification exams and project stands. In recent years, FOSDEM has been hosting more than 5000 developers annually at the ULB Solbosch campus. Due to the circumstances, FOSDEM 2022 will be organized as an on-line event. The participation in FOSDEM is totally free, although the organizers gratefully accept donations and sponsorship. No registration is necessary, but attendees are expected to follow the FOSDEM's code of conduct [7]. Important Dates Recap * 2021-12-28: Deadline for talk proposal submission * 2021-12-31: Schedule published and speakers notified of acceptance * 2022-01-15: Deadline for talk pre-recoding submission * 2022-02-05: Devroom taking place on-line Contact In case of any comments, questions and suggestions, please do not hesitate to contact the devroom organizers via the devroom's mailing list [3]. The primary organizers of the devroom in 2022 are: * Sebastian Sumpf * Martin Decky Links [1] https://fosdem.org/2022/ [2] https://penta.fosdem.org/submission/FOSDEM22/ [3] https://lists.fosdem.org/listinfo/microkernel-devroom [4] https://archive.fosdem.org/2012/schedule/track/microkernel_os_devroom.html [5] http://fosdem.microkernel.info/ [6] https://fosdem.org/ [7] https://fosdem.org/2022/practical/conduct/

1 0