32 bit kernel on 64 bit machine