[PATCH] lib: sbi: Order the publication of IPI device nodes

[Nickolai Zeldovich]

From: Nickolai Zeldovich <nickolai.zeldovich at gmail.com>

sbi_ipi_add_device() links the new node into ipi_dev_node_list with
plain stores while warm harts already walk the list with plain loads
in sbi_ipi_raw_clear(true).  A reader can see the node pointer before
the node's fields and the device's per-hart data are visible.

Publish the node after smp_wmb() and pair it with smp_rmb() after each
node load in the all-devices walk.

Signed-off-by: Nickolai Zeldovich <nickolai.zeldovich at gmail.com>
Co-Authored-By: Claude Fable 5.1 <noreply at anthropic.com>
---
This bug was found in the process of formally verifying the correctness
of OpenSBI on top of the Sail RISC-V semantics using Lean.

Summary:

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.

lib/sbi/sbi_ipi.c | 25 +++++++++++++++++++++++-- 1 file changed, 23
insertions(+), 2 deletions(-)

FYI, the same change is also filed as GitHub pull request #430:
https://github.com/riscv-software-src/opensbi/pull/430

diff --git a/lib/sbi/sbi_ipi.c b/lib/sbi/sbi_ipi.c
index b04a5877..e933ccd7 100644
--- a/lib/sbi/sbi_ipi.c
+++ b/lib/sbi/sbi_ipi.c
@@ -314,6 +314,14 @@ void sbi_ipi_raw_clear(bool all_devices)
 
 	if (all_devices) {
 		sbi_list_for_each_entry(entry, &ipi_dev_node_list, head) {
+			/*
+			 * Pair with the smp_wmb() in sbi_ipi_add_device():
+			 * a warm hart may reach here while the cold hart is
+			 * still adding devices.  Order the load of the node
+			 * pointer before the loads of the node's contents
+			 * and of the per-hart data that ipi_clear() reads.
+			 */
+			smp_rmb();
 			if (entry->dev->ipi_clear)
 				entry->dev->ipi_clear();
 		}
@@ -349,9 +357,22 @@ void sbi_ipi_add_device(const struct sbi_ipi_device *dev)
 	entry = sbi_zalloc(sizeof(*entry));
 	if (!entry)
 		return;
-	SBI_INIT_LIST_HEAD(&entry->head);
 	entry->dev = dev;
-	sbi_list_add_tail(&entry->head, &ipi_dev_node_list);
+	entry->head.prev = ipi_dev_node_list.prev;
+	entry->head.next = &ipi_dev_node_list;
+
+	/*
+	 * Warm harts walk ipi_dev_node_list in sbi_ipi_raw_clear(true)
+	 * from wait_for_coldboot() onwards, concurrently with the cold
+	 * hart's cold-boot initialization.  Make the node's contents
+	 * (and the device's per-hart data set up by its cold_init)
+	 * visible before the node becomes reachable from the list head.
+	 * The reader pairs with this through the smp_rmb() in
+	 * sbi_ipi_raw_clear().
+	 */
+	smp_wmb();
+	ipi_dev_node_list.prev->next = &entry->head;
+	ipi_dev_node_list.prev = &entry->head;
 
 	if (!ipi_dev || ipi_dev->rating < dev->rating)
 		ipi_dev = dev;
-- 
2.55.0