I wonder how vDSO works for an x32 ABI program (ie a program with 32 bit pointers, but access to the rest of the x86-64 feature set).