Index: sys/arm/include/cpu-v6.h
===================================================================
--- sys/arm/include/cpu-v6.h
+++ sys/arm/include/cpu-v6.h
@@ -345,12 +345,23 @@
 /* Broadcasting operations. */
 #if __ARM_ARCH >= 7 && defined SMP
 
+#ifdef CPU_CORTEXA8
+#define	ARM_HAVE_MP_EXTENSIONS	(cpuinfo.mp_ext != 0)
+#else
+#define	ARM_HAVE_MP_EXTENSIONS	1
+#endif
+
 static __inline void
 tlb_flush_all(void)
 {
 
 	dsb();
-	_CP15_TLBIALLIS();
+	if (ARM_HAVE_MP_EXTENSIONS)
+		_CP15_TLBIALL();
+#ifdef CPU_CORTEXA8
+	else
+		_CP15_TLBIALLIS();
+#endif
 	dsb();
 }
 
@@ -359,7 +370,12 @@
 {
 
 	dsb();
-	_CP15_TLBIASIDIS(CPU_ASID_KERNEL);
+	if (ARM_HAVE_MP_EXTENSIONS)
+		_CP15_TLBIASID(CPU_ASID_KERNEL);
+#ifdef CPU_CORTEXA8
+	else
+		_CP15_TLBIASIDIS(CPU_ASID_KERNEL);
+#endif
 	dsb();
 }
 
@@ -370,7 +386,12 @@
 	KASSERT((va & PAGE_MASK) == 0, ("%s: va %#x not aligned", __func__, va));
 
 	dsb();
-	_CP15_TLBIMVAAIS(va);
+	if (ARM_HAVE_MP_EXTENSIONS)
+		_CP15_TLBIMVA(va | CPU_ASID_KERNEL);
+#ifdef CPU_CORTEXA8
+	else
+		_CP15_TLBIMVAAIS(va);
+#endif
 	dsb();
 }
 
@@ -384,8 +405,16 @@
 	    size));
 
 	dsb();
-	for (; va < eva; va += PAGE_SIZE)
-		_CP15_TLBIMVAAIS(va);
+	if (ARM_HAVE_MP_EXTENSIONS) {
+		for (; va < eva; va += PAGE_SIZE)
+			_CP15_TLBIMVA(va | CPU_ASID_KERNEL);
+	}
+#ifdef CPU_CORTEXA8
+	else {
+		for (; va < eva; va += PAGE_SIZE)
+			_CP15_TLBIMVAAIS(va);
+	}
+#endif
 	dsb();
 }
 #else /* SMP */
@@ -409,19 +438,23 @@
 
 	dsb();
 	va &= ~cpuinfo.dcache_line_mask;
-	for ( ; va < eva; va += cpuinfo.dcache_line_size) {
 #if __ARM_ARCH >= 7 && defined SMP
-		_CP15_DCCMVAU(va);
-#else
-		_CP15_DCCMVAC(va);
-#endif
+	if (ARM_HAVE_MP_EXTENSIONS) {
+		for ( ; va < eva; va += cpuinfo.dcache_line_size)
+			_CP15_DCCMVAU(va);
+	} else
+#endif
+	{
+		for ( ; va < eva; va += cpuinfo.dcache_line_size)
+			_CP15_DCCMVAC(va);
 	}
 	dsb();
 #if __ARM_ARCH >= 7 && defined SMP
-	_CP15_ICIALLUIS();
-#else
-	_CP15_ICIALLU();
+	if (ARM_HAVE_MP_EXTENSIONS)
+		_CP15_ICIALLUIS();
+	else
 #endif
+		_CP15_ICIALLU();
 	dsb();
 	isb();
 }
@@ -431,10 +464,11 @@
 icache_inv_all(void)
 {
 #if __ARM_ARCH >= 7 && defined SMP
-	_CP15_ICIALLUIS();
-#else
-	_CP15_ICIALLU();
+	if (ARM_HAVE_MP_EXTENSIONS)
+		_CP15_ICIALLUIS();
+	else
 #endif
+		_CP15_ICIALLU();
 	dsb();
 	isb();
 }
@@ -444,10 +478,11 @@
 bpb_inv_all(void)
 {
 #if __ARM_ARCH >= 7 && defined SMP
-	_CP15_BPIALLIS();
-#else
-	_CP15_BPIALL();
+	if (ARM_HAVE_MP_EXTENSIONS)
+		_CP15_BPIALLIS();
+	else
 #endif
+		_CP15_BPIALL();
 	dsb();
 	isb();
 }
@@ -460,12 +495,15 @@
 
 	dsb();
 	va &= ~cpuinfo.dcache_line_mask;
-	for ( ; va < eva; va += cpuinfo.dcache_line_size) {
 #if __ARM_ARCH >= 7 && defined SMP
-		_CP15_DCCMVAU(va);
-#else
-		_CP15_DCCMVAC(va);
-#endif
+	if (ARM_HAVE_MP_EXTENSIONS) {
+		for ( ; va < eva; va += cpuinfo.dcache_line_size)
+			_CP15_DCCMVAU(va);
+	} else
+#endif
+	{
+		for ( ; va < eva; va += cpuinfo.dcache_line_size)
+			_CP15_DCCMVAC(va);
 	}
 	dsb();
 }