- Devel - lists.sel4.systems

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 02 Nov '17

02 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 31 Oct '17

31 Oct '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