diff --git a/xen/arch/arm/vgic-v2.c b/xen/arch/arm/vgic-v2.c
index dc9f95b..5370020 100644
--- a/xen/arch/arm/vgic-v2.c
+++ b/xen/arch/arm/vgic-v2.c
@@ -258,9 +258,9 @@ static int vgic_v2_distr_mmio_read(struct vcpu *v, mmio_info_t *info,
         if ( rank == NULL ) goto read_as_zero;
 
         vgic_lock_rank(v, rank, flags);
-        ipriorityr = rank->ipriorityr[REG_RANK_INDEX(8,
-                                                     gicd_reg - GICD_IPRIORITYR,
-                                                     DABT_WORD)];
+        ipriorityr = ACCESS_ONCE(rank->ipriorityr[REG_RANK_INDEX(8,
+                                     gicd_reg - GICD_IPRIORITYR,
+                                     DABT_WORD)]);
         vgic_unlock_rank(v, rank, flags);
         *r = vgic_reg32_extract(ipriorityr, info);
 
@@ -499,7 +499,7 @@ static int vgic_v2_distr_mmio_write(struct vcpu *v, mmio_info_t *info,
 
     case VRANGE32(GICD_IPRIORITYR, GICD_IPRIORITYRN):
     {
-        uint32_t *ipriorityr;
+        uint32_t *ipriorityr, priority;
 
         if ( dabt.size != DABT_BYTE && dabt.size != DABT_WORD ) goto bad_width;
         rank = vgic_rank_offset(v, 8, gicd_reg - GICD_IPRIORITYR, DABT_WORD);
@@ -508,7 +508,10 @@ static int vgic_v2_distr_mmio_write(struct vcpu *v, mmio_info_t *info,
         ipriorityr = &rank->ipriorityr[REG_RANK_INDEX(8,
                                                       gicd_reg - GICD_IPRIORITYR,
                                                       DABT_WORD)];
-        vgic_reg32_update(ipriorityr, r, info);
+        priority = ACCESS_ONCE(*ipriorityr);
+        vgic_reg32_update(&priority, r, info);
+        ACCESS_ONCE(*ipriorityr) = priority;
+
         vgic_unlock_rank(v, rank, flags);
         return 1;
     }
diff --git a/xen/arch/arm/vgic-v3.c b/xen/arch/arm/vgic-v3.c
index d10757a..8abc069 100644
--- a/xen/arch/arm/vgic-v3.c
+++ b/xen/arch/arm/vgic-v3.c
@@ -521,8 +521,9 @@ static int __vgic_v3_distr_common_mmio_read(const char *name, struct vcpu *v,
         if ( rank == NULL ) goto read_as_zero;
 
         vgic_lock_rank(v, rank, flags);
-        ipriorityr = rank->ipriorityr[REG_RANK_INDEX(8, reg - GICD_IPRIORITYR,
-                                                     DABT_WORD)];
+        ipriorityr = ACCESS_ONCE(rank->ipriorityr[REG_RANK_INDEX(8,
+                                     reg - GICD_IPRIORITYR,
+                                     DABT_WORD)]);
         vgic_unlock_rank(v, rank, flags);
 
         *r = vgic_reg32_extract(ipriorityr, info);
@@ -630,7 +631,7 @@ static int __vgic_v3_distr_common_mmio_write(const char *name, struct vcpu *v,
 
     case VRANGE32(GICD_IPRIORITYR, GICD_IPRIORITYRN):
     {
-        uint32_t *ipriorityr;
+        uint32_t *ipriorityr, priority;
 
         if ( dabt.size != DABT_BYTE && dabt.size != DABT_WORD ) goto bad_width;
         rank = vgic_rank_offset(v, 8, reg - GICD_IPRIORITYR, DABT_WORD);
@@ -638,7 +639,9 @@ static int __vgic_v3_distr_common_mmio_write(const char *name, struct vcpu *v,
         vgic_lock_rank(v, rank, flags);
         ipriorityr = &rank->ipriorityr[REG_RANK_INDEX(8, reg - GICD_IPRIORITYR,
                                                       DABT_WORD)];
-        vgic_reg32_update(ipriorityr, r, info);
+        priority = ACCESS_ONCE(*ipriorityr);
+        vgic_reg32_update(&priority, r, info);
+        ACCESS_ONCE(*ipriorityr) = priority;
         vgic_unlock_rank(v, rank, flags);
         return 1;
     }
diff --git a/xen/arch/arm/vgic.c b/xen/arch/arm/vgic.c
index 83569b0..18fe420 100644
--- a/xen/arch/arm/vgic.c
+++ b/xen/arch/arm/vgic.c
@@ -227,14 +227,8 @@ struct vcpu *vgic_get_target_vcpu(struct vcpu *v, unsigned int virq)
 static int vgic_get_virq_priority(struct vcpu *v, unsigned int virq)
 {
     struct vgic_irq_rank *rank = vgic_rank_irq(v, virq);
-    unsigned long flags;
-    int priority;
-
-    vgic_lock_rank(v, rank, flags);
-    priority = rank->priority[virq & INTERRUPT_RANK_MASK];
-    vgic_unlock_rank(v, rank, flags);
 
-    return priority;
+    return ACCESS_ONCE(rank->priority[virq & INTERRUPT_RANK_MASK]);
 }
 
 bool vgic_migrate_irq(struct vcpu *old, struct vcpu *new, unsigned int irq)
