It turns out that it works perfectly fine for generating 32-bits vDSOs as well. While there, get rid of the extraneous .s file extension.
Ed Schouten