Question about RISCV cpu_start

Since RISCV spec allows WFI to be implemented as a NOP, shouldn't asm("WFI"); be in a while loop, as is commonly done?

https://github.com/apache/nuttx/blob/master/arch/risc-v/src/common/riscv_cpustart.c#L78

```
void riscv_cpu_boot(int cpu)
{
....
/* Enable machine software interrupt for IPI to boot */

up_enable_irq(RISCV_IRQ_SOFT);

/* Wait interrupt */

asm("WFI");

#ifdef CONFIG_BUILD_KERNEL
/* Initialize the per CPU areas */
...
}
```