[PATCH 4.9 017/264] random: use a different mixing algorithm for add_device_randomness()