Comment by breadbox

A valid point! Clearly the correct solution would be for the kernel module to check if the filename contains the substring "32", and if so it should load it as a 32-bit binary.