- Devel - lists.sel4.systems

AARCH64 with CAMKES (Questions)
by Michael DeFrancis 06 Dec '17

06 Dec '17

Can camkes be used with ARM AARCH64? I am attempting to build a linux virtual machine on top of the zynqmp ultrascape+ / sel4 kernel, and using the tk1 vmm project as my reference point. When the build system attempts to generate camkes-gen.mk, it fails - displaying an error indicating that aarch64 is not a valid architecture specification for camkes. I see that valid arm options are aarch32 or arm_hyp. Is arm_hyp what I am looking for here? What would I need to do in order to strip the camkes dependencies out of the tk1 vmm project? Thanks, Mike D Computer Security Engineer - Intelligent Automation, Inc. (301)294-5263 ________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.

3 3

UEFI support for x86
by Edward Sandberg 05 Dec '17

05 Dec '17

Is there a plan to add UEFI support in seL4 for x86 hardware in the near future? Newer x86 boards are frequently UEFI only. It is possible to get around the lack of UEFI support, as I have done with the UP board: https://up-community.org/wiki/Hardware_Specification but I am hitting problems which I will detail below. When I compile using ia32_debug_xml_defconfig and boot using the resulting images the board fails to find the RSDP location. To fix this I had to modify the source code a bit: * seL4test/projects/util_libs/libplatsupport/src/plat/pc99/acpi/acpi.h + #define UPBOARD_RSDP 0x5B161000 * seL4test/projects/util_libs/libplatsupport/src/plat/pc99/acpi/acpi.c - acpi->rsdp = acpi_sig_search(acpi, ACPI_SIG_RSDP, strlen(ACPI_SIG_RSDP), - (void *) BIOS_PADDR_START, (void *) BIOS_PADDR_END); + acpi->rsdp = (void *)UPBOARD_RSDP; * seL4test/kernel/src/plat/pc99/machine/acpi.c - for (addr = (char*)BIOS_PADDR_START; addr < (char*)BIOS_PADDR_END; addr += 16) { + for (addr = (char*)0; addr < (char*)PPTR_BASE; addr += 16) { It would be handy to have this as a kernel parameter to cover cases where it is not successfully discovered automatically. With these changes I can boot the board and several tests pass but then I get stuck on INTERRUPT0001 (Test interrupts with timer). I don't get a test failure or an error the board just sits and makes no more progress. Someone had that test fail in this post: https://sel4.systems/pipermail/devel/2017-February/001328.html and the first recommendation was to check if the irq of the timer was correctly found. I booted the board into linux to find the correct irq which was listed as 0 in /proc/interupts. I added a printf to handleInterrupt in the kernel source, recompiled and when I booted seL4 I found that the irq reported to handleInterrupt is 125 (which sel4 reports as the max interrupt value) every time that function is called. Adding this printf also showed me that when the test hangs the board hasn't crashed or locked up as calls to handleInterrupt are made continuously. At this point I noticed that before any tests started to run several ACPI tables are not recognized: Parsing ACPI tables Skipping table FPDTD, unknown Skipping table FIDT<9c>, unknown Skipping table UEFIB, unknown Skipping table TPM24, unknown Skipping table LPIT^D^A, unknown Skipping table BCFG9^A, unknown Skipping table PRAM0, unknown Skipping table CSRTL^A, unknown Skipping table BCFG9^A, unknown Skipping table OEM0<84>, unknown Skipping table OEM1@, unknown Skipping table PIDVÜ, unknown Skipping table RSCI,, unknown Skipping table WDAT^D^A, unknown Warning: skipping table ACPI XSDT Maybe one or more of those tables needs to be loaded to handle interrupts properly. The LPIT table is conspicuous in the case of the timer test but I think other tests are likely to depend on the other tables. Any suggestions about porting this type of hardware? -- Edward Sandberg Adventium Labs 111 3rd Avenue S. Suite #100 Minneapolis, MN 55401 ed.sandberg(a)adventiumlabs.com

4 10

seL4_Send vs. seL4_Call
by Stefan Wallentowitz 05 Dec '17

05 Dec '17

Hi everyone, I have built a very simple application that loads another process, which is very similar to the tutorials. For testing I wanted to send from the second process to the first one using seL4_Send and observe that the second process never continues after the seL4_Send blocked, despite the receiver called seL4_Recv and got the message. If I call seL4_Call and the receiver does seL4_Recv + seL4_ReplyRecv it works without any other changes to the code. I am wondering if I am understanding something fundamentally wrong and/or what the best strategy to debug this behavior is. Thanks for your help! Cheers, Stefan

2 1

camkes-gen.mk generated prerequisites
by Gordon Clark 01 Dec '17

01 Dec '17

We have a multi component camkes application with each component using a few common services and then having application interfaces to a small number of other components.All these components are imported into a top level system description camkes file. Examining the generated camkes I see that all the generated header and source files have exactly the same make prerequisites meaning a change to logically unrelated components causes them all to be regenerated and recompiled. Now I have discovered the camkes cache this is less of an issue but is there a better way we can structure our application to reduce the edit-compile-go cycle ? Regards Gordon

2 1

seL4SharedData
by Zippy Maniac 30 Nov '17

30 Nov '17

We have a security requirement on our ARM based product using CAmkES 2.2.x to ensure all sensitive data declared in specific seL4SharedData regions are erased on detection of a power failure. We achieve this by overwriting the data with a known pattern that we read back from a separate component before declaring the device as secured. This is working fine. But we need to guarantee that the overwrite data is actually written to DDR and we aren't just using cached values. This means flushing the L1 and L2 data caches specific regions. We could use seL4HardwareMMIO regions and declare our data in the memory map and use these regions as un-cached. Or use the _hardware_cached attribute and call the provided flush method when necessary. Our main issue with doing this, except the fiddle of mapping multiple different sized regions into the memory map, is we could potentially expose the physical locations of the sensitive data rather than having it wrapped in the virtual address space of a component. Having a flush method on seL4SharedData would be the ideal solution. We are not in a position to upgrade our CAmkES version on this product at the moment. Any thoughts? Zippy

4 3

Tx1 UART and GiC distributor PPTR address
by Muneeswaran Rajendran 27 Nov '17

27 Nov '17

Hi, The PPTR address range between UART and GIC distributor was 12k (kernel/include/plat/tx1/plat/machine/device.h). But when refer in TX1 reference sheet the length was specified as 64byte for UART,4k for GIC distributor and 8k for interrupt controller. can you please point out the reference or reason to choose this address for Tx1 board? /* These devices are used by the seL4 kernel. */ #define UARTA_PPTR 0xffffffffffff0000 #define GIC_DISTRIBUTOR_PPTR 0xffffffffffff3000 #define GIC_CONTROLLER_PPTR 0xffffffffffff4000 These addresses are used during kernel device map to access in the userspace map_kernel_devices : kernel_devices[i].paddr :0x50042000 kernel_devices[i].pptr 0xffffffffffff4000 map_kernel_frame - armKSGlobalKernelPT[GET_PT_INDEX(vaddr)]: 0xffffff800002b000 vaddr :0x1f4 map_kernel_devices : kernel_devices[i].paddr :0x50041000 kernel_devices[i].pptr 0xffffffffffff3000 map_kernel_frame - armKSGlobalKernelPT[GET_PT_INDEX(vaddr)]: 0xffffff800002b000 vaddr :0x1f3 map_kernel_devices : kernel_devices[i].paddr :0x70006000 kernel_devices[i].pptr 0xffffffffffff0000 map_kernel_frame - armKSGlobalKernelPT[GET_PT_INDEX(vaddr)]: 0xffffff800002b000 vaddr :0x1f0 Regards, Munees

1 0

Caught cap fault in send phase at address 0x0 @Tx2
by Muneeswaran Rajendran 23 Nov '17

23 Nov '17

Hi seL4 Dev Team, I am bringing up the sel4 kernel on tx2 board with ref of Tx1. I encountered the TLB invalidation hang issue after kernel map window setup. I do not know the exact reason for hang so just disable that piece of code to look further execution of sel4 kernel. After that it dropped into the usersapce and throwing the cap fault or vm fault issue. Does anyone has come across this type of issue and how it debugged?. Please share your thought or pointers to debug this issue. I shared the full log details here. ## Starting application at 0x82000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A57 r1p3 paddr=[82000000..827abfff] kernel_phys_start: 0xffffffff80000000 kernel_phys_end:0xffffffff8022fcdf load_elf : image_size 0x230000 ELF-loading image 'kernel' paddr=[80000000..8022ffff] vaddr=[ffffff8000000000..ffffff800022ffff] virt_entry=ffffff8000000000 load_elf : image_size 0x5e9000 ELF-loading image 'sel4test-driver' paddr=[80230000..80818fff] vaddr=[400000..9e8fff] virt_entry=41b160 Enabling MMU and paging Jumping to kernel-image entry point... kernel_info.virt_entry : 0x0 user_info.phys_region_start : 0xffffffff80230000 user_info.phys_region_end:0xffffffff80819000 user_info.virt_region_start:0x400000 user_info.virt_region_end:0x9e9000 user_info.phys_virt_offset:0x7fe30000 user_info.virt_entry:0x41b160 Bootstrapping kernel Booting all finished, dropped to user space Caught cap fault in send phase at address 0x0 while trying to handle: vm fault on code at address 0x41b160 with status 0x82000010 in thread 0xffffff8027ef4200 "rootserver" at address 0x41b160 With stack: halting... Kernel entry via VM Fault, fault type: 4305248 Thanks in advance Muneeswaran R

1 0

Tx1 SMP and Hypervisor support
by Muneeswaran Rajendran 17 Nov '17

17 Nov '17

Hi Sel4 Dev Team, Any update of SMP and Hypervisor feature which fully functional on TX2. If its not available when will get this feature supported . Regards, Munees

3 4

1:1 Mapping of Zynqmp devices
by Chris Guikema 16 Nov '17

16 Nov '17

Hello, I am attempting to port the camkes-arm-vm to the zynqmp platform. For the TK1 and Exynos platforms, the physical address of the hardware devices are well below the kernelBase of 0xe0000000. However, for the zynqmp, these hardware devices are greater than the kernel base. This causes the "map_emulated_device" function call to fail for the GIC and any other passthrough devices. sel4utils_reserve_range_at_no_alloc@vspace.c:589 Range not available at 0xff010000, size 0x1000 Assertion failed: res.res (/home/chrisguikema/seL4/NAMC/camkes-arm-vm/libs/libsel4arm-vmm/src/devices.c: map_device: 160) Is there a way to 1:1 map these devices, even if they are above the kernelBase? Thanks, Chris

2 1

loading and booting seL4 on a tegra Tx2
by Muneeswaran Rajendran 15 Nov '17

15 Nov '17

Hi, I am trying to bring up sel4 on tegra Tx2 platform using tegra Tx1 as reference. I tweaked the important changes of UART,Timer configuration and IRQ number and also GIC controller, GIC distributor configuration w.r.t Tx2 after loading and booting the Tx2 board sel4 enter into init kernel to initialize the kerenl memory map for GIC and UART devices then control transfer to user space. I underdtand from ref manual both Tx1 and Tx2 using the same clock and baud rate for UART configuration. ## Starting application at 0x82000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A57 r1p3 paddr=[82000000..827abfff] kernel_phys_start: 0xffffffff80000000 kernel_phys_end:0xffffffff8022fcdf load_elf : image_size 0x230000 ELF-loading image 'kernel' paddr=[80000000..8022ffff] vaddr=[ffffff8000000000..ffffff800022ffff] virt_entry=ffffff8000000000 load_elf : image_size 0x5e9000 ELF-loading image 'sel4test-driver' paddr=[80230000..80818fff] vaddr=[400000..9e8fff] virt_entry=41b160 Enabling MMU and paging Jumping to kernel-image entry point... Also try to add debug print in the init kernel thread to understand the virtual memory set-up but its crashed with synchronous exception. It indicates that the UART driver till not available to log the messages this was seen in Tx1 and Tx2. Not able to check/debug further on this issue. Also experimented with various arbitrary address for UARTA_PPTR and GIC_PPTR because Tx1 UARTA has 64byte size in case of Tx2 its 1MB.but still nothing has improved the state remain same. I completely walk through the sel4 boot and arm MMU code.I do not see any board specific changes in this code apart from UART,GIC configuration and IRQ number. The assembly code of MMU mainly setting up TCR ,TTBR , TLB invalidation and pagetable setup for arma-57. Please let me know your thought on this issue and how do debug this kind of issue. Regards, Munees

2 2

loading and booting seL4test on a zynq7000
by Joel Svensson 13 Nov '17

13 Nov '17

Hello, I want to learn about seL4 so I am trying to get is started on the hardware I already have (a zynq 7000). I have generated the image: sel4test-driver-image-arm-zynq7000 Now I try to load that onto the zynq by executing these commands in XMD: connect arm hw rst fpga -f design_1_wrapper.bit source ps7_init.tcl ps7_init ps7_post_config dow sel4test-driver-image-arm-zynq7000 run All of the above seem to be successful. Then, I have a serial link hooked up to the board (uart) and there I get the following output (screen /dev/ttyUSB1 115200) : ELF-loader started on CPU: ARM Ltd. Cortex-A9 r3p0 paddr=[10000000..103c881f] ELF-loading image 'kernel' paddr=[0..2afff] vaddr=[e0000000..e002afff] virt_entry=e0000000 But then nothing more. I am lost what to do from this position in order to continue exploring seL4. I don't even know if what I see is an indication of a problem or not. If anyone has experience in running seL4 on zynq and if you sit on knowledge you want to share, please fill me in. Thank you

2 6

CAmkES mutex Question
by Brandon, Jeffrey - 0553 - MITLL 06 Nov '17

06 Nov '17

Hi, I've been taking a look at mutex implementations in the camkes-app example and I had a question. In the mutex example here https://github.com/seL4/camkes/tree/master/apps/mutex suppose I wanted to extend to add a third component C I need to add the corresponding camkes, source, Kbuild, and Kconfig files and then I need to add connections to the master mutex.camkes file correct? My first intuition was to add a connector: Assembly { Composition{ . Connection seL4MyConnector connection(from c.lock, to b.lock); . } } But this yields and error saying something to the effect "seL4MyConnector expects one from endpoint and two are specified" To remedy this I added another lock component to B, and made a connection between C and this new lock B provides. The new lock being implemented by the same template. My Questions: In this scenario do A B and C still have access to the same mutex? If A has a lock on the mutex, then C requests a lock, will this cause A to be unable to release the lock? In my mental model I have three threads of control, one each for A B and C, if A has a lock and then C requests a lock, does this block B (when it receives a message from C and is now blocked on requesting the mutex)? Then when A tries to release, B is blocked and cannot release the mutex on A's behalf. To put it another way, does this mutex example rely on B having direct access to the templated code and there only being two components? Secondarily, in the lockserver example https://github.com/seL4/camkes/tree/master/apps/lockserver a situation is presented where three clients access a single mutex through a single server. Would there be an issue if one of the clients also acted as the server? So for instance if A implemented the three pairs of lock unlock functions instead of the server and then B and C used seL4RPCCall connections to A in order to access them, would there be any synchronization issues? I'm relatively new to this and am trying to build a system with the help of camkes and I want to make sure I understand this before I get too far. I don't want to be working under incorrect assumptions. Thanks for taking the time to read this. Sincerely, Jeff Brandon Associate Staff MIT Lincoln Laboratory Secure Resilient Systems and Technology Ph: +1 781.981.9233

3 2

PPTR address computation on Sel4 Kernel
by Muneeswaran Rajendran 05 Nov '17

05 Nov '17

Hi sel4 development team, I understand from the sel4 kernel the paddr and pptr used in the kernel framework to compute the page table entry. I found from ref manual GICD_PADDR defined as (ARM_PERIPHBASE (0x50040000) + 0x1000) 0x50041000 for that GIC_DISTRIBUTOR_PPTR used as 0xffffffffffff3000. This details was not able to see in the ref manual and other sel4 reference. Can someone help to understand the pptr calculation w.r.t sel4? Thanks in advance Munees

2 1

UART initialisation on seL4 @TX1
by Muneeswaran Rajendran 03 Nov '17

03 Nov '17

Hi sel4 development team, I understand from the seL4 kernel the initial printf message are not routed through sel4 platform uart driver. Because the sel4 UART driver initialisation happened later when seL4 Main kernel initialization is finished. till then sel4 kernel uses u-boot UART driver to route the message. This interpretation is correct as per my understanding. Also mentioned in code as well debug output available via serial interface after kernel init thread started. /* debug output via serial port is only available from here */ printf("Bootstrapping kernel\n"); It means that when sel4 kernel comes up with u-boot uart driver and then later using sel4 uart driver. Please correct me if any thing wrong here and throw some input. Regards, Munees

2 2

Re: [seL4] Devel Digest, Vol 41, Issue 33
by ashokk＠spanidea.com 01 Nov '17

01 Nov '17

Hi Kofi, I tried with go command, but it is not working, board is getting hang... U-boot> go 0x10000000## Starting application at 0x10000000 ... after these i am not able to access the board, i need to reset again... Thanks & RegardsAshok From: "devel-request(a)sel4.systems" <devel-request(a)sel4.systems> To: devel(a)sel4.systems Sent: Monday, 30 October 2017 11:54 PM Subject: Devel Digest, Vol 41, Issue 33 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: Devel Digest, Vol 41, Issue 31 (Kofidoku.Atuah(a)data61.csiro.au) ---------------------------------------------------------------------- Message: 1 Date: Sun, 29 Oct 2017 23:56:03 +0000 From: <Kofidoku.Atuah(a)data61.csiro.au> To: <devel(a)sel4.systems> Subject: Re: [seL4] Devel Digest, Vol 41, Issue 31 Message-ID: <1509321363766.62194(a)data61.csiro.au> Content-Type: text/plain; charset="iso-8859-1" Hi Ashokk, I believe if you replace the command, "bootelf 0x10000000" with "go 0x10000000", That should be all that's needed to boot a raw binary image -- lemme know how things go though~ -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO

1 0

Re: [seL4] Devel Digest, Vol 41, Issue 31
by ashokk＠spanidea.com 30 Oct '17

30 Oct '17

Hi Kofi, Thanks for the steps, i am able to load sel4test-driver-image-arm-bcm2837 on RPI3. but my question is i generated a sel4test-driver-image-arm-bcm2837.bin(binary image) for RPI3 i want to load these image on RPI3, can you help me out to load these image on RPI3... Hardware/Rpi3 - seL4Wiki these steps are used to load elf image on RPI3.... but i want to load binary image on RPI3... | | | Hardware/Rpi3 - seL4Wiki | | | Thanks and Regards Ashokkumar From: "devel-request(a)sel4.systems" <devel-request(a)sel4.systems> To: devel(a)sel4.systems Sent: Thursday, 26 October 2017 8:48 PM Subject: Devel Digest, Vol 41, Issue 31 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: Loading bin image on RPI3(Remainder) (Kofidoku.Atuah(a)data61.csiro.au) ---------------------------------------------------------------------- Message: 1 Date: Thu, 26 Oct 2017 03:23:06 +0000 From: <Kofidoku.Atuah(a)data61.csiro.au> To: <devel(a)sel4.systems> Subject: Re: [seL4] Loading bin image on RPI3(Remainder) Message-ID: <1508988186794.61071(a)data61.csiro.au> Content-Type: text/plain; charset="iso-8859-1" Hi Ashokk, Thanks for pointing this issue out, and sorry I took so long to get back to you -- I've investigated and come up with a workaround until we can fix the underlying caching problem here: could you try following the instructions on this page? https://wiki.sel4.systems/Hardware/Rpi3#preview There should be a pre-built U-Boot binary image there which should successfully load your seL4 kernel image. Please let me know how things go~ -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO

2 1

Re: [seL4] Loading bin image on RPI3(Remainder)
by Kofidoku.Atuah＠data61.csiro.au 26 Oct '17

26 Oct '17

Hi Ashokk, Thanks for pointing this issue out, and sorry I took so long to get back to you -- I've investigated and come up with a workaround until we can fix the underlying caching problem here: could you try following the instructions on this page? https://wiki.sel4.systems/Hardware/Rpi3#preview There should be a pre-built U-Boot binary image there which should successfully load your seL4 kernel image. Please let me know how things go~ -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO

1 0

Some guidance when using AutoCorres.
by Dan DaCosta 25 Oct '17

25 Oct '17

seL4 Developers: Consider the following c structure declarations: struct foo_struct{ uint16_t subfield; }; struct bar_struct{ struct foo foo; }; I am wondering if anyone has any suggestions on how I might go about proving something like this: s[Ptr &(bar→[''foo_C'']) := subfield_C_update (λ_. b) (heap_MissionCommand_struct_C s (Ptr &(bar→[''foo_C''])))] = s[Ptr &(bar→[''missioncommand_C''])→subfield := b] where s of type lifted_globals, bar is of type foo_struct_C, and b is of type word16. I *think* it should be provable, i.e., "updating all of the foo field with a copy of what was there originally modulo some change to subfield is equivalent to making that change directly to the subfield." I apologize in for taking this "into the weeds" but some of the definitions being used are buried in the AutoCorres translation and I am unsure how to make my question more abstract. Thanks in Advance! Dan DaCosta

3 2

Booting seL4 in bbb (beaglebone black)
by Sathish Kumar Balasubramaniam -ERS, HCL Tech 25 Oct '17

25 Oct '17

I tried booting sel4test in bbb. but i got the following after u-boot. Any idea for this crash ? U-Boot# echo $loadaddr 0x82000000 U-Boot# fatload mmc 0 ${loadaddr} sel4test.bin reading sel4test.bin 4108544 bytes read in 245 ms (16 MiB/s) U-Boot# go ${loadaddr} ## Starting application at 0x82000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A8 r3p2 paddr=[82000000..823fc81f] ELF-loading image 'kernel' paddr=[80000000..80036fff] vaddr=[f0000000..f0036fff] virt_entry=f0000000 ELF-loading image 'sel4test-driver' paddr=[80037000..80514fff] vaddr=[8000..4e5fff] virt_entry=21c9c Enabling MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Booting all finished, dropped to user space Caught cap fault in send phase at address 0x0 while trying to handle: unknown syscall 0xf0005 in thread 0xf7fec500 "rootserver" at address 0x18b60 With stack: 0x3d88a0: 0x84ac 0x3d88a4: 0x1711c 0x3d88a8: 0x46c0f 0x3d88ac: 0x0 0x3d88b0: 0x84ac 0x3d88b4: 0x172cc 0x3d88b8: 0x3e5224 0x3d88bc: 0x46c0f 0x3d88c0: 0x84ac 0x3d88c4: 0xecfc 0x3d88c8: 0x31 0x3d88cc: 0x0 0x3d88d0: 0x0 0x3d88d4: 0x0 0x3d88d8: 0x0 0x3d88dc: 0x0 ::DISCLAIMER:: ---------------------------------------------------------------------------------------------------------------------------------------------------- The contents of this e-mail and any attachment(s) are confidential and intended for the named recipient(s) only. E-mail transmission is not guaranteed to be secure or error-free as information could be intercepted, corrupted, lost, destroyed, arrive late or incomplete, or may contain viruses in transmission. The e mail and its contents (with or without referred errors) shall therefore not attach any liability on the originator or HCL or its affiliates. Views or opinions, if any, presented in this email are solely those of the author and may not necessarily reflect the views or opinions of HCL or its affiliates. Any form of reproduction, dissemination, copying, disclosure, modification, distribution and / or publication of this message without the prior written consent of authorized representative of HCL is strictly prohibited. If you have received this email in error please delete it and notify the sender immediately. Before opening any email and/or attachments, please check them for viruses and other defects. ----------------------------------------------------------------------------------------------------------------------------------------------------

2 2

Re: [seL4] sel4Test development Tx1 platform
by Kofidoku.Atuah＠data61.csiro.au 24 Oct '17

24 Oct '17

Hi Munees, I went through some methods for how to boot the seL4 kernel on a stock TX1 board yesterday and wrote this guide: https://wiki.sel4.systems/Hardware/jetsontx1 It goes through the steps for getting seL4 booted using an SD Card, the internal 15GiB mass storage on the TX1, or using a USB cable and the DFU protocol.? DFU is probably a lot faster/better for you f you're doing active development. Could you try one of these methods and let me know if any of them works for you? -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO

2 1

Loading bin image on RPI3(Remainder)
by ashokk＠spanidea.com 23 Oct '17

23 Oct '17

Hi all, I built a bin image from sel4test (https://github.com/seL4/sel4test).I am trying to load .bin image on RPI-3, but it's failing. I am following below steps... U-Boot> fatload mmc 0 0x00200000 kernel.binreading kernel.bin2108096 bytes read in 329 ms (6.1 MiB/s)U-Boot> go 0x00200000## Starting application at 0x00200000 ... i got stuck here... Along with this i also tried with two another methods but facing same issue..METHOD-1 :-==========U-Boot> fatload mmc 0 0x00200000 kernel.binreading kernel.bin2108096 bytes read in 330 ms (6.1 MiB/s)U-Boot> loadb 0x00200000 115200## Ready for binary (kermit) download to 0x00200000 at 115200 bps..U-Boot> load mmc 0:1 0x00200000 kernel.bin2108096 bytes read in 330 ms (6.1 MiB/s)U-Boot> go 0x00200000## Starting application at 0x00200000 ...METHOD-2:- ===========U-Boot> load mmc 0:1 0x00200000 kernel.binreading kernel.bin2108096 bytes read in 330 ms (6.1 MiB/s)U-Boot> go 0x00200000## Starting application at 0x00200000 ... please guide me through this issue, i wanted to load kernel.bin(sel4test-driver-image-arm-bcm2837.bin) file on RPI-3.... RegardsAshok

1 0

Questions on seL4's scheduling
by Norrathep Rattanavipanon 21 Oct '17

21 Oct '17

Hello, I have a few questions about seL4's scheduling model in the main (formally verified) branch. 1) I see the time slice parameter in make menuconfig. Is that where I can change the scheduler's time slice correct? And the unit is in timer tick period I suppose? 2) I kind of remember the discussion we had that if an interrupt handler has lower priority than the currently running task, then the interrupt wouldnt happen. So what if both of them have the same priority, would the kernel schedule the currently running task until it uses up all of its timeslice, then issues the interrupt notification or would the interrupting process get executed right away? Best Regards, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

4 11

64 bit ARM ELF image load in Tx1 platform
by Muneeswaran Rajendran 18 Oct '17

18 Oct '17

Hi All, I have been trying to load 64bit seL4 (kernel+user space) ELF image on Tx1 board but it's failed to start the application and crashed with reason '"Synchronous Abort" handler, esr 0x02000000' always. Just walk through the Tx1 u-boot code and found that 'load_elf_image_phdr(unsigned long addr)' is using 32bit ELF header structure pointer to load the program header. I would like to understand whether 64bit ELF image load handled using 32bit elf header itself or we need to configure u-boot to load 64 bit ELF image ? I have modified the kernel base addr as 0xffffffc000080000 and phyadd as 0x80080000 to boot sel4 app image on TX1 board nothing has worked out. Please share details if someone succeeded to bring sel4 app elf image on Tx1 platform. Regards, Munees

4 5

Loading bin image on RPI3
by ashokk＠spanidea.com 17 Oct '17

17 Oct '17

Hi, I am trying to load .bin image on RPI-3, but i am not able to do that one i am following below steps... U-Boot> fatload mmc 0 0x00200000 kernel.binreading kernel.bin2108096 bytes read in 329 ms (6.1 MiB/s)U-Boot> go 0x00200000## Starting application at 0x00200000 ... i got stuck... Along with this i also tried with two another methods but facing same issue..METHOD-1 U-Boot> fatload mmc 0 0x00200000 kernel.binreading kernel.bin2108096 bytes read in 330 ms (6.1 MiB/s)U-Boot> loadb 0x00200000 115200## Ready for binary (kermit) download to 0x00200000 at 115200 bps..U-Boot> load mmc 0:1 0x00200000 kernel.binreading kernel.bin2108096 bytes read in 330 ms (6.1 MiB/s)U-Boot> go 0x00200000## Starting application at 0x00200000 ... METHOD-2 U-Boot> load mmc 0:1 0x00200000 kernel.binreading kernel.bin2108096 bytes read in 330 ms (6.1 MiB/s)U-Boot> go 0x00200000## Starting application at 0x00200000 ... please guide me through this issue, i wanted to load sel4test.bin(sel4test-driver-image-arm-bcm2837.bin) file on RPI-3.... RegardsAshok

1 0

sel4Test development Tx1 platform
by Muneeswaran Rajendran 14 Oct '17

14 Oct '17

Hi All I able to build sel4Test driver for TX1 platform. but the final outputimage is not a executable image it shows as data format :~/sel4Test$ file images/sel4test-driver-image-arm-tx1.bin images/sel4test-driver-image-arm-tx1.bin: data used 'aarch64-linux-gnu-' toolchain for cross compilation. but in the kernel obj shows as 64 bit ARM aarch64 format. ~/sel4Test$ file build/kernel/kernel.o build/kernel/kernel.o: ELF 64-bit LSB relocatable, ARM aarch64, version 1 (SYSV), not stripped And cross checked in the tk1 platform the generated output file as exe file format. ~/sel4Test$ file images/sel4test-driver-image-arm-tk1 images/sel4test-driver-image-arm-tk1: ELF 32-bit LSB executable, ARM, EABI5 version 1 (SYSV), statically linked, stripped Can you please someone help me to get final out image as executable format. Also share the procedure to load the sel4Test driver on TX1 board to verify the test. Thanks in advance Munees

3 6

does seL4 support NVIDIA Jetson Tx2 board ?
by ashokk＠spanidea.com 13 Oct '17

13 Oct '17

Hi , I am newbie to sel4 and currently working on one hobby project.I want to bring sel4 kernel on TX2 board. Can you guide me that is there any support available for tx2 for . If yes then provide some docs related to that. Thank you.

5 9

Re: [seL4] Devel Digest, Vol 41, Issue 11
by ashokk＠spanidea.com 11 Oct '17

11 Oct '17

Hi, I am going through the SEL4 userspace code of UART driver for TX1/TK1 board but i have some doubts in the below given link..https://github.com/seL4/util_libs/blob/master/libplatsupport/mach_inc… In serial.h file they are defining IRQ numbers #define UARTA_IRQ 68 #define UARTB_IRQ 69 #define UARTC_IRQ 78 #define UARTD_IRQ 122 I am not able to find the above IRQ numbers in TX1/TK1 datasheet...can you please point out where they are referring these IRQ numbers(68, 69, 78, 122)... RegardsAshok From: "devel-request(a)sel4.systems" <devel-request(a)sel4.systems> To: devel(a)sel4.systems Sent: Tuesday, 10 October 2017 6:31 AM Subject: Devel Digest, Vol 41, Issue 11 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: TX1 user-space drivers (Kofidoku.Atuah(a)data61.csiro.au) 2. Re: sel4Test development Tx1 platform (Kofidoku.Atuah(a)data61.csiro.au) ---------------------------------------------------------------------- Message: 1 Date: Mon, 9 Oct 2017 23:32:17 +0000 From: <Kofidoku.Atuah(a)data61.csiro.au> To: <devel(a)sel4.systems> Subject: Re: [seL4] TX1 user-space drivers Message-ID: <1507591937169.95333(a)data61.csiro.au> Content-Type: text/plain; charset="iso-8859-1" Munees, I'm fairly sure that the TX1 can use the UART driver in there, since we have that driver in regression, being tested almost daily on a TX1 board -- that driver is the one used by seL4test on the TX1 in this test here: https://github.com/seL4/sel4test/blob/master/apps/sel4test-tests/src/tests/… You also asked whether you have to migrate anything to the TX1. To my knowledge, no, because the TX1 is already running in regression internally, and that UART driver I linked you to is used by the TX1 port with no modifications. As for your question about the TX2, I cannot comment on whether or not the TX2 works the same as the TX1 because I have no experience with the TX2, since we do not have this board internally, and because seL4 does not officially support the TX2. If you want to port seL4 to the TX2, it would require some effort in figuring out what the differences between the TX1 and TX2 are, as far as I can tell :) -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO

2 1

TX1 user-space drivers
by ashokk＠spanidea.com 10 Oct '17

10 Oct '17

Hi, I am trying write UART driver in SEL4 user-space driver for TX1 board.Shall i get any reference(docs or ref.code) to write these driver.. Thanks & RegardsAshok

3 3

SMP on Zynq7000 zc702
by Jesse Millwood 05 Oct '17

05 Oct '17

Hello, I realize that the only officially supported SMP platform is the i.mx6 but I did see some code on 6.0 to master for SMP and the zynq7000 so I am trying to test out some SMP functionality on my zc702 board. I am wondering if anyone has this working because my system is failing when compiling from master and the 6.0 and compatible tags. My second core seems to be coming up but the system ultimately fails and prints out: Bo ot nKgE RaNlEl L fDinAiTsAh eAdBO, RdT!r ppFaeud lttio nugs eirn stspraucctei o n: 0xe001d1b0 o FAR: 0xfffffff8 DFSR: 0x807 halting... Kernel entry via Syscall, number: 1, Call Cap type: 1, Invocation tag: 37 Which seems to be "Booting all finished, dropped to user space" from core0 and "KERNEL DATA ABORT!" from core1. The "0xe001d1b0" seems to be the label of the "idle_thread" function. While stepping through via JTAG, I have verified that core1 gets through "init_kernel" and then enters "restore_user_context" at some point in "restore_user_context" the fault registers as shown in the printed output are set. I think it is either in the c_exit_hook in restore_user_context or after the program branches to "0xFFF0010" which is "ldr pc,0xFFFF0030". This branches to the "arm_data_abort_exception" label, which goes to "kernel_data_fault" label and then to "kernel data abort". I'm having trouble exactly pin pointing where the fault occurs but it seems to be close to there. Has anyone had similar issues with SMP? It seems to get fairly far without setting the fault registers. I have tried to step through the execution over JTAG and here are some of my (verbose) notes | CORE0 Address | Core0 Function | Core0 Instruction | CORE1 Address | Core1 Function | Core1 Instruction | DFSR | DFAR | Note | |---------------+-----------------------------+------------------------+---------------+------------------------------------+----------------------+------------+------------+------| | 0x10000000 | label: start | =cpsid aif= | 0xFFFFFF34 | | =mvn r0,#0x0f= | 0x00000000 | 0x00005000 | | | 0x10003A2C | call: platform_init | =bl -x10003DD8= | 0xFFFFFF30 | | =wfe= | 0x00000000 | 0x00005000 | | | 0x10003ACC | call: smp_boot | =bl 0x100039FC= | 0xFFFFFF34 | | =mvn r0,#0x0f= | 0x00000000 | 0x00005000 | | | 0x10003ADO | ret: smp_boot | =bl 0x10005C54= | 0x10000020 | in: non_boot_core | =orr r0,r0,#0x40= | 0x00000000 | 0x00005000 | 2 | | 0x10003ADC | =if(is_hyp_mode())= | =beq 0x10003AF0= | 0x10002200 | label: arm_disable_dcaches | =push {r14}= | 0x00000000 | 0x00005000 | | | 0x10003AFC | call: arm_enable_mmu | =bl 0x10002174= | 0xE0006190 | in: try_init_kernel_secondary_core | =beq 0xE0001680= | 0x00000000 | 0x00005000 | 1 | | 0xE0001D70 | label: init_kernel | =push {r11,r14}= | 0xE0001680 | in: try_init_kernel_secondary_core | =beq 0xE0001680= | 0x00000000 | 0x00005000 | 1 | | 0xE0001814 | label: try_init_kernel | =push {r11,r14}= | 0xE0001690 | in: try_init_kernel_secondary_core | =beq 0xE0001680= | 0x00000000 | 0x00005000 | 1 | | 0xE0001B80 | call: create_initial_thread | =str r0, [r11,#-0x14]= | 0xE0001680 | in: try_init_kernel_secondary_core | =beq 0xE0001680= | 0x00000000 | 0x00005000 | 1 | | 0xE0001C48 | call: SMP_COND_STATEMENT | =bl 0xE0003C20= | 0xE0001680 | in: try_init_kernel_secondary_core | =beq 0xE0001680= | 0x00000000 | 0x00005000 | 1, 3 | | 0xE0001C4C | call: SMP_COND_STATEMENT | =bl 0xE00017D8= | 0xE0001680 | in: try_init_kernel_secondary_core | =beq 0xE0001680= | 0x00000000 | 0x00005000 | 1, 4 | | 0xE0001C50 | NODE_LOCK_SYS | =bl 0xE0019280= | 0xE0019288 | in: getCurrentCPUIndex | =sub r13,r13,#0x8= | 0x00000000 | 0x00005000 | 5 | | 0xE0001D1C | call: arch_pause | =bl 0xE0019DB0= | 0xE0019290 | in: getCurrentCPUIndex | =str r0,[r11,#-0x8]= | 0x00000000 | 0x00005000 | 6 | | 0xE0001D40 | in: clh_lock_acquire | =uxtb r3,r3= | 0xE00037F4 | in: init_core_state | =pop {r4,r11,pc}= | 0x00000000 | 0x00005000 | | | 0xE0001D20 | in: clh_lock_acquire | =mov r2,#0xE800= | 0xE0003754 | in: init_core_state | =movw r2,#0xE8E0= | 0x00000000 | 0x00005000 | 7 | | 0xE0001D40 | in: clh_lock_acquire | =uxtb r3,r3= | 0xE00017C4 | in: try_init_kernel_secondary | =mov r3,#0x1= | 0x00000000 | 0x00005000 | 8 | | 0xE0001D40 | in: clh_lock_acquire | =uxtb r3,r3= | 0xE002A06C | in: schedule | =push {r11,r14}= | 0x00000000 | 0x00005000 | 9 | | 0xE0001D40 | in: clh_lock_acquire | =uxtb r3,r3= | 0xE002979C | in: activateThread | =push {r11, r14}= | 0x00000000 | 0x00005000 | 10 | | 0xE0001D40 | in: clh_lock_acquire | =uxtb r3,r3= | 0xE001D24C | label: Arch_activateIdleThread | =push {r11}= | 0x00000000 | 0x00005000 | 11 | | 0xE0001D38 | in: clh_lock_acquire | =ldr r3,[r3,#0x4]= | 0xE0000054 | in: start | =b 0xE001CEC8= | 0x00000000 | 0x00005000 | 12 | Notes 1. Core1 is in a =while (!node_boot_lock)= loop 2. In =smp_boot=, CORE1 changes after =init_cpus= (branch location: ZSR:10003A08) - In =smp_boot=, =boot_cpus= is called - This sets the =CPU_JUMP_PTR= =*((volatile uint32_t*)CPU_JUMP_PTR) = (uint32_t)entry;= - calls =dsb= (data synchronization barrier) - After this call, CPU1 goes to =FFFFFF2C: dsb sy= - And then =sev= - After this call, CPU1 goes to the =non_boot_core= label - SEV - SEV causes an event to be signaled to all cores within a multiprocessor system. If SEV is implemented, WFE must also be implemented. - WFE - If the Event Register is not set, WFE suspends execution until one of the following events occurs: - an IRQ interrupt, unless masked by the CPSR I-bit - an FIQ interrupt, unless masked by the CPSR F-bit - an Imprecise Data abort, unless masked by the CPSR A-bit - a Debug Entry request, if Debug is enabled - an Event signaled by another processor using the SEV instruction. - If the Event Register is set, WFE clears it and returns immediately. - If WFE is implemented, SEV must also be implemented. - After CPU0 executes =arm_enable_mmu()= from the =main= function - by the end of =smp_boot= core1 is just starting =non_boot_main= 3. The =SMP_COND_STATEMENT= is calling =clh_lock_init= 4. The =SMP_COND_STATEMENT= is calling =release_secondary_cpus= 5. right after Core0 returned from releasing secondary cpus - First time Core1 has exited the loop - Core1's stack is - =getCurrentCPUINdex= - =init_core_state= - =try_init_kernel_secondary_core= - =init_kernel= 6. Core0 is in a =while(big_kernel_lock.node_owners[cpu].next->value ! = CLHState_Granted)= - Core0 is in a static inline function =clh_lock_acquire= in =try_init_kernel= - Core1 is in =getCurrentCPUIndex= but being called from =tcbDebugAppend= - =tcbDebugAppend= is being called from a =for= loop in =init_core_state= 7. Core0 is still in the previously mentioned while loop - Core1 is in "init_core_state" and has exited the for loop that called =tcbDebugAppend(NODE_STATE_ON_CORE(ksIdleThread, i))= 8. Core0 is still in the previously mentioned while loop - Core1 has returned to =try_init_kernel_secondary_core= from =init_core_state= and is at the end of the function 9. Core0 is still in the previously mentioned while loop - Core1 has entered the =init_kernel= call and then the =schedule= function. 10. Core0 is still in the previously mentioned while loop - Core1 has entered the =activateThread= call after =schedule= in =init_kernel= 11. Core0 is still in the previously mentioned while loop - Core1 seems to have dropped into the =case ThreadState_IdleThreadState:= case when switching on =switch (thread_state_get_tsType(NODE_STATE(ksCurThread)->tcbState))= - This was in =activateThread= 12. Core0 is still in the previously mentioned while loop - Core1 has exited =init_kernel= and is now branching to =restore_user_context= To test everything out I am using the "camkes-sols-master" manifest and building the "CAmkES Hello World application with events and dataports". The changes I made are * I edited the top level CAmkES file to set the affinity for two separate cores. * Upped the Max Number of CPU nodes to 2 The rest of the config is pretty standard. I have it attached to this message. The FSBL and ps7_init script I use are the standard ones created for the zc702 from the 2017.2 version of the Xilinx XSDK. I am booting from jtag and first run the ps7_init script and then flash the fsbl and then the "capdl-loader-experimental-image-arm-zynq7000" that was built. I am wondering if anyone is using a modified fsbl or ps7_init that does something else, if there is config value that I missed, or if it is still in development? If it is still in development I'd like to work with whoever is Thanks, Jesse Millwood

3 4

Question about IO ports in CAmKES
by John Backes 05 Oct '17

05 Oct '17

I have a question about the Real-time Clock component (RTC) for the x86 VMM found here: https://github.com/SEL4PROJ/global-components/blob/master/components/RTC/RT… Here is the text of the camkes file: import <RTC.idl4>; import <PutChar.idl4>; component CMOS { hardware; provides IOPort cmos_address; provides IOPort cmos_data; attribute string cmos_address_attributes = "0x70:0x70"; attribute string cmos_data_attributes = "0x71:0x71"; } component RTC { provides RTC rtc; maybe uses PutChar putchar; uses IOPort cmos_address; uses IOPort cmos_data; attribute int heap_size = 0; /* Connect the hardware RTC to the RTC component */ composition { component CMOS cmos; connection seL4HardwareIOPort rtc_cmos_address(from cmos_address, to cmos.cmos_address); connection seL4HardwareIOPort rtc_cmos_data(from cmos_data, to cmos.cmos_data); } configuration { cmos.cmos_address_attributes <- cmos_address_attributes; cmos.cmos_data_attributes <- cmos_data_attributes; } } What is the meaning of the last two statements in the configuration block? what is the scoping rules for the "cmos_address_attributes" and "cmos_data_attributes" variables? It looks like these attributes are already set in the definition of the CMOS component? They seemed to be assigned again in the configuration block? - John

2 2

SEL4 on Rasperry pi 3
by ashokk＠spanidea.com 04 Oct '17

04 Oct '17

Hi, I successfully compiled and run sel4 image for rasperry pi 3. while running it successfully passes all the tests,then it stopped now what? I need to bring sel4 kernel on top of rasperry pi 3... do you guys have any idea or links please share with me.. i am following below link..https://research.csiro.au/tsblog/sel4-raspberry-pi-3/ RegardsAshok

2 1

Re: [seL4] seL4 website down
by Mike Clark 03 Oct '17

03 Oct '17

Yes, it appears to be down. Mike On Oct 2, 2017 12:39 PM, <keith(a)matellio.com> wrote: Is it just me or is everyone having trouble accessing the seL4 website? I’m getting the following: MOD_PYTHON ERROR ProcessId: 29222 Interpreter: 'sel4.systems.keg.ertos.in.nicta.com.au' ServerName: 'sel4.systems.keg.ertos.in.nicta.com.au' DocumentRoot: '/var/www/seL4/content' URI: '/Community/mailman/home.pml' Location: '/Community' Directory: None Filename: '/var/www/seL4/content/Community/mailman/home.pml' PathInfo: None Phase: 'PythonHandler' Handler: 'ertos' Traceback (most recent call last): File "/usr/lib/python2.7/dist-packages/mod_python/importer.py", line 1537, in HandlerDispatch default=default_handler, arg=req, silent=hlist.silent) File "/usr/lib/python2.7/dist-packages/mod_python/importer.py", line 1202, in _process_target module = import_module(module_name, path=path) File "/usr/lib/python2.7/dist-packages/mod_python/importer.py", line 304, in import_module return __import__(module_name, {}, {}, ['*']) File "/var/www/seL4/code/ertos.py", line 9, in <module> from bib import html_bib, html_abstract, yearlist, get_bibtex File "/var/www/seL4/code/bib.py", line 11, in <module> rg = cfg.get('core', 'rg') File "/usr/lib/python2.7/ConfigParser.py", line 618, in get raise NoOptionError(option, section) NoOptionError: No option 'rg' in section: 'core' Keith _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel

2 1

seL4 website down
by keith＠matellio.com 03 Oct '17

03 Oct '17

Is it just me or is everyone having trouble accessing the seL4 website? I'm getting the following: MOD_PYTHON ERROR ProcessId: 29222 Interpreter: 'sel4.systems.keg.ertos.in.nicta.com.au' ServerName: 'sel4.systems.keg.ertos.in.nicta.com.au' DocumentRoot: '/var/www/seL4/content' URI: '/Community/mailman/home.pml' Location: '/Community' Directory: None Filename: '/var/www/seL4/content/Community/mailman/home.pml' PathInfo: None Phase: 'PythonHandler' Handler: 'ertos' Traceback (most recent call last): File "/usr/lib/python2.7/dist-packages/mod_python/importer.py", line 1537, in HandlerDispatch default=default_handler, arg=req, silent=hlist.silent) File "/usr/lib/python2.7/dist-packages/mod_python/importer.py", line 1202, in _process_target module = import_module(module_name, path=path) File "/usr/lib/python2.7/dist-packages/mod_python/importer.py", line 304, in import_module return __import__(module_name, {}, {}, ['*']) File "/var/www/seL4/code/ertos.py", line 9, in <module> from bib import html_bib, html_abstract, yearlist, get_bibtex File "/var/www/seL4/code/bib.py", line 11, in <module> rg = cfg.get('core', 'rg') File "/usr/lib/python2.7/ConfigParser.py", line 618, in get raise NoOptionError(option, section) NoOptionError: No option 'rg' in section: 'core' Keith

1 0

Integer overflow bug in capdl-loader
by Jeff Kubascik 30 Sep '17

30 Sep '17

Hello, I am working with seL4 7.0.0 on the zynq7000 platform. I have come across a bug that occurs when a device physical memory region includes the highest address, i.e. where the memory region ends at 0xFFFFFFFF on 32 bit systems. When I create a CAmkES component that uses the highest address, I see the following error. ELF-loader started on CPU: ARM Ltd. Cortex-A9 r3p0 paddr=[10000000..100ac81f] ELF-loading image 'kernel' paddr=[0..32fff] vaddr=[e0000000..e0032fff] virt_entry=e0000000 ELF-loading image 'capdl-loader-experimental' paddr=[33000..1aefff] vaddr=[8000..183fff] virt_entry=befc Enabling MMU and paging Bootstrapping kernel Booting all finished, dropped to user space <<seL4(CPU 0) [decodeUntypedInvocation/210 T0xffdfd100 "rootserver" @8fa8]: Untyped Retype: Insufficient memory (1 * 4096 bytes needed, 0 bytes available).>> Warning: using printf before serial is set up. This only works as your printf is backed by seL4_Debug_PutChar() [Err seL4_NotEnoughMemory]: I have traced this problem to an integer overflow bug in the capdl-loader. The patch below shows how I have addressed this error. >From 22c9dd76a31713c98710830c2ea865a4e5d8a078 Mon Sep 17 00:00:00 2001 From: Jeff Kubascik <jeff.kubascik(a)dornerworks.com> Date: Wed, 27 Sep 2017 13:52:36 -0400 Subject: [PATCH] Fixed integer overflow bug in capdl-loader that occurs when a device physical memory region ends at 0xFFFFFFFF --- capdl-loader-app/src/main.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/capdl-loader-app/src/main.c b/capdl-loader-app/src/main.c index 34eedb0..305da2a 100644 --- a/capdl-loader-app/src/main.c +++ b/capdl-loader-app/src/main.c @@ -554,7 +554,7 @@ static int find_device_object(void *paddr, seL4_Word type, int size_bits, seL4_C /* Assume we are allocating from a device untyped. Do a linear search for it */ for (unsigned int i = 0; i < bootinfo->untyped.end - bootinfo->untyped.start; i++) { if (bootinfo->untypedList[i].paddr <= (uintptr_t)paddr && - bootinfo->untypedList[i].paddr + BIT(bootinfo->untypedList[i].sizeBits) >= (uintptr_t)paddr + BIT(size_bits)) { + bootinfo->untypedList[i].paddr + BIT(bootinfo->untypedList[i].sizeBits) - 1 >= (uintptr_t)paddr + BIT(size_bits) - 1) { /* just allocate objects until we get the one we want. To do this * correctly we cannot just destroy the cap we allocate, since * if it's the only frame from the untyped this will reset the -- 2.7.4 I have added a -1 to the end address calculations to fix the edge case when bootinfo->untypedList[i].paddr + BIT(bootinfo->untypedList[i].sizeBits) is equal to 0x100000000, an integer overflow. The current statement is comparing the address of the next byte past the end of the memory region. My change is comparing the address of the last byte in the memory region. I have tested this fix on the zynq7000 and it works. However, I am not too familiar with the capdl-loader. Are there any problems with this fix that I have not considered? Thanks, Jeff Kubascik

2 2

ARM 64-bit Support in seL4
by keith＠matellio.com 29 Sep '17

29 Sep '17

Not sure if this is the best place to post this question but I noticed on the seL4 roadmap page on the website that 64-bit support for ARM is due out at the end of 3Q2017. Is that correct, and if so, can someone give me some hints of where to look for it in the repository?

4 3

sel4 on QEMU
by ashokk＠spanidea.com 28 Sep '17

28 Sep '17

Hi, I am trying to run sel4 on QEMU, i am following this steps(https://wiki.sel4.systems/Hardware/Qemu) make clean make optiplex9020_defconfig make silentoldconfig make but while doing make i am getting following error.. /home/arun/test_default/libs/libsel4camkes/src/gdb_server/gdb.c: In function ‘get_breakpoint_format’:/home/arun/test_default/libs/libsel4camkes/src/gdb_server/gdb.c:130:27: error: ‘seL4_InstructionBreakpoint’ undeclared (first use in this function) *break_type = seL4_InstructionBreakpoint; ^/home/arun/test_default/libs/libsel4camkes/src/gdb_server/gdb.c:130:27: note: each undeclared identifier is reported only once for each function it appears in/home/arun/test_default/libs/libsel4camkes/src/gdb_server/gdb.c:131:19: error: ‘seL4_BreakOnRead’ undeclared (first use in this function) *rw = seL4_BreakOnRead; ^/home/arun/test_default/libs/libsel4camkes/src/gdb_server/gdb.c:135:27: error: ‘seL4_DataBreakpoint’ undeclared (first use in this function) *break_type = seL4_DataBreakpoint; ^/home/arun/test_default/libs/libsel4camkes/src/gdb_server/gdb.c:136:19: error: ‘seL4_BreakOnWrite’ undeclared (first use in this function) *rw = seL4_BreakOnWrite; ^/home/arun/test_default/libs/libsel4camkes/src/gdb_server/gdb.c:146:19: error: ‘seL4_BreakOnReadWrite’ undeclared (first use in this function) *rw = seL4_BreakOnReadWrite; ^make[1]: *** [src/gdb_server/gdb.o] Error 1make: *** [libsel4camkes] Error 2 can you please give any solution to solve these errors.. RegardsAshok

2 2

Sel4 compilation error for RasperryPi-3
by ashokk＠spanidea.com 27 Sep '17

27 Sep '17

Hi I am trying to cross-compile sel4 for rasperry-pi-3. i am executing following command on sel4 kernel source to cross-compile. TOOLPREFIX=arm-linux-gnueabi- ARCH=arm PLAT=bcm2837 ARMV=armv8-a CPU=cortex-a53 i am getting following error while doing make [BF_GEN] arch/object/structures_gen.h [BF_GEN] plat/machine/hardware_gen.h [BF_GEN] 32/mode/api/shared_types_gen.h [CPP] src/arch/arm/armv/armv8-a/32/machine_asm.s_pp In file included from src/arch/arm/armv/armv8-a/32/machine_asm.S:11:0: ./include/config.h:17:22: fatal error: autoconf.h: No such file or directory compilation terminated. make: *** [src/arch/arm/armv/armv8-a/32/machine_asm.s_pp] Error 1 rm 32/mode/api/shared_types_gen.h plat/machine/hardware_gen.h arch/object/structures_gen.h is there any solution for this... RegardsAshok

2 1

General question about software
by Raymond Jennings 26 Sep '17

26 Sep '17

So, I know that at a basic level, a block device driver would probably need I/O permissions, and I'm guessing that it would be handling requests from a file system driver. Is that basically how the seL4 software ecosystem is laid out? What's typical for how "software in the wild" is actually organized and layered on top of the microkernel? I only know about seL4 from a theoretical standpoint, read the manual and stuff, and mostly familiar with the actual kernel, but I'm a complete noob when it comes to actual software.

3 2

Raspberry pi 3 compilation error
by Prathamesh Rahate 26 Sep '17

26 Sep '17

Hi, I am trying to cross-compile seL4 for rapsberry pi 3 using steps mentioned hereseL4 on the Raspberry Pi 3 | | | seL4 on the Raspberry Pi 3 | | | I am getting following error while compiling, are there any patches available to fix this error: [STAGE] libsel4sync.a[libs/libsel4sync] done.[apps/sel4test-tests] building... [HEADERS] [STAGE] test_init_data.h [STAGE] arch/* [STAGE] arch_frame_type.h [STAGE] autoconf.h [CC] src/helpers.o [CC] src/main.o [CC] src/tests/multicore.o [CC] src/tests/preempt.o [CC] src/tests/serial_server.o [CC] src/tests/breakpoints.o [CC] src/tests/scheduler.o [CC] src/tests/pagetables.o [CC] src/tests/inc_untyped.o [CC] src/tests/interrupt.o [CC] src/tests/sync.o [CC] src/tests/iopt.o [CC] src/tests/ioports.o [CC] src/tests/vspace.o [CC] src/tests/ipc.o [CC] src/tests/schedcontext.o [CC] src/tests/fpu.o [CC] src/tests/ept.o [CC] src/tests/trivial.o [CC] src/tests/binding.o [CC] src/tests/cnodeops.o [CC] src/tests/threads.o [CC] src/tests/cspace.o [CC] src/tests/regressions.o/tmp/cc7e2jo9.s: Assembler messages:/tmp/cc7e2jo9.s:120: Error: selected processor does not support ARM mode `ldrex r2,[r3]'/tmp/cc7e2jo9.s:154: Error: selected processor does not support ARM mode `strex r0,r3,[r2]'make[1]: *** [src/tests/regressions.o] Error 1make: *** [sel4test-tests] Error 2user@user-Lenovo:~/seL4test$ Thanks,Prathamesh

2 1

User-space drivers
by ashokk＠spanidea.com 25 Sep '17

25 Sep '17

Hi guys, This is Ashokkumar, i want to write a sample serial(UART) communication user-space driver in sel4,can i get any help from your side. I am just started sel4 i don't know how to build and execute the programs,if you have any documents or examples about user-space programs please share with me... RegardsAshok

2 1

Some questions regarding seL4, U-Boot, and Raspberry Pi 3 patches
by Austin Seipp 21 Sep '17

21 Sep '17

Hello *, I hope you're all doing well. I recently got seL4 running on my Raspberry Pi 3, and wanted to report some notes here and ask some questions regarding the port, and perhaps get some help working on a patch (or twelve, I'm sure.) Recently I followed the Data61 blog post here to get a recent copy of seL4 on my RPi, but hit a few errors along the way that burned some time. In particular I got burned by the U-Boot glitch and getting seL4 building due to a glitch in the 'repo' setup for sel4test: https://research.csiro.au/ tsblog/sel4-raspberry-pi-3/ I ended up writing my own blog post, with effectively "fully reproducible" instructions (e.g. one of the codepad.org links on the RPi3 wiki page was dead) for a recent build. This includes proper setup for uboot.env in order to `fatload` and `bootm` the seL4 ELF binary off disk, the right U-Boot version, and using Docker to build the seL4 image: https://inner-haven.net/posts/2017-09-15-sel4-rpi3.html That's all fine, but... I got curious about this U-Boot glitch, as even a recent (git) copy of U-Boot still suffered from the issue reported in the original Data61 blog post. I found it strange this regression would exist for nearly 9 months, unless it was possibly something intentional (e.g. an intended behavioral change) or it went unreported. The glitch is this: after booting the seL4 binary, the system immediately hangs with no output after trying to start the sel4test application. This glitch did not occur in versions of U-Boot up-to v2017.01. Versions v2017.03 and later (to now) suffer. I decided to spend some time bisecting this problem and found the issue. Versions of U-Boot after v2017.01 include the following patch, which causes the data cache to be enabled prior to U-Boot loading and executing ELF binaries: https://github.com/thoughtpolice/u-boot/commit/ 995eab8b5b580b67394312b1621c60a71042cd18 This behavior previously existed as a workaround for QNX, which required that the dcache be disabled before execution. U-Boot, previously, disabled the dcache when booting *any* ELF binary at all (the binary can of course enable it or check to see if it isn't enabled already), as a simplistic workaround. This patch changes it to only disable the dcache on U-Boot images (uImages) marked as QNX ELF binaries, so that QNX systems boot properly still. It would seem then that seL4 -- or at least sel4test -- requires the dcache to be disabled upon entry for the RPi3. If the dcache is enabled, as in the above patch, it otherwise hangs immediately. In fact, a recent copy of U-Boot *can* execute seL4 properly: you simply have to use `./tools/mkimage` inside U-Boot to mark the application as `mkimage -C none -A arm -T kernel -O qnx -d <input> <output>` first -- this creates a uImage with the appropriate header to mark the ELF as a QNX binary. U-Boot recognizes this and appropriately disables the dcache before application entry, once you use `bootm` or something. I took the time to write a patch to U-Boot in order to add a new OS definition -- "sel4" -- in order to address this problem more clearly. My change is here: https://github.com/thoughtpolice/u-boot/commit/ 720caf6c398584658abfa883d4d390f4b6200269 With this change, you can mark any seL4 binary as `-O sel4` to create an appropriately bootable uImage, with the dcache appropriately disabled. Assuming this is in place, the following U-Boot commands will execute seL4: U-Boot> setenv bootfile uImage U-Boot> fatload mmc 0 ${loadaddr} ${bootfile} U-Boot> bootm ${loadaddr} ## Booting kernel from Legacy Image at 00200000 ... Image Name: Image Type: ARM seL4 Kernel Image (uncompressed) Data Size: 3385548 Bytes = 3.2 MiB Load Address: 00000000 Entry Point: 00000000 Verifying Checksum ... OK Loading Kernel Image ... OK CACHE: Misaligned operation at range [20000000, 200078bc] CACHE: Misaligned operation at range [200078bc, 2032a720] CACHE: Misaligned operation at range [2032c000, 2033c820] ## Starting application at 0x20000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 paddr=[20000000..2033c81f] ELF-loading image 'kernel' paddr=[0..32fff] vaddr=[e0000000..e0032fff] virt_entry=e0000000 ELF-loading image 'sel4test-driver' paddr=[33000..44dfff] vaddr=[10000..42afff] virt_entry=2a03c Enabling MMU and paging Jumping to kernel-image entry point... ---- So with that all done, it's clear there's a change needed *somewhere* but I'm not sure where or what to do: 1) Is the above the right approach? Clearly, seL4 on the RPi3 assumed a disabled dcache during its development, but this has now changed, so for this platform something will need to be fixed, such as the above. 2) Or perhaps this is not a U-Boot problem, but should be fixed in seL4. Or in sel4test. For example, is there an option to assume the dcache is already enabled in the configuration? Maybe that should be toggled instead. Or does seL4 *always* assume it is disabled at boot? What about non-RPi3 platforms like other ARM systems? These likely use U-Boot as well, but it's unclear if the cache should be disabled here, too. In this case, the above U-Boot patch is (in theory) wrong, but if that's true, it was always wrong to begin with (as it always disabled the cache prior to ELF loading). If something like this was the case, then the rpi3 configurations (or perhaps some bootinfo code) needs to change. 3) Alternatively, this is just an outright bug in seL4 that should be fixed and U-Boot was previously masking it. (I'm not sure if the proofs cover this one :) 4) Perhaps it should be a mix of both. For example, perhaps the sel4/sel4test code should be changed to assume an already-enabled dcache, or fixed outright. But perhaps a U-Boot patch would still be good to submit upstream: for example, I could submit the above patch upstream, but *remove* the dcache code. This would allow U-Boot users to mark seL4 binaries appropriately for clarity and future compatibility and make U-Boot "officially support" seL4. And in the future, should seL4 need more patches/workarounds/requirements from U-Boot, it would be easier to add and maintain them. --- I'd prefer not to run myself into dead ends trying to get the wrong solution upstream to either seL4 or U-Boot, and it would be great to fix this for users. I'd also like to look into more adventurous stuff in the future (like multicore on the RPi3 which seems unsupported), so any advice is appreciated to get started. Even then: bisection and the patch creation only took an hour, so if it's wrong, not much was lost. -- Regards, Austin - PGP: 4096R/0x91384671

2 3

Re: [seL4] Some questions regarding seL4, U-Boot, and Raspberry Pi 3 patches
by Steven Johnston 20 Sep '17

20 Sep '17

Hi Austin I can confirm your blog post building method works. When attempting to boot from the SD card I receive a Wrong Image Format error: Hit any key to stop autoboot: 0 reading kernel.img 3385548 bytes read in 236 ms (13.7 MiB/s) Wrong Image Format for bootm command ERROR: can't get kernel image! However I was able to successfully network load the image and boot: U-Boot> dhcp 192.168.222.123:kernel.img Waiting for Ethernet connection... done. BOOTP broadcast 1 BOOTP broadcast 2 BOOTP broadcast 3 DHCP client bound to address 192.168.216.122 (1257 ms) Using sms0 device TFTP from server 192.168.222.123; our IP address is 192.168.216.122 Filename 'kernel.img'. Load address: 0x200000 Loading: ... done Bytes transferred = 3385548 (33a8cc hex) U-Boot> bootelf CACHE: Misaligned operation at range [20000000, 200078bc] CACHE: Misaligned operation at range [200078bc, 2032a720] CACHE: Misaligned operation at range [2032c000, 2033c820] ## Starting application at 0x20000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 paddr=[20000000..2033c81f] ELF-loading image 'kernel' paddr=[0..32fff] vaddr=[e0000000..e0032fff] virt_entry=e0000000 ELF-loading image 'sel4test-driver' paddr=[33000..44dfff] vaddr=[10000..42afff] virt_entry=2a03c Enabling MMU and paging Jumping to kernel-image entry point... ... Starting test 118: Test all tests ran Test suite passed. 118 tests passed. All is well in the universe Thank you for the push on RPI3! It helped me finish a thread I started months ago and also inadvertently confirmed the serial GPIO on a RPI3 I had been using was not operational. Steve > Date: Mon, 18 Sep 2017 01:49:40 +0000 > From: <Adrian.Danis(a)data61.csiro.au> > To: <aseipp(a)pobox.com>, <devel(a)sel4.systems> > Subject: Re: [seL4] Some questions regarding seL4, U-Boot, and > Raspberry Pi 3 patches > Message-ID: <829193ff-4b95-8d98-c2ad-6e626fdb5e1f(a)data61.csiro.au> > Content-Type: text/plain; charset="utf-8" > > Hi Austin, > > Thanks for the detective work! > > seL4 (or more specifically in this case the elfloader-tool) should be able to tolerate being started with either the cache enabled or disabled. In fact if you look in the mmu code (https://github.com/seL4/seL4_tools/blob/master/elfloader-tool/src/arch-arm/…) you should notice some rough logic of > > if cache enabled > clean cache > disable cache > invalidate cache > > That code only operates on the architected caches though, and not on any platform specific cache controllers, although to my knowledge the rpi3 only has ARM architected caches. I would not be surprised if there were any errors in the dcache macro that walks through the cache levels though, which would be my guess as to where the problem is. > > I will create an issue internally to track this down, but will probably be a little while before anyone has time so if you're interested in fixing the elfloader then you're both welcome and encouraged to. Either way appreciate your efforts thus far. > > Adrian > > On Sun 17-Sep-2017 4:21 AM, Austin Seipp wrote: > Hello *, > > I hope you're all doing well. I recently got seL4 running on my Raspberry Pi 3, and wanted to report some notes here and ask some questions regarding the port, and perhaps get some help working on a patch (or twelve, I'm sure.) > > Recently I followed the Data61 blog post here to get a recent copy of seL4 on my RPi, but hit a few errors along the way that burned some time. In particular I got burned by the U-Boot glitch and getting seL4 building due to a glitch in the 'repo' setup for sel4test: https://research.csiro.au/tsblog/sel4-raspberry-pi-3/ > > I ended up writing my own blog post, with effectively "fully reproducible" instructions (e.g. one of the codepad.org<http://codepad.org> links on the RPi3 wiki page was dead) for a recent build. This includes proper setup for uboot.env in order to `fatload` and `bootm` the seL4 ELF binary off disk, the right U-Boot version, and using Docker to build the seL4 image: https://inner-haven.net/posts/2017-09-15-sel4-rpi3.html > > That's all fine, but... > > I got curious about this U-Boot glitch, as even a recent (git) copy of U-Boot still suffered from the issue reported in the original Data61 blog post. I found it strange this regression would exist for nearly 9 months, unless it was possibly something intentional (e.g. an intended behavioral change) or it went unreported. > > The glitch is this: after booting the seL4 binary, the system immediately hangs with no output after trying to start the sel4test application. This glitch did not occur in versions of U-Boot up-to v2017.01. Versions v2017.03 and later (to now) suffer. > > I decided to spend some time bisecting this problem and found the issue. Versions of U-Boot after v2017.01 include the following patch, which causes the data cache to be enabled prior to U-Boot loading and executing ELF binaries: > > https://github.com/thoughtpolice/u-boot/commit/995eab8b5b580b67394312b1621c… > > This behavior previously existed as a workaround for QNX, which required that the dcache be disabled before execution. U-Boot, previously, disabled the dcache when booting *any* ELF binary at all (the binary can of course enable it or check to see if it isn't enabled already), as a simplistic workaround. This patch changes it to only disable the dcache on U-Boot images (uImages) marked as QNX ELF binaries, so that QNX systems boot properly still. > > It would seem then that seL4 -- or at least sel4test -- requires the dcache to be disabled upon entry for the RPi3. If the dcache is enabled, as in the above patch, it otherwise hangs immediately. > > In fact, a recent copy of U-Boot *can* execute seL4 properly: you simply have to use `./tools/mkimage` inside U-Boot to mark the application as `mkimage -C none -A arm -T kernel -O qnx -d <input> <output>` first -- this creates a uImage with the appropriate header to mark the ELF as a QNX binary. U-Boot recognizes this and appropriately disables the dcache before application entry, once you use `bootm` or something. > > I took the time to write a patch to U-Boot in order to add a new OS definition -- "sel4" -- in order to address this problem more clearly. My change is here: > > https://github.com/thoughtpolice/u-boot/commit/720caf6c398584658abfa883d4d3… > > With this change, you can mark any seL4 binary as `-O sel4` to create an appropriately bootable uImage, with the dcache appropriately disabled. > > Assuming this is in place, the following U-Boot commands will execute seL4: > > U-Boot> setenv bootfile uImage > U-Boot> fatload mmc 0 ${loadaddr} ${bootfile} > U-Boot> bootm ${loadaddr} > ## Booting kernel from Legacy Image at 00200000 ... > Image Name: > Image Type: ARM seL4 Kernel Image (uncompressed) > Data Size: 3385548 Bytes = 3.2 MiB > Load Address: 00000000 > Entry Point: 00000000 > Verifying Checksum ... OK > Loading Kernel Image ... OK > CACHE: Misaligned operation at range [20000000, 200078bc] > CACHE: Misaligned operation at range [200078bc, 2032a720] > CACHE: Misaligned operation at range [2032c000, 2033c820] > ## Starting application at 0x20000000 ... > > ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 > paddr=[20000000..2033c81f] > ELF-loading image 'kernel' > paddr=[0..32fff] > vaddr=[e0000000..e0032fff] > virt_entry=e0000000 > ELF-loading image 'sel4test-driver' > paddr=[33000..44dfff] > vaddr=[10000..42afff] > virt_entry=2a03c > Enabling MMU and paging > Jumping to kernel-image entry point... > > ---- > > So with that all done, it's clear there's a change needed *somewhere* but I'm not sure where or what to do: > > 1) Is the above the right approach? Clearly, seL4 on the RPi3 assumed a disabled dcache during its development, but this has now changed, so for this platform something will need to be fixed, such as the above. > > 2) Or perhaps this is not a U-Boot problem, but should be fixed in seL4. Or in sel4test. For example, is there an option to assume the dcache is already enabled in the configuration? Maybe that should be toggled instead. Or does seL4 *always* assume it is disabled at boot? What about non-RPi3 platforms like other ARM systems? These likely use U-Boot as well, but it's unclear if the cache should be disabled here, too. In this case, the above U-Boot patch is (in theory) wrong, but if that's true, it was always wrong to begin with (as it always disabled the cache prior to ELF loading). > > If something like this was the case, then the rpi3 configurations (or perhaps some bootinfo code) needs to change. > > 3) Alternatively, this is just an outright bug in seL4 that should be fixed and U-Boot was previously masking it. (I'm not sure if the proofs cover this one :) > > 4) Perhaps it should be a mix of both. For example, perhaps the sel4/sel4test code should be changed to assume an already-enabled dcache, or fixed outright. But perhaps a U-Boot patch would still be good to submit upstream: for example, I could submit the above patch upstream, but *remove* the dcache code. This would allow U-Boot users to mark seL4 binaries appropriately for clarity and future compatibility and make U-Boot "officially support" seL4. And in the future, should seL4 need more patches/workarounds/requirements from U-Boot, it would be easier to add and maintain them. > > --- > > I'd prefer not to run myself into dead ends trying to get the wrong solution upstream to either seL4 or U-Boot, and it would be great to fix this for users. I'd also like to look into more adventurous stuff in the future (like multicore on the RPi3 which seems unsupported), so any advice is appreciated to get started. Even then: bisection and the patch creation only took an hour, so if it's wrong, not much was lost. > > -- > Regards, > Austin - PGP: 4096R/0x91384671 > > > > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems<mailto:Devel@sel4.systems> > https://sel4.systems/lists/listinfo/devel > > >

1 0

Problem making the manual
by Raymond Jennings 18 Sep '17

18 Sep '17

I got an error log when I tried "make" in the manual directory. I got this: ====> Generating doxygen-output/xml/group__GeneralSystemCalls.xml ====> Generating doxygen-output/xml/group__DebuggingSystemCalls.xml ====> Generating doxygen-output/xml/group__BenchmarkingSystemCalls.xml ====> Generating doxygen-output/xml/group__ObjectApiX86.xml ====> Generating doxygen-output/xml/group__ObjectApiArm.xml ====> Generating doxygen-output/xml/group__ObjectApiAarch32.xml ====> Generating doxygen-output/xml/group__ObjectApiAarch64.xml ====> Generating doxygen-output/xml/group__ObjectApiIa32.xml ====> Generating doxygen-output/xml/group__ObjectApiX64.xml ====> Generating generated/GeneralSystemCalls.tex Traceback (most recent call last): File "tools/parse_doxygen_xml.py", line 327, in <module> sys.exit(main()) File "tools/parse_doxygen_xml.py", line 321, in main output_str = generate_general_syscall_doc(args.input, args.level) File "tools/parse_doxygen_xml.py", line 276, in generate_general_syscall_doc details, params, ret = parse_detailed_desc(member, ref_dict) File "tools/parse_doxygen_xml.py", line 157, in parse_detailed_desc ret_type = types_iter.next() AttributeError: 'list_iterator' object has no attribute 'next' make: *** [Makefile:126: generated/GeneralSystemCalls.tex] Error 1

3 3

I need help porting camkes/arm/vmm to new hardware
by Michael DeFrancis 14 Sep '17

14 Sep '17

To the sel4 development community: I am working on porting the sel4 virtual machine from the tk1 to a variety of arm hardware platforms, starting with the Xilinx parts listed below - and I could use some help getting started. I have the following hardware: - Tegra tk1 - Xilinx zynq7000 (zc706) - Xilinx zynq9000 (zcu102) I am successfully ported the 64 bit sel4 kernel to run on the zynq9000, but now I need to port the arm/vmm to run on the zynq9000 hardware as well. I am happy to share these updates with the sel4 community at large. I am uncertain what the best way to do this is - should I submit all of the changes to github, or is there another development repository? I would like to first port the arm/vmm from https://github.com/SEL4PROJ/camkes-arm-vm to the zynq7000<https://github.com/SEL4PROJ/camkes-arm-vm%20to%20the%20zynq7000> for testing, before porting it to the 64 bit zynq9000 platform. Could someone please put me in touch with the author of the arm/vmm that is designed to run on the tegra/tk1 hardware? I have some specific questions to ask regarding platform-specific files. At a high level, I know that I need to change the addresses of peripherals that are passed to my linux kernel (buildroot) for the zynq7000, but I am uncertain where to start. If someone could point me in the right direction, that would be very helpful. Further, if I could talk to a real person about this over the phone, that would be even better. My work phone is (1)(301)294-5263 and my cell phone is (1)(571)271-7278 - feel free to call me and leave me a message. I have not posted to devel(a)sel4.systems<mailto:devel@sel4.systems> previously, though I have been working on the sel4 project for a few months now. I work for Intelligent Automation Inc. in Rockville, Maryland - USA. ________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.

2 1

Announcing 7.0.0 release
by Kent.Mcleod＠data61.csiro.au 05 Sep '17

05 Sep '17

= seL4 Version 7.0.0 Release = Announcing the release of seL4 7.0.0 with the following changes: == Changes == * Support for building standalone ia32 kernel added in e7327fa6df3 * ia32: Set sensible defaults for FS and GS selectors in c2f6d48bcf2 * aarch64: Use tpidrro_el0 for IPC buffer instead of tpidr_el0 in ae9fe9b5d18 * More seL4 manual documentation added for aarch64 object invocations * Default NUM_DOMAINS set to 16 for x86-64 standalone builds in baa9798f793 * libsel4: Return seL4_Error in invocation stubs in 8fb06eecff9 ''' This is a source code level breaking change ''' * Add a CMake based build system in 0b73072016e * x86: Increase TCB size for debug builds in 4c8be8f4f91 * libsel4: x86: Remove nested struct declarations in a8d6315eb16 ''' This is a source code level breaking change ''' * Bugfix: x86: Unmap pages when delete non final frame caps in 08b9265563a = Notable changes = * CMake based build system added: Initial experimental support has been added for using CMake for building the kernel and some user level libraries. Currently the only project that takes advantage of this is seL4test when using the cmake.xml manifest in sel4test-manifest. Documentation can be found at: https://github.com/seL4/seL4_tools/tree/master/cmake-tool = Upgrade notes = * This release is not source compatible with previous releases. * seL4 invocations that previously returned long now return seL4_Error which is an enum. Our libraries have already been updated to reflect this change, but in other places where seL4 invocations are used directly, the return types will need to be updated to reflect this change. * On x86 some structs in the Bootinfo have been rearranged. This only affects seL4_VBEModeInfoBlock_t which is used if VESA BIOS Extensions (VBE) information is being used. = Known issues = * One of our tests is non-deterministicly becoming unresponsive on the SMP release build on the Sabre IMX.6 platform, which is a non verified configuration of the kernel. We are working on fixing this problem, and will likely do a point release once it is fixed. = Full changelog = Use `git log 6.0.0..7.0.0` in https://github.com/seL4/seL4 = More details = See the 7.0.0 manual <http://sel4.systems/Info/Docs/seL4-manual-7.0.0.pdf> included in the release or ask on the mailing list!

1 0

UX/RT - an seL4-based OS in the style of QNX and Plan 9
by Andrew Warkentin 03 Sep '17

03 Sep '17

I mentioned this here earlier, but I haven't really gone into a lot of detail about it here. I am planning to write an seL4-based OS similar to QNX and Plan 9 called UX/RT. I am intending it to be both an embedded OS (mostly for the larger types of embedded systems where QNX or Linux would be used, as opposed to simpler ones) as well as a desktop OS. I plan to use as much third-party code as possible to avoid making lots of extra work (likely LKL <https://github.com/lkl/linux> and/or the NetBSD rump kernel for device drivers, disk filesystems, and the network stack; a libc based on musl; and basic commands forked from those of FreeBSD). UX/RT will be a pure Unix-like system with no concept of "personality-neutral" services, and the root server will implement a subset of the Unix API directly (as in QNX, although the root server will be completely separate from the kernel of course, unlike that of QNX). However, there will be a Linux compatibility layer implemented with libraries and filesystem servers. I am going to avoid C for new code as much as possible for security, preferring Rust for anything performance-critical. The main concept behind the design will be to take "everything is a file" as far as it possibly can go. Nearly all resources in the system will appear in the filesystem, even things like process memory (kernel memory and the interface to the root server will be among the few non-files in the system, although the API of the root server will be implemented with an anonymous FD internally). The filesystem will be a combination of a thin layer on top of L4 IPC with read() and write() calling L4 IPC directly (short transfers will probably be sent entirely in message registers and long ones sent by using shared pages), and a memory mapping layer. The VFS will implement the name service and memory mapping parts of the filesystem; read() and write() will bypass the VFS layer entirely and will use seL4 IPC to communicate directly with the other thread. There will also be APIs that expose message registers and shared pages more directly although they will do it in a way that interoperates with read() and write() (these will mostly be used with a new "message-special" file type that preserves message boundaries but otherwise acts like a normal byte stream if used with read() or write()). No provisions will be made for use of IPC or capabilities outside the filesystem. Security will be based on an ACL-per-process model, where the root server will have an in-memory list of files for each process specifying which files it is allowed to access, as opposed to a hierarchical pure-capability model like other L4-based systems (a pure capability model seems like it would be a poor fit for a pure Unix-like system). It will be possible to either specify rwx permission bits explicitly or use the mode from the filesystem; it will also be possible for an ACL entry to specify all files under a particular directory. File descriptors will be implemented as groups of capabilities, and the root server will hand them out when a process successfully opens a file (unlike in QNX there will be no need for individual filesystem servers to check whether the client process is authorized to access a file). There will be an ACL management server that will persistently associate permissions with programs, and it will also be possible for sufficiently privileged processes to dynamically modify the ACLs of other processes. I currently have a bootloader, some basic infrastructure for building boot ISO images, and a patch for seL4 to support QNX-like XIP single-image boot using a variant of Multiboot2. I can build a boot ISO with a system image containing only the kernel, but it crashes with a triple fault somewhere in either the bootloader or the kernel (I haven't yet tried to track down where it's occurring). Once I move on to user mode code, I'm going to be using the Rust libraries from Robigalia as a basis for the root server (higher-level Rust-based components will use a normal Unix build of the Rust standard library instead). The code I have so far can be found at <https://gitlab.com/uxrt> for UX/RT itself and <https://gitlab.com/uxrt-bos> for the bootloader. I have some (long and not particularly well-organized) notes on my plans for UX/RT's architecture at <https://gitlab.com/uxrt/uxrt-toplevel/blob/master/architecture_notes>. Anybody is more than welcome to contribute if they want.

2 2

VGA buffer as stdout
by Michal Podhradsky 31 Aug '17

31 Aug '17

Hello, I have a question about standard output. I have a camkes component than can write into text-mode VGA buffer (basically it follows this simple example http://wiki.osdev.org/Bare_Bones#Writing_a_kernel_in_C ) but I would like to be able to redirect the kernel messages during startup to be printed on screen using VGA buffer. Once another component (either Linux in a VM, or some other camkes app) will initialize, it will be able to take control over the screen output (and for example show login window etc). My questions is - is this possible with seL4? And if so, what would it entail? I guess in the minimal version, I would have to provide a different implementation of seL4_DebugPutChar, is that correct? The VGA standard seems to define the buffer to be at 0xB8000, so it should be consistent between x86 platforms. Regards Michal

5 11

benchmark - idle utilization
by Alexander Boettcher 31 Aug '17

31 Aug '17

Hello, we use the seL4 benchmark interface to feed Genode's trace infrastructure with information about the CPU utilization of threads and of idle times. In general the integration was reasonable straightforward. One minor point we had. It seems that the idle time of a CPU can only be requested by a thread running on the vary same CPU. Requesting the CPU idle times of a remote CPU (the calling thread is on another CPU) is not supported, right ? In principle we may start on each CPU a thread just for the sake of requesting the idle utilization time, which however looks a bit of overkill. We "kind of" circumvent the issue for us by changing the syscall handling in the kernel in that regard, that the CPU number of the requested target thread is taken instead that of the caller thread, e.g. like this: --- a/src/benchmark/benchmark_utilisation.c +++ b/src/benchmark/benchmark_utilisation.c @@ -36,6 +36,11 @@ void benchmark_track_utilisation_dump(void) tcb = TCB_PTR(cap_thread_cap_get_capTCBPtr(lu_ret.cap)); buffer[BENCHMARK_TCB_UTILISATION] = tcb->benchmark.utilisation; /* Requested thread utilisation */ +#if CONFIG_MAX_NUM_NODES > 1 + if (tcb->tcbAffinity < ksNumCPUs) + buffer[BENCHMARK_IDLE_UTILISATION] = NODE_STATE_ON_CORE(ksIdleThread, tcb->tcbAffinity)->benchmark.utilisation; /* Idle thread utilisation */ + else +#endif buffer[BENCHMARK_IDLE_UTILISATION] = NODE_STATE(ksIdleThread)->benchmark.utilisation; /* Idle thread utilisation */ #ifdef CONFIG_ARM_ENABLE_PMU_OVERFLOW_INTERRUPT With this change, we still have to create a thread on every CPU (since we need a capability for the syscall), but at least the threads must not be running actively. Does this change (the patch) make sense to you and is it worthwhile to adjust in general on your side - or would you advise/envision another approach/direction ? (like specifying the cpu number for the idle times directly via the syscall or having a explicit syscall just for cpu idle times [but there are no specific thread idle capabilities as syscall parameter] etc.) Another question: Currently it seems that no idle CPU times are provided, as long as no user thread is actively running on that specific CPU. We can handle it, no problem in general - however we would have to adjust generic code (which runs on 8 different kernels) specifically for seL4 to handle this minor case. Could this possibly be changed (easily) ? Thanks, Alex. -- Alexander Boettcher Genode Labs http://www.genode-labs.com - http://www.genode.org Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth

2 3

Compile errors for Beaglebone Black
by Todd_Peterson＠mgtsciences.com 31 Aug '17

31 Aug '17

Hi, I am trying to compile seL4 for the BBB. I am getting the following errors when it gets to timer_service. I am following the instructions at https://github.com/seL4/refos-manifest. I got past another compile error by adding a typedef to device_timer.h for pstimer_t. Any help is appreciated. // tfp, added to avoid compiler error typedef uint32_t pstimer_t; [apps/timer_server] building... [HEADERS] [STAGE] autoconf.h [CC] src/state.o In file included from /home/users/staff/tpeterson/sel4/beagle/stage/arm/am335x/include/refos-util/device_io.h:22:0, from /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.h:21, from /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/state.h:27, from /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/state.c:24: /home/users/staff/tpeterson/sel4/beagle/stage/arm/am335x/include/refos-rpc/data_client_helper.h: In function 'data_open_map': /home/users/staff/tpeterson/sel4/beagle/stage/arm/am335x/include/refos-rpc/data_client_helper.h:95:69: warning: passing argument 6 o f 'data_open' from incompatible pointer type [-Wincompatible-pointer-types] d.dataspace = data_open(session, name, flags, mode, dspaceSize, &errnoRetVal); ^ In file included from /home/users/staff/tpeterson/sel4/beagle/stage/arm/am335x/include/refos-util/device_io.h:21:0, from /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.h:21, from /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/state.h:27, from /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/state.c:24: /home/users/staff/tpeterson/sel4/beagle/stage/arm/am335x/include/refos-rpc/data_client.h:72:11: note: expected 'int ** (*)()' but ar gument is of type 'int *' seL4_CPtr data_open(seL4_CPtr session, char* name, int flags, int mode, int size, int* errno); ^ [CC] src/device_timer.o /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c: In function 'device_timer_handle_irq': /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:146:5: warning: implicit declaration of function 'timer _handle_irq' [-Wimplicit-function-declaration] timer_handle_irq(s->timerDev, irq); ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c: In function 'device_timer_init': /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:239:5: error: unknown type name 'timer_config_t' timer_config_t config; ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:240:11: error: request for member 'vaddr' in something not a structure or union config.vaddr = ps_io_map(&io->opsIO.io_mapper, dm_timer_paddrs[TIMER_ID], ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:240:52: error: 'dm_timer_paddrs' undeclared (first use in this function) config.vaddr = ps_io_map(&io->opsIO.io_mapper, dm_timer_paddrs[TIMER_ID], ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:240:52: note: each undeclared identifier is reported on ly once for each function it appears in /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:242:11: error: request for member 'irq' in something no t a structure or union config.irq = dm_timer_irqs[TIMER_ID]; ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:242:18: error: 'dm_timer_irqs' undeclared (first use in this function) config.irq = dm_timer_irqs[TIMER_ID]; ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:243:16: error: request for member 'vaddr' in something not a structure or union if (!config.vaddr) { ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:248:19: warning: implicit declaration of function 'ps_g et_timer' [-Wimplicit-function-declaration] s->timerDev = ps_get_timer(TIMER_ID, &config); ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:248:17: warning: assignment makes pointer from integer without a cast [-Wint-conversion] s->timerDev = ps_get_timer(TIMER_ID, &config); ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:250:11: error: request for member 'vaddr' in something not a structure or union config.vaddr = ps_io_map(&io->opsIO.io_mapper, dm_timer_paddrs[TICK_ID], ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:252:11: error: request for member 'irq' in something no t a structure or union config.irq = dm_timer_irqs[TICK_ID]; ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:253:16: error: request for member 'vaddr' in something not a structure or union if (!config.vaddr) { ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:258:16: warning: assignment makes pointer from integer without a cast [-Wint-conversion] s->tickDev = ps_get_timer(TICK_ID, &config); ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:273:41: error: request for member 'properties' in somet hing not a structure or union for (uint32_t i = 0; i < s->timerDev->properties.irqs; i++) { ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:274:19: warning: implicit declaration of function 'time r_get_nth_irq' [-Wimplicit-function-declaration] int irq = timer_get_nth_irq(s->timerDev, i); ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:282:44: error: request for member 'properties' in somet hing not a structure or union for (uint32_t i = 0; i < s->tickDev->properties.irqs; i++) { ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:289:21: warning: implicit declaration of function 'time r_start' [-Wimplicit-function-declaration] int error = timer_start(s->tickDev); ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:310:13: warning: implicit declaration of function 'time r_periodic' [-Wimplicit-function-declaration] error = timer_periodic(s->timerDev, TIMER_PERIODIC_MAX); ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c: In function 'device_timer_get_time': /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:344:21: warning: implicit declaration of function 'time r_get_time' [-Wimplicit-function-declaration] uint64_t time = timer_get_time(s->timerDev); ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:345:21: error: request for member 'properties' in somet hing not a structure or union if (!s->timerDev->properties.upcounter) { ^ make[1]: *** [/home/users/staff/tpeterson/sel4/beagle/stage/arm/am335x/common/common.mk:265: src/device_timer.o] Error 1 make: *** [tools/common/project.mk:331: timer_server] Error 2 Todd Peterson Chief Embedded Systems Engineer Management Sciences, Inc. 6022 Constitution Ave NE Albuquerque, NM 87144 505-255-8611 (office) 505-205-7057 (cell) This email message and any attachments are for the sole use of the intended recipient(s) and may contain proprietary and/or confidential information which may be privileged or otherwise protected from disclosure. Any unauthorized review, use, disclosure or distribution is prohibited. If you are not the intended recipient(s), please contact the sender by reply email and destroy the original message and any copies of the message as well as any attachments to the original message.

1 0

Genode OS Framework 17.08 with extended seL4 support
by Alexander Boettcher 30 Aug '17

30 Aug '17

Hello, we're happy to announce the version 17.08 of the Genode OS Framework. Within the last release cycle (3-months) we upgraded our Genode/seL4 support from kernel version 3.2.0 to 6.0.0, enabled x86_64 and ARM support, added UEFI support to the seL4 kernel and enabled SMP for x86. A summary of changes and features are: - Hardware-accelerated graphics for Intel Gen-8 GPUs - The seL4 6.0 kernel on ARM and 64-bit x86 hardware - Genode as Xen DomU - Preliminary UEFI support for NOVA, base-hw, and seL4 - New server for capturing reports to files - New runtime for the sequential execution of components - Support for boot-time initialized frame buffer - FatFS-based VFS plugin - Extended non-blocking operation of the VFS - Refined time handling - Updated Muen separation kernel The long version of the official release documentation: https://genode.org/documentation/release-notes/17.08 All the best, -- Alexander Boettcher Genode Labs http://www.genode-labs.com - http://www.genode.org Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth

2 1

x86_64 kernel crash
by Alexander Boettcher 30 Aug '17

30 Aug '17

Hello, we're are in progress of extending our Genode/seL4 support, namely adding x86_64 and ARM support. During this work I encountered on x86_64 some sporadically crashes of the seL4 kernel. It happened during the debugging of our roottask on seL4 in form of a page fault in the kernel ("KERNEL EXCEPTION") or a static assertion in the kernel (see below). >From my understanding, this shouldn't be possible based on your verification work. Nevertheless, it happens reliable. (To be fair, the roottask was in this scenario already a bit confused and did things wrong - which however should never be enough to force the kernel in an exception or assertion - I presume.) I saved and stripped down the scenario which causes the kernel exception with high reliably and hope you can re-produce it and find the root cause. I stripped down the scenario to just the Genode image binary and the steps we did to create the seL4 kernel from the vanilla sources. Steps to reproduce: qemu-system-x86_64 -no-kvm -serial stdio -m 512 -kernel sel4 -initrd bomb_image.elf The binaries of "bomb_image.elf" can be found at [1] and the kernel "sel4" at [2]. The kernel is based on seL4 6.0 and a patch to pc99/autoconf.h (see [0]). Beside that it is the vanilla 6.0 kernel: https://github.com/seL4/seL4.git git commit 8564ace4dfb622ec69e0f7d762ebfbc8552ec918 "update VERSION file to 6.0.0" patch -p1 <~autoconfig.patch BOARD=x86_64 ARCH=x86 SEL4_ARCH=x86_64 PLAT=pc99 DEBUG=1 make objcopy -O elf32-i386 kernel.elf.strip sel4 (Qemu complains otherwise about 64bit elf for boot) The final "sel4" binary can be used with the "bomb_image.elf" and qemu as pointed out above. I tried Qemu 2.5.0 as shipped with Ubuntu 16.04 LTS and Qemu 2.8.0 (self-compiled). On real hardware the scenario typically leads after a while (kernel booted, roottask booted, scenario starts to run) to a reboot (without the messages or assertion as in the Qemu case, see below). The tool-chain for Genode is based on GNU GCC 6.3.0 (see [3] and [4]). The kernel was either compiled with Genode's toolchain (6.3.0) or with the standard GCC as provided by Ubuntu 16.04 LTS (GCC 5.4.0). On x86_32 I could not reproduce the issue. (On ARM I did not try.) I hope the information are helpful - if you need more just ask. Cheers, Alex. ========== KERNEL EXCEPTION ========== Vector: 0xe ErrCode: 0x0 IP: 0xffffffff80720e60 SP: 0xffffffff80740e08 FLAGS: 0x6 CR0: 0x8000003b CR2: 0x3007065 (page-fault address) CR3: 0x1ffb000 (page-directory physical address) CR4: 0x220 Stack Dump: *0xffffffff80740e08 == 0xffffff8001a99b00 *0xffffffff80740e10 == 0xffffffff80729b1f *0xffffffff80740e18 == 0x1 *0xffffffff80740e20 == 0xffffffff80721c59 *0xffffffff80740e28 == 0xffffffff *0xffffffff80740e30 == 0x0 *0xffffffff80740e38 == 0xffffff801f02b740 *0xffffffff80740e40 == 0xffffff801f02b740 *0xffffffff80740e48 == 0x1 *0xffffffff80740e50 == 0xffffff8001a99000 *0xffffffff80740e58 == 0x7 *0xffffffff80740e60 == 0x59 *0xffffffff80740e68 == 0xffffff8001a99b00 *0xffffffff80740e70 == 0xffffffff80729cf3 *0xffffffff80740e78 == 0x9000000000000007 *0xffffffff80740e80 == 0xffffff8001a99059 *0xffffffff80740e88 == 0xffffff80ffffffff *0xffffffff80740e90 == 0xffffffff80740f18 *0xffffffff80740e98 == 0xffffff800013c200 *0xffffffff80740ea0 == 0x10000 Halting... halting... Kernel entry via Syscall, number: 1, Call Cap type: 10, Invocation tag: 16 or seL4 failed assertion '(cte_t*)mdb_node_get_mdbNext(destSlot->cteMDBNode) == NULL && (cte_t*)mdb_node_get_mdbPrev(destSlot->cteMDBNode) == NULL' at src/object/cnode.c:457 in function cteInsert halting... Kernel entry via Syscall, number: 1, Call Cap type: 10, Invocation tag: 18 or a fault by the roottask (and not in the kernel). So - this is no issue for the kernel: Caught cap fault in send phase at address 0x0 while trying to handle: vm fault on data at address 0x18 with status 0x4 in thread 0xffffff800013c200 "child of: 'rootserver'" at address 0x20419cf [0] https://github.com/alex-ab/genode/blob/crash_sel4_kernel_vanilla/autoconfig… [1] https://github.com/alex-ab/genode/raw/crash_sel4_kernel_vanilla/image_bomb.… [2] https://github.com/alex-ab/genode/raw/crash_sel4_kernel_vanilla/sel4 [3] https://genode.org/download/tool-chain [4] https://sourceforge.net/projects/genode/files/genode-toolchain/17.05/ -- Alexander Boettcher Genode Labs http://www.genode-labs.com - http://www.genode.org Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth

2 3

Arm VMM Vchan
by Enrique Leon 26 Aug '17

26 Aug '17

Hello to All, I am trying to do some message passing between a vm component and a camkes component. I have tried by enabling the Vchan option on the build system and compiling the helloworld linux user level program on a tk1. I received an error about the /dev/vmm_manager not being able to open. What is the proper method of setting up the Vchan communication for camkes-arm-vmm on a tk1? Thank You

1 0

Re: [seL4] Devel Digest, Vol 39, Issue 26
by talos 25 Aug '17

25 Aug '17

Dear, I used "qemu-system-i386 -m 1024 -kernel images/kernel-ia32-pc99 -initrd images/capdl-loader-experimental-image-ia32-pc99" It showed "Booting from ROM" Thanks, Sincerely ------------------ Original ------------------ From: "devel-request";<devel-request(a)sel4.systems>; Date: Thu, Aug 24, 2017 10:00 AM To: "devel"<devel(a)sel4.systems>; Subject: Devel Digest, Vol 39, Issue 26 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: about camkesvm (Kofidoku.Atuah(a)data61.csiro.au) ---------------------------------------------------------------------- Message: 1 Date: Thu, 24 Aug 2017 00:00:19 +0000 From: <Kofidoku.Atuah(a)data61.csiro.au> To: <devel(a)sel4.systems> Subject: Re: [seL4] about camkesvm Message-ID: <1503532819201.94096(a)data61.csiro.au> Content-Type: text/plain; charset="iso-8859-1" Hey Talos, Sorry we didn't make this clearer on that page: those defconfigs build an x86-pc image; not an ARM image. Could you try running Qemu again, but with something similar to, qemu-system-i386 -m <WHATEVER_RAM_SIZE_YOU_WANT> -kernel <SEL4_KERNEL_IMAGE> -initrd <CAPDL_INITRD_IMAGE> And tell me what happens? Sorry for the inconvenience. -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO ________________________________ From: Devel <devel-bounces(a)sel4.systems> on behalf of talos <2486580938(a)qq.com> Sent: 22 August 2017 15:39 To: devel Subject: [seL4] about camkesvm Hi I started the tutorial following the link: https://wiki.sel4.systems/CAmkESVM I used "make minimal_defconfig" substituting "make cma34cr_minimal_defconfig" for int the directory config there is minimal_defconfig then make and qemu-system-arm -M kzm -nographic -kernel images/capdl-loader-experimental-image-ia32-pc99 but the error is Segmentation fault (core dumped) what's wrong? Thanks Sincerely -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://sel4.systems/pipermail/devel/attachments/20170824/cd4992b3/attachmen…> ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel ------------------------------ End of Devel Digest, Vol 39, Issue 26 *************************************

2 1

camkes-arm-vm Platform Support
by Robert VanVossen 25 Aug '17

25 Aug '17

Hello, Is Data61 or anyone else working on porting camkes-arm-vm to platforms other than the TK1? Thank you, Robbie VanVossen DornerWorks, Ltd.

2 1

about camkesvm
by talos 24 Aug '17

24 Aug '17

Hi I started the tutorial following the link: https://wiki.sel4.systems/CAmkESVM I used "make minimal_defconfig" substituting "make cma34cr_minimal_defconfig" for int the directory config there is minimal_defconfig then make and qemu-system-arm -M kzm -nographic -kernel images/capdl-loader-experimental-image-ia32-pc99 but the error is Segmentation fault (core dumped) what's wrong? Thanks Sincerely

2 1

Raspberry Pi3 + seL4
by Steven Johnston 23 Aug '17

23 Aug '17

Has anyone had issues with serial when running the test suite on a Raspberry Pi 3b? Currently I am following the blog post: https://research.csiro.au/tsblog/sel4-raspberry-pi-3/ In the seL4test project I have successfully compiled sel4test-driver-image-arm-bcm2837 from rpi3_debug_xml_defconfig. Along with this I have the following files: bootcode.bin, start.elf, u-boot.bin, and config.txt. Bootcode.bin and start.elf are from the current Raspian firmware. Config.txt just contains a line to enable UART ("enable_uart=1") and one to point and u-boot.bin ("kernel=u-boot.bin"). And per the comment section of the seL4 post I downgraded the version of u-boot to before March 2017 (currently using Jan 2017). I am not deviating from the blog posting but I am experiencing an issue not mentioned. I have no serial output (I do have a u-boot terminal prompt through HDMI, so I can load/boot the binary). When I boot seL4 I receive the misaligned cache messages (through HDMI) and then it hangs. Without serial I have no eyes to see if the seL4 tests are running. Other than wiring into the RPI3 UART (GND/TX/RX on pins 6/8/10) and enabling UART in config.txt is there another step I'm missing? Thanks for any direction you can point me in, Steve

2 2

VMM ARM SMP support
by Joyce Peng(彭美僑) 22 Aug '17

22 Aug '17

Hi seL4, I see below link to know VMM support SMP at Q3’17. I want to know does it ready and has any restriction? Thank you. https://sel4.systems/Info/Roadmap/ Low-level Userland Status Date Feature Location deferred to Q3’17 SMP-capable virtual-machine monitor (VMM) master Joyce.Peng (彭美僑)

1 0

Re: [seL4] mpu vs mmu
by Thomas Dundon 21 Aug '17

21 Aug '17

Thanks for the information. Looking at eChronos now. > > ---------- Forwarded message ---------- > From: <Ihor.Kuz(a)data61.csiro.au> > To: <devel(a)sel4.systems> > Cc: > Bcc: > Date: Sun, 20 Aug 2017 23:57:34 +0000 > Subject: Re: [seL4] mpu vs mmu > > > On 21 Aug 2017, at 8:05 am, Gernot.Heiser(a)data61.csiro.au wrote: > > > > On 21 Aug 2017, at 03:00, Thomas Dundon <dundon.thomas(a)gmail.com> wrote: > >> > >> Does an MPU, e.g. on a Cortex M3, provide enough functionality to > support seL4? > > > > No, it doesn’t. The seL4 model is fundamentally based on the ability to > virtualise hardware resources. > > > > If you don’t have that, then you can’t dod much more than a > memory-protected RTOS. If you’re after an RTOS with a (not yet complete) > verification story, look at eChronos: https://ts.data61.csiro.au/ > projects/TS/echronos/ > > > > In particular we have some work in the pipeline that adds (ARM > Cortex-M3/4) MPU support to eChronos (it’s currently in the process of > being code-reviewed and will be released after that). > > Ihor. > > > > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel > >

1 0

mpu vs mmu
by Thomas Dundon 21 Aug '17

21 Aug '17

Does an MPU, e.g. on a Cortex M3, provide enough functionality to support seL4? Thanks, Tom

3 2

i.MX7 Support?
by Steven Johnston 19 Aug '17

19 Aug '17

Has anyone had luck running the seL4test suite with an i.MX7 processor? I acquired a Toradex Colibri board (https://www.toradex.com/computer-on-modules/colibri-arm-family/nxp-freescal…) and am testing it out. Using the docker environment when I brew a seL4test config file either by hand or through menuconfig results in a 'libplatsupport' failure. There is platform support for the i.MX7 in the kernel source and imx7/armv7-a/cortex-a7 options in the seL4 git Makefile. Using the following make options results in another failure on multiple #error defines: "TOOLPREFIX=arm-none-eabi- ARCH=arm PLAT=imx7 ARMV=armv7-a CPU=cortex-a7 make" Thanks for any help or direction you can point me in, Steve

1 0

rumprun + rust + camkes
by Michal Podhradsky 18 Aug '17

18 Aug '17

Hello Kent, I extended the rumprun+rust example (available in this PR <https://github.com/seL4/camkes/pull/4>) with a simple camkes connection between the rumprum camkes component and a serial server component, as shown below (full code here <https://github.com/GaloisInc/camkes/blob/devel_rust_app/apps/rumprun_rust/r…> ): * composition {* * component rumprun_platform_layer rrpl;* * component rumprun_rust hello1;* * RUMPRUN_META_CONNECTION(hello1, rrpl)* * component rumprun hello2;* * RUMPRUN_META_CONNECTION(hello2, rrpl)* * component Server server;* * connection seL4SharedData conn(from hello1.camkes_buffer, to server.buffer);* * connection seL4Notification simpleEvent1(from hello1.camkes_ev, to server.ev);* * connection seL4Notification simpleEvent2(from server.ev1, to hello1.camkes_ev1);* * }* I added a simple rust program <https://github.com/GaloisInc/camkes/blob/devel_rust_app/apps/rumprun_rust/c…> (running on rumprun_rust): *fn main() {* * println!("Hello rust!");* * unsafe {* * camkes_ev_emit();* * }* * println!("Waiting for event!");* * unsafe {* * camkes_ev1_wait();* * }* * println!("Got event!");* *}* *#[no_mangle]* *extern {* * fn camkes_ev_emit();* * fn camkes_ev1_wait(); * *}* In order to compile the cargo project, I added a build.rs script <https://github.com/GaloisInc/camkes/blob/devel_rust_app/apps/rumprun_rust/c…> to package the generated camkes object file (camkes.o) into an archite that cargo can link against. The problem is, that the generated camkes.c file contains its own main function: *int USED main(int argc UNUSED, char *argv[]) {* * assert(argc == 2);* * assert(strcmp(argv[0], "camkes") == 0);* * int thread_id = (int)(uintptr_t)(argv[1]);* * return post_main(thread_id);* *}* which collides with the *fn main()* defined in rust. (I get *multiple definition of `main'* error). How is this handled in rumprun_ethernet <https://github.com/GaloisInc/camkes/blob/devel_rust_app/apps/rumprun_ethern…> example? There is also a main function for the rumpkernel component <https://github.com/GaloisInc/camkes/blob/devel_rust_app/apps/rumprun_ethern…>, and the main() from camkes, but the compilation process handles this correctly. Could you point me in the right direction? Regards Michal

2 6

Can I run Android on camkes-arm-vm with tk1 board?
by li94575 05 Aug '17

05 Aug '17

Hi, Now, Linux4.3 kernel can work well on camkes-arm-vm, does that mean we can run an Android system based on this kernel? I have tried to replace the roofs with an Android ramdisk, but Linux can not excute the Init program. The error is showing below: [ 10.598871] Freeing unused kernel memory: 4168K (c0a74000 - c0e86000) [ 10.761443] Kernel panic - not syncing: Attempted to kill init! exitcode=0x00000004 [ 10.761443] [ 10.770568] CPU: 0 PID: 1 Comm: init Tainted: G W 4.3.0-rc5-00024-gec4c02c-dirty #122 [ 10.779510] Hardware name: NVIDIA Tegra SoC (Flattened Device Tree) [ 10.785795] [<c00167ec>] (unwind_backtrace) from [<c0012958>] (show_stack+0x10/0x14) [ 10.793537] [<c0012958>] (show_stack) from [<c008f054>] (panic+0x94/0x220) [ 10.800407] [<c008f054>] (panic) from [<c0025b9c>] (do_exit+0x7fc/0x8f4) [ 10.807101] [<c0025b9c>] (do_exit) from [<c0025d70>] (do_group_exit+0x3c/0xf0) [ 10.814318] [<c0025d70>] (do_group_exit) from [<c002f3ec>] (get_signal+0x1a4/0x754) [ 10.821971] [<c002f3ec>] (get_signal) from [<c001a748>] (do_signal+0x84/0x61c) [ 10.829188] [<c001a748>] (do_signal) from [<c0012604>] (do_work_pending+0xa4/0xb4) [ 10.836750] [<c0012604>] (do_work_pending) from [<c000f6b4>] (slow_work_pending+0xc/0x20) [ 10.844919] ---[ end Kernel panic - not syncing: Attempted to kill init! exitcode=0x00000004 Is this a problem that current VMM does not support FPU? or other reasons caused the problem？

2 11

rumprum and camkes
by Michal Podhradsky 05 Aug '17

05 Aug '17

Hello all, mostly Kent, I read your blog post about rumpkernels on sel4: https://research.csiro.au/tsblog/using-rump-kernels-to-run-unmodified-netbs… and after experimenting with the rumprun apps (such as the ethernet one <https://github.com/seL4/camkes/tree/master/apps/rumprun_ethernet>) I think it is a great addition to sel4. So I have few questions. I need to run two different rumpkernels, each with its own address space, connected only through dataports/events. 1- does the current rumpkernel backend support having this separation? According to your thesis <http://www.disy.cse.unsw.edu.au/theses_public/16/kentm.pdf>, all rumpkernel threads run in a single sel4 thread - is that correct? 2- Right now, I can combine multiple rumprun components in one application (lets say *runmprun_hello* and *rumprun_pthreads*). butI can have only one rumprun_platform_layer per application, correct? An example below: *assembly {* * composition {* * component rumprun_platform_layer rrpl;* * component rumprun hello;* * RUMPRUN_META_CONNECTION(hello, rrpl)* * component rumprun_pthreads pthreads;* * RUMPRUN_META_CONNECTION(pthreads, rrpl)* * }* * configuration {* * hello.rump_config = {"cmdline": "hello World!" };* * RUMPRUN_COMPONENT_CONFIGURATION(hello, 0)* * pthreads.rump_config = {"cmdline": "./pthreads_test 4" };* * RUMPRUN_COMPONENT_CONFIGURATION(pthreads, 1)* * }* *}* If I instantiate another *rumprun_platform* component, it wont compile. 3 - how can I go around defining/adding my own rumpkernels? Lets say I want to build a rumpkernel with rust support <https://github.com/rumpkernel/rumprun-packages/tree/master/rust> (you have an sel4 example here <https://github.com/SEL4PROJ/rumprun-sel4-demoapps/tree/master/userapps/rust>) and integrate it with the rumprun_hello <https://github.com/seL4/camkes/blob/master/apps/rumprun_hello/rumprun_hello…> app. Regards Michal

2 1

camkes-vm cma34cr_picotcp doesn't build
by Michal Podhradsky 05 Aug '17

05 Aug '17

Hello, when I do a fresh init of the camkes-vm repository: *repo init -u https://github.com/seL4/camkes-vm-manifest <https://github.com/seL4/camkes-vm-manifest>* *repo sync* and then I want to build the cma34cr_picotcp app: *make clean* *make make cma34cr_picotcp_defconfig* *make silentoldconfig* *make* I get the following error: *Makefile:76: *** No CAmkES application selected. Stop.* Do you guys have any CI server set up? If not, I would be happy to help set something up, this is not the first time an existing configuration doesn't build. Regards Michal

2 2

network on seL4
by Gábor Székely 03 Aug '17

03 Aug '17

Hi, I would like to use network (TCP) on seL4, I know that I should probably be using lwip, however I have no idea how to properly initialize it (this is the first time I'm working in such a hardware close environment), so I need some help or some kind of example, but I don't know where to look. I'm working on ia32. I also tried to run the rumprun hello world, the compillation finishes, however I get the following output when I try to run it: https://pastebin.com/MiMB0N62 Regards, Gábor Székely

4 4

rump kernel test, compilation issues
by Steven Harp 31 Jul '17

31 Jul '17

A couple of issues building the latest seL4 NetBSD rumpkernel demoapps, hello-ia32-x86_64_qemu_defconfig / hello-x86_64-x86_64_qemu_defconfig. (Ref: https://github.com/SEL4PROJ/rumprun-sel4-demoapps ) 1. In libsel4muslcsys sys_morecore.c: > /host/libs/libsel4muslcsys/src/sys_morecore.c:248:16: error: ‘vaddr’ undeclared (first use in this function) > return vaddr; > ^ Speculatively, should it return: (long) placement_vaddr ? 2. In rumprun/platform/sel4/entry.c > entry.c:91:9: error: implicit declaration of function 'allocman_add_untypeds_from_timer_objects' [-Werror=implicit-function-declaration] > allocman_add_untypeds_from_timer_objects(allocator, env->custom_simple.timer_config.hw.to); Not sure where this function should be found... Same results in native build (Xenial) and in docker build container. Any suggestions warmly appreciated. // Steve

2 1

Recursive call to malloc crash system
by Fabrizio Bertocci 27 Jul '17

27 Jul '17

Hi all, I have a system configured to use dynamic heap through the vspace. I'm working with 5.2.0 and using pc99 simulator through qemu. Everything is occurring in the root task, as I haven't even completed my bootstrapping code. In this configuration, whenever my code calls malloc() and there is a low memory condition (where there is not enough space on the heap to fulfill my request), malloc() end up calling __expand_heap(). Here it first attempts to expand the heap through brk syscall, then if fails uses mmap() to attempt to get more pages from the virtual memory. In both cases (brk and mmap) end up calling a function in the vspace that attempts to make available new pages. Unfortunately the code in the libself4utils/src/vspace/vspace.c, end up calling malloc() for the sel4utils_res structure. As you expect, we are already in a no-memory condition, so a subsequent call to malloc() might end up calling __expand_heap() and so on... (depending on the bytes left on the heap, this nested malloc might succeed if the initial block was larger than the size of sel4utils_res structure). So, everything loops until the whole system crash because of stack overflow. Why vspace uses malloc() to dynamically allocate those structures, causing the whole system to fail? To test, I have changed the implementation in vspace.c to use a static buffer pool, and it seems it solve my issue, but am I doing something wrong in the bootstrap code ? Any help is appreciated, Regards, Fabrizio Bertocci Real-Time Innovations, Inc. Sunnyvale, CA

3 4

Invalid package ID: "array-0.5.1.1 base-4.9.0.0 binary-0.8.3.0 bytestring-0.10.8.1"
by tj5527 23 Jul '17

23 Jul '17

Another problem when making sel4. The make program complains Invalid package ID: "array-0.5.1.1 base-4.9.0.0 binary-0.8.3.0 bytestring-0.10.8.1". [parse-capDL] building... make: Entering directory '/path/to/sel4/projects/capdl/capDL-tool' stack setup stack will use a locally installed GHC For more information on paths, see 'stack path' and 'stack exec env' To use this GHC and packages outside of a project, consider using: stack ghc, stack ghci, stack runghc, or stack exec stack build --only-dependencies Invalid package ID: "array-0.5.1.1 base-4.9.0.0 binary-0.8.3.0 bytestring-0.10.8.1" Makefile:39: recipe for target 'sandbox' failed make: *** [sandbox] Error 1 How can I fix this? Thank you. Ubuntu 16.04 LTS GNU Make 4.1 gcc version 5.4.0 20160609

3 4

Sydney `taste of seL4' miniconference/developer day
by Peter.Chubb＠data61.csiro.au 19 Jul '17

19 Jul '17

Hi Folks, Next January 22--26, linux.conf.au will be in Sydney, Australia. We're planning on submitting a proposal for a one-day miniconference to be held in conjunction with the main conference. We'd like to line up potential speakers now, before submitting. If you are doing something cool and open source with seL4, and would like to speak at that miniconference, please let me know. linux.conf.au is one of the best grass-roots open-source and Linux conferences around; if you're doing anything cool that's open source with seL4 (or with Linux), then I'd encourage you to submit a proposal to the main conference as well, at https://linux.conf.au/ Peter Chubb -- Dr Peter Chubb Tel: +61 2 9490 5852 http://ts.data61.csiro.au/ Trustworthy Systems Group Data61 (formerly NICTA)

1 0

Question on endpoint cap write permission
by Jimmy Brush 13 Jul '17

13 Jul '17

Hello, in the 6.0 manual section 3.1.4 the table shows that Write permission on an endpoint cap permits sending to the endpoint. however, in section 4.2.2 it says without the Write permission on the RECEIVING endpoint cap, any cap sent over IPC gets diminished. Am I missing something? It seems the Write permission is overloaded to mean two different things. This would seem to imply that to receive an undiminished capability via IPC you must have both send and receive permission to the endpoint you are receiving against. Which would mean if you wanted to limit someone to only receiving and never sending against an endpoint by giving them an endpoint cap with only Read permission, they would necessarily also NEVER be able to receive an undiminished capability. Thanks, JB

4 5

Compile problems about camkes-vm project
by deng.chao1＠zte.com.cn 11 Jul '17

11 Jul '17

SGkgZXZlcnlvbmU6DQoNCiAgSSB0cnkgdG8gcnVuIHZtIG9uIHNlTDQuIA0KDQogIEkgaGF2ZSBk b3dubG9hZGVkIFZNIHByb2plY3QgdXNpbmcgInJlcG8gaW5pdCAtdSBodHRwczovL2dpdGh1Yi5j b20vc2VMNC9jYW1rZXMtdm0tbWFuaWZlc3QuZ2l0Ii4gDQoNCiAgSSB1c2UgY29tbWFuZHM6DQoN CiAgICAgIG1ha2UgY21hMzRjcl90d292bV9kZWZjb25maWcNCg0KICAgICAgbWFrZSBzaWxlbnRv bGRjb25maWcNCg0KICAgICAgbWFrZSANCg0KdG8gY29tcGlsZSB0aGUgcHJvamVjdCwgYnV0IGhl cmUgcmVwb3J0cyBwcm9ibGVtcy4NCg0KICBUaGUgZmlyc3QgcHJvYmxlbSBpcywgaXQgY2FuIG5v dCBmaW5kIGxpYnBpY290Y3AuIEkgaGF2ZSBjaGVjayB0aGUgc291cmNlIGNvZGUsIGl0IGRvZXNu J3QgaW5jbHVkZSBkaXJlY3RvcnkgbGlicy9saWJwaWNvdGNwLy4NCg0KU28gSSBnZXQgcmlkIG9m IHRoZSBsaWJwaWNvdGNwIHBhcnQgYnkgY29tbWVudCBpdCBpbiB0aGUgS2NvbmZpZyBmaWxlLg0K DQogIE5leHQsIHRoZSBvdGhlciBwcm9ibGVtIGFjY3VycyBhcyBibG93aW5nOg0KDQoJIi9ob21l L2RlbmdjaGFvL21qL2NhbWtlcy12bS90b29scy9jYW1rZXMvY2Fta2VzLm1rOjEzNzogL2hvbWUv ZGVuZ2NoYW8vbWovY2Fta2VzLXZtL2J1aWxkL3g4Ni9wYzk5L2NtYTM0Y3JfdHdvdm0vY2Fta2Vz LWdlbi5tazogTm8gc3VjaCBmaWxlIG9yIGRpcmVjdG9yeQ0KDQogCVtHRU5dIGNhbWtlcy1nZW4u bWsNCg0KCUVSUk9SOkNBbWtFUzovaG9tZS9kZW5nY2hhby9tai9jYW1rZXMtdm0vYXBwcy9jbWEz NGNyX3R3b3ZtL3ZtLmNhbWtlczoyMzoxOTogICAgICAgICBjb21wb25lbnQgRWNobyBlY2hvDQoN CglFUlJPUjpDQW1rRVM6ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIF5eXl5eXg0KDQoJRVJST1I6 Q0Fta0VTOm5vbi1vcHRpb25hbCBpbnRlcmZhY2UgZWNoby50aW1lciBpcyBub3QgY29ubmVjdGVk DQoNCgltYWtlWzFdOiAqKiogWy9ob21lL2RlbmdjaGFvL21qL2NhbWtlcy12bS9idWlsZC94ODYv cGM5OS9jbWEzNGNyX3R3b3ZtL2NhbWtlcy1nZW4ubWtdIGVycm9yIDI1NSINCg0KICANCg0KICBJ IGhhdmUgdHJpZWQgY29uZmlnIHRoZSBwcm9qZWN0IHRvIGNtYTM0Y3Jfc2luZ2xldm1fZGVmY29u ZmlnIG9yIGNtYTM0Y3JfdWJ1bnR1X2RlZmNvbmZpZywgYWxzbyByZXBvcnMgdGhlIHNhbWUgZXJy b3IuDQoNCiAgQW5kIHRoZSBjMTYyX3R3b3ZtIGNvbmZpZywgc2VlbXMgaXQgaGFkIGFsc28gYmVl biByZW1vdmVkIGZvciB0aGUgY2Fta2VzLXZtIHByb2plY3Q/DQoNCiAgQ291bGQgYW55b25lIHJl bHkgbWUgb24gdGhlIGtpbmRuZXNzPw0KDQoJCQkJCQkJCSAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgICAgICAgIHlvdXJzIERlbmdDaGFv

2 1

L4Re IPC share memory that share file in one Linux filesystem and be visible to other Linuxes
by Joyce Peng(彭美僑) 05 Jul '17

05 Jul '17

Hi L4, I want to share a file in one Linux filesystem and be visible to other Linuxes that all run on top Fiasco.OC. It seems an IPC communication between L4re vm tasks. And access a file in Linux filesystem is a mechanism with kernel block device driver. But I only notice two char device drivers that use L4re library l4shmc in L4linux. It is l4ser_shm and l4shmnet. May you give some information about this work how to work. Thanks. Joyce Peng(彭美僑)

2 1

malloc & errno
by Fabrizio Bertocci 05 Jul '17

05 Jul '17

Hi all, I am facing a puzzling problem related to muslc. While running some tests with the ia32 simulator (qemu), have noticed that whenever I call malloc() and I run out of memory (because my morecore buffer is too small), I am getting some kernel crash. I have traced the issue to the place where errno is set to -ENOMEM. Referencing to errno is platform-dependent and end up calling a function that retrieve the struct pthread associated and access errno as one of the field of the struct pthread. What is the correct process to set up a heap from the root task in such a way that we can call malloc() and correctly handle error conditions through errno? I am pretty sure I am doing something wrong in my initialization code (I have based my main(0 on the code from the tutorials), because I am also having other problems with malloc(). (even after I increase my heap area). For example, in some cases a call to malloc() end up calling a cascade of functions that eventually (from inside muslc) end up calling again malloc(). As consequence it enters in an infinite loop that stop only after it exhaust the initial stack. I could not find any clear example that show how to correctly set up a system to use muslc. Can anyone point me to a good example that shows how to bootstrap a system for the 5.2.0 branch? Regards, Fabrizio Bertocci Real-Time Innovations, Inc. Sunnyvale, CA

2 1

make: stack: Command not found
by tj5527 04 Jul '17

04 Jul '17

A newbie question. I follow the link [1] trying to build sel4 with qemu. But when `make`ing the binary, it throws error message `make: stack: Command not found`. I `apt-get install stacks` but it still fails with the same error. What packages should I install for making sel4 with Ubuntu 16.04 LTS, GNU Make 4.1, and gcc version 5.4.0 20160609? Thanks [Error Message] -- Build files have been written to: /path/to/sel4/stage/x86/pc99/accelerator ninja: no work to do. [apps/vm] building... [HEADERS] [STAGE] autoconf.h [apps/vm] done. [parse-capDL] building... make: Entering directory '/path/to/sel4/projects/capdl/capDL-tool' stack setup make: stack: Command not found Makefile:39: recipe for target 'sandbox' failed make: *** [sandbox] Error 127 make: Leaving directory '/path/to/sel4/projects/capdl/capDL-tool' Makefile:53: recipe for target '/path/to/sel4/stage/x86/pc99/parse-capDL/parse-capDL' failed make: *** [/path/to/sel4/stage/x86/pc99/parse-capDL/parse-capDL] Error 2 [1] https://wiki.sel4.systems/Hardware/Qemu

1 1

elfloader-tool
by Yevgeny Lavrov 30 Jun '17

30 Jun '17

Hi Is there any instruction on how to compile and use elfloader-tool? More specifically: I want to link seL4 image with other image to try out on i.MX6 platform. Thanks

2 1

vmm documentation
by Mike Clark 29 Jun '17

29 Jun '17

Is there any documentation on how the VMM works? If I wanted to start hacking on the VMM and extend its capability, where should I start looking to learn how it works, etc? That might be a pretty broad topic, because there are lots of ways the VMM can be extended, I'm sure. Broad is fine, until I get things more figured out.

4 17

Why armel for the seL4 ARM VMM?
by John Backes 27 Jun '17

27 Jun '17

I was curious why the ARM VMM for the TK1 only seems to support the use of armel based distributions? Does special care need to be taken in the VMM to handle guest floating point instructions if the OS is armhf based? - John

2 1

How does the seL4 kernel revoke frame cap?
by Norrathep Rattanavipanon 24 Jun '17

24 Jun '17

Hello, I was wondering when we call seL4_cnode_delete on a (mapped) frame cap, does the kernel also handle unmapping the frame (in addition to withdrawing authority) as well? Or the user-space has to ensure that the frame is unmapped first before calling delete? I tried my code without unmapping that frame when deleting the cap and it seems to work fine. So I guess the kernel handles that? Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

3 5

Tutorial app hello-camkes-mcs not working
by Nicholas VanderStel 24 Jun '17

24 Jun '17

I've been able to build and run the hello-camkes-mcs example app from the camkes-mcs-tutorials.xml manifest both on a SabreLite board and in QEMU. However, when I try to run the app with the budget and period values given in the solution file, the client tasks don't appear to be running as they should. See the output from running on the SabreLite here: https://pastebin.com/RM0aisyF After that point it seems to hang. I tried smaller budget & period values and have been able to get one client task running, but the second task doesn't appear to be running. Has anyone been able to run this example with different results? Thanks, Nick VanderStel

1 0

Help with libethdriver
by Fabrizio Bertocci 22 Jun '17

22 Jun '17

Hi all, I am facing an issue with our existing project (currently based on seL4 1.0). I am in the process of migrating our project to the latest version of seL4. After all the required changes I am facing a problem I need some help. In our code, we use libplatsupport for timer & serial I/O as well as the libethdriver in order to use the network interface of the IMX6 board. The problem appears that the IOMUX device registers are mapped twice. A first time from libplatsupport (and never released): -> sel4platsupport_new_io_ops() -> calls: mux_sys_init() -> calls the macro: MAP_IF_NULL(io_ops, IMX6_IOMUXC, _mux.iomuxc); This end up mapping the device region IMX6_IOMUXC: 0x20e0000 - 0x20e100 (size_bits=12). So far so good... but then they are mapped again from the ethernet driver: ethif_new_lwip_driver_no_malloc() -> call my initialization fn -> call ethif_imx6_init() -> call setup_iomux_enet() that end up mapping again the region @ IOMUXC_PADDR = 0x20e1000 This second time, the mapping function _utspace_split_alloc fails because apparently the region 0x20e000 has been already mapped (and is not in the regions available). If I comment out the call to mux_sys_init() in libsel4platsupport_new_io_ops() my ethernet driver successfully initialize (but clearly that's not the correct workaround). Any suggestions? Regards, Fabrizio Bertocci Real-Time Innovations, Inc. Sunnyvale, CA

2 1

Questions about TK1-SOM Memory Management
by Daniel Wang 22 Jun '17

22 Jun '17

Hi Adrian, Thank you very much for your explain. I might have some misunderstanding about the source code. First may I ask what the kernel window means? Does it means the virtual memory space kernel can access (through pptr_t)? I can see the dev_p_regs[] (kernel/src/plat/tk1/machine/hardware.c) has multiple parts: the first is the RAM part, VM_HOST_PA_START - VM_HOST_PA_START + VM_HOST_PA_SIZE (0xb0000000 — 0xf0000000), the rest are real device region from 0x01000000 - 0x7c000000 approximately. I guess my question is why put the second half as a “device” instead of putting it together in avail_p_regs[]? Is it somehow due to the support of virtualization? Here is the booting procedure according to my understanding, could you take a look and see if I got it right? 1. the code start at the ELF-loader main() (tools/elfloader/src/arch-arm/boot.c) which is loaded in physical memory 0x82000000 for TK1 (tools/elfloader/gen_boot_image.sh) 2. the boot code unpack the ELF and find the kernel image and the user-land image, the kernel is loaded at 0x80000000 the user land image is loaded at 0x80037000 approximately 3. MMU is enabled and a “boot" page directory is created that maps physical 0x80000000 to (0xe0000000 - 0xf0000000) 4. enter the kernel code _start, which setup up vector table and kernel stack; then init_kernel(); then try_init_kernel() calls map_kernel_window() I’m not sure why map_kernel_windows() remap the virtual address kernelBase (start from 0xe0000000) to physical address physBase (0x80000000) again or did I miss anything? Also I’m not sure what those armHSGlobalPGD[], armHSGlobalPD[] for, I assume it is for context switch? (deleted diagram due to size limit) Thanks -Dan

2 3

drivers in seL4
by 杰尔米 22 Jun '17

22 Jun '17

Hi all， I want to know more about the mechanism of device driver in seL4. How does seL4 support userspace drivers? if I want to write a driver(e.g. serial port) base on seL4, how to do that? can any one help? Best Regards! Jeremy

3 2

Questions about TK1-SOM Memory Management
by Daniel Wang 20 Jun '17

20 Jun '17

Hi all, I’m trying to get a better understand about the implementation details of seL4 for TK1-SOM. Most of the code are very clear, but I’m little confused on the available physical memory in TK1-SOM. I’m wondering why In the hardware.c file (/kernel/src/plat/tk1/machine/hardware.c), the avail_p_regs[] ={.start = 0x80000000, .end = 0xa7f00000 } instead of 0x80000000 - 0xffffffff? Thank you very much! -Dan

2 1

Linux binaries constructed by Buildroot cannot run on tk1 board
by li94575 20 Jun '17

20 Jun '17

Hi， I use Buildroot 2016.08.1 with the config "buildroot_tk1_initrd_defconfig" to compile linux-tegra(https://github.com/SEL4PROJ/linux-tegra/tree/sel4), everything goes well. But the linux binary cannot output any logs, camkes-arm-vm stops at “Starting VM”. Can anyone tells me where might be wrong? I have tried using cross-compiler arm-none-linux-gnueabi-(2014.05) to compile linux-tegra, and that linux binary can work.

2 4

seL4test with 4.0, 5.1 failed on Ubuntu
by Daniel Wang 16 Jun '17

16 Jun '17

Hi all, I’m testing the new versions of seL4 (,4.0, 5.0, 5.1, etc.) using the sel4test-manifest. I tried both Ubuntu 16 and Ubuntu 14. For 3.2 version both I32 and KZM_simulation built just fine. However for the higher version (4.0. 5.1, 5.2) only I32 built properly. KZM_simulation keep failing on both Ubuntu 14 and 16. Anyone has the similar issues? Thanks -Dan FYI: [apps/sel4test-tests] done. [KERNEL] [MKDIR] src/arch/arm/api [PBF_GEN] arch/object/structures.pbf [PBF_GEN] arch/api/shared_types.pbf [PBF_GEN] plat/machine/hardware.pbf [PBF_GEN] api/types.pbf [BF_GEN] arch/object/structures_gen.h [BF_GEN] arch/api/shared_types_gen.h [BF_GEN] plat/machine/hardware_gen.h [BF_GEN] api/types_gen.h [CPP] src/arch/arm/armv/armv6/machine_asm.s_pp [AS] src/arch/arm/armv/armv6/machine_asm.o [CPP] src/arch/arm/32/halt.s_pp [AS] src/arch/arm/32/halt.o [CPP] src/arch/arm/32/head.s_pp [AS] src/arch/arm/32/head.o [CPP] src/arch/arm/32/idle.s_pp [AS] src/arch/arm/32/idle.o [CPP] src/arch/arm/32/traps.s_pp [AS] src/arch/arm/32/traps.o [CPP] src/arch/arm/32/hyp_traps.s_pp [AS] src/arch/arm/32/hyp_traps.o [TOUCH] sources_list_updated [CPP_GEN] kernel_all.c [CPP] kernel_all.c_pp [CP] kernel_final.c [CC] kernel_final.s /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c: In function ‘doFlush’: /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:1929:10: error: ‘ARMPDClean_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:1929:10: note: each undeclared identifier is reported only once for each function it appears in /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:1930:10: error: ‘ARMPageClean_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:1933:10: error: ‘ARMPDInvalidate_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:1934:10: error: ‘ARMPageInvalidate_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:1937:10: error: ‘ARMPDCleanInvalidate_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:1938:10: error: ‘ARMPageCleanInvalidate_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:1941:10: error: ‘ARMPDUnify_Instruction’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:1942:10: error: ‘ARMPageUnify_Instruction’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c: In function ‘decodeARMPageDirectoryInvocation’: /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2217:10: error: ‘ARMPDClean_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2218:10: error: ‘ARMPDInvalidate_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2219:10: error: ‘ARMPDCleanInvalidate_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2220:10: error: ‘ARMPDUnify_Instruction’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c: In function ‘decodeARMPageTableInvocation’: /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2335:21: error: ‘ARMPageTableUnmap’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2344:41: error: ‘ARMPageTableMap’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c: In function ‘decodeARMFrameInvocation’: /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2440:10: error: ‘ARMPageMap’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2562:10: error: ‘ARMPageRemap’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2680:10: error: ‘ARMPageUnmap’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2699:10: error: ‘ARMPageClean_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2700:10: error: ‘ARMPageInvalidate_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2701:10: error: ‘ARMPageCleanInvalidate_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2702:10: error: ‘ARMPageUnify_Instruction’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2772:10: error: ‘ARMPageGetAddress’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c: In function ‘decodeARMMMUInvocation’: /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2818:45: error: ‘ARMASIDControlMakePool’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2887:45: error: ‘ARMASIDPoolAssign’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/Makefile:566: recipe for target 'kernel_final.s' failed make[1]: *** [kernel_final.s] Error 1 tools/common/project.mk:254: recipe for target 'kernel_elf' failed make: *** [kernel_elf] Error 2

2 2

seL4_Fault_t and friends seems to be missing in user libsel4
by Alexander Boettcher 15 Jun '17

15 Jun '17

Hello, if I compile and link seL4 5.2.0 ARCH=x86 PLAT=pc99 SEL4_ARCH=x86_64 make and I finally try to use the generated syscall/libsel4 headers, the compiler complains about missing seL4_Fault types and functions in libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/faults.h like seL4_Fault_t seL4_Fault_tag seL4_Fault_VMFault_new and a lot more. These structs and functions seems to be generated only for the kernel side, e.g. in kernel_final.c they show up, but there are no traces of them on the user level side. Do I just miss a configuration option ? Thanks, -- Alexander Boettcher Genode Labs http://www.genode-labs.com - http://www.genode.org Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth

2 4

[Camkes] Is there any way to declare hierarchical header files and does CamKES support C++ boost preprocessor?
by Tran Cuong 14 Jun '17

14 Jun '17

Hello everybody, I'm conducting a C-project, in which the code is utilizing boost library to define several macros. This source code is running well in Linux and using only standard C library (I had tested this libraries individually by some mini-programs on CamKES). My project is organized as follows: - Top folder: + "components" folder contains my c code + "include" folder contains 1 .h file boost1.h and 1 folder test ++ sub-folder "test" contains 1 file boost2.h ++ content of boost1.h is just include "test/boost2.h" + "Makefile" is declared as below: TARGETS := $(notdir ${SOURCE_DIR}).cdl ADL := tst-macro.camkes Client_CFILES := \ $(patsubst ${SOURCE_DIR}/%,%,$(wildcard ${SOURCE_DIR}/components/Client/src/*.c)) \ $(patsubst ${SOURCE_DIR}/%,%,$(wildcard ${SOURCE_DIR}/components/Client/src/plat/${PLAT}/*.c)) \ $(patsubst ${SOURCE_DIR}/%,%,$(wildcard ${SOURCE_DIR}/components/Client/src/arch/${ARCH}/*.c)) Client_ASMFILES := \ $(patsubst ${SOURCE_DIR}/%,%,$(wildcard ${SOURCE_DIR}/components/Client/crt/arch-${ARCH}/crt0.S)) \ $(patsubst ${SOURCE_DIR}/%,%,$(wildcard ${SOURCE_DIR}/components/Client/src/*.S)) \ $(patsubst ${SOURCE_DIR}/%,%,$(wildcard ${SOURCE_DIR}/components/Client/src/arch/${ARCH}/*.S)) \ $(patsubst ${SOURCE_DIR}/%,%,$(wildcard ${SOURCE_DIR}/components/Client/src/plat/${PLAT}/*.S)) Client_HFILES := \ $(patsubst ${SOURCE_DIR}/%,%,$(wildcard ${SOURCE_DIR}/components/Client/include/*)) include ${PWD}/tools/camkes/camkes.mk - This above Makefile, I imitated from another application, and when I compiled the project, there are some errors related to directory of "test/boost2.h". I suspect that there is something wrong with Client_HFILES declaration, since maybe it is only valid for a list of .h files, not for hierarchical folders. - I really want to dive into CamKES, but I only have a little knowledge about this. My project is due so I hope to get some positive advice from you for 2 questions: + The right way to declare multi-level libraries as in my example. + Besides, does CamKES support boost preprocessing lib. Currently I'm using the toolchain arm-none-eabi- Thank all of you for the time and attention. Dinh-Cuong -- ------------------- TRAN Dinh Cuong (Mr) Email : cuongtd4(a)gmail.com

2 2

Trustworthy and mixed critical
by Jonathan C Day 14 Jun '17

14 Jun '17

Dear all, The first of these terms has an... interesting history. In a nutshell, it's not always used appropriately. Clearly that's not going to be the case with SEL4, but what exactly is meant? Mixed critical is another term that I'm cautious over. It's not completely clear to me if the mixing refers to relaxed constraints for utilisation reasons or something else. (Correct me if I'm mistaken, but I don't think SEL4 implements FLASK, which would be the obvious way to provide differing constraints, relaxed constraints within the trusted computing model. It's totally the wrong level.) I have absolutely no doubt SEL4 will retain all the provable integrity ever claimed (by anyone involved), but this experimental-proto-main branch confuses me on what fundamentally changes. Jonathan Day

2 1

Compilation of seL4 kernel 5.2.0
by Alexander Boettcher 14 Jun '17

14 Jun '17

Hello, I want to compile just the seL4 kernel (5.2.0) and tried it by invoking: alex@max:~/sel4.git$ ARCH=x86 PLAT=pc99 SEL4_ARCH=ia32 make but the compile fails (attached below). Do I need to setup/configure something beforehand ? It seems some defines are not set. The host is a 64bit Ubuntu 16.04 LTS. Thanks, Alex. alex@max:~/sel4.git$ git log commit 3695232f9603af60d56f97072082d90f30e98b0e Author: Kent McLeod <Kent.Mcleod(a)data61.csiro.au> Date: Wed May 31 17:21:29 2017 +1000 update VERSION file to 5.2.0 alex@max:~/sel4.git$ ARCH=x86 PLAT=pc99 SEL4_ARCH=ia32 make [MKDIR] arch/object [PBF_GEN] arch/object/structures.pbf [PBF_GEN] plat/32/plat_mode/machine/hardware.pbf [PBF_GEN] 32/mode/api/shared_types.pbf [BF_GEN] arch/object/structures_gen.h [BF_GEN] plat/32/plat_mode/machine/hardware_gen.h [BF_GEN] 32/mode/api/shared_types_gen.h [CPP] src/arch/x86/32/machine_asm.s_pp [AS] src/arch/x86/32/machine_asm.o [CPP] src/arch/x86/32/traps.s_pp [AS] src/arch/x86/32/traps.o [CPP] src/arch/x86/32/head.s_pp [AS] src/arch/x86/32/head.o [CPP] src/arch/x86/multiboot.s_pp [AS] src/arch/x86/multiboot.o [TOUCH] sources_list_updated [CPP_GEN] kernel_all.c [CPP] kernel_all.c_pp In file included from ./include/arch/x86/arch/fastpath/fastpath.h:14:0, from src/arch/x86/32/c_traps.c:15: ./include/arch/x86/arch/32/mode/fastpath/fastpath.h:137:2: error: #error "Invalid method to set IPCBUF/TLS" #error "Invalid method to set IPCBUF/TLS" ^ ./include/arch/x86/arch/32/mode/fastpath/fastpath.h:168:2: error: #error "Invalid method to set IPCBUF/TLS" #error "Invalid method to set IPCBUF/TLS" ^ src/arch/x86/32/c_traps.c:198:2: error: #error "Invalid method to set IPCBUF/TLS" #error "Invalid method to set IPCBUF/TLS" ^ src/arch/x86/32/c_traps.c:238:2: error: #error "Invalid method to set IPCBUF/TLS" #error "Invalid method to set IPCBUF/TLS" ^ Makefile:729: recipe for target 'kernel_all.c_pp' failed make: *** [kernel_all.c_pp] Error 1 rm plat/32/plat_mode/machine/hardware_gen.h 32/mode/api/shared_types_gen.h src/arch/x86/32/machine_asm.s_pp src/arch/x86/32/traps.s_pp src/arch/x86/multiboot.s_pp arch/object/structures_gen.h src/arch/x86/32/head.s_pp -- Alexander Boettcher Genode Labs http://www.genode-labs.com - http://www.genode.org Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth

2 2

seL4-test on Beaglebone black
by Fabrizio Bertocci 14 Jun '17

14 Jun '17

Hi, I am posting this email as reference to anyone who want/need to run seL4 on a BeagleBone Black (BBB). The post at https://wiki.sel4.systems/Hardware/Beaglebone is great, unfortunately even if I followed exactly those instructions, I ended up hitting some walls here and there. I eventually managed to solve those issues and run successfully seL4test on my BBB. First of all the build system. I have tried unsuccessfully to find arm-linux-eabi for CentOS 7 (my preferred distribution for building on Linux), but apparently is an easy-to-find only on Ubuntu... so I ended up creating a VM with Ubuntu 16.04. If someone knows how to get arm-linux-eabi on CentOS please let me know... Unfortunately even with Ubuntu not everything went as smooth as I hoped. It appears that Python "past" module is no longer available for 16.04, so build fails on kernel/tools/lex.py. According to the comment right before the failing import statement, it appears this module is just declared but not used, so commenting it out (or removing it entirely) would fix this issue: #from past.builtins import cmp One more issue: when using either one of the following configurations as start point: - bamboo_bbone_black_debug_xml_defconfig - bbone_black_debug_xml_defconfig The build system will end up producing a binary image and not an ELF image. Producing an ELF image can be more useful if you want to use objdump to get a disassembly (for debugging later). So I changed the configuration with: make menuconfig Navigate to: Tools -> Build elfloader -> Boot image type and select "ELF Boot Image" instead of "Binary Boot Image" Save your configuration then build: make Now manually convert the produced ELF image in a binary: arm-linux-gnueabi-objcopy --output-target binary images/sel4test-driver-image-arm-am335x sel4test.bin then copy the file 'sel4test.bin' onto the SD card formatted as FAT32 Now, in my BBB (rev A5A) if I try to follow the instructions from the wiki page previously mentioned, I get a crash right away (illegal instruction). The problem is that in my BBB the uBoot environment variable ${loadaddr} is set to 0x80200000 and not 0x82000000 (the start address of the produced image). BBB have RAM mapped from address 0x80000000 to 0x9FFFFFFF (512Mb), so running from 0x82000000 is ok. So to load and run, use instead: fatload mmc 0 0x82000000 sel4test.bin go 0x82000000 That's it. Test should load and run successfully: Test suite passed. 220 tests passed. 220/220 tests passed. All is well in the universe. Hope this help saving some time... Regards, Fabrizio

1 0

Important note for CAmkES users
by Stephen.Sherratt＠data61.csiro.au 13 Jun '17

13 Jun '17

We've just released CAmkES 3.0.0 (release notes<https://wiki.sel4.systems/CAmkES%203.0.0>), and with it, all changes staged on our development branch, CAmkES Next, have been merged into the "master" branch of the camkes-tool repo (https://github.com/seL4/camkes-tool) We'll be continuing to develop CAmkES on its "master" branch, and cease making new commits to the "next" branch. # What this means for you As CAmkES 3.0.0 is incompatible with older versions of CAmkES, any projects tracking the master branch of camkes-tool will probably not build after this change. Also, as all new development is now being done on the master branch, any projects tracking the next branch of camkes-tool will no longer receive updates. If you're in either category, you'll need to update your project's repo manifest. # Migration Instructions If your project tracks either the "master", or "next" branch of the camkes-tool, you'll need to update your project's manifest. To check if this applies to you, look in your projects repo manifest xml file (typically in .repo/manifest.xml at the top level of your project) for the line: <project name="camkes-tool.git" path="tools/camkes"> (this implicitly tracks "master") OR <project name="camkes-tool.git" path="tools/camkes" revision="master"> OR <project name="camkes-tool.git" path="tools/camkes" revision="next"> If your manifest has either of those lines, take a look at the migration guide in the CAmkES 3.0.0 release notes: https://wiki.sel4.systems/CAmkES%203.0.0#Migrating It covers a range of different scenarios and explains how to change your manifest so your project will continue to work. If the camkes-tool revision in your manifest specifies a particular version of CAmkES (e.g. 'revision="camkes-2.3.1"'), you don't need to migrate.

1 0

Pre-release of mixed criticality seL4 extensions
by Anna.Lyons＠data61.csiro.au 13 Jun '17

13 Jun '17

= seL4-5.2.0-mcs = The first round of mixed-criticality extensions for seL4 are now available for your perusal and usage. This is a prerelease of features that are currently our candidate for verification. They are *not* verified and most likely contain bugs. If you encounter any, please report them ;) We have more features in development coming, but this is the first lot. = Release Notes = Detailed release notes can be found on our wiki: https://wiki.sel4.systems/seL4%205.2.0-mcs = Upgrade Notes = This version is not compatible with seL4 5.2.0, but forks the API based on that kernel version. Branches are available in most of our libraries to use, and CAmkES and capdl already have support for this pre-release on their latest release and master branch. = Major Changes = A summary of major changes can be found at: https://wiki.sel4.systems/seL4%205.2.0-mcs#Highlights A tutorial covering the new features can be found at: https://wiki.sel4.systems/seL4%205.2.0-mcs = Source Code = https://github.com/seL4/seL4/tree/5.2.0-mcs = Full Change Log = Use: git log 5.2.0..5.2.0-mcs

1 0

Announcing CAmkES 3.0.0
by Stephen.Sherratt＠data61.csiro.au 13 Jun '17

13 Jun '17

We're pleased to announce the release of CAmkES 3.0.0. This is a major release, which contains all work from our development branch, also known as CAmkES Next. Future development on CAmkES will occur on the "master" branch. Importantly, this means no further commits will be made to the "next" branch, so users will need to update their manifests to point at the "master" branch, or alternatively, the "camkes-3.0.0" tag created with this release. = Release Notes = Detailed release notes can be found on our wiki: https://wiki.sel4.systems/CAmkES%203.0.0 = Upgrade Notes = Dependencies for running CAmkES have changed since the previous release. Instructions for installing dependencies on several linux distros can be found here: https://wiki.sel4.systems/CAmkES#Build_dependencies If you were tracking the master branch of the camkes-tool in your project, you'll need to modify your project's manifest for it to continue to work. Migration instructions for a variety of situations can be found at: https://wiki.sel4.systems/CAmkES%203.0.0#Migrating = Major Changes = A summary of major changes can be found at: https://wiki.sel4.systems/CAmkES%203.0.0#New_Features = Examples = mkdir camkes-examples && cd camkes-examples repo init -u https://github.com/seL4/camkes-manifest.git -m default-3.0.x.xml repo sync tests/x86-simple.tcl # builds and runs simple example = Source Code = https://github.com/seL4/camkes-tool/ = Full Change Log = Use: git log camkes-3.0.0...$(git merge-base camkes-2.3.1 camkes-3.0.0) = More Details = Manual: https://github.com/seL4/camkes-tool/blob/camkes-3.0.0/docs/index.md Wiki: https://wiki.sel4.systems/CAmkES Enjoy!

1 0

Missing pico_device.h
by Michal Podhradsky 09 Jun '17

09 Jun '17

Hello, the recent commits in broke the build of util_libs <https://github.com/seL4/util_libs/commits/master> broke the build of camkes- <https://github.com/seL4/camkes-vm>vm <https://github.com/seL4/camkes-vm>. To recreate the error, do: mkdir test_defaultcd test_defaultrepo init -u https://github.com/seL4/camkes-vm-manifest.gitrepo sync make cleanmake optiplex9020_defconfigmake silentoldconfigmake You will get: *In file included from /test_default/libs/libethdrivers/src/pico_dev_eth.c:15:0:/test_default/stage/x86/pc99/include/ethdrivers/pico_dev_eth.h:16:26: fatal error: pico_device.h: No such file or directorycompilation terminated.* Regards Michal

1 0

Temporally disable write-access on memory pages
by Norrathep Rattanavipanon 09 Jun '17

09 Jun '17

Hello, I have a question regarding the best way to temporally disable write-access on memory pages. Suppose in the user-space, there are two processes: initial user-space process and process A, which is created by the initial process. Process A has its own virtual memory space. Now we want to find a way to enforce the memory inside process A to be temporally R/O to process A (since we want to have the initial process compute a function on that memory snapshot.) Currently, what we are doing now is to lock all memory pages of process A by calling the "remap" function inside the initial process. But then we realize that doing that does not help much. Since process A owns capabilities to its memory pages, process A also can call "remap" function to unlock the locked memory pages (please correct me if it's wrong). This will cause the memory to be inconsistent when computing a function on that memory. My question is is there anyway to enforce how a page locking (make it R/O) works in seL4 so that ONLY the entity that locked the page can unlock it? For example, in this case, we want to make sure that only the initial process can unlock the pages that he locked earlier. Thank you, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 2

Fwd: k_vmm_manager: failed on sel4 hypervisor connection
by Michal Podhradsky 08 Jun '17

08 Jun '17

Hello all, I am running camkes-vm on x86 architecture, following the example on wiki https://wiki.sel4.systems/CAmkESVM#Cross_VM_Connectors with the exception that I want to invoke the stringReverse component <https://github.com/podhrmic/camkes-vm/tree/master/components/StringReverse> . I am running the optiplex9020_defconfig example with only one VM, and when I start booting the guest linux system, I see the following error: *[ 1.282326] dataport: loading out-of-tree module taints kernel.* *[ 1.290615] dataport: module license 'unspecified' taints kernel.* *[ 1.306854] Disabling lock debugging due to kernel taint* *[ 1.319664] dataport initialized with major number 247* *vmm_vmcall_handler:55 | Failed to find handler for token:2* *[ 1.325411] incorrect event context magic number (expected 42, got -677408512)insmod: can't insert '/lib/modules/4.8.16/kernel/drivers/vmm/consumes_event.ko': Operation not ermitted* *[ 1.337441] emits_event initialized with major number 245* *[ 1.356391] k_vmm_manager: failed on sel4 hypervisor connection |-1|* Then when I log into linux and call `string_reverse <https://github.com/podhrmic/camkes-vm/tree/master/linux/pkg/string_reverse>` program, I get the following error: *# string_reverse * *[ 8.360164] BUG: unable to handle kernel paging request at d881f2c0* *[ 8.360164] IP: [<d00a69f0>] chrdev_open+0xab/0x100* *[ 8.360164] *pde = 17867067 *pte = 00000000 * *[ 8.360164] Oops: 0000 [#1]* *[ 8.360164] Modules linked in: emits_event(PO) dataport(PO)* *[ 8.360164] CPU: 0 PID: 691 Comm: string_reverse Tainted: P O 4.8.16 #1* *[ 8.360164] task: d79c9740 task.stack: d6ae0000* *[ 8.360164] EIP: 0060:[<d00a69f0>] EFLAGS: 00010286 CPU: 0* *[ 8.360164] EIP is at chrdev_open+0xab/0x100* *[ 8.360164] EAX: d881f2c0 EBX: 00000000 ECX: d79b0d00 EDX: 00000000* *[ 8.360164] ESI: d79b0d00 EDI: d6add808 EBP: d6ae1e10 ESP: d6ae1df8* *[ 8.360164] DS: 007b ES: 007b FS: 0000 GS: 0033 SS: 0068* *[ 8.360164] CR0: 80050033 CR2: d881f2c0 CR3: 16ad9000 CR4: 00102690* *[ 8.360164] DR0: 00000000 DR1: 00000000 DR2: 00000000 DR3: 00000000* *[ 8.360164] DR6: fffe0ff0 DR7: 00000400* *[ 8.360164] Stack:* *[ 8.360164] d7ac9be0 d7ac9be0 00000001 d7ac9be0 d6add808 00000000 d6ae1e30 d00a2370* *[ 8.360164] d6ae1e28 d7ac9be8 d00a6945 d7ac9be0 d69db010 d7462d80 d6ae1e4c d00a2cf8* *[ 8.360164] d79c2b80 d79c2b80 00000000 d6ae1ebc d7462d80 d6ae1eb0 d00ae159 d6ae1e64* *[ 8.360164] Call Trace:* *[ 8.360164] [<d00a2370>] do_dentry_open+0x197/0x216* *[ 8.360164] [<d00a6945>] ? cdev_put+0x1a/0x1a* *[ 8.360164] [<d00a2cf8>] vfs_open+0x45/0x4e* *[ 8.360164] [<d00ae159>] path_openat+0x822/0x970* *[ 8.360164] [<d007a468>] ? __alloc_pages_nodemask+0x11c/0x770* *[ 8.360164] [<d00ae2d8>] do_filp_open+0x31/0x77* *[ 8.360164] [<d00b6293>] ? __alloc_fd+0xbb/0xfe* *[ 8.360164] [<d00a2e56>] do_sys_open+0x54/0xc7* *[ 8.360164] [<d00a2ee1>] SyS_open+0x18/0x1a* *[ 8.360164] [<d0000ee1>] do_fast_syscall_32+0x7a/0xb8* *[ 8.360164] [<d047831f>] sysenter_past_esp+0x40/0x6a* *[ 8.360164] Code: 11 89 f0 e8 e1 fa ff ff 83 f8 01 19 db 31 d2 83 e3 fa 89 d0 e8 4d ff ff ff 85 db 75 59 8b 46 28 85 c0 75 0c* *[ 8.360164] EIP: [<d00a69f0>] chrdev_open+0xab/0x100 SS:ESP 0068:d6ae1df8* *[ 8.360164] CR2: 00000000d881f2c0* *[ 8.360164] ---[ end trace 46873a57a343e435 ]---* *[ 8.376285] string_reverse (691) used greatest stack depth: 6496 bytes left* *Killed* which seems like the program is trying to access memory that it is not supposed to. If I follow the example from wiki (here https://wiki.sel4. systems/CAmkESVM#Cross_VM_Connectors ) I get the same error, but triggered by `print_client` program. Have you seen a problem like this before? How do I correctly load the kernel module? Regards Michal

2 5

Using linux-tk1-debian on camkes-arm-vm
by Mike Clark 05 Jun '17

05 Jun '17

I have seL4 running on a TK1 using linux-tk1-initrd. I'd like to get the linux-tk1-debian version running to load the userspace off of the emmc drive of the TK1. FWIW, I did flash the TK1 to the latest verison, R21.5. The default DTS has root=/dev/mmcblk0p2 in the bootargs. When booting with this, I get a kernel panic. I also tried changing that to root=/dev/mmcblk0p1 (since that partition was the larger one on the emmc). It also gives a kernel panic, albeit a different message. With mmcblk0p1, the message I get is: [ 10.092841] EXT2-fs (mmcblk0p1): error: couldn't mount because of unsupported optional features (240) [ 10.102749] EXT4-fs (mmcblk0p1): couldn't mount as ext3 due to feature incompatibilities [ 10.137427] EXT4-fs (mmcblk0p1): mounted filesystem with ordered data mode. Opts: (null) [ 10.145696] VFS: Mounted root (ext4 filesystem) on device 179:1. [ 10.162679] devtmpfs: mounted [ 10.165845] Freeing unused kernel memory: 252K (c0aa9000 - c0ae8000) [ 10.224352] Kernel panic - not syncing: Attempted to kill init! exitcode=0x00000004 [ 10.224352] [ 10.233480] CPU: 0 PID: 1 Comm: init Tainted: G W 4.3.0-rc5 #1 [ 10.240429] Hardware name: NVIDIA Tegra SoC (Flattened Device Tree) [ 10.246713] [<c0015d30>] (unwind_backtrace) from [<c0012b74>] (show_stack+0x10/0x14) [ 10.254457] [<c0012b74>] (show_stack) from [<c009247c>] (panic+0xa0/0x214) [ 10.261330] [<c009247c>] (panic) from [<c002566c>] (complete_and_exit+0x0/0x1c) [ 10.268627] [<c002566c>] (complete_and_exit) from [<00000000>] ( (null)) [ 10.275408] ---[ end Kernel panic - not syncing: Attempted to kill init! exitcode=0x00000004 With mmcblk0p2, the message I get is: [ 10.095124] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010) - read(0x1000000) [ 10.102907] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem in 1th superblock [ 10.111127] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010) - read(0xfb000000) [ 10.118994] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem in 2th superblock [ 10.126711] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010) - read(0x1000000) [ 10.134472] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem in 1th superblock [ 10.142167] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010) - read(0xfb000000) [ 10.149983] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem in 2th superblock [ 10.159891] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010) - read(0x1000000) [ 10.167669] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem in 1th superblock [ 10.175842] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010) - read(0xfb000000) [ 10.183743] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem in 2th superblock [ 10.191391] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010) - read(0x1000000) [ 10.199146] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem in 1th superblock [ 10.206813] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010) - read(0xfb000000) [ 10.214653] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem in 2th superblock [ 10.222551] Kernel panic - not syncing: VFS: Unable to mount root fs on unknown-block(179,2) [ 10.230976] CPU: 0 PID: 1 Comm: swapper Tainted: G W 4.3.0-rc5 #1 [ 10.238184] Hardware name: NVIDIA Tegra SoC (Flattened Device Tree) [ 10.244462] [<c0015d30>] (unwind_backtrace) from [<c0012b74>] (show_stack+0x10/0x14) [ 10.252205] [<c0012b74>] (show_stack) from [<c009247c>] (panic+0xa0/0x214) [ 10.259079] [<c009247c>] (panic) from [<c0aaa238>] (mount_block_root+0x21c/0x230) [ 10.266554] [<c0aaa238>] (mount_block_root) from [<c0aaa368>] (mount_root+0x11c/0x124) [ 10.274459] [<c0aaa368>] (mount_root) from [<c0aaa4bc>] (prepare_namespace+0x14c/0x194) [ 10.282451] [<c0aaa4bc>] (prepare_namespace) from [<c0aa9dec>] (kernel_init_freeable+0x1c0/0x1d0) [ 10.291315] [<c0aa9dec>] (kernel_init_freeable) from [<c07c4b20>] (kernel_init+0x8/0xe8) [ 10.299397] [<c07c4b20>] (kernel_init) from [<c000f4d8>] (ret_from_fork+0x14/0x3c) [ 10.306959] ---[ end Kernel panic - not syncing: VFS: Unable to mount root fs on unknown-block(179,2) Is there a guide for how to setup the emmc on the TK1 to boot using linux-tk1-debian? Will an older version of the TK1 image from Nvidia work or do I need to do a custom debian install (like this https://wiki.debian.org/InstallingDebianOn/NVIDIA/Jetson-TK1)?

2 3

Running Linux on top of seL4
by Daniel Wang 05 Jun '17

05 Jun '17

Hi all, Is there any guide about how to run Linux on top of seL4? Or has anyone done that before that can give me some hints? Thanks -Dan

4 6

Re: [seL4] 回复： camkes-manifest project make failed for arm
by Hesham.Almatary＠data61.csiro.au 02 Jun '17

02 Jun '17

Hi Talos, Are you following some instructions or getting started guides? e.g. camkes getting started guide [1] is using kzm config (arm_simple_defconfig). You can know which target at the time you're configuring the project by: 1) reading the *_defconfig you ran make with, 2) make menuconfig, 3) or after this from the .config file from where you run make *_defconfig or make menuconfig. Hope that helps. [1] https://sel4.systems/Info/CAmkES/GettingStarted.pml Best, Hesham ________________________________ From: talos <2486580938(a)qq.com> Sent: Friday, June 2, 2017 1:42 PM To: Almatary, Hesham (Data61, Kensington NSW) Subject: 回复： [seL4] camkes-manifest project make failed for arm Hi Hesham, How could I get which targets I used? Thanks for your patient! ------------------ 原始邮件 ------------------ 发件人: "Hesham.Almatary";<Hesham.Almatary(a)data61.csiro.au>; 发送时间: 2017年6月2日(星期五) 中午11:11 收件人: "talos"<2486580938(a)qq.com>; 抄送: "devel"<devel(a)sel4.systems>; 主题: Re: [seL4] camkes-manifest project make failed for arm Hi Talos, Thanks for reporting this. It seems like it’s an issue with KZM (ARMv6) targets which I assume you’re using? I submitted a fix, should be public on GitHub soon. Meanwhile, you can use the following patch to get around this error. diff --git a/include/util.h b/include/util.h index d6afdbb..4b05430 100644 --- a/include/util.h +++ b/include/util.h @@ -11,7 +11,6 @@ #ifndef __UTIL_H #define __UTIL_H -#define BIT(n) (1ul << (n)) #define MASK(n) (BIT(n)-1ul) #define IS_ALIGNED(n, b) (!((n) & MASK(b))) #define ROUND_DOWN(n, b) (((n) >> (b)) << (b)) @@ -23,6 +22,7 @@ #ifndef __ASSEMBLER__ #define NULL ((void *)0) +#define BIT(n) (1ul << (n)) #define PACKED __attribute__((packed)) #define NORETURN __attribute__((__noreturn__)) @@ -131,6 +131,10 @@ CONST popcountl(unsigned long x) } #define POPCOUNTL(x) __builtin_popcountl(x) +#else /* __ASSEMBLER__ */ + + +#define BIT(n) (1 << (n)) Cheers, Hesham On 2 Jun 2017, at 10:41 am, Hesham.Almatary(a)data61.csiro.au<mailto:Hesham.Almatary@data61.csiro.au> wrote: Hi Talos, This might be because of this change [1] to the kernel. Since this change has passed on our local machines, I'd be interested to know which toolchain version are you using (specifically binutils)? [1] https://github.com/seL4/seL4/commit/1930cf2e44908cb8faa5b315651bdb1958102f8f Cheers, Hesham ________________________________ From: Devel <devel-bounces(a)sel4.systems<mailto:devel-bounces@sel4.systems>> on behalf of talos <2486580938(a)qq.com<mailto:2486580938@qq.com>> Sent: Friday, June 2, 2017 9:59 AM To: devel Subject: [seL4] camkes-manifest project make failed for arm When I make the project, it said that: /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S: Assembler messages: /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:56: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:56: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:82: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:82: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:117: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:117: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:128: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:128: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:168: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:168: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:185: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:185: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:213: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:213: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/Makefile:653: recipe for target 'src/arch/arm/32/traps.o' failed make[1]: *** [src/arch/arm/32/traps.o] Error 1 tools/common/project.mk:258: recipe for target 'kernel_elf' failed make: *** [kernel_elf] Error 2 But I make successfully for x86 What's matter? Thanks! _______________________________________________ Devel mailing list Devel(a)sel4.systems<mailto:Devel@sel4.systems> https://sel4.systems/lists/listinfo/devel

1 0

camkes-manifest project make failed for arm
by talos 02 Jun '17

02 Jun '17

When I make the project, it said that: /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S: Assembler messages: /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:56: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:56: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:82: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:82: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:117: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:117: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:128: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:128: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:168: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:168: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:185: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:185: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:213: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:213: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/Makefile:653: recipe for target 'src/arch/arm/32/traps.o' failed make[1]: *** [src/arch/arm/32/traps.o] Error 1 tools/common/project.mk:258: recipe for target 'kernel_elf' failed make: *** [kernel_elf] Error 2 But I make successfully for x86 What's matter? Thanks!

2 2

Re: [seL4] Devel Digest, Vol 37, Issue 2
by talos 02 Jun '17

02 Jun '17

Dear Hesham This is binutils information 2.26.1-1ubuntu1~16.04.4 Thanks ------------------ Original ------------------ From: "devel-request";<devel-request(a)sel4.systems>; Date: Fri, Jun 2, 2017 08:56 AM To: "devel"<devel(a)sel4.systems>; Subject: Devel Digest, Vol 37, Issue 2 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. Running multiple VMs under ARM and C++ under SeL4? (John Backes) 2. camkes-manifest project make failed for arm (=?ISO-8859-1?B?dGFsb3M=?=) 3. Re: camkes-manifest project make failed for arm (Hesham.Almatary(a)data61.csiro.au) 4. Re: Running multiple VMs under ARM and C++ under SeL4? (Adrian.Danis(a)data61.csiro.au) ---------------------------------------------------------------------- Message: 1 Date: Thu, 1 Jun 2017 11:41:49 -0500 From: John Backes <john.backes(a)gmail.com> To: devel(a)sel4.systems Subject: [seL4] Running multiple VMs under ARM and C++ under SeL4? Message-ID: <CAGzTpxHy_b+RWx33=xXv=vyEAwRttE3no-S21hwhqtBX6ZRG-w(a)mail.gmail.com> Content-Type: text/plain; charset="utf-8" Does the ARM VMM currently support running multiple virtual machines. Also, as a side question, how hard would it be to compile general C++ code that makes heavy use of the standard template library for use in a camkes component? I assume this would be non-trivial? - John -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://sel4.systems/pipermail/devel/attachments/20170601/5de7f205/attachmen…> ------------------------------ Message: 2 Date: Fri, 2 Jun 2017 07:59:34 +0800 From: "=?ISO-8859-1?B?dGFsb3M=?=" <2486580938(a)qq.com> To: "=?ISO-8859-1?B?ZGV2ZWw=?=" <devel(a)sel4.systems> Subject: [seL4] camkes-manifest project make failed for arm Message-ID: <tencent_0DEA523F71A09CF508392575(a)qq.com> Content-Type: text/plain; charset="iso-8859-1" When I make the project, it said that: /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S: Assembler messages: /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:56: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:56: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:82: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:82: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:117: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:117: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:128: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:128: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:168: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:168: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:185: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:185: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:213: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:213: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/Makefile:653: recipe for target 'src/arch/arm/32/traps.o' failed make[1]: *** [src/arch/arm/32/traps.o] Error 1 tools/common/project.mk:258: recipe for target 'kernel_elf' failed make: *** [kernel_elf] Error 2 But I make successfully for x86 What's matter? Thanks! -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://sel4.systems/pipermail/devel/attachments/20170602/a0e0e40f/attachmen…> ------------------------------ Message: 3 Date: Fri, 2 Jun 2017 00:41:15 +0000 From: <Hesham.Almatary(a)data61.csiro.au> To: <2486580938(a)qq.com>, <devel(a)sel4.systems> Subject: Re: [seL4] camkes-manifest project make failed for arm Message-ID: <1496364075337.38653(a)data61.csiro.au> Content-Type: text/plain; charset="iso-8859-1" Hi Talos, This might be because of this change [1] to the kernel. Since this change has passed on our local machines, I'd be interested to know which toolchain version are you using (specifically binutils)? [1] https://github.com/seL4/seL4/commit/1930cf2e44908cb8faa5b315651bdb1958102f8f Cheers, Hesham ________________________________ From: Devel <devel-bounces(a)sel4.systems> on behalf of talos <2486580938(a)qq.com> Sent: Friday, June 2, 2017 9:59 AM To: devel Subject: [seL4] camkes-manifest project make failed for arm When I make the project, it said that: /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S: Assembler messages: /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:56: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:56: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:82: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:82: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:117: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:117: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:128: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:128: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:168: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:168: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:185: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:185: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:213: Error: missing ')' /home/talos/camkes-manifest/kernel/src/arch/arm/32/traps.S:213: Error: garbage following instruction -- `ldr sp,=kernel_stack_alloc+(1ul<<(12))' /home/talos/camkes-manifest/kernel/Makefile:653: recipe for target 'src/arch/arm/32/traps.o' failed make[1]: *** [src/arch/arm/32/traps.o] Error 1 tools/common/project.mk:258: recipe for target 'kernel_elf' failed make: *** [kernel_elf] Error 2 But I make successfully for x86 What's matter? Thanks! -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://sel4.systems/pipermail/devel/attachments/20170602/516c7463/attachmen…> ------------------------------ Message: 4 Date: Fri, 2 Jun 2017 00:56:24 +0000 From: <Adrian.Danis(a)data61.csiro.au> To: <john.backes(a)gmail.com>, <devel(a)sel4.systems> Subject: Re: [seL4] Running multiple VMs under ARM and C++ under SeL4? Message-ID: <ad050360-e6ef-eeb2-7130-dc66fb368f51(a)data61.csiro.au> Content-Type: text/plain; charset="utf-8" Hi John, The ARM VMM does not currently support multiple virtual machines, this is something we are working on adding. To properly use the C++ standard template library you would need to build a cross compiler for a CAmkES system based seL4 system. This is something we have never done. Whether this is trivial or not depends entirely upon whether you find building cross compilers trivial or not. Adrian On Fri 02-Jun-2017 2:41 AM, John Backes wrote: Does the ARM VMM currently support running multiple virtual machines. Also, as a side question, how hard would it be to compile general C++ code that makes heavy use of the standard template library for use in a camkes component? I assume this would be non-trivial? - John _______________________________________________ Devel mailing list Devel(a)sel4.systems<mailto:Devel@sel4.systems> https://sel4.systems/lists/listinfo/devel -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://sel4.systems/pipermail/devel/attachments/20170602/c454560f/attachmen…> ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel ------------------------------ End of Devel Digest, Vol 37, Issue 2 ************************************

1 0

Running multiple VMs under ARM and C++ under SeL4?
by John Backes 02 Jun '17

02 Jun '17

Does the ARM VMM currently support running multiple virtual machines. Also, as a side question, how hard would it be to compile general C++ code that makes heavy use of the standard template library for use in a camkes component? I assume this would be non-trivial? - John

2 1

The path where the kernel jumps to apps
by shijun zhao 31 May '17

31 May '17

Hi, I’m tracing the path where sel4 kernel jumps to an application, such as hello-1. >From the Makefile for apps I know that the entry of the hello-1.bin is *_sel4_start* which is defined in the sel4_crt0.S (the directory is sel4_tutorials/projects/sel4_libs_libsel4platsupport/src/arch/arm). The *_sel4_start* function first calls a C function called *sel4_InitBootInfo*, and finally jumps to the *_start* function which is defined in the crt0.S. However the *_start* in crt0.S calls the sel4_InitBootInfo again. What confuses me is that the sel4_InitBootInfo function requires an input argument passed by R0, however the R0 has been set to zero in the _sel4_start function, so I think the calling of sel4_InitBootInfo in the _start will not run correctly. Or is the path where the kernel jumps to the app (_sel4_start->_start->main) wrong? I paste referred codes below: */******sel4_crt0.S********************/* _sel4_start: /* Setup a stack for ourselves. */ ldr sp, =_stack_top /* Setup bootinfo. The pointer to the bootinfo struct starts in 'r0'. */ bl seL4_InitBootInfo ............ mov r0, #0 // *The R0 is modified, so it doesn't store the bootinfo structure anymore!* ............ /* Now go to actual _start */ ldr pc, =_start */*********crt0.S********************/* _start: /* Setup a stack for ourselves. */ ldr sp, =_stack_top */* Setup bootinfo. The pointer to the bootinfo struct starts in 'r0'. */* * bl seL4_InitBootInfo //Since R0 has been modified by _sel4_start, sel4_InitBootInfo will not run correctly.* /* Call constructors and other initialisation functions. */ bl _init /* Call main. */ bl main b exit Best Regards, Shijun Zhao

2 2

How to prove correctness of my own program?
by Adam Badura 30 May '17

30 May '17

I expect this might be (or even probably is) a bad place to ask this but at the same time I didn't find any better coming from the Contact Information page (http://sel4.systems/contact/) I'm working on a conference paper (not sure if I will make it but still trying to - code::dive <http://codedive.pl/> if anyone would be interested) about proving program correctness. Considering my own knowledge in the field and expected knowledge of the audience there would be nothing new in that paper - more like an update on what is the current state of the field. Yet I wanted to supply also some examples. As main example I would like to show proof (or at least parts of it) of correctness (adherence to specification) of C++ code, possibly reduced to C code if need be. After research in this topic and finding this project some time ago it felt natural to reuse its tools. But I fail to do so. Could you possibly guide me? Using your tools and techniques what should I do to prove correctness of some piece of code. I think source code level would be more than enough - for this task no need to verify binary in any form. As a side example I would like to show how your proves look like. I'm not sure what you are generating / writing as a proof (that gets later verified automatically). I imagine a sequence of something. Some formulas in natural deduction perhaps? Or something else? Whatever that would be I guess it must be pretty long so it is not like I would show and analyze it all but instead would like to somehow let the audience "feel the size". If - as I expect - this is not the right place to ask and you cannot help me with above questions, could you at least point me to where to ask them? Adam Badura

2 1

camkes-arm-vm not registering GPIO?
by Steven Johnston 30 May '17

30 May '17

Hi All, I am playing around with the capabilities of the camkes-arm-vm project pn the Tegra TK1 and and wondering if someone else has come across this issue. It looks like GPIO functionality is not available in the buildroot. I can confirm the GPIO source is present and is being built: camkes-arm-vm/libs/libplatsupport/rc/plat/tk1/gpio.c camkes-arm-vm/libs/libplatsupport/plat_include/tk1/platsupport/plat/gpio.h [CC] src/plat/tk1/gpio.o The expected sysfs support is not present and looking and the relevant dmesg: # dmesg | grep gpio [ 0.057543] gpiochip_add: GPIOs 0..255 (tegra-gpio) failed to register [ 1.485061] input: gpio-keys as /devices/soc0/gpio-keys/input/input0 Any thoughts on what could be causing GPIO to the failing to register? Steven

2 4

About timer tests (CONFIG_HAVE_TIMER) in sel4test testsuites
by Jesse-SC Chou (周書正) 26 May '17

26 May '17

Hi seL4-hackers, I am porting the sel4test project to my custom target board, which contains an ARM Cortex-A7 core. The porting work is based on NVidia TK1 Cortex-A15 platform. In current stage, the seL4 kernel has booted up and the test benches can be tested. I can pass all tests except for the timer tests (turn off CONFIG_HAVE_TIMER). In my target, only ARM generic timer is used. My questions are: 1. Are the timer tests (CONFIG_HAVE_TIMER) designed for other platform timer besides ARM generic timer? If I only use ARM generic timer, should these timer tests be passed? 2. My goal is to running Linux with seL4 VMM on my target. The sel4platsupport_get_default_timer() is platform specific. If I only use ARM generic timer, should sel4platsupport_get_default_timer() be ported to return the ARM generic timer? If yes, is there any example for me to reference? BRs, Jesse

2 2

CapDL Spec Error
by Chris Guikema 22 May '17

22 May '17

Hello All, Has anyone come across this error before? [GEN] imx6_net.cdl While forming CapDL spec: failed to find dataport symbol 'camkes router router_send_buf data' in ELF router_group_bin make[1]: *** [imx6_net.cdl] Error 255 make[1]: *** Deleting file `imx6_net.cdl' make: *** [imx6_net] Error 2 Thanks, Chris Guikema

2 4

Blog post: seL4, CAmkES, and L4v dependencies
by Luke.Mondy＠data61.csiro.au 19 May '17

19 May '17

Hello all, We have published a blog post about how we manage software dependencies within Trustworthy Systems, and how it has been adapted to produce a relatively user-friendly interface. It is relevant for people both new and old to the seL4 ecosystem, as it simplifies and compartmentalises the elaborate software dependencies sometimes required to get things to build. You can read the blog post here: https://research.csiro.au/tsblog/getting-started-sel4-camkes-l4v-dependenci… If you have any feedback or changes you would like made, please let us know on the GitHub repo. Cheers, Luke -- Luke Mondy, Systems Administrator, Trustworthy Systems DATA61 | CSIRO M +61 0415 281 991 | https://ts.data61.csiro.au

1 0

Is there has any seL4 project support ARM Cortex-A7 ?
by Joyce Peng(彭美僑) 19 May '17

19 May '17

Hi Everyone, Is there has any seL4 project support ARM Cortex-A7 ? I found seL4 official projects in below link. https://github.com/seL4 https://github.com/SEL4PROJ I use sel4test project that repo from https://github.com/seL4/sel4test-manifest.git And I found Xilinx zynq7000 support ARM Cortex-A9 in sel4test like below. File: sel4test/projects/sel4test/master-configs/zynq7000_release_xml_defconfig # # seL4 System # # CONFIG_ARCH_X86 is not set CONFIG_ARCH_ARM=y CONFIG_ARCH_AARCH32=y # CONFIG_ARM1136JF_S is not set # CONFIG_ARM_CORTEX_A8 is not set CONFIG_ARM_CORTEX_A9=y # CONFIG_ARM_CORTEX_A15 is not set # CONFIG_PLAT_EXYNOS54XX is not set I can’t find seL4 project support ARM cortex-A7. Does anyone find it? Thanks, Joyce Peng

3 3

sel4test data abort when boot strap test program
by Joyce Peng(彭美僑) 19 May '17

19 May '17

Hi all, I tried to run seL4 test suite on my ARM Cortex-A7 target board. There is no error message when boot up seL4 kernel and boot strap test program on seL4 user land. But I got a “data abort” message after call sel4utils_map_page(..vaddr) and do memset(vaddr, 0, PAGE_SIZE_4K); There are some debug information list below. <1> I add debug message before the program that happen data abort diff --git a/libsel4utils/src/vspace/bootstrap.c b/libsel4utils/src/vspace/bootstrap.c index c366a35..70d378a 100644 --- a/libsel4utils/src/vspace/bootstrap.c +++ b/libsel4utils/src/vspace/bootstrap.c @@ -107,13 +107,13 @@ static void *alloc_and_map(vspace_t *vspace, size_t size) { error = sel4utils_map_page(data->vka, data->vspace_root, frame.cptr, vaddr, seL4_AllRights, 1, objects, &num); + LOG_ERROR("my-hacker\n"); if (error) { vka_free_object(data->vka, &frame); LOG_ERROR("Failed to map bootstrap frame at %p, error: %d", vaddr, error); return NULL; } + LOG_ERROR("my-hacker alloc_and_map() before memset vaddr=0x%x\n",vaddr); /* Zero the memory */ memset(vaddr, 0, PAGE_SIZE_4K); <2>Printed messages: ELF-loader started on CPU: ARM Ltd. Cortex-A7 r0p5 paddr=[20000000..2051881f] ELF-loading image 'kernel' paddr=[22000000..22032fff] vaddr=[e0000000..e0032fff] virt_entry=e0000000 ELF-loading image 'sel4test-driver' paddr=[22033000..22463fff] vaddr=[8000..438fff] virt_entry=15f50 Enabling MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Booting all finished, dropped to user space Warning: using printf before serial is set up. This only works as your printf is backed by seL4_Debug_PutChar() alloc_and_map@bootstrap.c:111 my-hacker alloc_and_map@bootstrap.c:119 my-hacker alloc_and_map() before memset() vaddr=0xdf7fe000 <3>When happen data abort, the value of CPU registers: r1:0 r3:0xdf7fe000 lr:0xcbe8 <4>Objdump sel4test-driver. 0000cbc8 <memset>: cbc8: e3520000 cmp r2, #0 cbcc: e92d4030 push {r4, r5, lr} cbd0: 08bd8030 popeq {r4, r5, pc} cbd4: e0803002 add r3, r0, r2 cbd8: e6ef1071 uxtb r1, r1 cbdc: e3520002 cmp r2, #2 cbe0: e5431001 strb r1, [r3, #-1] cbe4: e5c01000 strb r1, [r0] cbe8: 98bd8030 popls {r4, r5, pc} cbec: e3520006 cmp r2, #6 It seems to write virtual address 0xdf7ff000. <5>The virtual address 0xdf7fe000 is not map in page table It seems sel4utils_map_page() not create page table for user land program correctly. Can anyone help me, how to solve this problem? Thanks! Joyce Peng(彭美僑)

4 12

seL4 on Cortex-A5
by Andrew Gacek 19 May '17

19 May '17

Is there any support for seL4 on the Cortex-A5? -Andrew

3 2

Change Access Right to Memory Pages
by Norrathep Rattanavipanon 04 May '17

04 May '17

Hello, I have some questions about how to change access rights in seL4. (I'm using native seL4, not camkes) 1) Currently, I'm using seL4_ARCH_Page_Remap to change an access right (from R/W to R/O) to a specific page (of other processes) at run-time. I'm doing as follows: seL4_CPtr frame = vspace_get_cap(&(p.vspace), p.thread.stack_top-1); // only for the stack int error = seL4_ARCH_Page_Remap(frame, ppd.cptr, seL4_CanRead, seL4_ARCH_Default_VMAttributes); Am I doing it correctly? The code seems to work fine for me but I just want to double check. 2) If my understanding in 1) is correct, the remap function only takes 1 cap at a time. So if I want to modify access rights of many pages, do I have to call the remap function multiple times? Or is there a more efficient way to do so? 3) I am also curious how the kernel handles the remap function. Does it simply flip/change some bits? Or does it involve page-related operations as well? e.g. unmap that page first and then remap the same region with a new access right? I guess it should be the former but I need to be sure about that. Thank you, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

4 7

seL4 Upgrading Issues
by Chris Guikema 04 May '17

04 May '17

Hello, I have developed an Ethernet application using CAmkES 2.2 and seL4 3.2. Because we are going to open-source the design and other documentation, I thought it would be a good idea to upgrade to the latest version of seL4 and CAmkES. I can pull the latest kernel and merge the compatible libraries with my changes and get everything to compile; however, when I load it on the board it fails... Failed to find any untyped capable of creating an object at address 0x20c4000 Failed to find a way to map address 0x20c4000 Failed to find any untyped capable of creating an object at address 0x20c8000 Failed to find a way to map address 0x20c8000 Failed to find any untyped capable of creating an object at address 0x20e0000 Failed to find a way to map address 0x20e0000 Failed to find any untyped capable of creating an object at address 0x21bc000 Failed to find a way to map address 0x21bc000 Here is my CAmkES configuration which sets up the Ethdrivers cnode and untypes. Keep in mind this works with seL4 3.2 ethdriver.simple = true; ethdriver.cnode_size_bits = 12; ethdriver.simple_untyped20_pool = 4; ethdriver.heap_size = 0; ethdriver.mmios = "0x02188000:0x4000:12, 0x021BC000:0x4000:12, 0x020E0000:0x4000:12, 0x020A4000:0x4000:12, 0x020B0000:0x4000:12, 0x020C4000:0x4000:12, 0x020C8000:0x1000:12"; Can anyone see the problem? Thanks, Chris Guikema

2 2

Re: [seL4] Memory protections within userspace and hardware/driver support
by Devin Harper 03 May '17

03 May '17

Hi, I read the whole FAQ. Does the "bug-free" protections for privacy apply to within each app of the same Linux virtual machine (overcoming memory bugs built in apps), between apps of the same Linux virtual machine (overcoming memory bugs built in the Linux kernel/GNU distro), or merely between different virtual machines (allowing any Linux kernel/GNU distro to be compromised, just not allowing them to compromise each other)? Furthermore, do I understand correctly that sel4 will only work on a few pieces of computer hardware, or will it work on everything the Linux kernel supports (has drivers for)? If sel4 will work on everything the Linux kernel supports (has drivers for), then do the same bug-free promises hold true on those hardwares in addition to the hardwares sel4 has already been tested on? Thanks!

2 1

Can I running camkes-arm-vm on HiKey board
by li94575 02 May '17

02 May '17

Hi all, Now, only exynos5 and tk1 are supported for running virtualised Linux on seL4. If I want to port it to HiKey board, is this possible?

3 2

questions about TK1 VM
by PX 01 May '17

01 May '17

Hi, all I have some questions about TK1 VM. I want to save the execution status of the TK1 VM. First, I stop the VM, then I use the function, seL4_TCB_ReadRegisters() to read the VM's registers into a buffer. Here are my questions: 1. Before I call the function, seL4_TCB_ReadRegisters(), do I need to flush TLB of CPU? If so, where is the library I need to check for this function? 2. The register values in the structure, seL4_UserContext, are VMM's physical addresses or virtual addresses? Best wishes Peng

2 1

sel4test failing TEST_SCHED0004 on iMX6
by Robert Kaiser 20 Apr '17

20 Apr '17

Hi all, I just tried to run the test suite on iMX6. Using the current version from github, I got this result: ---------------------------- ..... Test suite failed. 200/202 tests passed. 200/202 tests passed. *** FAILURES DETECTED *** ---------------------------- Further checking into the log shows this: ---------------------------- ..... Starting test 51: TEST_SCHED0004 TEST_SCHED0004 Running test SCHED0004 (Test threads at all priorities) _allocman_cspace_alloc@allocman.c:252 Regular cspace alloc failed, and failed from watermark vka_alloc_object_at_maybe_dev@object.h:46 Failed to allocate cslot: error 1 new_pages_at_vaddr@vspace.c:331 Failed to allocate page sel4utils_configure_thread_config@thread.c:77 ipc buffer allocation failed Assertion failed: error == 0 ([.....]/seL4test/apps/sel4test-tests/src/helpers.c: create_helper_thread: 346) Failure: result == SUCCESS at line 343 of file [.....]/seL4test/apps/sel4test-driver/src/main.c Failure: Test check failure (see log). at line 0 of file ..... ---------------------------- The same test is run a second time further down below the log, giving the same result. I tested this on two different IMX6 platforms (SabreLite and Wandboard). Both showed identical results. Is this a known problem? Cheers Robert -- Robert Kaiser Technische Informatik Hochschule RheinMain Wiesbaden Rüsselsheim Computer Engineering RheinMain University of Applied Sciences robert.kaiser(a)hs-rm.de http://www.cs.hs-rm.de/~kaiser tel:(+49)611-9495-1292 fax:(+49)611-9495-1210 Postanschrift/Postal Address: Robert Kaiser, Hochschule RheinMain, FB DCSM/Informatik Unter den Eichen 5, 65195 Wiesbaden, Germany

2 2

smaccm/sel4arm-vmm-manifest complie problem
by 高文博 19 Apr '17

19 Apr '17

hi everyone! i am doing research about sel4.i used https://github.com/smaccm/sel4arm-vmm-manifest code. and complie it.than it build out kernel.elf only. but where is linux? expecting your answers. thanks very much! gao. -- 高文博数据通信科学技术研究所

2 1

smaccm/sel4arm-vmm-manifest compile problem
by 高文博 15 Apr '17

15 Apr '17

hi everyone! i am doing research about sel4.i used https://github.com/smaccm/sel4arm-vmm-manifest code. and compile it.than it build out kernel.elf only. but where is linux? expecting your answers. thanks very much! gao.

1 0

how to debug libsel4allocman
by Vasily A. Sartakov 14 Apr '17

14 Apr '17

Greetings I am using a 4.0 compatible seL4 snapshot derived from mainline several months ago as a base for seL4/MIPS port. Currently, I am debugging sel4tests. My goal — make everything working before moving to hardware. By «everything» I mean different configurations of the system (optimization flags, syscall attributes, fast/slow path, etc). For example, most stable build uses «CONFIG_LIB_SEL4_INLINE_INVOCATIONS», less stable build, which I am debugging now, uses «CONFIG_LIB_SEL4_PUBLIC_SYMBOLS». This configuration crashes at the start when I am trying to allocate memory for the first test: Starting test suite sel4test Starting test 0: TEST_TRIVIAL0001 TEST_TRIVIAL0001 b24e68 b0cc4c b0cc2c b0cc2c sel4test-tests 0 0 * Loading segment 00400000-->005748a4 * Loading segment 00575000-->00689d84 alloc->num_cspace_slots = 30 alloc->num_cspace_slots = 29 alloc->num_cspace_slots = 28 alloc->num_cspace_slots = 27 alloc->num_cspace_slots = 26 alloc->num_cspace_slots = 25 alloc->num_cspace_slots = 24 alloc->num_cspace_slots = 23 alloc->num_cspace_slots = 22 alloc->num_cspace_slots = 21 alloc->num_cspace_slots = 20 alloc->num_cspace_slots = 19 alloc->num_cspace_slots = 18 alloc->num_cspace_slots = 17 alloc->num_cspace_slots = 16 alloc->num_cspace_slots = 15 alloc->num_cspace_slots = 14 alloc->num_cspace_slots = 13 alloc->num_cspace_slots = 12 alloc->num_cspace_slots = 11 alloc->num_cspace_slots = 10 alloc->num_cspace_slots = 9 alloc->num_cspace_slots = 8 alloc->num_cspace_slots = 7 alloc->num_cspace_slots = 6 alloc->num_cspace_slots = 5 alloc->num_cspace_slots = 4 alloc->num_cspace_slots = 3 alloc->num_cspace_slots = 2 alloc->num_cspace_slots = 1 _allocman_cspace_alloc@allocman.c:254 Regular cspace alloc failed, and failed from watermark alloc->num_cspace_slots == 0_refill_watermark:374 slota = 0 alloc->num_cspace_slots = 1 _allocman_cspace_alloc@allocman.c:254 Regular cspace alloc failed, and failed from watermark alloc->num_cspace_slots == 0_refill_watermark:374 slota = 0 alloc->num_cspace_slots = 1 _allocman_cspace_alloc@allocman.c:254 Regular cspace alloc failed, and failed from watermark I see, that: 243: error = alloc->cspace.alloc(alloc, alloc->cspace.cspace, slot); returns the error, and then we allocating memory from the watermark. In other builds (for example, with CONFIG_LIB_SEL4_INLINE_INVOCATIONS attributes), I do not see this issue - there are no errors on return. So, I need to debug function to be sure that I am receiving in the kernel proper arguments and so one, but I do not understand how this part of the code works. Do you have any documentation, or slides or just simple diagrams how this allocator work? What functions are responsible for generating error return, where exactly allocation is performed and how to debug this. Thank you.

1 0

Questions about userspace memory allocation
by Daniel (Xiaolong) Wang 11 Apr '17

11 Apr '17

Hi all, I have a couple questions hope someone can help me clear it out. I understand that after booting up, the kernel keep tracking of all physical memory as Untyped and hand it over to the init thread. It seems like the kernel create both idlethread and init thread and, but it only create a TCB object. 1). I wonder when the init thread's frame and PD are created, and how the thread's stack and heap is allocated? 2). I wonder is there a limit or default value for how much physical memory init thread uses at booting time? Thanks -Dan

2 1

Questions about Userspace memory allocation
by Daniel Wang 09 Apr '17

09 Apr '17

Hi all, I have a couple questions hope someone can help me clear it out. I understand that after booting up, the kernel keep tracking of all physical memory as Untyped and hand it over to the init thread. It seems like the kernel create both idlethread and init thread and, but it only create a TCB object. 1). I wonder when the init thread's frame and PD are created, and how the thread's stack and heap is allocated? 2). I wonder is there a limit or default value for how much physical memory init thread uses at booting time? Thanks -Dan

1 0

Creating process from not root process
by rad021993＠yandex.ru 02 Apr '17

02 Apr '17

Hi all, I try to create process (process2) from not root process (process1). Process1 has own cspace and vspace (fields 'create_cspace' and 'create_vspace' are set to true in process1' config). I try to create process2 like in the root process (4-th example in sel4 tutorials), but I can't obtain bootinfo to create allocman. As I understood it, this info available only from root process. Also I found function to create allocman via bootstrap function (like in example_bootstrap.c), but I also need to get process1' vspace and cspace to attach them to allocman. I do not understand, how I can get the needed info. Could you tell me how I can do it? Best regards, Rinat Dobrokhotov

2 1

Re: [seL4] Devel Digest, Vol 35, Issue 1
by talos 01 Apr '17

01 Apr '17

Re: 1. Re: errors when make camkes-tutorials-manifest the output of ls -al for my .stack directory: drwxrwxr-x 4 talos talos 4096 3月 29 17:19 .stack my username is talos Thanks ------------------ Original ------------------ From: "devel-request";<devel-request(a)sel4.systems>; Date: Sat, Apr 1, 2017 06:29 AM To: "devel"<devel(a)sel4.systems>; Subject: Devel Digest, Vol 35, Issue 1 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: errors when make camkes-tutorials-manifest (Stephen.Sherratt(a)data61.csiro.au) 2. Announcing seL4 5.0.0 (Kent.Mcleod(a)data61.csiro.au) 3. Creating process from not root process (rad021993(a)yandex.ru) 4. Confusion with various memory address (Daniel (Xiaolong) Wang) ---------------------------------------------------------------------- Message: 1 Date: Fri, 31 Mar 2017 03:46:28 +0000 From: <Stephen.Sherratt(a)data61.csiro.au> To: <devel(a)sel4.systems> Subject: Re: [seL4] errors when make camkes-tutorials-manifest Message-ID: <1490931983542.96806(a)data61.csiro.au> Content-Type: text/plain; charset="iso-8859-1" Hi Talos, Are you the owner of /home/talos/.stack ? For comparison, the output of ls -al for my .stack directory: drwxr-xr-x 10 ssteve ssteve 4096 Jan 24 15:25 .stack My username is ssteve. You could also try renaming your .stack directory so stack can create a new one for you. Cheers, Stephen ________________________________ From: Devel <devel-bounces(a)sel4.systems> on behalf of talos <2486580938(a)qq.com> Sent: Thursday, 30 March 2017 9:28 PM To: devel Subject: [seL4] errors when make camkes-tutorials-manifest Hi, When I made this tutorials, there was an error; You are not the owner of '/home/talos/.stack/'. Aborting to protect file permissions. Retry with '--allow-different-user' to disable this precaution How can I do this, thanks! -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://sel4.systems/pipermail/devel/attachments/20170331/b3b2c08e/attachmen…>

1 0

Confusion with various memory address
by Daniel (Xiaolong) Wang 01 Apr '17

01 Apr '17

Hi all, I have a probably a dumb question that need some clarification. I was reading the kernel source code and I’m little bit confused with the three data type: paddr_t, pptr_t, vptr_t and the following three data struct related to them. typedef struct region { pptr_t start; pptr_t end; } region_t; typedef struct p_region { paddr_t start; paddr_t end; } p_region_t; typedef struct v_region { vptr_t start; vptr_t end; } v_region_t; Based on how those are being used I assume the paddr_t and p_region are data struct for physical address, vptr_t and v_region are for virtual address. According to the following functions seem that the translation between physical address to pptr_r is by adding/subtracting a offset. But I’m confused with the pptr_t and region I wonder what are those for? Tank you very much! static inline void* CONST ptrFromPAddr(paddr_t paddr) { return (void*)(paddr + physMappingOffset); } static inline paddr_t CONST addrFromPPtr(void* pptr) { return (paddr_t)pptr - physMappingOffset; } static inline region_t CONST paddr_to_pptr_reg(p_region_t p_reg) { return (region_t) { p_reg.start + physMappingOffset, p_reg.end + physMappingOffset }; } static inline p_region_t CONST pptr_to_paddr_reg(region_t reg) { return (p_region_t) { reg.start - physMappingOffset, reg.end - physMappingOffset }; } Thanks -Dan

2 1

Announcing seL4 5.0.0
by Kent.Mcleod＠data61.csiro.au 31 Mar '17

31 Mar '17

We are pleased to announce the release of 5.0.0 of seL4. Listed below are a few of the key changes in this release: Below are the changes to the seL4 ABI and API: Generic changes: * Add missing case to seL4_getFault (seL4_Fault_DebugException) * Explicitly pack bootinfo data structures * Modify FinalizeLog syscall - Now returns a number of entries in the log * Extend bootinfo to support potentially arbitrary additional structures * Deprecate bootinfo management in libsel4 - a replacement, platsupport_get_bootinfo can be found in libsel4platsupport x86 specific changes: * Pass VBE information from multiboot through bootinfo * Remove PAE support x86-64 specific changes: * VT-x related cap and object definitions added * seL4_VMEnter syscall added arm specific changes: * ARM-HYP: VCPU interface for manipulating banked registers added * plat: added nvidia tx1 support * ARM-HYP: Add support for save/restore of debug registers * Add aarch64 implementation = Upgrade notes = * This release breaks both API and ABI and is not source compatible with the earlier versions. = Full changelog = Use {{{git log 4.0.0..5.0.0}}} in https://github.com/seL4/seL4 = More details = See the 5.0.0 manual (http://sel4.systems/Info/Docs/seL4-manual-5.0.0.pdf) included in the release for detailed descriptions of the new features. The release tarballs can be directly downloaded from: https://github.com/seL4/seL4/archive/5.0.0.tar.gz [9e143c75c68edcaefc5506caea341890 5.0.0.tar.gz] Contributors: Adrian Danis Hesham Almatary Amirreza Zarrabi Kent McLeod Jack Suann Kofi Doku Atuah Amirreza Zarrabi Donny Yang Anna Lyons Stephen Sherratt Partha Susarla Thomas Sewell Frank Li Jeff Waugh Berkus Decker Corey Richardson Kent Mcleod Please let us know of any issues that you run into by creating an issue in the issue tracker: https://github.com/seL4/seL4/issues -- Kent McLeod Kernel engineer DATA61 | CSIRO E kent.mcleod at data61.csiro.au www.data61.csiro.au CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61

1 0

errors when make camkes-tutorials-manifest
by talos 31 Mar '17

31 Mar '17

Hi, When I made this tutorials, there was an error; You are not the owner of '/home/talos/.stack/'. Aborting to protect file permissions. Retry with '--allow-different-user' to disable this precaution How can I do this, thanks!

2 1

Allocation manager and processes
by Rinat Dobrokhotov 28 Mar '17

28 Mar '17

Hi all, 1. Could you check if my thoughts are right? The allocation manager is global object and there is only one instance for whole system. If I need in creation kernel objects I should create _one_ allocman above some array of memory. 2. I have the first question because I work with processes now. In the root process I create two different processes based on the elf image via allocman. Then I try to manage (suspend, change priority, etc.) process1 by process2. But I can't get process1 object from process2 because both of them belong to root process and belong to root process' memory space. As I understand it, I should copy cap which belongs to process1 to process2, then I will be able to manage them. Could you tell me if I am right? -- Best regards, Rinat Dobrokhotov

2 1

CapDL & RT
by Richard Habeeb 23 Mar '17

23 Mar '17

Hello all, I see that the master branch of CapDL has some support for the RT kernel, but I am having some trouble building it against the current public sel4 RT branch. Which version of the RT kernel does capDL work with? Or, is it still a work in progress? Thanks, Richard -- Richard Habeeb Research Assistant, Computer Science, USF PGP: https://goo.gl/VhmGGu https://habeebr.bitbucket.io/

2 1

sel4 kernel boot problem on i.mx6q board
by shijun zhao 21 Mar '17

21 Mar '17

Hi everyone, I am running sel4 on i.mx6q sabre board. I use the sabre_debug_xml_defconfig config file. However, the image stops at "Jumping to kernel-image entry point..." when I run it on the board. Following is the printed messages: ## Starting application at 0x20000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A9 r2p10 paddr=[20000000..2030081f] ELF-loading image 'kernel' paddr=[80000000..80032fff] vaddr=[e0000000..e0032fff] virt_entry=e0000000 ELF-loading image 'sel4test-driver' paddr=[80033000..80406fff] vaddr=[10000..3e3fff] virt_entry=203d0 Enabling MMU and paging Jumping to kernel-image entry point... There are some warnings during compilation, all of which are caused by arm-none-eabi/bin/ld. And I see that the sel4 wiki shows how to solve the warnings: *To fix, do make menuconfig visit seL4 Libraries→Build musl C Library and untick libmuslc use precompiled archive then do make clean and attempt to rebuild.* However, there is no *Build musl C library* in my menuconfig, and there are only *libmuslc *and *libsel4muslcsys *options in the seL4 libraries. Can anyone tell me how to solve this problem? Thanks! Best Regards, Shijun

2 4

Help accessing physical address on zynq7000
by Brandon, Jeffrey - 0553 - MITLL 21 Mar '17

21 Mar '17

Hello, I've been getting started with seL4 on the zynq7000 and I am looking for resources on how to read/write physical memory for memory mapped io purposes. If there is a relevant tutorial or manual to reference I haven't come across it yet so I wanted to ask here. Any other guidance as to how to think about and work with capabilities would be useful at this stage. I'm working with a modified version of the sel4test repository. Looking at that I found env.simple (simple_t defined https://github.com/seL4/seL4_libs/blob/a1c031b0885dec4ddf1ee1f8866bcd23dcca6 ac3/libsel4simple/include/simple/simple.h) which seems to contain function pointers for some relevant functions to what I'm trying to do, but I am not entirely sure how to go about using them. What needs to be initialized first and how do I go about that? Any guidance greatly appreciated, Thanks. Jeff Brandon Associate Staff MIT Lincoln Laboratory 05-53 Secure Resilient Systems and Technology Ph: 781.981.9233

2 1

TK1 VMM SMMU Translation Error
by Enrique Leon 15 Mar '17

15 Mar '17

Hello All, We have recently run into an issue trying to boot the TK1 VMM on a TK1 Jetson board. The kernel tries to run but soon runs into translation errors after a couple of seconds. We are using the non-secure dtb with the initrd image. Here are some of the lines, it continues on like this and never stops. SMMU Address translation error: ID: 1 address: 0x0 type: 6 direction: 0x0 IOPT permission: read 0x0 write 0x0 nonsecure 0x0 SMMU Address translation error: ID: 1 address: 0x18fc00 type: 6 direction: 0x0 IOPT permission: read 0x0 write 0x0 nonsecure 0x SMMU Address translation error: ID: 1 address: 0x912c0 type: 6 direction: 0x0 We had success running the VM using the previous commit from camkes-arm-vmm repo, but the newest commit has introduced this issue. We have isolated it to line 93 in the "vmm_common.camkes" file. Removing "0x54200000:18", // Display A" from the file fixes the problem and we can boot as normal. We are also running Uboot 2010-10-rc5 as suggested by a email on the board. I am still new to working down to this level of code so any help in understanding this problem is appreciated.

3 3

Linux Virtualization on ODROID-XU4
by Norrathep Rattanavipanon 14 Mar '17

14 Mar '17

Hi, I tried to run Linux on top of seL4 in ODROID-XU4 device. I followed the instruction in https://sel4.systems/Community/Devdays/Workshop2016/ihor-sel4ws2016.pdf. I run with normal u-boot. And I got to the part that it printed out: We used 57776 CSlots (11.02% of our CNode) Done; suspending... Initialising UART driver Initialising UART driver Then it stops there. Any idea of what went wrong here? Best, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 2

How to implement RM scheduling on seL4
by wang 07 Mar '17

07 Mar '17

Hello, I'm now studying seL4/seL4test and try to implement the RM scheduling on seL4test. I understand how the RM scheduling works, but just don't know how to make it happen on seL4test. So where can I start? In addition, I put the sel4test driver image on my board and run, it shows "206/206 tests passed. All is well in the universe" at the last line. Does it means that the seL4test project runs correctly? Thanks!

3 3

Using Rump kernels to run unmodified NetBSD drivers on seL4
by Kent.Mcleod＠data61.csiro.au 07 Mar '17

07 Mar '17

Last year for my honors thesis I evaluated rump kernels as a way of running unmodified NetBSD drivers on seL4. This work has recently been pushed out with a corresponding blog post: https://research.csiro.au/tsblog/using-rump-kernels-to-run-unmodified-netbs…. This was done by adding support for the Rumprun unikernel to use seL4 as a target platform. Currently ia32 and x86_64 is supported and we have tested the e1000 network card driver and networking stack using Dell Sandy Bridge and Haswell machines. Rump kernels are a project that allows unmodified NetBSD OS component reuse in other systems (http://rumpkernel.org/) We want to use rump kernels as a way of providing drivers and other OS components such as filesystems and networking stacks on seL4 such as in CAmkES components. Some sample applications can be found here (https://github.com/SEL4PROJ/rumprun-sel4-demoapps) and a link to the thesis can be found here (http://www.disy.cse.unsw.edu.au/theses_public/16/kentm.pdf) Kent McLeod

2 1

ARM timer driver and interrupts
by Wladislav Wiebe 01 Mar '17

01 Mar '17

Hello, I wrote a new timer driver for this timer device: http://www.ti.com/lit/ug/sprugv5a/sprugv5a.pdf I am already able to run the seL4 testsuite successfully, except the interrupt/timer tests. It waits forever @ wait_for_timer_interrupt(env); I've uploaded the driver temporary to: https://github.com/wwladikw/devel/blob/master/timer.c Any idea what could be wrong? I am able to run the timer periodically or as oneshot. The gic_390 interrupt driver in the kernel should also be compatible with the gic_400, for my understanding, right? The SoC I am using contains a Coretex A15. Thanks a lot in advance! Wladislav Wiebe

3 9

Boot Hyp mode in elfloader
by SHI, Yao 27 Feb '17

27 Feb '17

I am trying to boot CAmkES-ARM-VM and got problem in elfloader. I tested Jetson-TK1 and TK1-SOM. The results are same. I've set bootm_boot_mode=nonsec in u-boot and tracked registers in function switch_to_hyp_mode(). 1) Enter switch_to_hyp_mode(), after asm volatile ("mrc p15, 0, %0, c1, c1, 0":"=r"(scr)); ==> scr == 0x100, in which NS==0, HCE==1, SCD==0, SIF==0 2) Then switch_to_hyp_mode() changes NS to 1, so scr==0x101 asm volatile ("mcr p15, 0, %0, c1, c1, 0"::"r"(scr)); 3) switch_to_hyp_mode() changes cpsr to Hyp mode asm volatile ("cps %0\n\t" "isb\n" ::"I"(HYPERVISOR_MODE)); 4) The final step, switch_to_hyp_mode() reads cpsr, asm volatile ("mrs %0, cpsr":"=r"(scr)); ==> scr == 0x6000001da, in which cpsr.M==0x1a, cpsr.I==1, cpsr.F==1, cpsr.A==1 Finally, the process died here. My questions are, 1) Are NS==0 and HCE==1 correct when entering switch_to_hyp_mode() ? 2) Is the final status (cpsr.F==cpsr.I==cpsr.A==1) expected? 3) Any other mistake I might make? Yao

2 4

Clarification on seL4 on RPi3b
by Joseph Adam Powers 23 Feb '17

23 Feb '17

It seems to be necessary for me to use the debug output using a serial cable on UART0 u-boot seems to be waiting for a Ethernet or serial cable connection to finish boot process. I don't have the serial cable so I just need some understanding that that is the case considering that I followed the rest of the instructions on the blog at https://research.csiro.au/tsblog/sel4-raspberry-pi-3/ , newbie question btw.

2 1

RT and domains
by rad021993＠yandex.ru 22 Feb '17

22 Feb '17

Hi, Could you tell me why did you not implement domains in RT kernel version? Are there any difficulties? I'm going to add support of domains, and at the first sight I don't see any difficulties.

3 3

seL4 no longer support zynq7000 board?
by wang 22 Feb '17

22 Feb '17

Hello, https://wiki.sel4.systems/Hardware On this seL4wiki hardware page I find the link of Zynq7000 turns grey, and the page says "This page does not exist yet. You can create a new empty page, or use one of the page templates." So it means seL4 do not support zynq7000 any more? And how can I run seL4/seL4test on zynq7000 board? Thanks!

2 1

seL4/seL4test on odroid-xu4
by wang 17 Feb '17

17 Feb '17

Hello, I've just got my odroid-xu4 board and tried to port seL4test onto it, but met some problems that cannot procceed. Do you have any guide or tutorial for it step by step? I think I may have problem of initializing and partitioning of a new sd card(main problem?). And maybe something is wrong with the uboot or fastboot, but I'm not quite sure about that. This is my fist time using this devel, don't know whether this message was sent correctly or not :) Looking forward to get some help by you guys. Thanks! Wang

1 0

seL4/seL4test on odroid-xu4
by wang 17 Feb '17

17 Feb '17

Hello, I've just got my odroid-xu4 board and tried to port seL4test onto it, but met some problems that cannot procceed. Do you have any guide or tutorial for it step by step? I think I may have problem of initializing and partitioning of a new sd card(main problem?). And maybe something is wrong with the uboot or fastboot, but I'm not quite sure about that. This is my fist time using this devel, don't know whether this message was sent correctly or not :) Looking forward to get some help by you guys. Thanks! Wang

1 0

camkes DMA with predetermined physical addresses
by Gareth Howard 17 Feb '17

17 Feb '17

1 0

Deriving and Revoking IRQControl caps
by Andrew Gacek 16 Feb '17

16 Feb '17

Based on the seL4 manual it sounds like IRQControl caps only support one level of derivation. What is the reason for this restriction? We encountered a case where we wanted to hand out an IRQControl for a specific irq and then later revoke access, but we couldn't do it because the IRQControl for a specific irq is already a derived capability. -Andrew

5 10

imx6 U-Boot Issues
by Chris Guikema 16 Feb '17

16 Feb '17

Hello, I am using the i.mx6 to test a networking example that function in QEMU. To load the application, I am using the u-boot that comes pre-compiled on the micro-sd. I am able to dhcp to my tftpserver and grab the seL4 image, and when I run the "go 20000000" command, I get the following: ## Starting application at 0x20000000 ... AP Kernel returned back to the elf-loader. abort() called. Looking through the code, that error is in non_boot_main, yet that function call is wrapped by #ifdef CONFIG_SMP_ARM_MPCORE Which is undefined. That makes me think that the main() in boot.c is not being accessed and the elfloader isn't being run properly. Is this a u-boot issue, or is it that way I have everything setup? Is it a requirement to use the pre-compiled u-boot binary for the i.mx6? Thanks, Chris Guikema

2 2

CAmkES ARM VM boot on TK1
by SHI, Yao 15 Feb '17

15 Feb '17

Hi, I am trying to run CAmkES ARM VM on TK1. I downloaded built the image using: repo init -u https://github.com/SEL4PROJ/camkes-arm-vm-manifest repo sync make tk1_vm_defconfig make And then ran the image on the hardware. It stopped after loading seL4 in nonsecure HYP mode, Tegra124 (Jetson TK1) # bootelf CACHE: Misaligned operation at range [90000000, 90007408] CACHE: Misaligned operation at range [90007408, 9134c900] CACHE: Misaligned operation at range [9134c900, 9134c908] CACHE: Misaligned operation at range [91350000, 91360820] ## Starting application at 0x90000000 ... ELF loader: monitor mode init done Copy monitor mode vector from 90001000 to a7f00000 size 50 Number of IRQs: 192 Load seL4 in nonsecure HYP mode 600001da Then I tried to build a monitor mode image and got this, Tegra124 (Jetson TK1) # bootelf CACHE: Misaligned operation at range [90000000, 90007250] CACHE: Misaligned operation at range [90007250, 9134c710] CACHE: Misaligned operation at range [91350000, 91360820] ## Starting application at 0x90000000 ... ELF loader: monitor mode init done Copy monitor mode vector from 90001000 to a7f00000 size 50 ELF-loader started on CPU: ARM Ltd. Cortex-A15 r3p3 paddr=[90000000..9136081f] ELF-loading image 'kernel' paddr=[80000000..80031fff] vaddr=[e0000000..e0031fff] virt_entry=e0000000 ELF-loading image 'capdl-loader-experimental' paddr=[80032000..8155bfff] vaddr=[10000..1539fff] virt_entry=17580 Enabling MMU and paging Jumping to kernel-image entry point... abort() called. Anyone may tell me the possible problem? Thank you very much. Yao

4 8

Coretex A15 periodic timer interrupts
by Wladislav Wiebe 14 Feb '17

14 Feb '17

Hello, I wonder if the generic timer https://github.com/seL4/util_libs/blob/master/libplatsupport/src/arch/arm/g… can be extended by timer->periodic timer->handle_irq to be able to run the sel4 testsuite which requires timer IRQ's such as https://github.com/seL4/sel4test/blob/master/apps/sel4test-tests/src/tests/… Right now I am able to get timer_get_time(env->timer->timer); by using the generic timer, but I am missing the periodic time and the irq handler for the Coretex A15 generic timer implementation. Some ideas if there is some tricky way to get it running? Thanks in advance! - Wladislav Wiebe

1 0

Re: [seL4] SDHC drivers (cont.)
by Norrathep Rattanavipanon 13 Feb '17

13 Feb '17

Hi Siwei, So, I tried the code using Kingston microSDHC but it still couldnt read the card. However, the code works perfectly when loaded from the SD slot (with microSD to SD adapter), instead of the microSD slot. I also found that for some reasons, if mmc dev 1 is used in u-boot, the program wouldnt be able to read/write the micro-sd card. I'm kind of good for now but still curious about that. Do you have any idea what might have caused this? Best, Oak On Mon, Jan 23, 2017 at 11:07 AM, Norrathep Rattanavipanon <nrattana(a)uci.edu > wrote: > Thanks Siwei. I really appreciate your help. > Yeah so I tried your image with three different micro-sd cards and none of > them works (still stuck after printing the card's capacity). > I'll buy Kingston microsdhc class 4 and try on that, will let you know if > it works or not. > > Best, > Oak > > On Mon, Jan 23, 2017 at 12:03 AM, <Siwei.Zhuang(a)data61.csiro.au> wrote: > >> Hi Oak, >> >> >> Here is what exactly I did, >> >> >> $ mkdir sel4-sdcard >> >> $ cd sel4-sdcard >> >> $ repo init -u https://github.com/SEL4PROJ/sel4-tutorials-manifest.git >> -m sel4-tutorials-master.xml >> >> $ repo sync >> >> $ cd projects >> >> $ git clone https://github.com/SEL4PROJ/projects_libs.git >> >> $ cd ../libs >> >> $ ln -sf ../projects/projects_libs/libsdhcdrivers libsdhcdrivers >> >> $ ln -sf ../projects/seL4_libs/libsel4sync libsel4sync >> >> >> Then, I copied my sdcard app into sel4-sdcard/apps. >> >> The sdcard app directory has Kconfig, Kbuild, Makefile and src/main.c >> >> >> ------------ Kconfig ---------------- >> menuconfig APP_SDCARD >> bool "SD card" >> default y >> depends on HAVE_LIBC >> depends on LIB_SEL4_PLAT_SUPPORT >> depends on LIB_SEL4_VKA >> depends on LIB_SEL4_UTILS >> depends on LIB_UTILS >> depends on LIB_CPIO >> depends on LIB_SEL4 >> depends on LIB_ELF >> help >> SD card app. >> >> >> >> ------------ Kbuild ----------------- >> apps-$(CONFIG_APP_SDCARD) += sdcard >> >> sdcard: common libsel4utils libutils libsel4 libmuslc libsel4muslcsys \ >> libsel4vka libsel4allocman libsel4vspace libsel4simple >> libsel4simple-default \ >> libsel4platsupport libsel4platsupport libcpio libelf \ >> libsel4sync libsdhcdrivers libsel4debug >> >> ------------ Makefile --------------- >> # Targets >> TARGETS := sdcard.bin >> >> ENTRY_POINT := _sel4_start >> >> # Source files required to build the target >> CFILES := $(patsubst $(SOURCE_DIR)/%,%,$(wildcard >> $(SOURCE_DIR)/src/*.c)) >> ASMFILES := $(patsubst $(SOURCE_DIR)/%,%,$(wildcard >> $(SOURCE_DIR)/src/*.S)) >> OFILES := archive.o >> >> # Libraries required to build the target >> LIBS = c sel4 sel4muslcsys sel4vka sel4allocman \ >> platsupport sel4platsupport sel4vspace elf \ >> sel4utils sel4simple utils sel4simple-default cpio \ >> sel4sync sdhcdrivers sel4debug >> #CFLAGS += -Werror >> >> include $(SEL4_COMMON)/common.mk >> >> archive.o: ${COMPONENTS} >> $(Q)mkdir -p $(dir $@) >> ${COMMON_PATH}/files_to_obj.sh $@ _cpio_archive $^ >> >> >> I also edited sel4-sdcard/Kconfig, added the following to the related >> menus, >> >> source "apps/sdcard/Kconfig" >> >> source "libs/libsdhcdrivers/Kconfig" >> >> source "libs/libsel4sync/Kconfig" >> >> >> I've attached the config file, copy it to configs directory, then do >> "make sdcard_defconfig". >> >> I've also attached the binary image that I compiled. >> >> >> Since the u-boot command works, it doesn't seem that the controller is >> disabled. Also try another card if possible, my card is Kingston micro SDHC >> class 4. The driver only implements very basic single block read/write. I'm >> not surprised that it doesn't work for some cards. >> >> >> - Siwei >> >> >> ------------------------------ >> *From:* Norrathep Rattanavipanon <nrattana(a)uci.edu> >> *Sent:* Monday, 23 January 2017 4:59 PM >> *To:* Zhuang, Siwei (Data61, Kensington NSW) >> >> *Subject:* Re: [seL4] SDHC drivers (cont.) >> >> Hi Siwei, >> >> Thank you for helping me out. I am still unable to get it to work even if >> using your code with the latest kernel (4.0) and latest libraries >> (downloaded from https://github.com/SEL4PROJ/sel4-tutorials-manifest >> master branch) >> >> I also tried calling mmc read command in u-boot and it was able to read >> data from the card just fine. >> I'm not really sure how I can check if the host controller works >> properly. Do you mean I can do it in seL4? >> >> Also, is it possible if you can upload the binary image file (and the >> build config) so that I can test on my board really quick? I suspect that >> either I miss something for the build or my micro-sd is not working. >> >> Thank you again for your help, >> Oak >> >> On Thu, Jan 19, 2017 at 11:12 AM, Norrathep Rattanavipanon < >> nrattana(a)uci.edu> wrote: >> >>> Hi Siwei, >>> >>> Yes, I believe mmc_card_capacity returns the correct value (4026531840 >>> <(402)%20653-1840> - my microsd is 4GB). >>> >>> And my code does not do any interrupt handling. In fact, that's all the >>> code in the root userspace process (besides initializing vka, vspace and >>> simple objects) and there is no other process. >>> >>> I also tried using a callback as mmc_block_read's argument, instead of >>> using NULL, but it also does not work. >>> >>> On Wed, Jan 18, 2017 at 8:41 PM, <Siwei.Zhuang(a)data61.csiro.au> wrote: >>> >>>> Hi Oak, >>>> >>>> >>>> Do you get the correct card capacity by calling mmc_card_capacity? If >>>> you don't, you'd need to check if the hardware is enabled in your >>>> bootloader. >>>> >>>> >>>> Are you doing any interrupt handling? As you don't supply a callback >>>> function to mmc_block_read, the read function would block until the >>>> hardware responses. In this case, mmc_block_read handles the interrupt >>>> itself. It would trigger a dead lock if you also handles the interrupt. >>>> >>>> >>>> - Siwei >>>> >>>> >>>> ------------------------------ >>>> *From:* Devel <devel-bounces(a)sel4.systems> on behalf of Norrathep >>>> Rattanavipanon <nrattana(a)uci.edu> >>>> *Sent:* Thursday, 19 January 2017 9:54 AM >>>> *To:* Danis, Adrian (Data61, Kensington NSW) >>>> *Cc:* devel(a)sel4.systems; GTS >>>> *Subject:* Re: [seL4] SDHC drivers (cont.) >>>> >>>> Hi Adrian, >>>> >>>> Thank you for the reply. I fix it according to what you suggest but it >>>> still does not solve the problem (still hang at the same place. Do you have >>>> any other suggestions on what I should fix or how I should look into >>>> debugging it? >>>> >>>> Best, >>>> Oak >>>> >>>> On Tue, Jan 17, 2017 at 8:58 PM, <Adrian.Danis(a)data61.csiro.au> wrote: >>>> >>>>> Hi Oak, >>>>> >>>>> I don't know much about SD cards or this driver but it seems to me >>>>> like passing it a physical address of 0 isn't what you want, and whilst I >>>>> know nothing about the mmc hardware it seems reasonable to me that it might >>>>> hang trying to DMA to memory that doesn't exist. There is also the >>>>> additional problem that even if paddr was correct for the first page, there >>>>> is no guarantee that the 5 pages you have allocated are contiguously >>>>> physically even though they will be mapped contiguous virtually. >>>>> >>>>> My recommendation is to use the page dma allocator in >>>>> seL4_libs/libsel4utils/include/sel4utils/page_dma.h, this will >>>>> provide you an easy way to allocate/map pages for the purposes of DMA. So >>>>> instead of >>>>> >>>>> void *vaddr = vspace_new_pages(&vspace, seL4_AllRights, 5, seL4_PageBits); >>>>> uintptr_t paddr = 0; >>>>> >>>>> You would have >>>>> >>>>> ps_dma_man_t dma_man; >>>>> error = sel4utils_new_page_dma_alloc(&vka, &vspace, &dma_man); >>>>> void *vaddr = ps_dma_alloc(&dma_man, 5 * PAGE_SIZE_4K, PAGE_SIZE_4K, >>>>> 0, PS_MEM_NORMAL); >>>>> uintptr_t paddr = ps_dma_pin(&dma_man, vaddr, 5 * PAGE_SIZE_4K); >>>>> >>>>> As I said at the start, I don't know if this will actually fix your >>>>> current problem, but it's still something you will need to fix. >>>>> >>>>> Adrian >>>>> >>>>> >>>>> On Wed 18-Jan-2017 6:31 AM, Norrathep Rattanavipanon wrote: >>>>> >>>>> My apology that I have to continue the discussion from the old thread: >>>>> (http://sel4.systems/pipermail/devel/2016-October/001056.html) >>>>> My goal is to read and write data from/to micro sd in SabreLite >>>>> platform. >>>>> I tried both Adrain and Anna's suggestions in that thread and they >>>>> dont seem to fix the problem. Nothing returns error and I also changed >>>>> cacheable parameter in sel4utils_new_pages_at_vaddr to 0 (I believe this is >>>>> what Anna meant instead of setting 3rd argument of vspace_new_pages). >>>>> >>>>> The code's still stuck inside mmc_block_read function. I tracked it >>>>> down and it seems like BRR and BWR interrupt statuses are never set to 1 >>>>> I add my code below, please let me know if anything is wrong with my >>>>> code. >>>>> >>>>> ps_io_mapper_t io_mapper = {0}; >>>>> error = sel4platsupport_new_io_mapper(simple, vspace, vka, &io_mapper); >>>>> assert(error == 0); >>>>> >>>>> ps_io_ops_t io_ops = { >>>>> .io_mapper = io_mapper >>>>> }; >>>>> >>>>> sdio_host_dev_t* dev = (sdio_host_dev_t*) malloc(sizeof(*dev)); >>>>> assert(dev != NULL); >>>>> memset(dev, 0, sizeof(*dev)); >>>>> >>>>> enum sdio_id id = sdio_default_id(); // return id=3 >>>>> error = sdio_init(id, &io_ops, dev); >>>>> assert(error == 0); >>>>> >>>>> mmc_card_t* mmc_card = (mmc_card_t*) malloc(sizeof(*mmc_card)); >>>>> error = mmc_init(dev, &io_ops, mmc_card); >>>>> assert(error == 0 && mmc_card != NULL); >>>>> >>>>> void *vaddr = vspace_new_pages(&vspace, seL4_AllRights, 5, seL4_PageBits); >>>>> assert(vaddr != NULL); >>>>> >>>>> uintptr_t paddr = 0; >>>>> printf("mmc card capacity %llu bytes\n", mmc_card_capacity(*mmc_card)); >>>>> long read_len = mmc_block_read(*mmc_card, 0x50000, 1, vaddr, paddr, NULL, NULL); // Stuck here >>>>> printf("read %lu bytes\n", read_len); >>>>> >>>>> >>>>> >>>>> Thanks >>>>> Oak >>>>> >>>>> >>>>> >>>>> -- >>>>> Norrathep (Oak) Rattanavipanon >>>>> M.S. in Computer Science >>>>> University of California - Irvine >>>>> >>>>> >>>>> _______________________________________________ >>>>> Devel mailing listDevel@sel4.systemshttps://sel4.systems/lists/listinfo/devel >>>>> >>>>> >>>>> >>>> >>>> >>>> -- >>>> Norrathep (Oak) Rattanavipanon >>>> M.S. in Computer Science >>>> University of California - Irvine >>>> >>> >>> >>> >>> -- >>> Norrathep (Oak) Rattanavipanon >>> M.S. in Computer Science >>> University of California - Irvine >>> >> >> >> >> -- >> Norrathep (Oak) Rattanavipanon >> M.S. in Computer Science >> University of California - Irvine >> > > > > -- > Norrathep (Oak) Rattanavipanon > M.S. in Computer Science > University of California - Irvine > -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 1

seL4 on Zedboard
by Brandon, Jeffrey - 0553 - MITLL 01 Feb '17

01 Feb '17

Hi, I've been trying to get seL4 running on a Zedboard and I was wondering if there was any documentation on how to boot sle4 from an SD card. I've read http://sel4.systems/pipermail/devel/2016-December/001160.html and https://sel4.systems/Info/Hardware/General/ which mentions using ${loadaddr} but that doesn't seem to be defined on the Zedboard's u-boot. So far I've compiled the image targeting the zynq7000 and used the mkimage command from the general hardware page to try u-boot's fastboot, but fastboot doesn't seem to be available on the zynq either. I am a bit of a novice here. I worry that the solution may be simple but I am currently taking shots in the dark. I wanted to ask this list for any resources you may be aware of for getting sel4 test cases running on the Zed. Thanks for the help, Jeff Brandon 05-53 Secure Resilient Systems and Technology

2 3

arm_data_abort_exception
by Wladislav Wiebe 31 Jan '17

31 Jan '17

Hello, has somebody experience with running into arm_data_abort_exception after enabling the MMU/paging and jumping to the kernel image: .. ELF-loader started on CPU: ARM Ltd. Cortex-A15 r2p4 paddr=[90000000..904b041f] ELF-loading image 'kernel' paddr=[80000000..80033fff] vaddr=[f0000000..f0033fff] virt_entry=f0000000 ELF-loading image 'sel4test-driver' paddr=[80034000..8042dfff] vaddr=[10000..409fff] virt_entry=1e924 Enabling MMU and paging Jumping to kernel-image entry point... check_data_abort_exception() DFAR = 0xfff01014 DFSR = 0x7 ADFSR = 0x0 abort() called. I've dumped the DFAR/DFSR register -- Relevant config parts about the setup: CONFIG_ARCH_ARM_V7A=y CONFIG_ARCH_ARM=y CONFIG_ARCH_AARCH32=y CONFIG_ARM_CORTEX_A15=y CONFIG_PLAT_KEYSTONE=y Thanks in advance! -- WBR, Wladislav WIebe

2 12

Exposing ticks to the rt API
by Corey Richardson 30 Jan '17

30 Jan '17

Hi Anna, While analyzing some time related APIs, I've noticed that the x86 rt kernel assumes that the tsc frequency is constant and well represented by the measurement made at init by comparing against the PIT. It also exposes only microseconds and uses the internal calibration to convert that to/from ticks. I'm concerned about this behavior. The tsc can have up to 200ppm error if uncalibrated and not temperature controlled, from what I'm able to determine. I'd rather have all the public APIs take ticks and allow user space to determine how their timing requirements best correspond to ticks. This came up when wanting to measure how much running time a process/thread has used. Ideally, it's kept as a running count of ticks. In the current API, one can only observe microseconds consumed, converted by a potentially lossy ticksToUs (lossy when the rate isn't exactly known or tick->us conversion isn't an exact integer multiplication). It'd be more useful for me to have tick count directly. I'm also somewhat concerned with using the PIT to estimate the TSC rate, as I can't find anything about expected error of the PIT, and any slop there will influence all future kernel behaviors until reboot. One potential alternative is the ACPI PM timer or the HPET. Those run at higher frequencies, which would help reduce the error bounds on the rate estimation. Let me know what you think! If it's useful at all, I've written up some stuff about the work that inspired these thoughts: https://gitlab.com/robigalia/meta/blob/master/blog/_drafts/2016-12-23-what-… Merry Christmas, -- cmr http://octayn.net/

4 4

strange code in thread.c
by Berkus 30 Jan '17

30 Jan '17

Hi! Details here https://github.com/seL4/seL4/issues/57 do you guys keep an eye on github activity actually or it’s a bad medium for communcation?

2 1

I2C Driver for BeagleBone (AM335x) for CAmkES
by Richard Habeeb 25 Jan '17

25 Jan '17

Hey all, Has anyone setup I2C on a Beaglebone CAmkES application? Is the code in libplatsupport all that's needed? The i2d_id enum doesn't seem to include all the i2c modules ( https://github.com/seL4/libplatsupport/blob/master/plat_include/am335x/plat…) I didn't see an init function for the i2c_bus for am335x; for example, exynos uses the exynos_i2c_init. Any help is appreciated. Thanks, Richard -- Richard Habeeb Research Assistant, Computer Science, USF PGP: https://goo.gl/VhmGGu https://habeebr.bitbucket.io/

1 0

ARM LPAE?
by Wladislav Wiebe 21 Jan '17

21 Jan '17

Hello, I am trying to integrate TI Keystone 2 platform to seL4. What I have done so far is basically an initial port of the Kernel/libs/elfloader/Platform components and introducing a new keystone defconfig. Relevant config parts about the setup: CONFIG_ARCH_ARM_V7A=y CONFIG_ARCH_ARM=y CONFIG_ARCH_AARCH32=y CONFIG_ARM_CORTEX_A15=y CONFIG_PLAT_KEYSTONE=y At the end I am able to generate an image which looks like: $ arm-cortexa15-linux-gnueabihf-readelf -e images/sel4test-driver-image-arm-keystone ELF Header: Class: ELF32 .. Entry point address: 0xc0008000 .. (I am using the same entry point as Linux use it) So far, it stops booting in the elfloader -- output log: .. [ 29.705] ## Starting application at 0xc0008000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A15 r2p4 paddr=[c0008000..c032841f] -> Stop here <- Seems it stops loading @ elf_getMemoryBounds(). I suppose it is related to fact that the physical start address starts @ 0x840000000 which is beyond 32 Bit - so, LPAE support is required. The physical RAM setup looks like: bank 0: addr: 0x840000000 size: 0x17ec5000 (382 MB) bank 1: addr: 0x880000000 size: 0x80000000 (2048 MB) Do you have an idea if this is supposed to be supported on seL4? What should be the "physBase" and the "kernelBase" for such a setup? How should the "static const p_region_t BOOT_RODATA avail_p_regs" looks like? Thanks in advance! -- WBR, Wladislav WIebe

3 10

Re: [seL4] SDHC drivers (cont.)
by Siwei.Zhuang＠data61.csiro.au 20 Jan '17

20 Jan '17

Hi Oak, I tried your code. It works for me except that it seems that you are using old versions of seL4 kernel and libraries. Attached is the code I'm using, I merely add some initialization code to your code. It should work on the latest version of seL4 kernel and related libraries. If the code doesn't work for you. I would suggest, 1. If you are using u-boot, try its mmc command, see if you can access the card. 2. Have a look at the imx6 reference manual, chapter 67.2 and 67.3, check if the host controller is enabled properly. - Siwei ________________________________ From: Norrathep Rattanavipanon <nrattana(a)uci.edu> Sent: Friday, 20 January 2017 6:12 AM To: Zhuang, Siwei (Data61, Kensington NSW) Subject: Re: [seL4] SDHC drivers (cont.) Hi Siwei, Yes, I believe mmc_card_capacity returns the correct value (4026531840 - my microsd is 4GB). And my code does not do any interrupt handling. In fact, that's all the code in the root userspace process (besides initializing vka, vspace and simple objects) and there is no other process. I also tried using a callback as mmc_block_read's argument, instead of using NULL, but it also does not work. On Wed, Jan 18, 2017 at 8:41 PM, <Siwei.Zhuang(a)data61.csiro.au<mailto:Siwei.Zhuang@data61.csiro.au>> wrote: Hi Oak, Do you get the correct card capacity by calling mmc_card_capacity? If you don't, you'd need to check if the hardware is enabled in your bootloader. Are you doing any interrupt handling? As you don't supply a callback function to mmc_block_read, the read function would block until the hardware responses. In this case, mmc_block_read handles the interrupt itself. It would trigger a dead lock if you also handles the interrupt. - Siwei ________________________________ From: Devel <devel-bounces(a)sel4.systems> on behalf of Norrathep Rattanavipanon <nrattana(a)uci.edu<mailto:nrattana@uci.edu>> Sent: Thursday, 19 January 2017 9:54 AM To: Danis, Adrian (Data61, Kensington NSW) Cc: devel(a)sel4.systems; GTS Subject: Re: [seL4] SDHC drivers (cont.) Hi Adrian, Thank you for the reply. I fix it according to what you suggest but it still does not solve the problem (still hang at the same place. Do you have any other suggestions on what I should fix or how I should look into debugging it? Best, Oak On Tue, Jan 17, 2017 at 8:58 PM, <Adrian.Danis(a)data61.csiro.au<mailto:Adrian.Danis@data61.csiro.au>> wrote: Hi Oak, I don't know much about SD cards or this driver but it seems to me like passing it a physical address of 0 isn't what you want, and whilst I know nothing about the mmc hardware it seems reasonable to me that it might hang trying to DMA to memory that doesn't exist. There is also the additional problem that even if paddr was correct for the first page, there is no guarantee that the 5 pages you have allocated are contiguously physically even though they will be mapped contiguous virtually. My recommendation is to use the page dma allocator in seL4_libs/libsel4utils/include/sel4utils/page_dma.h, this will provide you an easy way to allocate/map pages for the purposes of DMA. So instead of void *vaddr = vspace_new_pages(&vspace, seL4_AllRights, 5, seL4_PageBits); uintptr_t paddr = 0; You would have ps_dma_man_t dma_man; error = sel4utils_new_page_dma_alloc(&vka, &vspace, &dma_man); void *vaddr = ps_dma_alloc(&dma_man, 5 * PAGE_SIZE_4K, PAGE_SIZE_4K, 0, PS_MEM_NORMAL); uintptr_t paddr = ps_dma_pin(&dma_man, vaddr, 5 * PAGE_SIZE_4K); As I said at the start, I don't know if this will actually fix your current problem, but it's still something you will need to fix. Adrian On Wed 18-Jan-2017 6:31 AM, Norrathep Rattanavipanon wrote: My apology that I have to continue the discussion from the old thread: (http://sel4.systems/pipermail/devel/2016-October/001056.html) My goal is to read and write data from/to micro sd in SabreLite platform. I tried both Adrain and Anna's suggestions in that thread and they dont seem to fix the problem. Nothing returns error and I also changed cacheable parameter in sel4utils_new_pages_at_vaddr to 0 (I believe this is what Anna meant instead of setting 3rd argument of vspace_new_pages). The code's still stuck inside mmc_block_read function. I tracked it down and it seems like BRR and BWR interrupt statuses are never set to 1 I add my code below, please let me know if anything is wrong with my code. ps_io_mapper_t io_mapper = {0}; error = sel4platsupport_new_io_mapper(simple, vspace, vka, &io_mapper); assert(error == 0); ps_io_ops_t io_ops = { .io_mapper = io_mapper }; sdio_host_dev_t* dev = (sdio_host_dev_t*) malloc(sizeof(*dev)); assert(dev != NULL); memset(dev, 0, sizeof(*dev)); enum sdio_id id = sdio_default_id(); // return id=3 error = sdio_init(id, &io_ops, dev); assert(error == 0); mmc_card_t* mmc_card = (mmc_card_t*) malloc(sizeof(*mmc_card)); error = mmc_init(dev, &io_ops, mmc_card); assert(error == 0 && mmc_card != NULL); void *vaddr = vspace_new_pages(&vspace, seL4_AllRights, 5, seL4_PageBits); assert(vaddr != NULL); uintptr_t paddr = 0; printf("mmc card capacity %llu bytes\n", mmc_card_capacity(*mmc_card)); long read_len = mmc_block_read(*mmc_card, 0x50000, 1, vaddr, paddr, NULL, NULL); // Stuck here printf("read %lu bytes\n", read_len); Thanks Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine _______________________________________________ Devel mailing list Devel(a)sel4.systems<mailto:Devel@sel4.systems> https://sel4.systems/lists/listinfo/devel -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

1 0

seL4 System Utilization / Benchmark
by Andrew Gacek 20 Jan '17

20 Jan '17

Hi, I'm interested in seeing how much of the CPU is being used by the various threads in my (camkes) application. I'd like a simple "Task Manager" style report of the form: 70% idle 25% can_obj_7_0_control_9_tcb 5% can_obj_7_Int_3_0000_tcb 0% can_obj_7_0_fault_handler_15_0000_tcb etc I've tried poking around libsel4bench, but I don't see any obvious way of benchmarking the whole system. From what I can tell, it's mostly designed to get cycle counts from specific code segments. Is that right? What's the best way to go about benchmarking the whole system? It's only for debugging, so I'm willing to make some quick-and-dirty changes to the kernel just to see the results. Thanks, Andrew

4 11

SDHC drivers (cont.)
by Norrathep Rattanavipanon 19 Jan '17

19 Jan '17

My apology that I have to continue the discussion from the old thread: ( http://sel4.systems/pipermail/devel/2016-October/001056.html) My goal is to read and write data from/to micro sd in SabreLite platform. I tried both Adrain and Anna's suggestions in that thread and they dont seem to fix the problem. Nothing returns error and I also changed cacheable parameter in sel4utils_new_pages_at_vaddr to 0 (I believe this is what Anna meant instead of setting 3rd argument of vspace_new_pages). The code's still stuck inside mmc_block_read function. I tracked it down and it seems like BRR and BWR interrupt statuses are never set to 1 I add my code below, please let me know if anything is wrong with my code. ps_io_mapper_t io_mapper = {0}; error = sel4platsupport_new_io_mapper(simple, vspace, vka, &io_mapper); assert(error == 0); ps_io_ops_t io_ops = { .io_mapper = io_mapper }; sdio_host_dev_t* dev = (sdio_host_dev_t*) malloc(sizeof(*dev)); assert(dev != NULL); memset(dev, 0, sizeof(*dev)); enum sdio_id id = sdio_default_id(); // return id=3 error = sdio_init(id, &io_ops, dev); assert(error == 0); mmc_card_t* mmc_card = (mmc_card_t*) malloc(sizeof(*mmc_card)); error = mmc_init(dev, &io_ops, mmc_card); assert(error == 0 && mmc_card != NULL); void *vaddr = vspace_new_pages(&vspace, seL4_AllRights, 5, seL4_PageBits); assert(vaddr != NULL); uintptr_t paddr = 0; printf("mmc card capacity %llu bytes\n", mmc_card_capacity(*mmc_card)); long read_len = mmc_block_read(*mmc_card, 0x50000, 1, vaddr, paddr, NULL, NULL); // Stuck here printf("read %lu bytes\n", read_len); Thanks Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

3 3

CAmkES Templates
by Chris Guikema 19 Jan '17

19 Jan '17

Hello, I am working on a CAmkES application attempting to build a seL4 Network Stack. I am basing this on the CAmkES-VM and utilizing UDP Protocol with the lwIP library. During my build process, I get quite a few linking errors like this: undefined reference to `pbuf_alloc' This is odd, because in the templates, the proper header files are being linked in. There are also warnings like this: Warning: no template for ethdriver_1.to.source Even though the connection does exist: connection seL4Ethdriver eth_driver(from router.ethdriver, to ethdriver.client); Is there something obvious I am doing wrong? Thanks Chris

2 2

questions about SMMU on TK1 VMM
by PX 18 Jan '17

18 Jan '17

Hi, I have some questions about the SMMU on the new version of TK1 VMM as follows: 1. In the source code, smmu.c, the IO ASID 1 is assigned to hardware engine, AFI, which is supposed to connect with PCIE devices. However, when I add 1 to vm.smmu in vm.camkes, the VM can not access Ethernet and cause a SMMU translation error. But it works if I add 0 to vm.smmu as suggested by Kent. whats the reason to do so? 2. Each IO device is assigned with an IO space mapping. However, there is no IO ASID associated with these mappings. Does that means these mappings are associated with an IO ASID in the order given in vm.smmu? 3. Is it possible for the VMM to change the IO mapping for a specific device? say, invalidate old mapping and load a new mapping? what's the rough idea to do so? thanks Peng

2 1

questions about PCIE SMMU for tk1 vmm
by PX 16 Jan '17

16 Jan '17

Hi, I am confused by the SMMU management for PCIE device in the updated TK1 VMM. The IO ASID for PCIE device is 0. However, the start IO ASID is from 1 as defined in smmu.h. When initialized, the lookup table, smmu_ioasid_to_pd, has no entry for IO asid 0 at all. I don't understand how the page table for PCIE device is generated and used by SMMU? which part source code should I check ? thanks Peng

2 1

Re: [seL4] quesitons about TK1 VMM
by Kent.Mcleod＠data61.csiro.au 14 Jan '17

14 Jan '17

Hi Peng, Adding the ethernet card requires adding the 0 ASID in the vm.camkes file that I mentioned in the previous email. vm.smmu = [0, 10, 24]; This gives permission for PCIE devices to read and write to memory. I confirmed that on the TK1 Jetson the ethernet port works after this change. You may need to run "ifconfig eth0 up" to enable the device once the image boots. Regards, Kent. ? ________________________________ From: PX <seawolf.peng(a)gmail.com> Sent: Friday, January 13, 2017 12:13 PM To: Mcleod, Kent (Data61, Kensington NSW) Subject: Re: quesitons about TK1 VMM Kent, I am using NVIDIA Jetson TK1 board. The reason I want to use insecure config is to enable VM Linux to use Ethernet port. I do not care about the SD card. How can I just add Ethernet card? is there a way for me to avoid adding SD card to The VM linux as you just suggest in your email? Thanks Peng On Thursday,January 12, 2017, <Kent.Mcleod(a)data61.csiro.au<mailto:Kent.Mcleod@data61.csiro.au>> wrote: Hi Peng, Which hardware are you using to run the image? This project has only been tested on the TK1-SOM made by Colorado Engineering. The ethernet port doesn't work as the version of Linux that we use doesn't support it. As for your second question, we configure the IOMMU to only let Linux use the emmc device and USB device on the TK1-SOM. The error is caused because Linux is trying to access a SD card device that it isn't authorized to access. The TK1-SOM doesn't have any SD card hardware so camkes doesn't set up access. If you want to use the Insecure config then you will need to modify apps/vm/vm.camkes and add the right ID to vm.smmu on line 443. To find out which ID to add we take the ID:98 from your Address translation error and look it up in the TK1 technical reference manual. In the memory controller section of the manual there is a "Error Data Capture: Status" section that starts on page 716. Using the table there you can look up ID:98 to see that it belongs to the SWGROUP sdmmc3a. We can now take this and look in seL4 ("kernel/include/plat/tk1/plat/machine/smmu.h?") to find the relevant ASID. From the list of ASIDs we see that SMMU_SDMMC3A_ASID is defined as 23. This is the ID that needs to be added to the vm.smmu array in vm.camkes. Hope this helps, Regards, Kent. ________________________________ From: Devel <devel-bounces(a)sel4.systems> on behalf of PX <seawolf.peng(a)gmail.com> Sent: Friday, January 13, 2017 9:03 AM To: devel(a)sel4.systems Subject: [seL4] quesitons about TK1 VMM Hi, I built a TK1 ARM VMM image from the source code SEL4PROJ/camkes-vm-manifest in GitHub. I have some quesitons about the tk1_vmlinux. Question 1: If I use the original tk1_vm_defconfig, the eth0 does not work in vm. Is the tk1_vm_linux in default not supposed to access Ethernet card? Hpw do I access Ethernet card in this case? Question 2: If I change the VM conifg into insecure, CONFIG_TK1_INSECURE=y, the VM can not get booted, I get "SMMU address translation error". The error message is appended as follows: " [ 10.503932] mmc1: Invalid maximum block size, assuming 512 bytes [ 10.566465] mmc1: SDHCI controller on 700b0400.sdhci [700b0400.sdhci] using ADMA 64-bit SMMU Address translation error: ID: 98 address: 0xae609000 type: 6 direction: 0x0 IOPT permission: read 0x0 write 0x0 nonsecure 0x0 [ 10.617123] mmc1: ADMA error" Is this error caused by bugs in source code or my wrong config? if the later case, what's the correct config? thanks Peng

2 1

quesitons about TK1 VMM
by PX 13 Jan '17

13 Jan '17

Hi, I built a TK1 ARM VMM image from the source code SEL4PROJ/camkes-vm-manifest in GitHub. I have some quesitons about the tk1_vmlinux. Question 1: If I use the original tk1_vm_defconfig, the eth0 does not work in vm. Is the tk1_vm_linux in default not supposed to access Ethernet card? Hpw do I access Ethernet card in this case? Question 2: If I change the VM conifg into insecure, CONFIG_TK1_INSECURE=y, the VM can not get booted, I get "SMMU address translation error". The error message is appended as follows: " [ 10.503932] mmc1: Invalid maximum block size, assuming 512 bytes [ 10.566465] mmc1: SDHCI controller on 700b0400.sdhci [700b0400.sdhci] using ADMA 64-bit SMMU Address translation error: ID: 98 address: 0xae609000 type: 6 direction: 0x0 IOPT permission: read 0x0 write 0x0 nonsecure 0x0 [ 10.617123] mmc1: ADMA error" Is this error caused by bugs in source code or my wrong config? if the later case, what's the correct config? thanks Peng

1 0

question about SEL4PROJ /camkes-arm-vm-manifest
by PX 13 Jan '17

13 Jan '17

Hi, all I try to build a TK1 ARM VMM image from the source code SEL4PROJ/camkes-vm-manifest in GitHub. However, I can not compile it. I get errors when the compiler tries to build "camkes-accelerator" . I don't put any new code yet. I just: 1) repo init the url ; 2) repo sync; 3) make tk1_vm_defconfig; and 4) make. Did I do something wrong here? thanks Peng

2 5

Overly eager xsave size rejection
by Corey Richardson 12 Jan '17

12 Jan '17

in src/arch/x86/machine/fpu.c:140 on 4.0.0, there is > if (x86_cpuid_ebx(0x0d, 0x0) != CONFIG_XSAVE_SIZE) { > printf("XSAVE buffer set set to %d, but should be %d\n", CONFIG_XSAVE_SIZE, x86_cpuid_ebx(0x0d, 0x0)); > return false; > } I want to force a large(r than 576) xsave region so that TCBBits is always 11, to help my userspace be vaguely more kernel-config-independent. I don't think it's a problem if the xsave buffer in the TCB is larger than the hardware will actually use? I also think this is buggy. Shouldn't it be querying ecx, since things like AVX aren't enabled in the kernel? To be clear, this is my suggested change: > if (x86_cpuid_ecx(0x0d, 0x0) > CONFIG_XSAVE_SIZE) { > printf("XSAVE buffer set set to %d, but should be at least %d\n", CONFIG_XSAVE_SIZE, x86_cpuid_ecx(0x0d, 0x0)); > return false; > } -- cmr http://octayn.net/ +16038524272

2 5

question about SEL4PROJ /camkes-arm-vm-manifest
by PX 12 Jan '17

12 Jan '17

Hi, all I posted this question yesterday, and get no answer. Let me to be more specific this time. I try to build a TK1 ARM VMM image from the source code SEL4PROJ/camkes-vm-manifest in GitHub. However, I can not compile it. I get errors when the compiler tries to parse capDL. The errors are appended as follows: " make: Entering directory '/home/dev/Documents/new_vmm/projects/capd /capDL-tool' stack setup make: stack: Command not found Makefile:37: recipe for target 'sandbox' failed make: *** [sandbox] Error 127 make: Leaving directory '/home/dev/Documents/new_vmm/projects/capdl/capDL-tool' Makefile:51: recipe for target '/home/dev/Documents/new_vmm/stage/arm/tk1/parse-capDL/parse-capDL' failed " I checked that there is a file called stack.ymal in the directory: ~/capdl/capDL-tool. My system is also installed latest ghc and ghc-prof. Anybody can help me on this problem? Thanks Peng

3 3

Using the seL4 Benchmark Tool
by Chris Guikema 12 Jan '17

12 Jan '17

Hello, I am currently attempting to use the seL4 Benchmark tool. After going through the menuconfig (kernel -> build options -> Enable Benchmarks -> Track threads and kernel utilization time), I attempt to rebuild, and get a host of errors: In file included from /home/chrisguikema/gdbtest/kernel/include/compound_types.h:16:0, from /home/chrisguikema/gdbtest/kernel/include/types.h:15, from /home/chrisguikema/gdbtest/kernel/src/api/faults.c:14: /home/chrisguikema/gdbtest/kernel/include/object/structures.h:249:5: error: unknown type name 'benchmark_util_t' benchmark_util_t benchmark; And a lot more, but all along the "not a structure or union" line, which makes me think that either the header file isn't being linked properly, or the #ifdefs aren't working for everything. Did I do something improperly in my setup? Thanks, Chris Guikema

2 1

Workshop debrief?
by Jeff Waugh 10 Jan '17

10 Jan '17

Hey there, I might be hoping a little too much for video, but will there be slides and notes from the Workshop? (Particularly interested in the gaps discussion.) Would be handy content on the wiki. :-) Thanks, Jeff

3 4

config-independent object type numbers
by Corey Richardson 10 Jan '17

10 Jan '17

Right now, object type numbers vary based on the kernel config (eg, CONFIG_VTX) etc. This is a huge source of pain for the Rust userspace libraries which don't integrate with seL4's build system. Is it possible for those enums to explicitly label every potential object type for a given architecture with a fixed number? -- cmr http://octayn.net/ +16038524272

2 2

seL4 as Xen guest / AWS
by Tony Arcieri 10 Jan '17

10 Jan '17

Has anyone managed to run seL4 as a Xen HVM guest? I was more specifically curious about running seL4 on an EC2 instance. I was curious about the possibility of using seL4 as the host OS for a "unikernel"-like deployment of a Rust application split into a small set of services living in different capability spaces (e.g. network, key storage / crypto) -- Tony Arcieri

3 3

sel4test 4.0.x.xml broken?
by Corey Richardson 09 Jan '17

09 Jan '17

It seems that the line <project name="seL4.git" path="kernel" revision="4.0.x-compatible"/> should be <project name="seL4.git" path="kernel" revision="4.0.0"/> Either that, or a tag is missing from the kernel repo. -- cmr http://octayn.net/ +16038524272

2 1

questions about the vgic maintenance for sel4 TK1 ARM VMM
by PX 09 Jan '17

09 Jan '17

Hi, all I have questions about the vgic maintenance for sel4 tk1 ARM VMM. When the VM acknowledges an IRQ, an exception is raised and is delivered to the VMM. Could someone explain how seL4 intercepts the VM ack? How is this exception is raised ? I am confused because the VM is supposed to totally control the MMIO of the device and can write any thing to the device. How can seL4 be triggered in this case? Which part of source code allows seL4 to intercept the VM ack? Thanks Peng

2 1

Interest in 32-bit x86 Rust userspace?
by Corey Richardson 07 Jan '17

07 Jan '17

Is anyone interested at all in the 32-bit x86 Rust userspace libraries? I'm considering dropping support for them, as I don't personally plan to have any support for them in Robigalia, instead focusing on x86_64. Note that this wouldn't impact any Rust CAmkES components using the support in the sel4 buildsystem, just the sel4-sys, rust-sel4, etc crates. -- cmr http://octayn.net/ +16038524272

1 0

DMA driver in VM
by PX 07 Jan '17

07 Jan '17

Hi, I have a generic question about DMA driver in the VM on sel4. How does the device driver in the vm put physical address in the DMA controller given that there is no emulation in sel4? I worked on TK1 sel4 hypervisor extention version, but cannot find any address translation from vmm. Thanks Peng

1 0

pic/no-pic and some other questions
by Vasily A. Sartakov 06 Jan '17

06 Jan '17

Greetings. I have merged MIPS port with 4.0.0 release. Now I would like to clean up my code and need to remove many small issues that I did not fix during the porting before making the code public. In fact, most of the current problems are related to toolchains: 1. The first problem is a position independent code. Could you please describe me seL4' vision about it? muclibs is building with -fPIC, but everything else doesn't, right? I have a very tricky set of GCC’ flags, related to MIPS’ GOT, small data, abicalls, pic/non-pic, etc, and many of them are not working together. 2. MIPS assembler has several features, one of them is that the -O0 code requires having an addition space above the top of the stack for 4 registers: > 43b610: 27bdffe8 addiu sp,sp,-24 <— start of the function > 43b614: afbf0014 sw ra,20(sp) > 43b618: afbe0010 sw s8,16(sp) > 43b61c: afb0000c sw s0,12(sp) > 43b620: 03a0f021 move s8,sp <— frame stack > 43b624: afc40018 sw a0,24(s8) <— save 1st arg for a subroutine call > 43b628: afc5001c sw a1,28(s8) <— save 2nd arg for the subroutine > 43b62c: afc60020 sw a2,32(s8) <— save 3rd arg for the subroutine So, each time when I am allocating new stack I should return not top of the stack, but top_of_the_stack - 4*sizeof(seL4_Word). As result, sel4utils_configure_thread_config becomes platform specific. Could you please consider a possibility to put it into the «arch» as sel4utils_arch_init_context, or add something like «sel4utils_arch_configure». Also, it is important: this is an issue only for -O0 code, as far I see, -O2 uses different methods for arguments passing. I am trying to build toolchains which do not use frame pointer this style for -O0 code, but I am not sure about the result. 3. I really like how you redesigned declaration syscalls. Now I have a freedom to modify syscalls and do not care about the mainline declarations because now there are syscall wrappers. However, my toolchain generates very poor code for CONFIG_LIB_SEL4_PUBLIC_SYMBOLS and «DEFAULT» — I have proper working code only for CONFIG_LIB_SEL4_INLINE_INVOCATIONS. What is the conceptual difference of these declaration attributes, what they affect? 4. Could you please tell me what was the C equivalent of this asm code: .global __syscall .type __syscall,%function __syscall: sub sp, sp, #4 push {r5,r6} adr r5, 1f ldr r6, 1f ldr r5, [r5,r6] str r5, [sp, #8] pop {r5, r6} pop {pc} .hidden __sysinfo 1: .word __sysinfo-1b something similar to __syscall6 from libmuslc/arch/<arch>_sel4/syscall_arch.h, right? Thank you. P/s Happy new year/merry xmass/happy holidays! -- Vasily A. Sartakov sartakov(a)ksyslabs.org

2 2

xsave region size for haswell/broadwell?
by Corey Richardson 06 Jan '17

06 Jan '17

Does anyone have a "maximal" xsave region size big enough for all the xsave-supporting features seL4 enables on Broadwell or Haswell? I don't have access to a machine with these features, so I can't run a program to get them with cpuid. -- cmr http://octayn.net/ +16038524272

2 1

questions about the address translation for a DMA driver in the ARM VM
by PX 05 Jan '17

05 Jan '17

Hi, all Happy new year! I have some urgent questions about address translation for a DMA driver in the ARM seL4-based VM. Your quick response is highly appreciated! 1. In the ARM sel4-based VM, the MMIO of a device is directly exposed to the device driver in the VM. When the DMA device driver allocates a DMA buffer to a device controller, the device driver can directly tell the real controller the IPA of the buffer starting address, instead of the real physical address. In other words, the device controller can only get the IPA of the buffer starting address. How can this device controller perform DMA without knowing the real PA of the buffer? Does seL4 perform some emulation here? How? 2. A closely related question to 1: when we develop a DMA driver in the VMM space, we put the real physical address of the device descriptor and real physical address of the DMA buffer in the controller registers through its MMIO. We found that the controller cannot find the correct place for the descriptor and the buffer. Do the seL4 hypervisor perform the address translation? If so, which source code does that? Thanks Peng

2 3

Build Error
by Daniel Romero 05 Jan '17

05 Jan '17

Hi, I am currently on a BeagleBone running Ubuntu 14.04 using gcc-arm-none-eabi. However I am getting the following error running 'make' after 'make menuconfig'. I am wondering if someone can guide me in the right direction [libs/libsel4] building... [GEN] include/sel4/types_gen.h Traceback (most recent call last): File "/home/ubuntu/seL4test/libs/libsel4/tools/bitfield_gen.py", line 26, in <module> from six.moves import range ImportError: No module named six.moves make[1]: *** [include/sel4/types_gen.h] Error 1 make: *** [libsel4] Error 2 Thank you, Hector Daniel Romero hdromero93(a)gmail.com

2 1

seL4test on Odroid-XU4
by Yevgeny Lavrov 05 Jan '17

05 Jan '17

Hello I ran into the following issue while running seL4test suite on Odroid-XU4: Exynos5422 # fatload mmc 0 0x48000000 sel4test-driver-image-arm-exynos5 there are pending interrupts 0x00000001 reading sel4test-driver-image-arm-exynos5 3149364 bytes read Exynos5422 # bootelf 0x48000000 ## Starting application at 0x41000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A7 r0p3 Switching CPU... ELF-loader started on CPU: ARM Ltd. Cortex-A15 r2p3 paddr=[41000000..4130441f] ELF-loading image 'kernel' paddr=[60000000..60037fff] vaddr=[e0000000..e0037fff] virt_entry=e0000000 ELF-loading image 'sel4test-driver' paddr=[60038000..60411fff] vaddr=[10000..3e9fff] virt_entry=1e74c Enabling MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Kernel init: Too many untyped regions for boot info Kernel init: Too many untyped regions for boot info Kernel init: Too many untyped regions for boot info .... 1 untypeds of size 10 1 untypeds of size 11 126 untypeds of size 12 2 untypeds of size 13 3 untypeds of size 14 3 untypeds of size 15 5 untypeds of size 16 3 untypeds of size 17 3 untypeds of size 18 3 untypeds of size 19 3 untypeds of size 20 2 untypeds of size 21 2 untypeds of size 22 1 untypeds of size 23 2 untypeds of size 24 2 untypeds of size 25 2 untypeds of size 26 2 untypeds of size 27 1 untypeds of size 29 Switching to a safer, bigger stack... seL4 Test ========= _allocman_utspace_alloc@allocman.c:301 Regular utspace alloc failed and not watermark for size 31 type 0 vka_alloc_object_at@object.h:57 Failed to allocate object of size 2147483648, error 1 _allocman_utspace_alloc@allocman.c:301 Regular utspace alloc failed and not watermark for size 30 type 0 vka_alloc_object_at@object.h:57 Failed to allocate object of size 1073741824, error 1 _allocman_utspace_alloc@allocman.c:301 Regular utspace alloc failed and not watermark for size 29 type 0 vka_alloc_object_at@object.h:57 Failed to allocate object of size 536870912, error 1 ..... _utspace_split_alloc@split.c:247 Failed to find any untyped capable of creating an object at address 0x12dd0000 vka_alloc_object_at@object.h:64 Failed to allocate object of size 4096 at paddr 0x12dd0000, error 1 init_timer_caps@main.c:348 [Cond failed: error] Failed to get untyped at paddr 0x12dd0000 for timer Ignoring call to sys_rt_sigprocmask Ignoring call to sys_gettid sys_tkill assuming self kill HYP mode is enabled, and seL4test suite is compiled in Debug Mode. Prior to running seL4test, I ran code from seL4 tutorials and those ran w/o any problems. Any suggestions on what I might have done wrong? Thanks

3 4

Exposing TSD on x86
by Corey Richardson 03 Jan '17

03 Jan '17

How do people feel about exposing the TSD (time-stamp disable) bit as a piece of state on the TCB? Ideally it'd be lazily switched. I vaguely want this in Robigalia for disabling access to real time in non-sufficiently-privileged processes. Best, -- cmr http://octayn.net/ +16038524272

2 2

Re: [seL4] Workshop debrief?
by Corey Richardson 20 Dec '16

20 Dec '16

I really ought to stop using my phone for email. Sent back to list. On Mon, Dec 19, 2016, at 05:25, Jeff Waugh wrote: > On Mon, Dec 19, 2016 at 8:19 PM, Corey Richardson > <corey(a)octayn.net> wrote: > > > I'm writing up my notes and will be publishing them on the > > Robigalia blog. > > Will send a link here when it's up. Ihor said he'd be collecting > > slides, > > not sure what the availability of those will be. > > > > Cool -- maybe let the list know too? -- cmr http://octayn.net/

1 0

RELEASE: Announcing CAmkES 2.3.0
by Stephen.Sherratt＠data61.csiro.au 15 Dec '16

15 Dec '16

Announcing the release of CAmkES 2.3.0 Changes in this release: * support for seL4 4.0.0 * new dependency: Haskell Stack (http://haskellstack.org) + Haskell Stack is a haskell version and package manager. It takes care of installing an appropriate version of ghc and cabal for building the capDL translator - part of CAmkES' build system. Check out an example CAmkES system with: repo init -u https://github.com/seL4/camkes-manifest.git -m default-2.3.x.xml repo sync For more information about CAmkES, see: https://wiki.sel4.systems/CAmkES Cheers, Stephen

1 0

ARM bootloaders that matter
by Jeff Waugh 14 Dec '16

14 Dec '16

Hi all, Out of interest, are there any ARM targets the seL4 development team / community care about that do not boot via u-boot or UEFI (whatever the implementation, be it u-boot, vendor-supplied, etc)? Thanks, Jeff

4 5

RELEASE: Announcing seL4 4.0.0
by Parthasarathi.Susarlaajay＠data61.csiro.au 13 Dec '16

13 Dec '16

We are pleased to announce the release of 4.0.0 of seL4. Listed below are a few of the key changes in this release: * Reorder bootinfo structure. * Add missing seL4_AllRights macro in libsel4. * Disallow kernel from using a device frame as an IPC buffer. * Syscall docs in manual now generated by doxygen. * Changes to make verification easier. * Various documentation fixes. * Benchmarks refactoring. * Coding style fixes. * Support for TLB and Cache management. * Preemptible backwards memzero for Retype. * Support for TCB operations in X86 multicore. * Support for raspberry-pi 3. ARM specific changes: * ARM Hyp refactoring. * Update VCPU fault definitions. * Add userspace invocations for hardware debugging. * Enable PMU export for V8. * Support ARM MPCore registers * Fix config dependency for 'IPC Buffer location'. * Use new cap rights structures in iospace. * Move initial setting of TPIDRURW register. * Add seL4_BenchmarkFlushCaches() for arm and ia32. * Support for prefetcher on Cortex-A9. * Fix fastpath_restore on ARM Hyp and implement slowpath and restore in C. * am335x: Prevent out of bounds array access. * TK1 + Remove temporary SMMU memory mapping support. + Correct SMMU PD and PT indexing. + Split the mux controller from the misc region. * OMAP: + Fix issues with OMAP IRQ Code. X86 specific changes: * Add userspace invocations for hardware debugging. * Avoid writing the fs/gs base unless necessary. * Explicitly declare adress of .phys.bss. * Add BSS regions for BOOT and PHYS code. * Write FS and GS base when restoring user context. * Initialize store area when using XSAVE variant instructions. * Efficiently pack objects for fastpath. * Increase IPI words to 3. * Support for x2APIC. * Support larger XSAVE region sizes. * Change ia32 to use fs register for IPC buffer. * Update the bootinfo for number of cores. * Initial support for SMP vt-x. * Split CPU ID management into mode and general. * Fix cpuid family/model composition. * Add X86_64 support. Please note that this release is not source compatible with earlier releases of seL4, please read https://research.csiro.au/tsblog/introduc ing-device-untyped-memory-sel4/ for more information regarding the changes. The release tarballs can be directly downloaded from: https://github.com/seL4/seL4/archive/4.0.0.tar.gz [259d9eadaddef579c2b98b91cf40d13a 4.0.0.tar.gz] The manual for this release can be downloaded here: http://sel4.systems/Info/Docs/seL4-manual-4.0.0.pdf Contributors: * Adrian Danis * Alexander Boettcher * Amirreza Zarrabi * Anna Lyons * Christian Helmuth * Corey Richardson * Donny Yang * Hesham Almatary * Jeff Waugh * Joel Beeren * Kent McLeod * Kofi Doku Atuah * Matthew Brecknell * Matthew Fernandez * Matt Rice * Rafal Kolanski * Stephen Sherratt * Thomas Sewell * Xin,Gao Please let us know of any issues that you run into by creating an issue in the issue tracker: https://github.com/seL4/seL4/issues -- Partha Susarla Kernel engineer DATA61 | CSIRO E parthasarathi.susarla(a)data61.csiro.au www.data61.csiro.au CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61

1 0

seL4 on Zinq7000 on QEMU
by Andrew Gacek 09 Dec '16

09 Dec '16

I'm trying to build and emulate a version of seL4 for the zinq7000 platform, but it crashes immediately. I've started by taking the camkes tutorial and building it for zinq7000: repo init -u https://github.com/seL4/camkes-manifest.git repo sync make arm_simple_defconfig make menuconfig # change seL4 platform to zinq7000 make When I try to emulate it, it crashes right away: qemu-system-arm -M xilinx-zynq-a9 -nographic -kernel images/capdl-loader-experimental-image-arm-zynq7000 qemu: fatal: Trying to execute code outside RAM or ROM at 0x10000000 R00=00000000 R01=00000000 R02=00000000 R03=00000000 R04=00000000 R05=00000000 R06=00000000 R07=00000000 R08=00000000 R09=00000000 R10=00000000 R11=00000000 R12=00000000 R13=00000000 R14=00000000 R15=10000000 PSR=400001d3 -Z-- A svc32 s00=00000000 s01=00000000 d00=0000000000000000 s02=00000000 s03=00000000 d01=0000000000000000 s04=00000000 s05=00000000 d02=0000000000000000 s06=00000000 s07=00000000 d03=0000000000000000 s08=00000000 s09=00000000 d04=0000000000000000 s10=00000000 s11=00000000 d05=0000000000000000 s12=00000000 s13=00000000 d06=0000000000000000 s14=00000000 s15=00000000 d07=0000000000000000 s16=00000000 s17=00000000 d08=0000000000000000 s18=00000000 s19=00000000 d09=0000000000000000 s20=00000000 s21=00000000 d10=0000000000000000 s22=00000000 s23=00000000 d11=0000000000000000 s24=00000000 s25=00000000 d12=0000000000000000 s26=00000000 s27=00000000 d13=0000000000000000 s28=00000000 s29=00000000 d14=0000000000000000 s30=00000000 s31=00000000 d15=0000000000000000 s32=00000000 s33=00000000 d16=0000000000000000 s34=00000000 s35=00000000 d17=0000000000000000 s36=00000000 s37=00000000 d18=0000000000000000 s38=00000000 s39=00000000 d19=0000000000000000 s40=00000000 s41=00000000 d20=0000000000000000 s42=00000000 s43=00000000 d21=0000000000000000 s44=00000000 s45=00000000 d22=0000000000000000 s46=00000000 s47=00000000 d23=0000000000000000 s48=00000000 s49=00000000 d24=0000000000000000 s50=00000000 s51=00000000 d25=0000000000000000 s52=00000000 s53=00000000 d26=0000000000000000 s54=00000000 s55=00000000 d27=0000000000000000 s56=00000000 s57=00000000 d28=0000000000000000 s58=00000000 s59=00000000 d29=0000000000000000 s60=00000000 s61=00000000 d30=0000000000000000 s62=00000000 s63=00000000 d31=0000000000000000 FPSCR: 00000000 Aborted Is there something I'm doing wrong? Thanks, Andrew

2 9

Virtio on camkes-vm
by Robert VanVossen 08 Dec '16

08 Dec '16

Hello, We are looking to add another virtio device to camkes-vm for guests to use. I have been looking through the code at how virtio_net works and I have a pretty decent understanding of how it is configured and used. I have a few design/philosophical questions though. 1. Was any of this (libethdriver, libpci, Ethdriver component, virtio_net.c, virtio_emul.c) ported from somewhere else, or was it all written from scratch? 2. Why is components/Init/src/virtio_net.c used in conjunction with vm0_config.init_cons instead of just using the VMNet templates? 3. Looks like pci handling was decoupled from drivers like libethdriver and it is left up to the VM Init component to configure PCI. What is the reason for that? 4. Virtio_emul.c appears to be the layer that actually provides the virtio interface to the VM. Would it make more sense to make this more generic to cover more devices, or should new emulation files be created for each device? Thanks, Robbie VanVossen

2 1

Huge kernel images no more
by Jeff Waugh 06 Dec '16

06 Dec '16

Hurrah, I was curious about the huge kernel images, and had it on my list to poke at. Adrian's changes merged last night sorted it: x86: Explicitly declare adress of .phys.bss x86: Add BSS regions for BOOT and PHYS code Simulation debug x86_64 image is down from 7.1M to 1.1M. That's more like it! Nice! :-) Thanks, Jeff

2 1

Bitcoin on seL4?
by Carl Dong 02 Dec '16

02 Dec '16

Hi all, I recently acquired a BD-SL-I.MX6 and will be tinkering with it to install seL4. A major use case for me is if I could run [bitcoind](https://en.bitcoin.it/wiki/Bitcoind) or at least [vanitygen](https://en.bitcoin.it/wiki/Vanitygen) on seL4. I'm very new to the system, but is there a relatively easy way of cross-compiling said software for seL4? Would love to spend some time learning. Cheers, Carl Dong accounts(a)carldong.me

4 3

seL4 Memory Management
by Mark Reus 01 Dec '16

01 Dec '16

Hi I have been going through some of the research papers about seL4. I wanted to understand the security features in the memory management. I am a little confused, hope someone can I help me. Quote from the paper "Finally, the kernel ensures that each physical frame mapped by the MMU at a useraccessible address is of the Frame object type. These Frame objects contain no kernel data and since they cannot overlap with other typed objects, direct user access to kernel data is not possible" I understand that seL4 promotes isolation between processes and no allocation is done by the kernel itself rather it is done by user level manager. Since we use untyped memory and we retype them, there is no overlap of objects. The user level resource managers can access both the kernel memory and other memory as well because they have capabilities to both. What exactly in the above quote causes the isolation of user level memory with kernel memory. I am of the notion that the kernel allocated objects are still accessible and can be modified to point to some other memory? Am I misunderstanding something? Regards Mark

4 4

Good C, bad C, verifiable C
by Jeff Waugh 30 Nov '16

30 Nov '16

Howdy, Is there a guide to the dos and don'ts of C according to the seL4 verification process? I kinda remember reading a quick summary somewhere, but can't find it on the wiki. Maybe I read it in one of the papers? I certainly remember reading the moral equivalent of "lol no strings". ;-) Thanks, Jeff

2 1

contiguous physical memory allocation for seL4
by PX 30 Nov '16

30 Nov '16

Hi, all I want to allocate a contiguous physical memory block (larger than a physical page) and map it to contiguous virtual addresses in the vspace, what's the best way to do it? Are there existing libraries allowing me to do that? thanks Peng

3 2

First International seL4 Workshop
by Gernot.Heiser＠data61.csiro.au 29 Nov '16

29 Nov '16

Hey seL4 community! We’d like to invite you to participate in the inaugural seL4 Workshop. Given the growth in the community we are starting an annual seL4 workshop where we can come together to share and learn what is being done with seL4. Unlike the previous developers days, the focus is much more on what is happening with seL4 and what interesting things are being done using seL4 rather than a learning or tutorial event. We’d like participants to join and: - present what they are doing with seL4 - demonstrate seL4-based projects - give tutorials on aspects of seL4 or tools, libraries, environments for working with seL4 - show results or progress of verification work involving seL4 - discuss interesting challenges (and possible solutions) they’ve encountered when using seL4 - discuss visions for the future of seL4 and high-assurance systems This workshop will take place on Thursday December 15, 2016 (and may be extended to December 16th if there is enough demand) in Malibu, CA, USA. Note that you are welcome to attend even if you do not present anything. Please register participation at: https://sel4.systems/Community/Devdays/ Participation is free, and we may be able to provide students with financial assistance for travel. This workshop is sponsored by the Center for Secure and Resilient Systems at HRL Laboratories, LLC, and by Data61. Gernot for the Data61 Trustworthy Systems Team

2 1

Re: [seL4] Timer for Performance Measurement
by Kofidoku.Atuah＠data61.csiro.au 29 Nov '16

29 Nov '16

?Hey Andrew, Sorry I took so long to get back to you: we have a benchmarking suite, seL4Bench (https://github.com/seL4/sel4bench/blob/master/apps/ipc/src/main.c) which should have userspace timers and precise timestamps available for most platforms. As I understand, you will just have to write a new microbenchmark of your own, and import your library, and then insert calls to the relevant timestamp counter functions (https://wiki.sel4.systems/Benchmarking%20guide)? Kofi Doku Atuah Kernel engineer DATA61 | CSIRO E kofidoku.atuah(a)data61.csiro.au www.data61.csiro.au CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61 ________________________________ From: Devel <devel-bounces(a)sel4.systems> on behalf of Andrew Mine <secondmine(a)gmail.com> Sent: 04 November 2016 16:30 To: devel(a)sel4.systems Subject: [seL4] Timer for Performance Measurement Hi Is there any inbuilt library to get the time like get_time in seL4? I want to measure IPC performance and overheads for my tasks. Regards Andrew

1 0

Re: [seL4] how to get timing information on seL4 user space
by Kofidoku.Atuah＠data61.csiro.au 29 Nov '16

29 Nov '16

??Hi Peng, Well, an atomic counter would suffice, and if you need to secure the counter, you could wrap it around with a server. You either need a hardware upcounter, or else a periodic event-timer that you can use to emulate a hardware upcounter; from there, you just use your upcounter for your jiffies. Libplatsupport has userspace timer drivers for most platforms we support: https://github.com/seL4/util_libs/tree/master/libplatsupport? Kofi Doku Atuah Kernel engineer DATA61 | CSIRO E kofidoku.atuah(a)data61.csiro.au www.data61.csiro.au CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61 ________________________________ From: Devel <devel-bounces(a)sel4.systems> on behalf of PX <seawolf.peng(a)gmail.com> Sent: 29 November 2016 08:27 To: devel(a)sel4.systems Subject: [seL4] how to get timing information on seL4 user space Hi, all I want to get number of ticks, similar to jiffies in Linux, in the ARM seL4 user space. How can I do it? Are there existing libraries I can use? If not, what's the best way to implement it? thanks Peng

1 0

how to get timing information on seL4 user space
by PX 29 Nov '16

29 Nov '16

Hi, all I want to get number of ticks, similar to jiffies in Linux, in the ARM seL4 user space. How can I do it? Are there existing libraries I can use? If not, what's the best way to implement it? thanks Peng

1 0

IPC measurements
by Neelesh Vemula 28 Nov '16

28 Nov '16

Hi I have been measuring the performance of my application and doing some comparisons with other kernels. I had a couple of queries. I am running seL4 on zynq device. I am using the given timer driver in libplatsupport to measure the clock cycles. Queries: 1) I have found the sample benchmark numbers for seL4 IPC from http://l4hq.org/docs/performance.php. Since I am running on Armv7 Cortex A9 , the time for one half way trip is 316 ns. Is this measured from system call to system call or from process to process? 2) I am trying to compare the performance on FreeRTOS and Linux, is there any such comparison on where seL4 stands? 3) Does the IPC time vary with the different api of ReplyRecv, Reply, seL4_NBRecv? I have this question because I am seeing that Reply is taking about twice the amount of clock cycles compared to Recv. In terms of my application, I am majorly looking at measuring one whole cycle which includes: 1) 1st Process sends message to 2nd Process 2) 2nd Process Reads from AXI device space 3) 2nd Process replies with Reply and waits for another command from 1st process 4) 1st process sends another message to 2nd Process 5) 2nd Process writes to the hardware 6) Time from step 1 to step 5 is measured. Results for this on seL4 : 3180 clock cycles FreeRTOS: 2414 clock cycles I am sure there is possibility of unnecessary overheads involved in my measurement, but I expected seL4 to be faster. Can someone help me in this regard. Regards Neelesh Vemula

2 1

Reading executable of the first process in kernel
by Norrathep Rattanavipanon 22 Nov '16

22 Nov '16

Hi, I want to modify the sel4 kernel to compute a checksum over the executable of the first process before executing it. The goal is to ensure that we execute the correct first process. What I'm doing right now is modify try_init_kernel() in kernel/src/archarm/kernel/boot.c by adding the following lines: for(i=ui_p_reg_start, i<ui_p_reg_end; i++) { checksum += *((char*) (i)); } My questions are the following: (1) Is this a right place to perform the checksum (inside try_init_kernel())? I assume in this function, seL4 kernel already takes over and thus this should do the job. (2) Based on my understanding, what I did was computing the checksum over the entire image (which may includes executable of other processes as well). Is there a way to just read the executable of the first process and ignore the rest in seL4 kernel? (3) I'm also curious: where/when does the seL4 kernel start the root process? I see the end of the same file (boot.c) that it just calls try_init_kernel() but does not load the root process. Best, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 1

Memory Management
by Mark Reus 22 Nov '16

22 Nov '16

Hi I have a general case about memory allocation in particular with that of the Vspace. I have been reading some documents and trying to compare how it is in Linux Kernel. Any program Virtual memory in a Linux kernel is as shown in picture below where all processes have 1GB of virtual memory which is mapped to kernel space for faster context switches and system calls. _____________________ | Kernel Space (1GB) | |_____________________| | | | User Mode Space | | (3 GB) | | | |_____________________| I have come across this this link http://os.inf.tu-dresden.de/pipermail/l4-hackers/2014/006262.html detailing a little about the sel4 memory management. But I haven't been able to completely comprehend it . I wanted to know if the seL4 kernel also has a similar mapping of kernel space. Regards Mark

2 1

Syscall errors with musl
by Rinat Dobrokhotov 21 Nov '16

21 Nov '16

Hi all, I have written simple programme which gets system time. I get syscall errors when programm is calling gettimeofday function: *main.c:* #include <time.h> #include <sys/time.h> #include <stdlib.h> #include <stdio.h> int main(int argc, char *argv[]) { int iterations = 1000000; struct timeval start, end; gettimeofday(&start, NULL); for (int i = 0; i < iterations; i++) { } gettimeofday(&end, NULL); printf("%ld\n", ((end.tv_sec * 1000000 + end.tv_usec) - (start.tv_sec * 1000000 + start.tv_usec))); return 0; *Errors:* libsel4muslcsys: Error attempting syscall 263 libsel4muslcsys: Error attempting syscall 78 Could you tell me where I mistook? -- Best regards, Rinat Dobrokhotov

2 1

seL4RPC vs seL4RPCCall?
by Andrew Gacek 18 Nov '16

18 Nov '16

What's the difference between seL4RPC and seL4RPCCall in CAmkES? Is there documentation on the various connectors somewhere? Thanks, Andrew

2 1

Send input to seL4 in QEMU
by Andrew Gacek 18 Nov '16

18 Nov '16

Hi, We are developing an seL4 application that will process UDP packets coming in over a network connection. Eventually, we'll be running this on real hardware with real drivers, but for now we are using QEMU. We have a python script that can generate packet payloads. Is there a way to send this information into QEMU so that we can develop our seL4 application without having the drivers and hardware in place? If it matters, we are using CAmkES as well. Thanks, Andrew

2 3