If threads called alloc_find_dev() with same device_path simultaneously, two device nodes could be allocated. This bug is not triggered by current code. Change-Id: Ifc87021c8d6f422901c5de5dd17392e3e2309afa Signed-off-by: Kyösti Mälkki <kyosti.malkki@gmail.com> Reviewed-on: http://review.coreboot.org/1188 Tested-by: build bot (Jenkins) Reviewed-by: Ronald G. Minnich <rminnich@gmail.com> Reviewed-by: Sven Schnelle <svens@stackframe.org>