[REQUIREMENTS][PATCH v2 1/6] reqs: clarify guest GICv3 virtual register model

[Mykola Kvach <mykola_kvach@xxxxxxxx>]

Clarify the guest GICv3 requirements by adding an Assumption of Use for Xen's
limited virtual GICv3 pending-state and active-state MMIO observation model.

Xen exposes a virtual GICv3 ABI rather than a complete emulation of the
physical GICv3 Distributor and Redistributor programmer's model. Virtual
interrupt lifecycle state is maintained through Xen virtual interrupt state and
through the virtual CPU interface acknowledge and completion path.

Do not add AoU coverage for DS, security-extension registers, legacy SGI MMIO,
WAKER or unimplemented ePPI/eSPI bits. Those cases follow architectural access
or capability rules rather than a Xen-specific guest compatibility assumption.

Keep exposed eSPI pending-state and active-state MMIO register groups in the
AoU, because Xen can expose and allow guest use of eSPIs while still providing
limited pending/active MMIO observation semantics for those INTIDs.

Signed-off-by: Mykola Kvach <mykola_kvach@xxxxxxxx>
---
Changes in v2:
- rephrase XenAoU~arm64_vm_compat_xen_virt_gicv3_reg_model~1 add details
  about Xen implementation.
---
 .../arm64/gicv3.rst                           | 37 +++++++++++++------
 1 file changed, 26 insertions(+), 11 deletions(-)

diff --git 
a/software_safety_reqs/domain_creation_and_runtime/domain_partially_emulated_resources/arm64/gicv3.rst
 
b/software_safety_reqs/domain_creation_and_runtime/domain_partially_emulated_resources/arm64/gicv3.rst
index 2ce30e5..e16576f 100644
--- 
a/software_safety_reqs/domain_creation_and_runtime/domain_partially_emulated_resources/arm64/gicv3.rst
+++ 
b/software_safety_reqs/domain_creation_and_runtime/domain_partially_emulated_resources/arm64/gicv3.rst
@@ -23,22 +23,37 @@ Rationale:
 Assumption of Use on a VM
 ^^^^^^^^^^^^^^^^^^^^^^^^^
 
-Domain shall not write to GICD_ISACTIVER<n> registers
------------------------------------------------------
+Guest compatibility with limited interrupt-state MMIO observation
+-----------------------------------------------------------------
 
-`XenAoU~arm64_vm_no_write_gicd_isactiver~1`
+`XenAoU~arm64_vm_compat_xen_virt_gicv3_reg_model~1`
 
 Description:
-Domains shall not write to GICD_ISACTIVER<n> registers.
+Guest software shall not rely on the GICv3 Distributor or Redistributor
+pending-state and active-state set/clear register aliases as an
+authoritative view of virtual interrupt state.
+
+This applies to GICD_ISPENDR<n>, GICD_ICPENDR<n>,
+GICD_ISACTIVER<n>, GICD_ICACTIVER<n>, their extended-SPI equivalents
+when exposed, and GICR_ISPENDR0, GICR_ICPENDR0,
+GICR_ISACTIVER0 and GICR_ICACTIVER0.
+
+For these registers:
+
+ - reads return zero regardless of Xen's internal pending or active state;
+ - set-pending writes are supported;
+ - clear-pending and clear-active writes are ignored;
+ - set-active writes are unsupported and result in a guest data abort.
+
+Guest software shall use the virtual CPU interface acknowledge and
+completion path for interrupt lifecycle handling.
 
 Rationale:
-Xen does not support the emulation of these registers, therefore the domain
-write accesses to GICD_ISACTIVER<n> registers will result in a fault injection.
-Also the domain write accesses to GICD_ICACTIVER<n> registers will be ignored.
-The more, the reading of an active status of the interrupts via said registers
-is not supported as well and Xen always exposes all bits in them as RAZ which
-might be an incorrect state of the GIC and confuse the domain's expectations.
-The domain should not rely on these registers.
+The virtual GICv3 implementation maintains interrupt state in Xen's
+internal pending queues and hardware List Registers, but does not
+reconstruct the above MMIO register state from those sources. Its
+readback and write behavior therefore differs from the Arm GICv3
+programmer's model.
 
 Domain shall not access ICC_SGI0R_EL1 and ICC_ASGI1R_EL1 registers
 ------------------------------------------------------------------
-- 
2.43.0