diff --git a/xen/arch/arm/include/asm/arm32/page.h b/xen/arch/arm/include/asm/arm32/page.h
index 715a9e4fef..6d1ff0636c 100644
--- a/xen/arch/arm/include/asm/arm32/page.h
+++ b/xen/arch/arm/include/asm/arm32/page.h
@@ -3,22 +3,6 @@
 
 #ifndef __ASSEMBLY__
 
-/* Write a pagetable entry.
- *
- * If the table entry is changing a text mapping, it is responsibility
- * of the caller to issue an ISB after write_pte.
- */
-static inline void write_pte(lpae_t *p, lpae_t pte)
-{
-    asm volatile (
-        /* Ensure any writes have completed with the old mappings. */
-        "dsb;"
-        /* Safely write the entry (STRD is atomic on CPUs that support LPAE) */
-        "strd %0, %H0, [%1];"
-        "dsb;"
-        : : "r" (pte.bits), "r" (p) : "memory");
-}
-
 /* Inline ASM to invalidate dcache on register R (may be an inline asm operand) */
 #define __invalidate_dcache_one(R) STORE_CP32(R, DCIMVAC)
 
diff --git a/xen/arch/arm/include/asm/arm64/page.h b/xen/arch/arm/include/asm/arm64/page.h
index 0cba266373..4f58c0382a 100644
--- a/xen/arch/arm/include/asm/arm64/page.h
+++ b/xen/arch/arm/include/asm/arm64/page.h
@@ -5,17 +5,6 @@
 
 #include <asm/alternative.h>
 
-/* Write a pagetable entry */
-static inline void write_pte(lpae_t *p, lpae_t pte)
-{
-    asm volatile (
-        /* Ensure any writes have completed with the old mappings. */
-        "dsb sy;"
-        "str %0, [%1];"         /* Write the entry */
-        "dsb sy;"
-        : : "r" (pte.bits), "r" (p) : "memory");
-}
-
 /* Inline ASM to invalidate dcache on register R (may be an inline asm operand) */
 #define __invalidate_dcache_one(R) "dc ivac, %" #R ";"
 
diff --git a/xen/arch/arm/include/asm/page.h b/xen/arch/arm/include/asm/page.h
index e7cd62190c..ea96983ab9 100644
--- a/xen/arch/arm/include/asm/page.h
+++ b/xen/arch/arm/include/asm/page.h
@@ -126,6 +126,7 @@
 #include <xen/errno.h>
 #include <xen/types.h>
 #include <xen/lib.h>
+#include <asm/atomic.h>
 #include <asm/system.h>
 
 #if defined(CONFIG_ARM_32)
@@ -237,6 +238,22 @@ static inline int clean_and_invalidate_dcache_va_range
             : : "r" (_p), "m" (*_p));                                   \
 } while (0)
 
+/*
+ * Write a pagetable entry.
+ *
+ * It is the responsibility of the caller to issue an ISB (if a new entry)
+ * or a TLB flush (if modified or removed) after write_pte().
+ */
+static inline void write_pte(lpae_t *p, lpae_t pte)
+{
+    /* Ensure any writes have completed with the old mappings. */
+    dsb(sy);
+    /* Safely write the entry. This should always be an atomic write. */
+    write_atomic(p, pte);
+    dsb(sy);
+}
+
+
 /* Flush the dcache for an entire page. */
 void flush_page_to_ram(unsigned long mfn, bool sync_icache);