diff --git a/repos/base-sel4/src/core/include/map_local.h b/repos/base-sel4/src/core/include/map_local.h
index 5c328f89b..21a88af88 100644
--- a/repos/base-sel4/src/core/include/map_local.h
+++ b/repos/base-sel4/src/core/include/map_local.h
@@ -53,11 +53,12 @@ namespace Genode {
 	/**
 	 * Flush memory mappings from core-local virtual address range
 	 */
-	inline bool unmap_local(addr_t virt_addr, size_t num_pages,
-	                        Platform * platform = nullptr)
+	inline bool unmap_local(addr_t const virt_addr, size_t const num_pages,
+	                        Platform * platform = nullptr,
+	                        bool const invalidate = false)
 	{
 		platform = platform ? platform : platform_specific();
-		return platform->core_vm_space().unmap(virt_addr, num_pages);
+		return platform->core_vm_space().unmap(virt_addr, num_pages, invalidate);
 	}
 }
 
diff --git a/repos/base-sel4/src/core/include/vm_space.h b/repos/base-sel4/src/core/include/vm_space.h
index cd4657fb0..ba62da385 100644
--- a/repos/base-sel4/src/core/include/vm_space.h
+++ b/repos/base-sel4/src/core/include/vm_space.h
@@ -245,6 +245,8 @@ class Genode::Vm_space
 		               Cache_attribute const cacheability, bool const write,
 		               bool const writable);
 		long _unmap_page(Genode::Cap_sel const &idx);
+		long _invalidate_page(Genode::Cap_sel const &, seL4_Word const,
+		                      seL4_Word const);
 
 		class Alloc_page_table_failed : Exception { };
 
@@ -392,7 +394,8 @@ class Genode::Vm_space
 			}
 		}
 
-		bool unmap(addr_t virt, size_t num_pages)
+		bool unmap(addr_t const virt, size_t const num_pages,
+		           bool const invalidate = false)
 		{
 			bool unmap_success = true;
 
@@ -403,6 +406,14 @@ class Genode::Vm_space
 
 				_page_table_registry.flush_page(virt + offset, [&] (Cap_sel const &idx, addr_t) {
 
+					if (invalidate) {
+						long result = _invalidate_page(idx, virt + offset,
+						                               virt + offset + 4096);
+						if (result != seL4_NoError)
+							error("invalidating ", Hex(virt + offset),
+							      " failed, idx=", idx, " result=", result);
+					}
+
 					long result = _unmap_page(idx);
 					if (result != seL4_NoError) {
 						error("unmap ", Hex(virt + offset), " failed, idx=",
diff --git a/repos/base-sel4/src/core/ram_dataspace_support.cc b/repos/base-sel4/src/core/ram_dataspace_support.cc
index 5277e8a27..448319e0c 100644
--- a/repos/base-sel4/src/core/ram_dataspace_support.cc
+++ b/repos/base-sel4/src/core/ram_dataspace_support.cc
@@ -67,7 +67,7 @@ void Ram_dataspace_factory::_clear_ds (Dataspace_component *ds)
 			*dst++ = 0;
 
 		/* unmap cleared page from core */
-		unmap_local(virt_addr, ONE_PAGE);
+		unmap_local(virt_addr, ONE_PAGE, nullptr, ds->cacheability() != CACHED);
 	}
 
 	/* free core's virtual address space */
diff --git a/repos/base-sel4/src/core/spec/arm/vm_space.cc b/repos/base-sel4/src/core/spec/arm/vm_space.cc
index 22b213b56..2cda2c2fd 100644
--- a/repos/base-sel4/src/core/spec/arm/vm_space.cc
+++ b/repos/base-sel4/src/core/spec/arm/vm_space.cc
@@ -47,6 +47,21 @@ long Genode::Vm_space::_unmap_page(Genode::Cap_sel const &idx)
 	return seL4_ARM_Page_Unmap(service);
 }
 
+long Genode::Vm_space::_invalidate_page(Genode::Cap_sel const &idx,
+                                        seL4_Word const start,
+                                        seL4_Word const end)
+{
+	seL4_ARM_Page const service = _idx_to_sel(idx.value());
+	long error = seL4_ARM_Page_CleanInvalidate_Data(service, 0, end - start);
+
+	if (error == seL4_NoError) {
+		seL4_ARM_PageDirectory const pd = _pd_sel.value();
+		error = seL4_ARM_PageDirectory_CleanInvalidate_Data(pd, start, end);
+	}
+
+	return error;
+}
+
 void Genode::Vm_space::unsynchronized_alloc_page_tables(addr_t const start,
                                                         addr_t const size)
 {
diff --git a/repos/base-sel4/src/core/spec/x86/vm_space.cc b/repos/base-sel4/src/core/spec/x86/vm_space.cc
index 067e08381..82b47b87a 100644
--- a/repos/base-sel4/src/core/spec/x86/vm_space.cc
+++ b/repos/base-sel4/src/core/spec/x86/vm_space.cc
@@ -39,3 +39,9 @@ long Genode::Vm_space::_unmap_page(Genode::Cap_sel const &idx)
 	seL4_X86_Page const service = _idx_to_sel(idx.value());
 	return seL4_X86_Page_Unmap(service);
 }
+
+long Genode::Vm_space::_invalidate_page(Genode::Cap_sel const &,
+                                        seL4_Word const, seL4_Word const)
+{
+	return seL4_NoError;
+}