sel4: unmapping of virtual memory

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

@@ -71,6 +71,14 @@ class Genode::Cnode_base
 
 		void copy(Cnode_base const &from, unsigned idx) { copy(from, idx, idx); }
 
+		/**
+		 * Delete selector from CNode
+		 */
+		void remove(unsigned idx)
+		{
+			seL4_CNode_Delete(sel(), idx, size_log2());
+		}
+
 		/**
 		 * Move selector from another CNode
 		 */

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

@@ -35,20 +35,18 @@ namespace Genode {
 	 */
 	inline bool map_local(addr_t from_phys, addr_t to_virt, size_t num_pages)
 	{
-		PDBG("map_local from_phys=0x%lx, to_virt=0x%lx, num_pages=%zd",
-		     from_phys, to_virt, num_pages);
-
 		platform_specific()->core_vm_space().map(from_phys, to_virt, num_pages);
-
 		return true;
 	}
 
 
+	/**
+	 * Flush memory mappings from core-local virtual address range
+	 */
 	inline bool unmap_local(addr_t virt_addr, size_t num_pages)
 	{
-		PDBG("not implemented");
-
-		return false;
+		platform_specific()->core_vm_space().unmap(virt_addr, num_pages);
+		return true;
 	}
 }
 

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

@@ -71,8 +71,19 @@ class Genode::Page_table_registry
 
 			public:
 
+				class Lookup_failed : Exception { };
+
 				Page_table(addr_t addr) : addr(addr) { }
 
+				Entry &lookup(addr_t addr)
+				{
+					for (Entry *e = _entries.first(); e; e = e->next()) {
+						if (_page_frame_base(e->addr) == _page_frame_base(addr))
+							return *e;
+					}
+					throw Lookup_failed();
+				}
+
 				void insert_entry(Allocator &entry_slab, addr_t addr, unsigned sel)
 				{
 					if (_entry_exists(addr)) {
@@ -82,6 +93,17 @@ class Genode::Page_table_registry
 
 					_entries.insert(new (entry_slab) Entry(addr, sel));
 				}
+
+				void remove_entry(Allocator &entry_slab, addr_t addr)
+				{
+					try {
+						Entry &entry = lookup(addr);
+						_entries.remove(&entry);
+						destroy(entry_slab, &entry);
+					} catch (Lookup_failed) {
+						PWRN("trying to remove non-existing page frame for 0x%lx", addr);
+					}
+				}
 		};
 
 		class Slab_block : public Genode::Slab_block { long _data[4*1024]; };
@@ -172,6 +194,40 @@ class Genode::Page_table_registry
 		{
 			_lookup(addr).insert_entry(_page_table_entry_slab, addr, sel);
 		}
+
+		/**
+		 * Discard the information about the given virtual address
+		 */
+		void forget_page_table_entry(addr_t addr)
+		{
+			try {
+				Page_table &page_table = _lookup(addr);
+				page_table.remove_entry(_page_table_entry_slab, addr);
+			} catch (...) {
+				PDBG("no PT entry found for virtual address 0x%lx", addr);
+			}
+		}
+
+		/**
+		 * Apply functor 'fn' to selector of specified virtual address
+		 *
+		 * \param addr  virtual address
+		 *
+		 * The functor is called with the selector of the page table entry
+		 * (the copy of the phys frame selector) as argument.
+		 */
+		template <typename FN>
+		void apply(addr_t addr, FN const &fn)
+		{
+			try {
+				Page_table        &page_table = _lookup(addr);
+				Page_table::Entry &entry      = page_table.lookup(addr);
+
+				fn(entry.sel);
+			} catch (...) {
+				PDBG("no PT entry found for virtual address 0x%lx", addr);
+			}
+		}
 };
 
 #endif /* _CORE__INCLUDE__PAGE_TABLE_REGISTRY_H_ */

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

@@ -99,8 +99,6 @@ struct Genode::Untyped_memory
 		int          const node_offset = phys_addr >> get_page_size_log2();
 		int          const num_objects = num_pages;
 
-		PDBG("create frame idx %x", node_offset);
-
 		int const ret = seL4_Untyped_RetypeAtOffset(service,
 		                                            type,
 		                                            offset,

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

@@ -96,6 +96,17 @@ class Genode::Vm_space
 			}
 		}
 
+		void _unmap_page(addr_t virt)
+		{
+			/* delete copy of the mapping's page-frame selector */
+			_page_table_registry.apply(virt, [&] (unsigned idx) {
+				_vm_cnode.remove(idx);
+			});
+
+			/* release meta data about the mapping */
+			_page_table_registry.forget_page_table_entry(virt);
+		}
+
 		void _map_page_table(unsigned pt_sel, addr_t to_virt)
 		{
 			seL4_IA32_PageTable     const service = pt_sel;
@@ -210,6 +221,14 @@ class Genode::Vm_space
 				_map_page(from_phys + offset, to_virt + offset);
 			}
 		}
+
+		void unmap(addr_t virt, size_t num_pages)
+		{
+			for (size_t i = 0; i < num_pages; i++) {
+				off_t const offset = i << get_page_size_log2();
+				_unmap_page(virt + offset);
+			}
+		}
 };
 
 #endif /* _CORE__INCLUDE__VM_SPACE_H_ */