It seems that L4Linux expects either x86_32 or arm. Would it work to compile the x86_32 version on x86_64? If not, why? What level of multiarch support does Genode have?