Hi Kent,

I did a fresh

repo init -u https://github.com/seL4/camkes-vm-manifest

so I am using the latest default.xml

Now I can get a bit further - although still not all the way - here is the full output: https://gist.github.com/podhrmic/bc86178e60fad64ab870ff1fa19992e3

and then the system as far as I can tell hangs - no serial or VGA output.

What could be the cause?

Regards
M

On Mon, Feb 19, 2018 at 4:07 PM, <Kent.Mcleod@data61.csiro.au> wrote:

Hi Michal,


Which revision of default.xml are you using?  Adrian thinks it could be potentially related to, and fixed by, this commit[1] if you don't have it yet.


Kent


[1] https://github.com/seL4/seL4/commit/3d6f4f9bb7bfe42628dfa555601401fa4efcdf2d




From: Devel <devel-bounces@sel4.systems> on behalf of Michal Podhradsky <mpodhradsky@galois.com>
Sent: Tuesday, February 20, 2018 9:37 AM
To: devel@sel4.systems
Subject: [seL4] CamkesVM CMA34CR_centos app
 
Hi all,

I have a CM34CR CPU module and I am trying to run the related camkes app on it. 

I choose the centos app: https://github.com/seL4/camkes-vm/blob/master/apps/vm/cma34cr_centos.camkes

I am using default camkes vm manifest from https://github.com/seL4/camkes-vm-manifest.

Compile with:
make clean
make cma34cr_centos_defcondig
make silentoldconfig
make

And then I create a bootable USB following instructions here.

Then after I load the kernel and capdl image, I get the following output on serial:

Boot config: parsing cmdline 'sel4kernel'
Boot config: console_port = 0x3f8
Boot config: debug_port = 0x3f8
Boot config: disable_iommu = false
Detected 1 boot module(s):
  module #0: start=0xd34000 end=0x3b387e8 size=0x2e047e8 name='rootserver'
Parsing GRUB physical memory map
    Physical Memory Region from 0 size 9d400 type 1
    Physical Memory Region from 9d400 size 2c00 type 2
    Physical Memory Region from e0000 size 20000 type 2
    Physical Memory Region from 100000 size 1ff00000 type 1
Adding physical memory region 0x100000-0x20000000
    Physical Memory Region from 20000000 size 200000 type 2
    Physical Memory Region from 20200000 size 1fe04000 type 1
Adding physical memory region 0x20200000-0x40004000
    Physical Memory Region from 40004000 size 1000 type 2
    Physical Memory Region from 40005000 size 64bab000 type 1
Adding physical memory region 0x40005000-0xa4bb0000
    Physical Memory Region from a4bb0000 size 1400000 type 2
    Physical Memory Region from a5fb0000 size 4a0f000 type 1
Adding physical memory region 0xa5fb0000-0xaa9bf000
    Physical Memory Region from aa9bf000 size 500000 type 2
    Physical Memory Region from aaebf000 size 100000 type 4
    Physical Memory Region from aafbf000 size 40000 type 3
    Physical Memory Region from aafff000 size 1000 type 1
Adding physical memory region 0xaafff000-0xab000000
    Physical Memory Region from ab000000 size 4a00000 type 2
    Physical Memory Region from f0000000 size 4000000 type 2
    Physical Memory Region from feb00000 size 4000 type 2
    Physical Memory Region from fec00000 size 1000 type 2
    Physical Memory Region from fed10000 size a000 type 2
    Physical Memory Region from fed1c000 size 4000 type 2
    Physical Memory Region from fee00000 size 1000 type 2
    Physical Memory Region from ffc00000 size 400000 type 2
    Physical Memory Region from 100000000 size 14f600000 type 1
Adding physical memory region 0x100000000-0x24f600000
Got VBE info in multiboot. Current video mode is 16767
ACPI: RSDP paddr=0xfe020
ACPI: RSDP vaddr=0xfe020
ACPI: RSDT paddr=0xaafda0c4
ACPI: RSDT vaddr=0xaafda0c4
Kernel loaded to: start=0x100000 end=0xc17000 size=0xb17000 entry=0x101269
ACPI: RSDT paddr=0xaafda0c4
ACPI: RSDT vaddr=0xaafda0c4
ACPI: FADT paddr=0xaaffb000
ACPI: FADT vaddr=0xaaffb000
ACPI: FADT flags=0x3c6a5
ACPI: DMAR paddr=0xaafde000
ACPI: DMAR vaddr=0xaafde000
ACPI: IOMMU host address width: 36
    ACPI: registering RMRR entry for region for device: bus=0x0 dev=0x1d fun=0x0
    ACPI: registering RMRR entry for region for device: bus=0x0 dev=0x1a fun=0x0
    ACPI: registering RMRR entry for region for device: bus=0x0 dev=0x14 fun=0x0
    ACPI: registering RMRR entry for region for device: bus=0x0 dev=0x2 fun=0x0
ACPI: 2 IOMMUs detected
ACPI: MADT paddr=0xaaff9000
ACPI: MADT vaddr=0xaaff9000
ACPI: MADT apic_addr=0xfee00000
ACPI: MADT flags=0x1
ACPI: MADT_APIC apic_id=0x0
ACPI: MADT_APIC apic_id=0x1
ACPI: MADT_APIC apic_id=0x2
ACPI: Not recording this APIC, only support 2
ACPI: MADT_APIC apic_id=0x3
ACPI: Not recording this APIC, only support 2
ACPI: MADT_IOAPIC ioapic_id=0 ioapic_addr=0xfec00000 gsib=0
ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0
ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xd
ACPI: 2 CPU(s) detected
ELF-loading userland images from boot modules:
size=0x41fc000 v_entry=0x409000 v_start=0x400000 v_end=0x45fc000 p_start=0x3b39000 p_end=0x7d35000
Moving loaded userland images to final location: from=0x3b39000 to=0xc17000 size=0x41fc000
Starting node #0 with APIC ID 0
Mapping kernel window is done

========== KERNEL EXCEPTION ==========
Vector:  0xd
ErrCode: 0x0
IP:      0xffffffff80115c04
SP:      0xffffffff80a0bfa0
FLAGS:   0x10046
CR0:     0x80010013
CR2:     0x0 (page-fault address)
CR3:     0xa12000 (page-directory physical address)
CR4:     0x110668

Stack Dump:
*0xffffffff80a0bfa0 == 0x0
*0xffffffff80a0bfa8 == 0x0
*0xffffffff80a0bfb0 == 0x3b39000
*0xffffffff80a0bfb8 == 0xffffffff80116b80
*0xffffffff80a0bfc0 == 0x0
*0xffffffff80a0bfc8 == 0x22a8
*0xffffffff80a0bfd0 == 0x0
*0xffffffff80a0bfd8 == 0x0
*0xffffffff80a0bfe0 == 0xffffffff80000000
*0xffffffff80a0bfe8 == 0x7e000
*0xffffffff80a0bff0 == 0xaa24c70c
*0xffffffff80a0bff8 == 0x1f
*0xffffffff80a0c000 == 0xfffffffff000ba86
*0xffffffff80a0c008 == 0xffffffff8081f0c0
*0xffffffff80a0c010 == 0x0
*0xffffffff80a0c018 == 0x0
*0xffffffff80a0c020 == 0x0
*0xffffffff80a0c028 == 0x0
*0xffffffff80a0c030 == 0x0
*0xffffffff80a0c038 == 0x0

Halting...
halting...
Kernel entry via Interrupt, irq 0


Any pointers at what is the cause of error here? The machien runs normally with vanilla CentOS so I don't think it is a hardware issue. Also, I am assuming the CMA34CR is identical to the one you have on your side (at least checking the lspci output against the camkes description the memory regions etc seem to match).

Thanks in advance.
M