Indan Zupancic

Also tested the FPU changes on aarch32 with virtual machine and aarch64 with virtual machine. They both boot Linux and seem functional. All seems fine, but I should add some...

Glad I wrote the sel4test, the wrapper function didn't save MR0, so it got lost.

It can actually be reproduced by sel4test, it's the same issue I ran into with https://github.com/seL4/sel4test/pull/134, but the test is currently disabled in CI for the Odroid-C4. It's high on...

> Do you get it deterministically on sel4test? Because I'm sure I saw it working there when I tried to reproduce Alain's initial report. I did for the tx2 before,...

I know this is a while ago, but I'm currently busy with the FPU code and spotted this open issue. 1) That's indeed wrong. 2) desired_features is set to 3...

So I think we should try to have high-level discussions on https://github.com/seL4/rfcs/pull/21 and only discuss implementation details here. We have unresolved high-level decisions that influence the implementation a lot. One...

Yes, don't do unaligned accesses on device memory. That also means, don't use memcpy or other stdlibc functions on device memory. You want the device memory attribute, otherwise writes may...

Yes, the issue stays around and searchable when it's marked closed. You're right it should be documented in the manual, it currently isn't. Re-opening the issue as a reminder for...

> The only case that's come up for me is when using dma pools. Uncached vs cached seems to be a tradeoff depending on the size of the transaction because...

Yes, it's very confusing. I think the idea was that `armv_handleVCPUFault` should figure out what trap it is exactly. The 32-bit code only checks for FPU faults, the 64-bit code...