Using the GICv2, software can change the CPU interfaces targeted by an interrupt (more precisely, an SPI) by writing to the corresponding GICD_ITARGETSR. The GICv2 specification states, in the paragraph "The effect of changes to an GICD_ITARGETSR" (page 4-108 in ARM IHI 0048B.b), that "[t]here is a small but finite time required for any change to take effect".
I am concerned by this sentence. After a write to GICD_ITARGETSR that removes a CPU from the targets, what does software need to do to wait until it is certain that said CPU will not acknowledge this SPI any more? (The specification is unclear to me; I cannot even answer this question in the simple case where the CPU making the write is the same as the one being removed from the targets.)