# K1456–K1460 controlled MSI-X prototype contract

The caller must validate a device's MSI-X capability, table BAR and offset,
table size, Pending Bit Array location, and the interrupt controller's
message doorbell resource before touching a table entry. A vector is claimed
masked. The message address and data must lie inside the validated controller
resource and represent an owned interrupt ID. The caller writes address and
data while masked, publishes with an ordered write to vector control, and
reads back the entry. A failed validation leaves prior vector ownership and
hardware table bytes unchanged.

Before release, the vector must be masked, device generation disabled,
pending state drained or explicitly retained, and the old table entry and
capability control restored. Distinct vector indices have distinct owners.
The bounded local model tests masked publication, invalid messages, duplicate
vectors, and release refusal while armed. It does not prove physical MSI-X
delivery. K1460 requires a disposable real PCI device, a validated GICv2m or ITS
doorbell route, and an observed guest interrupt before development guest
acceptance can be recorded.