diff --git a/src/arch/arm/64/kernel/vspace.c b/src/arch/arm/64/kernel/vspace.c
index 5844e734129..26f0628640b 100644
--- a/src/arch/arm/64/kernel/vspace.c
+++ b/src/arch/arm/64/kernel/vspace.c
@@ -68,12 +68,11 @@ enum mair_s2_types {
     S2_NORMAL = S2_NORMAL_INNER_WBC_OUTER_WBC
 };
 
-/* Leif from Linaro said the big.LITTLE clusters should be treated as
- * inner shareable, and we believe so, although the Example B2-1 given in
- * ARM ARM DDI 0487B.b (ID092517) says otherwise.
- */
-
-#define SMP_SHARE   3
+/* ARM DDI 0487J.a, section D8.5.2 */
+/* Linux will only run on cores within the same Inner Shareable domain.
+ * They make an assumption that all the PEs are under a single IS domain,
+ * and we do the same here. */
+#define INNER_SHAREABLE     3
 
 struct lookupPTSlot_ret {
     pte_t *ptSlot;
@@ -184,13 +183,13 @@ BOOT_CODE void map_kernel_frame(paddr_t paddr, pptr_t vaddr, vm_rights_t vm_righ
     word_t uxn = 1; /* unprivileged execute never */
 #endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
     word_t attr_index;
-    word_t shareable;
+
+    /* ARM ARM RPYFVQ: device memory is treated as Outer Shareable, and the PTE attribute has no effect. */
+    word_t shareable = INNER_SHAREABLE;
     if (vm_attributes_get_armPageCacheable(attributes)) {
         attr_index = NORMAL;
-        shareable = SMP_TERNARY(SMP_SHARE, 0);
     } else {
         attr_index = DEVICE_nGnRnE;
-        shareable = 0;
     }
     armKSGlobalKernelPT[GET_KPT_INDEX(vaddr, KLVL_FRM_ARM_PT_LVL(3))] = pte_pte_4k_page_new(uxn, paddr,
                                                                                             0, /* global */
@@ -244,7 +243,7 @@ BOOT_CODE void map_kernel_window(void)
                                                                                                                         paddr,
                                                                                                                         0,                        /* global */
                                                                                                                         1,                        /* access flag */
-                                                                                                                        SMP_TERNARY(SMP_SHARE, 0),        /* Inner-shareable if SMP enabled, otherwise unshared */
+                                                                                                                        INNER_SHAREABLE,
                                                                                                                         0,                        /* VMKernelOnly */
                                                                                                                         NORMAL
                                                                                                                     );
@@ -303,7 +302,7 @@ static BOOT_CODE void map_it_frame_cap(cap_t vspace_cap, cap_t frame_cap, bool_t
                                                               1,                              /* not global */
 #endif
                                                               1,                              /* access flag */
-                                                              SMP_TERNARY(SMP_SHARE, 0),              /* Inner-shareable if SMP enabled, otherwise unshared */
+                                                              INNER_SHAREABLE,
                                                               APFromVMRights(VMReadWrite),
 #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
                                                               S2_NORMAL
@@ -665,15 +664,12 @@ static pte_t makeUserPagePTE(paddr_t paddr, vm_rights_t vm_rights, vm_attributes
     word_t attridx = cacheable ? NORMAL : DEVICE_nGnRnE;
 #endif
 
-    /* Inner-shareable if SMP enabled, otherwise unshared (ignored for devices) */
-    word_t shareable = cacheable ? SMP_TERNARY(SMP_SHARE, 0) : 0;
-
     if (page_size == ARMSmallPage) {
         return pte_pte_4k_page_new(nonexecutable, paddr, nG, 1 /* access flag */,
-                                   shareable, APFromVMRights(vm_rights), attridx);
+                                   INNER_SHAREABLE, APFromVMRights(vm_rights), attridx);
     } else {
         return pte_pte_page_new(nonexecutable, paddr, nG, 1 /* access flag */,
-                                shareable, APFromVMRights(vm_rights), attridx);
+                                INNER_SHAREABLE, APFromVMRights(vm_rights), attridx);
     }
 }
 
@@ -1908,7 +1904,7 @@ exception_t benchmark_arch_map_logBuffer(word_t frame_cptr)
                              ksUserLogBuffer,
                              0,                         /* global */
                              1,                         /* access flag */
-                             SMP_TERNARY(SMP_SHARE, 0), /* Inner-shareable if SMP enabled, otherwise unshared */
+                             INNER_SHAREABLE,
                              0,                         /* VMKernelOnly */
                              NORMAL_WT);
 
diff --git a/src/arch/arm/64/machine/capdl.c b/src/arch/arm/64/machine/capdl.c
index 8445adc667a..590c9e03ed5 100644
--- a/src/arch/arm/64/machine/capdl.c
+++ b/src/arch/arm/64/machine/capdl.c
@@ -21,7 +21,7 @@ word_t get_tcb_sp(tcb_t *tcb)
 
 static void obj_frame_print_attrs(vm_page_size_t frameSize, paddr_t frameBase);
 static void cap_frame_print_attrs_pt(pte_t *ptSlot);
-static void cap_frame_print_attrs_impl(word_t SH, word_t AP, word_t NXN);
+static void cap_frame_print_attrs_impl(word_t AttrIndx, word_t AP, word_t NXN);
 static void cap_frame_print_attrs_vptr(word_t vptr, cap_t vspace);
 
 static void _cap_frame_print_attrs_vptr(word_t vptr, vspace_root_t *vspaceRoot);
@@ -55,12 +55,12 @@ static void arm64_cap_pud_print_slots(void *pgdSlot_or_vspace, vptr_t vptr);
 /* use when only have access to pte of frames */
 static void cap_frame_print_attrs_pt(pte_t *ptSlot)
 {
-    cap_frame_print_attrs_impl(pte_pte_page_ptr_get_SH(ptSlot),
+    cap_frame_print_attrs_impl(pte_pte_page_ptr_get_AttrIndx(ptSlot),
                                pte_pte_page_ptr_get_AP(ptSlot),
                                pte_pte_page_ptr_get_UXN(ptSlot));
 }
 
-static void cap_frame_print_attrs_impl(word_t SH, word_t AP, word_t NXN)
+static void cap_frame_print_attrs_impl(word_t AttrIndx, word_t AP, word_t NXN)
 {
     printf("(");
 
@@ -96,8 +96,8 @@ static void cap_frame_print_attrs_impl(word_t SH, word_t AP, word_t NXN)
         printf("X");
     }
 
-    /* Only has effect if SMP enabled */
-    if (SH != SMP_TERNARY(SMP_SHARE, 0)) {
+    /* DEVICE_nGnRnE is the only attribute we use for uncached memory right now. */
+    if (AttrIndx == DEVICE_nGnRnE) {
         printf(", uncached");
     }