sel4: convert frame pages back to untyped memory

to implement _revoke_ram_ds and to fix _unmap_local

Issue #2044

repos/base-sel4/src/core/include/cnode.h

@@ -71,7 +71,10 @@ class Genode::Cnode_base
 		 */
 		void remove(Index idx)
 		{
-			seL4_CNode_Delete(sel().value(), idx.value(), size_log2());
+			int ret = seL4_CNode_Delete(sel().value(), idx.value(), size_log2());
+			if (ret != seL4_NoError)
+				error(__PRETTY_FUNCTION__, ": seL4_CNode_Delete (",
+				      Hex(idx.value()), ") returned ", ret);
 		}
 
 		/**

repos/base-sel4/src/core/include/untyped_memory.h

@@ -39,7 +39,7 @@ struct Genode::Untyped_memory
 			                         get_page_size_log2());
 
 		if (alloc_ret.error()) {
-			PERR("%s: allocation of untyped memory failed", __FUNCTION__);
+			error(__PRETTY_FUNCTION__, ": allocation of untyped memory failed");
 			throw Phys_alloc_failed();
 		}
 
@@ -110,13 +110,47 @@ struct Genode::Untyped_memory
 			                                    node_offset,
 			                                    num_objects);
 
-			if (ret != 0) {
-				PERR("%s: seL4_Untyped_RetypeAtOffset (IA32_4K) returned %d",
-				     __FUNCTION__, ret);
+			if (ret != seL4_NoError) {
+				error(__FUNCTION__, ": seL4_Untyped_RetypeAtOffset (IA32_4K) "
+				      "returned ", ret);
 				return;
 			}
 		}
 	}
+
+
+	/**
+	 * Free up page frames and turn it so into untyped memory
+	 */
+	static inline void convert_to_untyped_frames(addr_t const phys_addr,
+	                                             addr_t const phys_size)
+	{
+		seL4_Untyped const service = Core_cspace::PHYS_CNODE_SEL;
+		int const space_size = Core_cspace::NUM_PHYS_SEL_LOG2;
+
+		for (addr_t phys = phys_addr; phys < phys_addr + phys_size;
+		     phys += get_page_size()) {
+
+			int const index = phys >> get_page_size_log2();
+			/**
+			 * Without the revoke, one gets sporadically
+			 *  Untyped Retype: Insufficient memory ( xx bytes needed, x bytes
+			 *                                        available)
+			 * for the phys_addr when it gets reused.
+			 */
+			int ret = seL4_CNode_Revoke(service, index, space_size);
+			if (ret != seL4_NoError)
+				error(__FUNCTION__, ": seL4_CNode_Revoke returned ", ret);
+
+			/**
+			 * Without the delete, one gets:
+			 *  Untyped Retype: Slot #xxxx in destination window non-empty
+			 */
+			ret = seL4_CNode_Delete(service, index, space_size);
+			if (ret != seL4_NoError)
+				error(__FUNCTION__, ": seL4_CNode_Delete returned ", ret);
+		}
+	}
 };
 
 #endif /* _CORE__INCLUDE__UNTYPED_MEMORY_H_ */

repos/base-sel4/src/core/platform.cc

@@ -75,7 +75,12 @@ bool Mapped_mem_allocator::_map_local(addr_t virt_addr, addr_t phys_addr,
 bool Mapped_mem_allocator::_unmap_local(addr_t virt_addr, addr_t phys_addr,
                                         unsigned size)
 {
-	return unmap_local(virt_addr, size / get_page_size());
+	if (!unmap_local(virt_addr, size / get_page_size()))
+		return false;
+
+	Untyped_memory::convert_to_untyped_frames(phys_addr, size);
+
+	return true;
 }
 
 

repos/base-sel4/src/core/ram_session_support.cc

@@ -32,7 +32,7 @@ void Ram_session_component::_export_ram_ds(Dataspace_component *ds)
 
 void Ram_session_component::_revoke_ram_ds(Dataspace_component *ds)
 {
-	PDBG("not implemented");
+	Untyped_memory::convert_to_untyped_frames(ds->phys_addr(), ds->size());
 }