Hi John,

This was answered recently here: http://sel4.systems/pipermail/devel/2017-June/001455.html

In summary, we don't currently give threads access to the FPU on arm and the VMM cannot emulate the instructions but this should change soon. There is a patch internally for making the FPU accessible that someone was testing with armhf on the TK1 today. When the patch gets moved, we may be able to update everything to use armhf toolchains.

Kent.

From: Devel <devel-bounces@sel4.systems> on behalf of John Backes <john.backes@gmail.com>
Sent: Tuesday, June 27, 2017 12:34 AM
To: devel
Subject: [seL4] Why armel for the seL4 ARM VMM?

I was curious why the ARM VMM for the TK1 only seems to support the use of armel based distributions? Does special care need to be taken in the VMM to handle guest floating point instructions if the OS is armhf based?

- John