diff --git a/repos/base-sel4/src/core/include/cnode.h b/repos/base-sel4/src/core/include/cnode.h index 32ced53f2..27a4db2f4 100644 --- a/repos/base-sel4/src/core/include/cnode.h +++ b/repos/base-sel4/src/core/include/cnode.h @@ -109,6 +109,10 @@ class Genode::Cnode_base class Genode::Cnode : public Cnode_base, Noncopyable { + private: + + addr_t _phys = 0UL; + public: class Untyped_lookup_failed : Exception { }; @@ -135,7 +139,7 @@ class Genode::Cnode : public Cnode_base, Noncopyable : Cnode_base(dst_idx, size_log2) { - create(phys_alloc, parent_sel, dst_idx, size_log2); + _phys = create(phys_alloc, parent_sel, dst_idx, size_log2); } /** @@ -160,13 +164,35 @@ class Genode::Cnode : public Cnode_base, Noncopyable create(untyped_pool, parent_sel, dst_idx, size_log2); } - ~Cnode() + void destruct(Range_allocator &phys_alloc) { - /* convert CNode back to untyped memory */ - /* revert phys allocation */ - PDBG("not implemented"); + if (!_phys) { + error("invalid call to destruct Cnode"); + return; + } + + int ret = seL4_CNode_Delete(seL4_CapInitThreadCNode, + sel().value(), 32); + if (ret != seL4_NoError) + error(__PRETTY_FUNCTION__, ": seL4_CNode_Delete (", + Hex(sel().value()), ") returned ", ret); + + Untyped_memory::free_page(phys_alloc, _phys); + + _phys = ~0UL; + } + + ~Cnode() + { + if (_phys == ~0UL) + return; + + /* convert CNode back to untyped memory */ + + error(__FUNCTION__, " - not implemented phys=", Hex(_phys), + " sel=", Hex(sel().value())); } }; diff --git a/repos/base-sel4/src/core/include/page_table_registry.h b/repos/base-sel4/src/core/include/page_table_registry.h index 51c83f822..1645c9684 100644 --- a/repos/base-sel4/src/core/include/page_table_registry.h +++ b/repos/base-sel4/src/core/include/page_table_registry.h @@ -79,6 +79,8 @@ class Genode::Page_table_registry Page_table(addr_t addr) : addr(addr) { } + Entry *first() { return _entries.first(); } + Entry &lookup(addr_t addr) { for (Entry *e = _entries.first(); e; e = e->next()) { @@ -221,6 +223,12 @@ class Genode::Page_table_registry */ Page_table_registry(Allocator &md_alloc) { } + ~Page_table_registry() + { + if (_page_tables.first()) + error("still entries in page table registry in destruction"); + } + /** * Register page table * @@ -299,6 +307,22 @@ class Genode::Page_table_registry PDBG("no PT entry found for virtual address 0x%lx", addr); } } + + template + void apply_to_and_destruct_all(FN const &fn) + { + for (Page_table *pt; (pt = _page_tables.first());) { + + Page_table::Entry *entry = pt->first(); + for (; entry; entry = entry->next()) + fn(entry->sel); + + pt->flush_all(_page_table_entry_alloc); + + _page_tables.remove(pt); + destroy(_page_table_alloc, pt); + } + } }; #endif /* _CORE__INCLUDE__PAGE_TABLE_REGISTRY_H_ */ diff --git a/repos/base-sel4/src/core/include/untyped_memory.h b/repos/base-sel4/src/core/include/untyped_memory.h index 43d44063b..eda1af3ff 100644 --- a/repos/base-sel4/src/core/include/untyped_memory.h +++ b/repos/base-sel4/src/core/include/untyped_memory.h @@ -53,6 +53,12 @@ struct Genode::Untyped_memory } + static inline void free_page(Range_allocator &phys_alloc, Genode::addr_t addr) + { + phys_alloc.free(reinterpret_cast(addr)); + } + + /** * Local utility solely used by 'untyped_sel' and 'frame_sel' */ diff --git a/repos/base-sel4/src/core/include/vm_space.h b/repos/base-sel4/src/core/include/vm_space.h index ff6cbeae1..5d3484551 100644 --- a/repos/base-sel4/src/core/include/vm_space.h +++ b/repos/base-sel4/src/core/include/vm_space.h @@ -113,8 +113,10 @@ class Genode::Vm_space LEAF_CNODE_SIZE_LOG2, phys_alloc); } - void destruct(Cap_sel_alloc &cap_sel_alloc) + void destruct(Cap_sel_alloc &cap_sel_alloc, + Range_allocator &phys_alloc) { + _cnode->destruct(phys_alloc); cap_sel_alloc.free(_cnode->sel()); } @@ -306,16 +308,31 @@ class Genode::Vm_space _vm_pad_cnode.copy(cspace, _vm_3rd_cnode.sel(), Cnode_index(0)); /* insert 2nd-level VM-pad CNode into 1st-level CNode */ - _top_level_cnode.copy(cspace, _vm_pad_cnode.sel(), Cnode_index(id)); + _top_level_cnode.copy(cspace, _vm_pad_cnode.sel(), Cnode_index(_id)); } ~Vm_space() { - _cap_sel_alloc.free(_vm_pad_cnode.sel()); - _cap_sel_alloc.free(_vm_3rd_cnode.sel()); + /* delete copy of the mapping's page-frame selectors */ + _page_table_registry.apply_to_and_destruct_all([&] (unsigned idx) { + _leaf_cnode(idx).remove(_leaf_cnode_entry(idx)); + + _sel_alloc.free(idx); + }); + + for (unsigned i = 0; i < NUM_LEAF_CNODES; i++) { + _vm_3rd_cnode.remove(Cnode_index(i)); + _vm_cnodes[i].destruct(_cap_sel_alloc, _phys_alloc); + } + _vm_pad_cnode.remove(Cnode_index(0)); + _top_level_cnode.remove(Cnode_index(_id)); + + _vm_3rd_cnode.destruct(_phys_alloc); + _vm_pad_cnode.destruct(_phys_alloc); + + _cap_sel_alloc.free(_vm_3rd_cnode.sel()); + _cap_sel_alloc.free(_vm_pad_cnode.sel()); - for (unsigned i = 0; i < NUM_LEAF_CNODES; i++) - _vm_cnodes[i].destruct(_cap_sel_alloc); } void map(addr_t from_phys, addr_t to_virt, size_t num_pages, diff --git a/repos/base-sel4/src/core/platform_pd.cc b/repos/base-sel4/src/core/platform_pd.cc index 87e1d5926..e73d8535e 100644 --- a/repos/base-sel4/src/core/platform_pd.cc +++ b/repos/base-sel4/src/core/platform_pd.cc @@ -194,6 +194,15 @@ Platform_pd::Platform_pd(Allocator * md_alloc, char const *label, Platform_pd::~Platform_pd() { + for (unsigned i = 0; i < sizeof(_cspace_cnode_2nd) / + sizeof(_cspace_cnode_2nd[0]); i++) { + _cspace_cnode_2nd[i]->destruct(*platform()->ram_alloc()); + platform_specific()->core_sel_alloc().free(_cspace_cnode_2nd[i]->sel()); + } + + _cspace_cnode_1st.destruct(*platform()->ram_alloc()); + platform_specific()->core_sel_alloc().free(_cspace_cnode_1st.sel()); + /* invalidate weak pointers to this object */ Address_space::lock_for_destruction(); }