lib: sbi: Order the publication of IPI device nodes

[zeldovich]

Summary

This bug was found in the process of formally verifying the correctness of OpenSBI on top of the Sail RISC-V semantics using Lean.

sbi_ipi_add_device() links a freshly allocated node into ipi_dev_node_list with plain stores, and warm harts walk that list with plain loads in sbi_ipi_raw_clear(true) while the cold hart is still inserting. A reader can see the new node pointer and then read the node's fields, or the device's per-hart data, before the writer's stores to them are visible. A release before the publishing stores and an acquire after the reader's load of each node close it.

An execution that triggers it

Setup: eight harts booting; the cold hart runs sbi_init's cold path; the other seven were released at wake_coldboot_harts() and run init_warmboot. RVWMO hardware.

1. Cold hart: sbi_ipi_init(true) → fdt_ipi_init → aclint_mswi_cold_init → sbi_ipi_add_device(&aclint_mswi). It calls sbi_zalloc for the node (entry), then stores entry->dev = &aclint_mswi and the node's prev and next links, then stores ipi_dev_node_list.prev->next = &entry->head (the publish). No fence between the two groups.
2. Warm hart 3, in parallel: init_warmboot → wait_for_coldboot (returns: coldboot_done was released earlier) → sbi_ipi_raw_clear(true) → sbi_list_for_each_entry(entry, &ipi_dev_node_list, head): loads ipi_dev_node_list.next.
3. Under RVWMO the cold hart's stores may become visible to hart 3 in any order. Hart 3's load returns the published pointer &entry->head (store from step 1's last group), but the stores to entry->dev and entry->head.next are not yet visible to hart 3.
4. Hart 3 loads entry->dev: it reads the sbi_zalloc'd zero, or garbage if the allocation reused memory. It then evaluates entry->dev->ipi_clear: a load through a NULL or wild pointer. Load through NULL faults in M-mode (no PMP region at 0 on virt): hart 3 traps through _trap_handler into sbi_trap_error, prints a register dump and hangs. The system comes up with 7 harts.
5. A second variant with the same window: hart 3 reads entry->head.next stale (zero) instead of &ipi_dev_node_list, so the walk never reaches the list head and dereferences address 0 on the next iteration.
6. A third variant needs no NULL: hart 3 reads dev->ipi_clear correctly but mswi_ipi_clear then reads the hart's own aclint_mswi_data pointer from its scratch, written by the cold hart in aclint_mswi_cold_init before the add. Without an acquire the dependent read of the scratch word is unordered too, and a stale NULL there makes mswi_ipi_clear return early without clearing a pending IPI, leaving the hart's msip latched: its first wfi in sbi_hsm_hart_wait returns immediately and it spins instead of sleeping, and a later HART_START IPI is indistinguishable from the stale one.

The walk is designed to tolerate an empty or partially populated list; it is not safe against a node whose contents are not yet visible. The all-devices walk in sbi_ipi_raw_clear is the only reader that runs concurrently with sbi_ipi_add_device; sbi_ipi_raw_send walks the list only after cold boot.

Verification

Proved: with the fences, every warm hart's sbi_ipi_raw_clear(true) satisfies its contract against the Sail RISC-V model under an RVWMO-faithful memory model, in both interleavings (empty list, node present). Without them the reader has no ordering on the node's fields and the contract is unprovable.