Changing the VMware settings shouldn't cause the problem. If you find yourself trying to solve this again in the future, maybe run "ninja -j1 -v" into a log file, and see if gcc is being invoked with the correct flags: "-march=nehalem -mno-mmx -mno-sse -mno-sse2 -mno-3dnow". These should prevent the instructions that are causing the user exception to occur in seL4test, yet the binary that you sent had instructions from the AVX SIMD extensions which the nehalem microarch doesn't have.

From: Jeremiah Peschka <jpeschka@pdx.edu>
Sent: Wednesday, October 24, 2018 1:11 AM
To: Devel@sel4.systems; Mcleod, Kent (Data61, Kensington NSW)
Subject: Re: [seL4] Kernel Exception in seL4 Tutorial

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.