Hi,

I can't tell from your output if the kernel had started the init task yet or not. If the init task has been started, this error usually indicates a toolchain that is trying to use FPU, which is not currently supported. FPU support that enables floating point toolchains on arm should be released soon. There will likely be an announcement on the mailing list when this happens.

Kind regards,

Kent McLeod

________________________________ From: Devel devel-bounces@sel4.systems on behalf of li94575 li94575@163.com Sent: Thursday, June 29, 2017 11:19 AM To: devel Subject: [seL4] Can I run Android on camkes-arm-vm with tk1 board?

Hi, Now, Linux4.3 kernel can work well on camkes-arm-vm, does that mean we can run an Android system based on this kernel? I have tried to replace the roofs with an Android ramdisk, but Linux can not excute the Init program. The error is showing below:

[ 10.598871] Freeing unused kernel memory: 4168K (c0a74000 - c0e86000) [ 10.761443] Kernel panic - not syncing: Attempted to kill init! exitcode=0x00000004 [ 10.761443] [ 10.770568] CPU: 0 PID: 1 Comm: init Tainted: G W 4.3.0-rc5-00024-gec4c02c-dirty #122 [ 10.779510] Hardware name: NVIDIA Tegra SoC (Flattened Device Tree) [ 10.785795] [<c00167ec>] (unwind_backtrace) from [<c0012958>] (show_stack+0x10/0x14) [ 10.793537] [<c0012958>] (show_stack) from [<c008f054>] (panic+0x94/0x220) [ 10.800407] [<c008f054>] (panic) from [<c0025b9c>] (do_exit+0x7fc/0x8f4) [ 10.807101] [<c0025b9c>] (do_exit) from [<c0025d70>] (do_group_exit+0x3c/0xf0) [ 10.814318] [<c0025d70>] (do_group_exit) from [<c002f3ec>] (get_signal+0x1a4/0x754) [ 10.821971] [<c002f3ec>] (get_signal) from [<c001a748>] (do_signal+0x84/0x61c) [ 10.829188] [<c001a748>] (do_signal) from [<c0012604>] (do_work_pending+0xa4/0xb4) [ 10.836750] [<c0012604>] (do_work_pending) from [<c000f6b4>] (slow_work_pending+0xc/0x20) [ 10.844919] ---[ end Kernel panic - not syncing: Attempted to kill init! exitcode=0x00000004

Is this a problem that current VMM does not support FPU? or other reasons caused the problem?

Hi,

I cannot think of any reasons why Linux3.10 wouldn't also work other than making similar modifications that we made to Linux4.3. The list of modifications that we made can be seen here: https://github.com/SEL4PROJ/linux-tegra/commits/sel4

If you wanted to try and add support for that version yourself, I would start by trying to build the current supported Linux version from source as described here: https://github.com/SEL4PROJ/camkes-arm-vm/blob/master/README.md

Once you have that working, then change out the source version of Linux with the version you would like to use. Then update the buildroot config to use the correct toolchains, kernel headers and source for the version you want. ​

You will then need to make changes to the Linux source so that it can run in the different hardware environment the vmm presents to it. This mostly relates to changes in the device tree layout file and anywhere in the sources where hardware values are hard coded. I would start trying to get the primary debug uart working first which will then make it easier to debug what is happening as you try and get Linux to initialise.

Hope this helps,

Kind regards,

Kent McLeod

________________________________ From: li94575 li94575@163.com Sent: Thursday, July 6, 2017 12:39 AM To: Mcleod, Kent (Data61, Kensington NSW) Cc: devel Subject: Re: [seL4] Can I run Android on camkes-arm-vm with tk1 board?

Haha, I can be sure that error is due to the lack of FPU supporting. I have updated to the latest version of camkes-arm-vm, and that error is has gone. But this version of Linux doesn't seem to be able to start Android. The Android 5.0 provided by Nvidia's official community for tk1 board is based on Linux3.10, which is very different from the current Linux4.3. If I want to use that version of Linux to run on the VM, what do I need to do? Thanks in advance！

At 2017-06-29 10:17:17, Kent.Mcleod@data61.csiro.au wrote:

Hi,

I can't tell from your output if the kernel had started the init task yet or not. If the init task has been started, this error usually indicates a toolchain that is trying to use FPU, which is not currently supported. FPU support that enables floating point toolchains on arm should be released soon. There will likely be an announcement on the mailing list when this happens.

Kind regards,

Kent McLeod

________________________________ From: Devel <devel-bounces@sel4.systemsmailto:devel-bounces@sel4.systems> on behalf of li94575 <li94575@163.commailto:li94575@163.com> Sent: Thursday, June 29, 2017 11:19 AM To: devel Subject: [seL4] Can I run Android on camkes-arm-vm with tk1 board?

Hi, Now, Linux4.3 kernel can work well on camkes-arm-vm, does that mean we can run an Android system based on this kernel? I have tried to replace the roofs with an Android ramdisk, but Linux can not excute the Init program. The error is showing below:

[ 10.598871] Freeing unused kernel memory: 4168K (c0a74000 - c0e86000) [ 10.761443] Kernel panic - not syncing: Attempted to kill init! exitcode=0x00000004 [ 10.761443] [ 10.770568] CPU: 0 PID: 1 Comm: init Tainted: G W 4.3.0-rc5-00024-gec4c02c-dirty #122 [ 10.779510] Hardware name: NVIDIA Tegra SoC (Flattened Device Tree) [ 10.785795] [<c00167ec>] (unwind_backtrace) from [<c0012958>] (show_stack+0x10/0x14) [ 10.793537] [<c0012958>] (show_stack) from [<c008f054>] (panic+0x94/0x220) [ 10.800407] [<c008f054>] (panic) from [<c0025b9c>] (do_exit+0x7fc/0x8f4) [ 10.807101] [<c0025b9c>] (do_exit) from [<c0025d70>] (do_group_exit+0x3c/0xf0) [ 10.814318] [<c0025d70>] (do_group_exit) from [<c002f3ec>] (get_signal+0x1a4/0x754) [ 10.821971] [<c002f3ec>] (get_signal) from [<c001a748>] (do_signal+0x84/0x61c) [ 10.829188] [<c001a748>] (do_signal) from [<c0012604>] (do_work_pending+0xa4/0xb4) [ 10.836750] [<c0012604>] (do_work_pending) from [<c000f6b4>] (slow_work_pending+0xc/0x20) [ 10.844919] ---[ end Kernel panic - not syncing: Attempted to kill init! exitcode=0x00000004

Is this a problem that current VMM does not support FPU? or other reasons caused the problem？

This could be due to an IOMMU configuration issue. Have you tried turning on the CONFIG_SMMU_INTERRUPT_ENABLE as well as CONFIG_PRINTING options in the seL4 kernel configuration? This will print out IOMMU faults that indicate the IOMMU isn't configured correctly.

Kent.

________________________________ From: li94575 li94575@163.com Sent: Saturday, July 29, 2017 12:07 AM To: Mcleod, Kent (Data61, Kensington NSW) Cc: devel Subject: Re: [seL4] Can I run Android on camkes-arm-vm with tk1 board?

Hi, Recently I have tried to start Linux310 in the VM according to the way you told. After giving the iomem in vm_common.camkes, most drivers of Linux310 can run well except the mmc driver. When the MMC driver initializes, I get an ADMA error with errorcode 0x00000006. I don't know what went wrong, so I sent this email for help. The error log is showing below ( full log and dts file is in mail attachment ):

[ 8.798419] mmc0: ADMA error [ 8.801293] sdhci: =========== REGISTER DUMP (mmc0)=========== [ 8.807119] sdhci: Sys addr: 0x00000000 | Version: 0x00000303 [ 8.812944] sdhci: Blk size: 0x00007200 | Blk cnt: 0x00000000 [ 8.818769] sdhci: Argument: 0x00000000 | Trn mode: 0x00000013 [ 8.824593] sdhci: Present: 0x01fb02f6 | Host ctl: 0x00000011 [ 8.830416] sdhci: Power: 0x0000000b | Blk gap: 0x00000000 [ 8.836241] sdhci: Wake-up: 0x00000000 | Clock: 0x00000407 [ 8.842065] sdhci: Timeout: 0x0000000e | Int stat: 0x00000001 [ 8.848001] sdhci: Int enab: 0x02ff000b | Sig enab: 0x02fc000b [ 8.853826] sdhci: AC12 err: 0x00000000 | Slot int: 0x00000000 [ 8.859649] sdhci: Caps: 0x376fd080 | Caps_1: 0x10002f77 [ 8.865473] sdhci: Cmd: 0x0000083a | Max curr: 0x00000000 [ 8.871293] sdhci: Host ctl2: 0x00003000 [ 8.875211] sdhci: ADMA Err: 0x00000006 | ADMA Ptr: 0x80000000 [ 8.881030] sdhci: ===========================================

I start the same Linux image without sel4, and that error does not appear.

At 2017-07-06 09:21:22, Kent.Mcleod@data61.csiro.au wrote:

Hi,

I cannot think of any reasons why Linux3.10 wouldn't also work other than making similar modifications that we made to Linux4.3. The list of modifications that we made can be seen here: https://github.com/SEL4PROJ/linux-tegra/commits/sel4

If you wanted to try and add support for that version yourself, I would start by trying to build the current supported Linux version from source as described here: https://github.com/SEL4PROJ/camkes-arm-vm/blob/master/README.md

Once you have that working, then change out the source version of Linux with the version you would like to use. Then update the buildroot config to use the correct toolchains, kernel headers and source for the version you want.

You will then need to make changes to the Linux source so that it can run in the different hardware environment the vmm presents to it. This mostly relates to changes in the device tree layout file and anywhere in the sources where hardware values are hard coded. I would start trying to get the primary debug uart working first which will then make it easier to debug what is happening as you try and get Linux to initialise.

Hope this helps,

Kind regards,

Kent McLeod

________________________________

Hi, I turned off the CONFIG_SMMU_INTERRUPT_ENABLE because of the SMMU address translation error, like this:

SMMU Address translation error: ID: 1 address: 0xbde00000 type: 6 direction: 0x0 IOPT permission: read 0x0 write 0x0 nonsecure 0x0

I tried to add the IDs 2 and 3 to the vm.smmu field in vm_common.camkes, but that does not work. Do I need to make any other changes?

At 2017-08-01 07:24:59, Kent.Mcleod@data61.csiro.au wrote:

This could be due to an IOMMU configuration issue. Have you tried turning on the CONFIG_SMMU_INTERRUPT_ENABLE as well as CONFIG_PRINTING options in the seL4 kernel configuration? This will print out IOMMU faults that indicate the IOMMU isn't configured correctly.

Kent.

ID 1 should correspond to the DC SMMU group which we assign ASSID 3, which is referred to in CAmkES as 2. We disable the video controller in our Linux configs and device tree file I believe, so I haven't tested if providing the correct SMMU configuration fixes your issue sorry. ?If you don't need the video controller, you could try disabling it in the Linux config and device tree specification.

Kind regards,

Kent.

________________________________ From: Devel devel-bounces@sel4.systems on behalf of li94575 li94575@163.com Sent: Thursday, August 3, 2017 11:29 PM To: devel Subject: Re: [seL4] Can I run Android on camkes-arm-vm with tk1 board?

Hi, I turned off the CONFIG_SMMU_INTERRUPT_ENABLE because of the SMMU address translation error, like this:

SMMU Address translation error: ID: 1 address: 0xbde00000 type: 6 direction: 0x0 IOPT permission: read 0x0 write 0x0 nonsecure 0x0

I tried to add the IDs 2 and 3 to the vm.smmu field in vm_common.camkes, but that does not work. Do I need to make any other changes?

At 2017-08-01 07:24:59, Kent.Mcleod@data61.csiro.aumailto:Kent.Mcleod@data61.csiro.au wrote:

This could be due to an IOMMU configuration issue. Have you tried turning on the CONFIG_SMMU_INTERRUPT_ENABLE as well as CONFIG_PRINTING options in the seL4 kernel configuration? This will print out IOMMU faults that indicate the IOMMU isn't configured correctly.

Kent.

?The ID 99 refers to the "global memory client ID" specific to the Tegra platform. They can be found in the Technical reference manual under section: 16.7.1.3 MC_ERR_STATUS_0

In this case it refers to the group sdmmc4a?.

Kent

________________________________ From: li94575 li94575@163.com Sent: Saturday, August 5, 2017 1:36 AM To: Mcleod, Kent (Data61, Kensington NSW) Cc: devel Subject: Re: [seL4] Can I run Android on camkes-arm-vm with tk1 board?

Thank you for your help! I disabled the video controller, and now Linux stopped at ADMA error, before that I got a SMMU address translation error again.

SMMU Address translation error: ID: 99 address: 0x80000000 type: 6 direction: 0x0 IOPT permission: read 0x0 write 0x0 nonsecure 0x0

The ID 99 seems to be out of range, but I don't know what's wrong with it.

At 2017-08-04 14:34:53, Kent.Mcleod@data61.csiro.au wrote:

ID 1 should correspond to the DC SMMU group which we assign ASSID 3, which is referred to in CAmkES as 2. We disable the video controller in our Linux configs and device tree file I believe, so I haven't tested if providing the correct SMMU configuration fixes your issue sorry. If you don't need the video controller, you could try disabling it in the Linux config and device tree specification.

Kind regards,

Kent.

________________________________ From: Devel <devel-bounces@sel4.systemsmailto:devel-bounces@sel4.systems> on behalf of li94575 <li94575@163.commailto:li94575@163.com> Sent: Thursday, August 3, 2017 11:29 PM To: devel Subject: Re: [seL4] Can I run Android on camkes-arm-vm with tk1 board?

Hi, I turned off the CONFIG_SMMU_INTERRUPT_ENABLE because of the SMMU address translation error, like this:

SMMU Address translation error: ID: 1 address: 0xbde00000 type: 6 direction: 0x0 IOPT permission: read 0x0 write 0x0 nonsecure 0x0

I tried to add the IDs 2 and 3 to the vm.smmu field in vm_common.camkes, but that does not work. Do I need to make any other changes?