Devel October 2017

devel@sel4.systems

21 participants
23 discussions

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

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel October 2017