We were seeing programs crash at the first system call when using some versions of glibc, but not others. It seems the difference is that the working glibc's are compiled without vdso support.

When glibc tries to use the vdso for system calls, it crashes at the sysenter instruction.

If we start l4linux with vdso32=0, the program is able to run.

Is sysenter expected to work under l4linux? It looks like it requires using msr's, so perhaps l4linux isn't able to setup sysenter? Should it be installing the int80 vdso function instead?

While investigating the vdso stuff to I also became curious. How difficult would it be to set up an l4 specific vdso? I assume just using l4 ipc directly would be more efficient than using int80?

Thanks,

Ryan Brown