The problem with math in kernel space is that the ARM doesn't do floating point. There is floating point emulation in the kernel that supports userland applications, but I'm not sure if it can be used in kernel space, and besides which, it is probably too slow to be desirable there.

Your suspicion is correct: NO FLOATING POINT WITHIN THE KERNEL. That applies to pretty much ANY decent kernel (Linux, *BSD, Solaris, ...). Though on Solaris one CAN do it if one manually saves/restores the FP state, dunno about the others.

The primary reason for such a ludicrous restriction, is that to be able to use floating point within a kernel requires that the kernel save/restore FP context whenever the kernel is entered/exited.. and the overhead of doing such is not nice to overall system performance.

Cheers