From: Muneeswaran Rajendran <m.rajendran@matellio.com>
Sent: 06 October 2017 18:45
To: Atuah, Kofi Doku (Data61, Kensington NSW)
Cc: devel@sel4.systems
Subject: Re: [seL4] does seL4 support NVIDIA Jetson Tx2 board ?

Hi kofidoku,

Thanks for detailed input. I try to build seL4 for tx1 platform there was compilation error autoconf.h missing in the include folder.

drwxrwxr-x 2 spanidea spanidea 4096 Oct 6 11:46 tk1
drwxrwxr-x 2 spanidea spanidea 4096 Sep 5 07:28 am335x
drwxrwxr-x 2 spanidea spanidea 4096 Sep 5 07:28 apq8064
-rw-rw-r-- 1 spanidea spanidea 992 Sep 5 07:28 arm_verified.cmake
drwxrwxr-x 2 spanidea spanidea 4096 Sep 5 07:28 exynos4
drwxrwxr-x 2 spanidea spanidea 4096 Sep 5 07:28 exynos5
drwxrwxr-x 2 spanidea spanidea 4096 Sep 5 07:28 hikey
drwxrwxr-x 2 spanidea spanidea 4096 Sep 5 07:28 imx31
drwxrwxr-x 2 spanidea spanidea 4096 Sep 5 07:28 imx6
drwxrwxr-x 2 spanidea spanidea 4096 Sep 5 07:28 imx7
drwxrwxr-x 2 spanidea spanidea 4096 Sep 5 07:28 omap3
drwxrwxr-x 2 spanidea spanidea 4096 Sep 5 07:28 pc99
drwxrwxr-x 2 spanidea spanidea 4096 Sep 5 07:28 zynq7000

I have created the tx1 folder and copy the tk1/autoconf.h file into it.

drwxrwxr-x 2 spanidea spanidea 4096 Oct 6 12:27 tx1

Later the compilation failed with below error messages

[MKDIR] arch/object
[PBF_GEN] arch/object/structures.pbf
[PBF_GEN] plat/machine/hardware.pbf
[PBF_GEN] 32/mode/api/shared_types.pbf
[BF_GEN] arch/object/structures_gen.h
[BF_GEN] plat/machine/hardware_gen.h
[BF_GEN] 32/mode/api/shared_types_gen.h
[CPP] src/arch/arm/armv/armv8-a/32/machine_asm.s_pp
[AS] src/arch/arm/armv/armv8-a/32/machine_asm.o
[CPP] src/arch/arm/32/head.s_pp
[AS] src/arch/arm/32/head.o
[CPP] src/arch/arm/32/traps.s_pp
[AS] src/arch/arm/32/traps.o
[CPP] src/arch/arm/32/hyp_traps.s_pp
[AS] src/arch/arm/32/hyp_traps.o
[CPP_GEN] kernel_all.c
[CPP] kernel_all.c_pp
src/arch/arm/object/vcpu.c:109:2: error: #error GIC_PL400_VCPUCTRL_PPTR must be defined for virtual memory access to the gic virtual cpu interface control
make: *** [kernel_all.c_pp] Error 1
rm 32/mode/api/shared_types_gen.h src/arch/arm/32/traps.s_pp plat/machine/hardware_gen.h src/arch/arm/32/head.s_pp src/arch/arm/armv/armv8-a/32/machine_asm.s_pp src/arch/arm/32/hyp_traps.s_pp arch/object/structures_gen.h

the macro 'GIC_PL400_VCPUCTRL_PPTR' was not defined in the 'include/plat/tx1/plat/machine/devices.h' hence compilation failed. But this macro was defined in tk1 include file.

can you please share the correct autoconf file for tx1 platform to build seL4 kernal.

Regards,

Munees

On Fri, Oct 6, 2017 at 12:20 PM, <Kofidoku.Atuah@data61.csiro.au> wrote:

Hey Munes and Ashok,

To my knowledge, seL4 supports the TX1 SoC, but not the TX2 explicitly.

If the TX1 and TX2 behave similarly, then there's probably a lot of code that can be shared between them. I can't comment on whether or not they are similar enough though.

That said, to help you begin the search to find out, you can look through the code we currently have for the TK1 and TX1. So the way the codebase is organized for the TK1 and TX1 right now, the common drivers for both of them are in libplatsupport/src/mach/nvidia (https://github.com/seL4/util_libs/tree/master/libplatsupport/src/mach/nvidia).

We personally have, internally, 3 boards for which the TK1 and TX1 SoCs are common:

(1) Colorado TK1-SOM.

(2) Nvidia Jetson TK1

(3) Some TX1-based board which I don't know much about off the top of my head.

The two TK1 platforms use the same "plat" code in libplatsupport/src/plat/tk1: https://github.com/seL4/util_libs/tree/master/libplatsupport/src/plat/tk1

And I see a TX1 platform folder here as well, though I'm not familiar with it myself (and frankly the files are empty anyway): https://github.com/seL4/util_libs/tree/master/libplatsupport/src/plat/tx1

--

Kofi Doku Atuah
Kernel engineer
DATA61 | CSIRO

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