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

[Yanyan.Shen]

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 look at the TX1 plat. Your SoC 
manual should also explain how to bring up secondary cores.


The elfloader assumes the the uart port for printf is initialised by the uboot 
or other boot loaders. Otherwise, the elfloader needs to set up the port.


Hope this can help a bit.



Regards,

Yanyan



From: Devel  on behalf of Diego Alejandro Parra 
Guzman 
Sent: Monday, February 18, 2019 6:11 PM
To: devel@sel4.systems
Subject: Re: [seL4] port SeL4 to renesas rcar-H3 development board

Hi guys !!!

Thank you for your quick replay.

I'm try to port Sel4 kernel to the renesas H3 ULCB board with two clusters 
(ARM57),(ARM53) each one with 4 cores

I just have couple of questions regarding with  the elf loader in sel4-tools:

there is  some files in elfloader-tool/plat/* those are intended to initialize 
the CPU and the UART on the platform. In there, there is a function written in 
assembly called  core_entry_head  and a function init_cpusimplemented in smp.c 
file.
Could you please explain me  a  little bit what is the purpose of these 
functions ?

In the case of init_cpus where is suppose to be that information? I means, I 
should  reference the ARM57 or ARM53 cpu manual or maybe to the boot section in 
the SoC manual.


from the other hand the renesas H3 ULCB doesn't have a physical UART port. 
Instead, it has an Serial Communication Interface with FIFO (SCIF) that can be 
configure properly to be compatible with UART interfaces. The point is that  
I'm using this interface in order to implement the __fputc()  function 
following the one implemented in sys_fput.c file.  Unfortunately,  I don't 
understand why in your implementation there is not an initialization for the 
UART.  could you tell me why not?

Thank you.

best regards

On Sat, 16 Feb 2019 at 06:57, Diego Alejandro Parra Guzman 
mailto:dapar...@correo.udistrital.edu.co>> 
wrote:
Hi guys !!!

Thank you for your quick replay.

I'm try to port Sel4 kernel to the renesas H3 ULCB board with two clusters 
(ARM57),(ARM53) each one with 4 cores

I just have couple of questions regarding with  the elf loader in sel4-tools:

there is  some files in elfloader-tool/plat/* those are intended to initialize 
the CPU and the UART on the platform. In there, there is a function written in 
assembly called  core_entry_head  and a function init_cpusimplemented in smp.c 
file.
Could you please explain me  a  little bit what is the purpose of these 
functions ?

In the case of init_cpus where is suppose to be that information? I means, I 
should  reference the ARM57 or ARM53 cpu manual or maybe to the boot section in 
the SoC manual.


from the other hand the renesas H3 ULCB doesn't have a physical UART port. 
Instead, it has an Serial Communication Interface with FIFO (SCIF) that can be 
configure properly to be compatible with UART interfaces. The point is that  
I'm using this interface in order to implement the __fputc()  function 
following the one implemented in sys_fput.c file.  Unfortunately,  I don't 
understand why in your implementation there is not an initialization for the 
UART.  could you tell me why not?

Thank you.

best regards

On Wed, 13 Feb 2019 at 15:21, Diego Alejandro Parra Guzman 
mailto:dapar...@correo.udistrital.edu.co>> 
wrote:

Hi,

I'm new with seL4 kernel and I would like to port it to the ARM-based renesas 
rcar-H3 board

I would like to ask of you have a development manual that i can follow with 
some basics about how to do it?

I followed the tutorials and so one. But  I will appreciate if you have 
something guidelines to start.

Thank you

BR
Diego.
--
Diego Alejandro Parra Guzmán
Estudiante de ingeniería electrónica
Universidad distrital FJC


--
Diego Alejandro Parra Guzmán
Estudiante de ingeniería electrónica
Universidad distrital FJC


--
Diego Alejandro Parra Guzmán
Estudiante de ingeniería electrónica
Universidad distrital FJC
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

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

[Yanyan.Shen]

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 the value of TTBR0_EL1. Also, if I remeber correctly, 
"isb" should be used after modifying a control register so that the 
modification can be observed by the instructions following the instruction that 
modifies the control register, through the effect of flushing pipeline and 
refetching instructions.?


ASID is used to reduce TLB flushes.



Regards,

Yanyan?





From: Devel  on behalf of Dd Nirvana 

Sent: Saturday, December 1, 2018 7:23 PM
To: devel@sel4.systems
Subject: [seL4] Is the ASID used in seL4 by default?

Hi guys,

 I found that seL4's ARM version still need "isb" and "dsb" around updating 
TTBR0_EL1.
 This fence will flush the TLB and will affect IPC performance. However, it 
seems that enabling ASID can avoid this costs.
 I am not sure, is there any concern that makes seL4 to avoid using ASID?

 BTW, I have seen ASID management in seL4 (ASID control and ASID pool), so 
maybe I misunderstood something?


Dong Du,
Shanghai Jiao Tong University
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

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

[Yanyan.Shen]

?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 running unsafe Linux VMs.
--- Are you going to run one SMP Linux VM or multiple single-core Linux VMs? We 
are developing the support for running Linux VM on aarch64, and hopefully we 
will push out the code out soon.

d) It's my understanding that seL4 lacks 64-bit multicore support for its own 
scheduler, but VMs running on seL4 could be provided with access to all the 
cores? (Eg: Linux)
- I believe the experimental aarch64 multicore support exists in the mainline 
seL4 kernel. A virtual machine monitor (VMM) needs to emulate the PSCI 
interface and intercept SMC calls so that the VMM is able to create multiple 
VCPUs and assigned the VCPUs to an SMP Linux VM. The scheduling of VCPUs is 
still managed by seL4.

e) It's my understanding that seL4 lacks heterogeneous task scheduling, and 
cannot manage both the Cortex R5 and Cortex A53 cores.
--- The Cortex R5 cores are not supported.

[1] It's not possible to boot an seL4 kernel on one processor and have it 
manage the other.
--- I do not quite understand this, but my initial response is NO. Please add 
more info.

[2] Use TrustZone to create vCPUs for the Cortex R5 and A53 modules and boot an 
seL4 kernel on each.
--- TrustZone does not create vCPUs (at least in the sense of virtualization). 
In seL4 parlance, a VCPU is an seL4 kernel object.

[3] Some domain specific protocol is required for the CPU modules to 
communicate and share resources.
--- The SoC may provide some hardware support for communicating between 
Cortex-A and Cortex-R CPU modules. I am not familiar with the Zynq board. 
Otherwise, shared memory should work.



Regards,

Yanyan



From: Devel  on behalf of Blam Kiwi 

Sent: Thursday, October 11, 2018 1:48 PM
To: devel@sel4.systems
Subject: [seL4] seL4 on Heterogeneous Processing Architectures (Zynq 
UltraScale+ MPSoCs)

I am investigating the use of seL4 on heterogeneous architectures such as the 
Zynq UltraScale+ MPSoCs. I have a non-trivial use-case I'm investigating that 
involves utilising both the Cortex-R5 cores and Core-A53 cores for different 
applications. I'm rather new to seL4 development so I'm a bit stuck and need 
some advice.

It's easiest if I just list my requirements and assumptions for my architecture 
design:

a) I am targeting the Zynq US+ platform and wish to use seL4 as the OS Kernel 
to manage system resources and run virtual machines.
b) I require the use of the Cortex R5 cores in DCLS mode for trusted code with 
high fault tolerance requirements.
c) I require the use of the Cortex A53 cores for running unsafe Linux VMs.
d) It's my understanding that seL4 lacks 64-bit multicore support for its own 
scheduler, but VMs running on seL4 could be provided with access to all the 
cores? (Eg: Linux)
e) It's my understanding that seL4 lacks heterogeneous task scheduling, and 
cannot manage both the Cortex R5 and Cortex A53 cores.

This leads me to make the following architectural conclusions:

[1] It's not possible to boot an seL4 kernel on one processor and have it 
manage the other.
[2] Use TrustZone to create vCPUs for the Cortex R5 and A53 modules and boot an 
seL4 kernel on each.
[3] Some domain specific protocol is required for the CPU modules to 
communicate and share resources.

Any help or advice would be appreciated.

Regards,
Robbie

___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

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

[Yanyan.Shen]

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 solve your problem.
  

Regards,
Yanyan


From: Devel  on behalf of Nicholas Pahl 

Sent: Saturday, September 29, 2018 2:26 AM
To: devel@sel4.systems
Subject: [seL4] Alignment fault without U-Boot Cache Enabled

Hi All,

I have noticed an alignment fault in the seL4 elfloader when running seL4 on an
AArch64 platform with dcache disabled in U-Boot. The alignment fault is caused
by reading the elf files header in the elfloader. The fault can be fixed
(hacked) by modifying the length of the elf file name, located before the elf
file header, to force a proper alignment.

Is the seL4 elfloader intended to be dependent on u-boot enabling the cache?

___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] SMC in seL4

[Yanyan.Shen]

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 suggest you 
modify the avail_p_regs[] in kernel/include/plat/imx6/plat/machine/hardware.h 
file. See the kernel/include/plat/tk1/plat/machine/hardware.h as an example.​



Regards,

Yanyan



From: Dongxu Ji 
Sent: Wednesday, August 29, 2018 12:02 AM
To: devel@sel4.systems; Shen, Yanyan (Data61, Kensington NSW)
Subject: Fwd: [seL4] SMC in seL4

Hi  Yanyan,
1. It doesn't set the NS bit to 1 in SCR(I just want it to return without do 
anything). The arm_monitor_vector and the smc_handler():

arm_monitor_vector:
ldr pc, [pc, #28]
ldr pc, [pc, #24]
ldr pc, =smc_handler
ldr pc, [pc, #16]
ldr pc, [pc, #12]
ldr pc, [pc, #8]
ldr pc, [pc, #4]
ldr pc, [pc, #0]

smc_handler:
movs pc, lr

2. I didn't do any extra work other than the boot log:

..
ELF-loader started on CPU: ARM Ltd. Cortex-A9 r2p10
  paddr=[2000..203fbfff]
ELF-loading image 'kernel'
  paddr=[1000..10026fff]
  vaddr=[e000..e0026fff]
  virt_entry=e000
ELF-loading image 'sel4test-driver'
  paddr=[10027000..10500fff]
  vaddr=[8000..4e1fff]
  virt_entry=25a6c
Enabling MMU and paging
Jumping to kernel-image entry point...

3. The initialization operations in platform_init.c:
set sp:
#define MONITOR_MODE(0x16)
#define MON_VECTOR_START(0x1100)
#define VECTOR_BASE 0x1100
#define STACK_TOP   (VECTOR_BASE + (1 << 12) - 0x10)

asm volatile ( "mrs r1, cpsr\n\t"
  "cps %0\n\t"
  "isb\n"
  "mov sp, %1\n\t"
  "msr cpsr, r1\n\t"
 ::"I"(MONITOR_MODE),"r"(STACK_TOP));

copy monitor mode vector to MON_VECTOR_START  and write into MVBAR:
uint32_t size = arm_monitor_vector_end - arm_monitor_vector;
printf("Copy monitor mode vector from %x to %x size %x\n", 
(arm_monitor_vector), MON_VECTOR_START, size);
memcpy((void *)MON_VECTOR_START, (void *)(arm_monitor_vector), size);
asm volatile ("dmb\n isb\n");
asm volatile ("mcr p15, 0, %0, c12, c0, 1"::"r"(MON_VECTOR_START));

I enter into SVC mode by software interrupt and call the function smc():
  asm (".arch_extension sec\n");
 asm volatile ("stmfdsp!, {r3-r11, lr}\n\t"
   "dsb\n"
   "smc #0\n"
   "ldmfdsp!, {r3-r11, pc}");

and then the problem arises.

Thank you,
Dongxu Ji


mailto:yanyan.s...@data61.csiro.au>> 于2018年8月28日周二 
下午8:30写道：

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



From: Devel  on behalf of 冀东旭 
mailto:jidongxu1...@gmail.com>>
Sent: Tuesday, August 28, 2018 1:02 PM
To: devel@sel4.systems
Subject: [seL4] SMC in seL4

Hello,

I'm porting sel4 to imx6q sabrelite as the trusted OS in trustzone.  I 
initialize the monitor mode by setting the sp to  STACK_TOP and copying 
arm_monitor_vector to MON_VECTOR_START according to the functions 
"install_monitor_hook()" and "switch_to_mon_mode()" in "platform_init.c".

#define VECTOR_BASE 0x1100(addr is not used by the seL4 kernel)

#define STACK_TOP   (VECTOR_BASE + (1 << 12) - 0x10)

#define MON_VECTOR_START0x1100(The VECTOR_BASE is the same as 
MON_VECTOR_START)

The smc_handle() in monitor.S, it does nothing but "movs pc, lr".  After 
calling smc in SVC mode, it hangs without any log.  If I comment the "smc #0", 
it can return the caller successfully in usr mode.

stmfdsp!, {r3-r11, lr}
dsb
smc #0
ldmfdsp!, {r3-r11, pc}

Is the sp in monitor mode appropriate? Or I need to do something else in 
initialization operations?  What's wrong with it?  Do you have any ideas?

Thank you!

Dongxu Ji
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] SMC in seL4

[Yanyan.Shen]

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



From: Devel  on behalf of 冀东旭 

Sent: Tuesday, August 28, 2018 1:02 PM
To: devel@sel4.systems
Subject: [seL4] SMC in seL4

Hello,

I'm porting sel4 to imx6q sabrelite as the trusted OS in trustzone.  I 
initialize the monitor mode by setting the sp to  STACK_TOP and copying 
arm_monitor_vector to MON_VECTOR_START according to the functions 
"install_monitor_hook()" and "switch_to_mon_mode()" in "platform_init.c".

#define VECTOR_BASE 0x1100(addr is not used by the seL4 kernel)

#define STACK_TOP   (VECTOR_BASE + (1 << 12) - 0x10)

#define MON_VECTOR_START0x1100(The VECTOR_BASE is the same as 
MON_VECTOR_START)

The smc_handle() in monitor.S, it does nothing but "movs pc, lr".  After 
calling smc in SVC mode, it hangs without any log.  If I comment the "smc #0", 
it can return the caller successfully in usr mode.

stmfdsp!, {r3-r11, lr}
dsb
smc #0
ldmfdsp!, {r3-r11, pc}

Is the sp in monitor mode appropriate? Or I need to do something else in 
initialization operations?  What's wrong with it?  Do you have any ideas?

Thank you!

Dongxu Ji
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] AARCH64 with CAMKES (Questions)

[Yanyan.Shen]

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 DeFrancis 

Sent: Wednesday, December 6, 2017 8:54 AM
To: Chubb, Peter (Data61, Kensington NSW)
Cc: devel@sel4.systems
Subject: Re: [seL4] AARCH64 with CAMKES (Questions)

Right.

I need to create an aarch64 (armv8-a) sel4 hypervisor and vmm in order to 
support our customers in the USA. I will contribute all back to community 
afterwards.

I need help getting started. Can you help?

Mike


Ramble..
I need the hypervisor pieces and the vmm pieces to run at aarch64 to do this. I 
am willing to do the heavy lifting myself and of course contribute back all of 
my changes - with whatever license agreement is necessary - but I think I need 
some help getting started. Could you or someone from your team point me in the 
right direction?

Getting an aarch64 hypervisor / linux demo running on top of sel4 will 
definitely help us to sell sel4 (no pun intended?) to US customers interested 
in using sel4 for safety critical systems.

I would prefer to stick with using camkes but I may have to strip all of the 
camkes stuff out if it expedites things on my end in order to meet our 
schedule.  I have reference code from the xen hypervisor (www.xen.world), that 
I can use as a baseline.



-Original Message-
From: peter.ch...@data61.csiro.au [mailto:peter.ch...@data61.csiro.au]
Sent: Tuesday, December 5, 2017 4:38 PM
To: Michael DeFrancis 
Cc: devel@sel4.systems
Subject: Re: [seL4] AARCH64 with CAMKES (Questions)

> "Michael" == Michael DeFrancis  writes:


Michael> I am attempting to build a linux virtual machine on top of the
Michael> zynqmp ultrascape+ / sel4 kernel, and using the tk1 vmm project
Michael> as my reference point.

The TK1 VMM runs in 32-bit mode.  We haven't written a hypervisor yet for 
aarch64.

arm_hyp is essentially armv7-a with VE; aarch32 is armv6 or later.
Both are 32-bit.

Patches are welcome (with Contributer licence agreement); we would really like 
to see a 64-bit virtual machine monitor.

Peter C
--
Dr Peter Chubb Tel: +61 2 9490 5852  http://ts.data61.csiro.au/
Trustworthy Systems Group   Data61 (formerly NICTA)




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.

___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel