This should prevent printf output from multiple threads getting garbled.
I don't know why IO ever worked properly -- probably it was always a bit
broken -- but the GFX11 devices have a different cache architecture and
trying to print from many threads at once corrupted the FILE buffers.
Andrew Stubbs