diff --git a/repos/base-tukija/src/core/include/platform.h b/repos/base-tukija/src/core/include/platform.h
index 7674a6ec68..9a0499a1d6 100644
--- a/repos/base-tukija/src/core/include/platform.h
+++ b/repos/base-tukija/src/core/include/platform.h
@@ -19,6 +19,7 @@
 #include <platform_generic.h>
 #include <core_mem_alloc.h>
 #include <address_space.h>
+#include <tukija/syscall-generic.h>
 
 namespace Core { class Platform; }
 
@@ -40,6 +41,8 @@ class Core::Platform : public Platform_generic
 		unsigned           _core_pd_sel     { 0 };  /* cap selector of root PD */
 		addr_t             _core_phys_start { 0 };
 
+		Tukija::Tip *_tip{nullptr};
+
 		/**
 		 * Virtual address range usable by non-core processes
 		 */
@@ -52,15 +55,23 @@ class Core::Platform : public Platform_generic
 		/* map of virtual cpu ids in Genode to kernel cpu ids */
 		uint16_t map_cpu_ids[MAX_SUPPORTED_CPUS];
 
-		addr_t _map_pages(addr_t phys_page, addr_t pages,
-		                  bool guard_page = false);
+
+		addr_t
+		_map_pages(addr_t phys_page, addr_t pages,
+				   bool guard_page = false);
 
 		size_t _max_caps = 0;
+		
+		/* space for mapping topology model */
+		alignas(4096) unsigned char topo_pages[8 * Tukija::PAGE_SIZE_BYTE];
 
 		void _init_rom_modules();
 
 		addr_t _rom_module_phys(addr_t virt);
 
+		Platform(const Platform &);
+		Platform& operator=(const Platform &);
+
 	public:
 
 		/**
diff --git a/repos/base-tukija/src/core/platform.cc b/repos/base-tukija/src/core/platform.cc
index 826ffec5c8..6e9ffb85fa 100644
--- a/repos/base-tukija/src/core/platform.cc
+++ b/repos/base-tukija/src/core/platform.cc
@@ -334,12 +334,10 @@ Core::Platform::Platform()
 	                       Mem_crd(BDA_VIRT, 0, Rights(true, false, false)),
 	                       _core_pd_sel);
 
-
 	/*
 	 * Now that we can access the I/O ports for comport 0, printf works...
 	 */
 
-
 	/*
 	 * remap main utcb to default utcb address
 	 * we do this that early, because Core_mem_allocator uses
@@ -349,6 +347,11 @@ Core::Platform::Platform()
 	              (addr_t)main_thread_utcb(), 1, Rights(true, true, false))) {
 		error("could not remap utcb of main thread");
 	}
+	
+	/*
+	 * Map Topology Information Pages (needed for correct mapping of CPU Ids)
+	 */
+
 
 	/*
 	 * Mark successful boot of hypervisor for automatic tests. This must be
@@ -358,10 +361,21 @@ Core::Platform::Platform()
 	log("\nHypervisor ", String<sizeof(hip.signature)+1>((char const *)&hip.signature),
 	    " (API v", hip.api_version, ")");
 
+	log("HIP resides at ", static_cast<const void *>(&hip));
+	log("TIP resides at ", reinterpret_cast<void *>(hip.topo_model), "(PA: ", hip.topo_phys ,")");
+
+	_tip = (Tip*)(hip.topo_model);
+	log("TIP has length ", _tip->length);
+	log("TIP reports following topology:");
+	log("Size of CPUset structure ", sizeof(Tukija::Cpuset));
+	_tip->for_each([&](Tukija::Tip::Domain &dom) {
+		log(dom);
+	});
+
 	/* init genode cpu ids based on kernel cpu ids (used for syscalls) */
 	warn_reorder = !hip.remap_cpu_ids(map_cpu_ids,
-	                                  sizeof(map_cpu_ids) / sizeof(map_cpu_ids[0]),
-	                                  (unsigned)boot_cpu());
+									  sizeof(map_cpu_ids) / sizeof(map_cpu_ids[0]),
+									  (unsigned)boot_cpu());
 
 	/* configure virtual address spaces */
 #ifdef __x86_64__
@@ -372,6 +386,7 @@ Core::Platform::Platform()
 
 	/* set up page fault handler for core - for debugging */
 	addr_t const ec_core_exc_sel = init_core_page_fault_handler(core_pd_sel());
+	
 
 	/* initialize core allocators */
 	size_t const num_mem_desc = (hip.hip_length - hip.mem_desc_offset)
@@ -412,6 +427,9 @@ Core::Platform::Platform()
 	region_alloc().remove_range((addr_t)__main_thread_utcb - get_page_size(),
 	                            get_page_size() * 4);
 
+	/* exclude TIP */
+	region_alloc().remove_range((addr_t)_tip, get_page_size() * 32);
+
 	/* sanity checks */
 	addr_t check [] = {
 		reinterpret_cast<addr_t>(__main_thread_utcb), CORE_PAGER_UTCB_ADDR,