I have not tweaked the microarchitecture settings for qemu - I rely on it for my teaching assistant duties as well as for seL4, so I leave it alone. Plus, this is a fresh VM that only exists for seL4, so I’ve changed almost nothing on it.

GCC: gcc (Ubuntu 7.3.0-27ubuntu1~18.04) 7.3.0
Clang: clang version 6.0.0-1ubuntu2 (tags/RELEASE_600/final)
qemu: QEMU emulator version 2.11.1(Debian 1:2.11+dfsg-1ubuntu7.6)

The qemu command being run is: 

qemu-system-x86_64 -cpu Nehalem,-vme,+pdpe1gb,-xsave,-xsaveopt,-xsavec,-fsgsbase,-invpcid,enforce -nographic -serial mon:stdio -m size=512M -kernel images/kernel-x86_64-pc99 -initrd images/hello-world-image-x86_64-pc99

The only other odd thing that it might be is that I have enabled VT-x/EPT support for the VM in VMware, I wouldn’t think that would cause any problems, though...

Jeremiah Peschka
On Oct 22, 2018, 23:37 -0700, Kent.Mcleod@data61.csiro.au, wrote:
​Happy that it is working for you in the Docker container. Based on the images you provided, it seems that the compiler is generating instructions for a newer microarchitecture than what qemu is simulating. This is why seL4test is getting a user exception. Do you tweak the microarchitecture settings at all? Otherwise what version is the compiler in the VM that you are using?

Kent.