Re: [seL4] port SeL4 to renesas rcar-H3 development board

Hi Diego, core_entry_head and init_cpus are for bringing up secondary cores. If you want to utilise more than one core, you need to implement the functions. I am not sure about your board, but PSCI (power state coordination interface) is usually used to bring up secondary cores. Please have a

Re: [seL4] Is the ASID used in seL4 by default?

Hi Dong, Per my understanding, "isb" and "dsb" do not flush TLB. "isb" has t??he effect of flushling pipeline. Roughly, "dsb" ensures that memory accesses and some TLB/cache maintenance instructions are completed before executing the instructions after "dsb". These opeartions may depend on

Re: [seL4] seL4 on Heterogeneous Processing Architectures (Zynq UltraScale+ MPSoCs)

?Hi Robbie, Sorry for the late response. b) I require the use of the Cortex R5 cores in DCLS mode for trusted code with high fault tolerance requirements. --- The Cortex R5 processors lack of MMUs, so seL4 does not support R processors. c) I require the use of the Cortex A53 cores for

Re: [seL4] Alignment fault without U-Boot Cache Enabled

Hi Nicholas, Recently, the commit addressing unaligned accesses for ELF64 files was added the elfloader. When MMU is disabled, reading or writing 64-bit data from/to 4-byte aligned addresses triggers a fault. I am not sure if you were using the updated elfloader. Hopefully, a git pull may

Re: [seL4] SMC in seL4

Hi Dongxu, As you can see, the arm_monitor_vector uses PC-relative addressing so that the code can be moved around in memory. I think ldr pc, =smc_handler breaks this. Also, please set the NS bit in SCR to 1 before returning. To reserve a memory region for the monitor-mode code and data, I

Re: [seL4] SMC in seL4

Hi, The smc_handle() in monitor.S, it does nothing but "movs pc, lr". Does it set the NS bit to 1 in SCR? Also, what did you do to ensure that 0x1100 is not used by the kernel? Could you share the code (if possible) so that I could better understand the problem. Regards, Yanyan

Re: [seL4] AARCH64 with CAMKES (Questions)

Hi, Mike, I am adding the ARMv8 hypervisor support for seL4 and related user-mode libraries (Tegra TX1 board). Let's discuss how could collaborate on this off-line. Regards, Yanyan From: Devel on behalf of Michael