- Devel - lists.sel4.systems

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

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 24 Oct '17

24 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 20 Oct '17

20 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