Hi Chris, This is expected. When the kernel is started by the bootloader, the processor is in protected mode and can only use 32-bit instructions. One of the first things the x86_64? kernel then does is to switch the processor to long mode and enable 64-bit instructions. Because of this, the initial entry point assembly is 32bit, but the rest of the kernel is 64bit. You can verify this by checking the intermediate kernel build file: $ file kernel/kernel.elf kernel/kernel.elf: ELF 64-bit LSB executable, x86-64, version 1 (SYSV), statically linked, with debug_info, not stripped This command is where the 64bit kernel is reformatted into a 32-bit elf: https://github.com/seL4/seL4_tools/blob/master/cmake-tool/common.cmake#L115 Kent. ________________________________ From: Devel on behalf of Chris Rothrock Sent: Thursday, August 30, 2018 10:40 PM To: devel@sel4.systems Subject: [seL4] 32 bit vs 64 bit When building the x86 demo for both 32 and 64 bit builds, it looks like the kernel is still a 32 bit elf file regardless of the build and only the sel4test-driver file is what is either 32 bit or 64 bit depending on which is selected. Is this normal or should the kernel also be 64 bit on the 64 bit build? -- Thank You, Chris Rothrock Senior System Administrator (315) 308-1637 [https://docs.google.com/uc?id=0B2xyRpsbQtDNVGlnSV9BWFBlUm8&export=download]