diff --git a/hal/aarch64/pmap.c b/hal/aarch64/pmap.c
index e7044526c..298dd1b15 100644
--- a/hal/aarch64/pmap.c
+++ b/hal/aarch64/pmap.c
@@ -265,7 +265,7 @@ static void _pmap_cacheOpAfterChange(descr_t newEntry, ptr_t vaddr, unsigned int
 
 
 /* Function creates empty page table */
-int pmap_create(pmap_t *pmap, pmap_t *kpmap, page_t *p, void *vaddr)
+int pmap_create(pmap_t *pmap, pmap_t *kpmap, page_t *p, const syspage_prog_t *prog, void *vaddr)
 {
 	pmap->ttl1 = vaddr;
 	pmap->addr = p->addr;
diff --git a/hal/armv7a/pmap.c b/hal/armv7a/pmap.c
index 35b59680d..650f53886 100644
--- a/hal/armv7a/pmap.c
+++ b/hal/armv7a/pmap.c
@@ -175,7 +175,7 @@ static void _pmap_asidDealloc(pmap_t *pmap)
 
 
 /* Function creates empty page table */
-int pmap_create(pmap_t *pmap, pmap_t *kpmap, page_t *p, void *vaddr)
+int pmap_create(pmap_t *pmap, pmap_t *kpmap, page_t *p, const syspage_prog_t *prog, void *vaddr)
 {
 	pmap->pdir = vaddr;
 	pmap->addr = p->addr;
diff --git a/hal/armv7m/arch/pmap.h b/hal/armv7m/arch/pmap.h
index b88db7ff7..c336ab8aa 100644
--- a/hal/armv7m/arch/pmap.h
+++ b/hal/armv7m/arch/pmap.h
@@ -17,6 +17,7 @@
 #define _PH_HAL_PMAP_ARMV7M_H_
 
 #include "hal/types.h"
+#include "syspage.h"
 
 /* Architecture dependent page attributes - used for mapping */
 #define PGHD_PRESENT    0x01
@@ -55,7 +56,7 @@ typedef struct _page_t {
 typedef struct _pmap_t {
 	void *start;
 	void *end;
-	u32 regions;
+	const hal_syspage_prog_t *hal;
 } pmap_t;
 
 #endif
diff --git a/hal/armv7m/pmap.c b/hal/armv7m/pmap.c
index 2529fa66c..7e53857b4 100644
--- a/hal/armv7m/pmap.c
+++ b/hal/armv7m/pmap.c
@@ -17,9 +17,14 @@
 #include "config.h"
 #include "syspage.h"
 #include "halsyspage.h"
+#include "lib/lib.h"
 #include <arch/cpu.h>
 #include <arch/spinlock.h>
 
+
+#define MPU_BASE ((volatile u32 *)0xe000ed90)
+
+
 /* clang-format off */
 enum { mpu_type, mpu_ctrl, mpu_rnr, mpu_rbar, mpu_rasr, mpu_rbar_a1, mpu_rasr_a1, mpu_rbar_a2, mpu_rasr_a2,
 	mpu_rbar_a3, mpu_rasr_a3 };
@@ -35,13 +40,19 @@ static struct {
 	volatile u32 *mpu;
 	unsigned int kernelCodeRegion;
 	spinlock_t lock;
+	int last_mpu_count;
 } pmap_common;
 
 
 /* Function creates empty page table */
-int pmap_create(pmap_t *pmap, pmap_t *kpmap, page_t *p, void *vaddr)
+int pmap_create(pmap_t *pmap, pmap_t *kpmap, page_t *p, const syspage_prog_t *prog, void *vaddr)
 {
-	pmap->regions = pmap_common.kernelCodeRegion;
+	if (prog != NULL) {
+		pmap->hal = &prog->hal;
+	}
+	else {
+		pmap->hal = NULL;
+	}
 	return 0;
 }
 
@@ -52,55 +63,40 @@ addr_t pmap_destroy(pmap_t *pmap, int *i)
 }
 
 
-static unsigned int pmap_map2region(unsigned int map)
+void pmap_switch(pmap_t *pmap)
 {
-	int i;
-	unsigned int mask = 0;
-
-	for (i = 0; i < sizeof(syspage->hs.mpu.map) / sizeof(*syspage->hs.mpu.map); ++i) {
-		if (map == syspage->hs.mpu.map[i]) {
-			mask |= (1 << i);
-		}
-	}
-
-	return mask;
-}
-
+	static const volatile u32 *RBAR_ADDR = MPU_BASE + mpu_rbar;
+	unsigned int allocCnt;
+	spinlock_ctx_t sc;
+	unsigned int i;
+	const u32 *tableCurrent;
 
-int pmap_addMap(pmap_t *pmap, unsigned int map)
-{
-	unsigned int rmask = pmap_map2region(map);
-	if (rmask == 0) {
-		return -1;
-	}
+	if (pmap != NULL && pmap->hal != NULL) {
+		hal_spinlockSet(&pmap_common.lock, &sc);
 
-	pmap->regions |= rmask;
+		allocCnt = pmap->hal->mpu.allocCnt;
+		tableCurrent = &pmap->hal->mpu.table[0].rbar;
 
-	return 0;
-}
+		/* Disable MPU */
+		hal_cpuDataMemoryBarrier();
+		*(pmap_common.mpu + mpu_ctrl) &= ~1;
+
+		for (i = 0; i < max(allocCnt, pmap_common.last_mpu_count); i += 4) {
+			/* RNR update is done by writes to RBAR */
+			__asm__ volatile(
+					"ldmia %[tableCurrent]!, {r3-r8, r10, r11} \n\t" /* Load 4 regions (rbar/rasr pairs) from table, update table pointer */
+					"stmia %[mpu_rbar], {r3-r8, r10, r11}      \n\t" /* Write 4 regions via RBAR/RASR and aliases */
+					: [tableCurrent] "+&r"(tableCurrent)
+					: [mpu_rbar] "r"(RBAR_ADDR)
+					: "r3", "r4", "r5", "r6", "r7", "r8", "r10", "r11");
+		}
 
+		/* Enable MPU */
+		*(pmap_common.mpu + mpu_ctrl) |= 1;
+		hal_cpuDataSyncBarrier();
 
-void pmap_switch(pmap_t *pmap)
-{
-	unsigned int i, cnt = syspage->hs.mpu.allocCnt;
-	spinlock_ctx_t sc;
+		pmap_common.last_mpu_count = allocCnt;
 
-	if (pmap != NULL) {
-		hal_spinlockSet(&pmap_common.lock, &sc);
-		for (i = 0; i < cnt; ++i) {
-			/* Select region */
-			*(pmap_common.mpu + mpu_rnr) = i;
-			hal_cpuDataMemoryBarrier();
-
-			/* Enable/disable region according to the mask */
-			if ((pmap->regions & (1 << i)) != 0) {
-				*(pmap_common.mpu + mpu_rasr) |= 1;
-			}
-			else {
-				*(pmap_common.mpu + mpu_rasr) &= ~1;
-			}
-			hal_cpuDataMemoryBarrier();
-		}
 		hal_spinlockClear(&pmap_common.lock, &sc);
 	}
 }
@@ -127,13 +123,21 @@ addr_t pmap_resolve(pmap_t *pmap, void *vaddr)
 int pmap_isAllowed(pmap_t *pmap, const void *vaddr, size_t size)
 {
 	const syspage_map_t *map = syspage_mapAddrResolve((addr_t)vaddr);
-	unsigned int rmask;
 	if (map == NULL) {
 		return 0;
 	}
-	rmask = pmap_map2region(map->id);
 
-	return ((pmap->regions & rmask) == 0) ? 0 : 1;
+	if (pmap->hal == NULL) {
+		/* Kernel pmap has access to everything */
+		return 1;
+	}
+
+	for (int i = 0; i < pmap->hal->mpu.allocCnt; ++i) {
+		if (pmap->hal->mpu.map[i] == map->id) {
+			return 1;
+		}
+	}
+	return 0;
 }
 
 
@@ -170,11 +174,8 @@ int pmap_segment(unsigned int i, void **vaddr, size_t *size, vm_prot_t *prot, vo
 
 void _pmap_init(pmap_t *pmap, void **vstart, void **vend)
 {
-	const syspage_map_t *ikmap;
-	unsigned int ikregion;
-	u32 t;
-	addr_t pc;
-	unsigned int i, cnt = syspage->hs.mpu.allocCnt;
+	unsigned int cnt = (syspage->hs.mpuType >> 8U) & 0xffU;
+	unsigned int i;
 
 	(*vstart) = (void *)(((ptr_t)_init_vectors + 7) & ~7);
 	(*vend) = (*((char **)vstart)) + SIZE_PAGE;
@@ -184,8 +185,11 @@ void _pmap_init(pmap_t *pmap, void **vstart, void **vend)
 	/* Initial size of kernel map */
 	pmap->end = (void *)((addr_t)&__bss_start + 32 * 1024);
 
+	pmap->hal = NULL;
+	pmap_common.last_mpu_count = cnt;
+
 	/* Configure MPU */
-	pmap_common.mpu = (void *)0xe000ed90;
+	pmap_common.mpu = MPU_BASE;
 
 	/* Disable MPU just in case */
 	*(pmap_common.mpu + mpu_ctrl) &= ~1;
@@ -196,17 +200,11 @@ void _pmap_init(pmap_t *pmap, void **vstart, void **vend)
 	hal_cpuDataMemoryBarrier();
 
 	for (i = 0; i < cnt; ++i) {
-		t = syspage->hs.mpu.table[i].rbar;
-		if ((t & (1 << 4)) == 0) {
-			continue;
-		}
-
-		*(pmap_common.mpu + mpu_rbar) = t;
-		hal_cpuDataMemoryBarrier();
+		/* Select region */
+		*(pmap_common.mpu + mpu_rnr) = i;
 
-		/* Disable regions for now */
-		t = syspage->hs.mpu.table[i].rasr & ~1;
-		*(pmap_common.mpu + mpu_rasr) = t;
+		/* Disable all regions for now */
+		*(pmap_common.mpu + mpu_rasr) = 0;
 		hal_cpuDataMemoryBarrier();
 	}
 
@@ -214,34 +212,5 @@ void _pmap_init(pmap_t *pmap, void **vstart, void **vend)
 	*(pmap_common.mpu + mpu_ctrl) |= 1;
 	hal_cpuDataMemoryBarrier();
 
-	/* FIXME HACK
-	 * allow all programs to execute (and read) kernel code map.
-	 * Needed because of hal_jmp, syscalls handler and signals handler.
-	 * In these functions we need to switch to the user mode when still
-	 * executing kernel code. This will cause memory management fault
-	 * if the application does not have access to the kernel instruction
-	 * map. Possible fix - place return to the user code in the separate
-	 * region and allow this region instead. */
-
-	/* Find kernel code region */
-	__asm__ volatile("\tmov %0, pc;" : "=r"(pc));
-	ikmap = syspage_mapAddrResolve(pc);
-	if (ikmap == NULL) {
-		hal_consolePrint(ATTR_BOLD, "pmap: Kernel code map not found. Bad system config\n");
-		for (;;) {
-			hal_cpuHalt();
-		}
-	}
-
-	ikregion = pmap_map2region(ikmap->id);
-	if (ikregion == 0) {
-		hal_consolePrint(ATTR_BOLD, "pmap: Kernel code map has no assigned region. Bad system config\n");
-		for (;;) {
-			hal_cpuHalt();
-		}
-	}
-
-	pmap_common.kernelCodeRegion = ikregion;
-
 	hal_spinlockCreate(&pmap_common.lock, "pmap");
 }
diff --git a/hal/armv7r/arch/pmap.h b/hal/armv7r/arch/pmap.h
index 7704082cd..a35c1c056 100644
--- a/hal/armv7r/arch/pmap.h
+++ b/hal/armv7r/arch/pmap.h
@@ -17,6 +17,7 @@
 #define _PH_HAL_PMAP_ARMV7R_H_
 
 #include "hal/types.h"
+#include "syspage.h"
 
 #define PGHD_PRESENT    0x01U
 #define PGHD_USER       0x04U
@@ -54,7 +55,7 @@ typedef struct _page_t {
 typedef struct _pmap_t {
 	void *start;
 	void *end;
-	u32 regions;
+	const hal_syspage_prog_t *hal;
 } pmap_t;
 
 #endif
diff --git a/hal/armv7r/pmap.c b/hal/armv7r/pmap.c
index 2cbe647a1..bf8b8f212 100644
--- a/hal/armv7r/pmap.c
+++ b/hal/armv7r/pmap.c
@@ -36,6 +36,7 @@ static struct {
 	unsigned int kernelCodeRegion;
 	spinlock_t lock;
 	int mpu_enabled;
+	int last_mpu_count[NUM_CPUS];
 } pmap_common;
 
 
@@ -104,9 +105,14 @@ static void pmap_mpu_disable(void)
 
 
 /* Function creates empty page table */
-int pmap_create(pmap_t *pmap, pmap_t *kpmap, page_t *p, void *vaddr)
+int pmap_create(pmap_t *pmap, pmap_t *kpmap, page_t *p, const syspage_prog_t *prog, void *vaddr)
 {
-	pmap->regions = pmap_common.kernelCodeRegion;
+	if (prog != NULL) {
+		pmap->hal = &prog->hal;
+	}
+	else {
+		pmap->hal = NULL;
+	}
 	return 0;
 }
 
@@ -117,60 +123,43 @@ addr_t pmap_destroy(pmap_t *pmap, int *i)
 }
 
 
-static unsigned int pmap_map2region(unsigned int map)
+void pmap_switch(pmap_t *pmap)
 {
-	if (pmap_common.mpu_enabled == 0) {
-		return 1;
-	}
-
+	const hal_syspage_prog_t *hal;
+	unsigned int allocCnt;
+	spinlock_ctx_t sc;
 	unsigned int i;
-	unsigned int mask = 0U;
-
-	for (i = 0U; i < sizeof(syspage->hs.mpu.map) / sizeof(*syspage->hs.mpu.map); ++i) {
-		if (map == syspage->hs.mpu.map[i]) {
-			mask |= (1UL << i);
-		}
-	}
-
-	return mask;
-}
 
-
-int pmap_addMap(pmap_t *pmap, unsigned int map)
-{
 	if (pmap_common.mpu_enabled == 0) {
-		return 0;
-	}
-
-	unsigned int rmask = pmap_map2region(map);
-	if (rmask == 0U) {
-		return -1;
+		return;
 	}
 
-	pmap->regions |= rmask;
-
-	return 0;
-}
+	if (pmap != NULL && pmap->hal != NULL) {
+		hal_spinlockSet(&pmap_common.lock, &sc);
 
+		hal = pmap->hal;
+		allocCnt = hal->mpu.allocCnt;
 
-void pmap_switch(pmap_t *pmap)
-{
-	unsigned int i, cnt = syspage->hs.mpu.allocCnt;
-	spinlock_ctx_t sc;
-	if (pmap_common.mpu_enabled == 0) {
-		return;
-	}
+		/* Disable MPU */
+		pmap_mpu_disable();
 
-	if (pmap != NULL) {
-		hal_spinlockSet(&pmap_common.lock, &sc);
-		for (i = 0; i < cnt; ++i) {
-			/* Select region */
+		for (i = 0; i < allocCnt; ++i) {
 			pmap_mpu_setMemRegionNumber(i);
+			pmap_mpu_setMemRegionRbar(hal->mpu.table[i].rbar);
+			pmap_mpu_setMemRegionRasr(hal->mpu.table[i].rasr);
+		}
 
-			/* Enable/disable region according to the mask */
-			pmap_mpu_setMemRegionStatus(((pmap->regions & (1UL << i)) != 0U) ? 1 : 0);
+		/* Disable all remaining regions */
+		for (; i < pmap_common.last_mpu_count[hal_cpuGetID()]; i++) {
+			pmap_mpu_setMemRegionNumber(i);
+			pmap_mpu_setMemRegionStatus(0);
 		}
 
+		/* Enable MPU */
+		pmap_mpu_enable();
+
+		pmap_common.last_mpu_count[hal_cpuGetID()] = allocCnt;
+
 		hal_spinlockClear(&pmap_common.lock, &sc);
 	}
 }
@@ -197,7 +186,7 @@ addr_t pmap_resolve(pmap_t *pmap, void *vaddr)
 int pmap_isAllowed(pmap_t *pmap, const void *vaddr, size_t size)
 {
 	const syspage_map_t *map;
-	unsigned int rmask;
+
 	if (pmap_common.mpu_enabled == 0) {
 		return 1;
 	}
@@ -206,9 +195,18 @@ int pmap_isAllowed(pmap_t *pmap, const void *vaddr, size_t size)
 	if (map == NULL) {
 		return 0;
 	}
-	rmask = pmap_map2region(map->id);
 
-	return ((pmap->regions & rmask) == 0U) ? 0 : 1;
+	if (pmap->hal == NULL) {
+		/* Kernel pmap has access to everything */
+		return 1;
+	}
+
+	for (int i = 0; i < pmap->hal->mpu.allocCnt; ++i) {
+		if (pmap->hal->mpu.map[i] == map->id) {
+			return 1;
+		}
+	}
+	return 0;
 }
 
 
@@ -246,12 +244,8 @@ int pmap_segment(unsigned int i, void **vaddr, size_t *size, vm_prot_t *prot, vo
 
 void _pmap_init(pmap_t *pmap, void **vstart, void **vend)
 {
-	const syspage_map_t *ikmap;
-	unsigned int ikregion;
-	u32 t;
-	unsigned int i;
-	unsigned int cnt = syspage->hs.mpu.allocCnt;
-
+	unsigned int cnt = (syspage->hs.mpuType >> 8U) & 0xffU;
+	int i;
 	*vstart = (void *)(((ptr_t)&_end + 7U) & ~7U);
 	*vend = (*((char **)vstart)) + SIZE_PAGE;
 
@@ -261,7 +255,10 @@ void _pmap_init(pmap_t *pmap, void **vstart, void **vend)
 
 	pmap->end = (void *)((addr_t)&__bss_start + 32U * 1024U);
 
-	pmap->regions = (1UL << cnt) - 1U;
+	pmap->hal = NULL;
+	for (i = 0; i < NUM_CPUS; i++) {
+		pmap_common.last_mpu_count[i] = cnt;
+	}
 
 	if (cnt == 0U) {
 		hal_spinlockCreate(&pmap_common.lock, "pmap");
@@ -277,46 +274,10 @@ void _pmap_init(pmap_t *pmap, void **vstart, void **vend)
 
 	for (i = 0; i < cnt; ++i) {
 		pmap_mpu_setMemRegionNumber(i);
-		t = syspage->hs.mpu.table[i].rbar;
-		if ((t & (0x1U << 4)) == 0U) {
-			continue;
-		}
-
-		pmap_mpu_setMemRegionRbar(t);
-		pmap_mpu_setMemRegionRasr(syspage->hs.mpu.table[i].rasr); /* Enable all regions */
+		pmap_mpu_setMemRegionStatus(0);
 	}
 
 	/* Enable MPU */
 	pmap_mpu_enable();
-
-	/* FIXME HACK
-	 * allow all programs to execute (and read) kernel code map.
-	 * Needed because of hal_jmp, syscalls handler and signals handler.
-	 * In these functions we need to switch to the user mode when still
-	 * executing kernel code. This will cause memory management fault
-	 * if the application does not have access to the kernel instruction
-	 * map. Possible fix - place return to the user code in the separate
-	 * region and allow this region instead. */
-
-	/* Find kernel code region */
-	/* parasoft-suppress-next-line MISRAC2012-RULE_11_1 "We need address of this function in numeric type" */
-	ikmap = syspage_mapAddrResolve((addr_t)_pmap_init);
-	if (ikmap == NULL) {
-		hal_consolePrint(ATTR_BOLD, "pmap: Kernel code map not found. Bad system config\n");
-		for (;;) {
-			hal_cpuHalt();
-		}
-	}
-
-	ikregion = pmap_map2region(ikmap->id);
-	if (ikregion == 0U) {
-		hal_consolePrint(ATTR_BOLD, "pmap: Kernel code map has no assigned region. Bad system config\n");
-		for (;;) {
-			hal_cpuHalt();
-		}
-	}
-
-	pmap_common.kernelCodeRegion = ikregion;
-
 	hal_spinlockCreate(&pmap_common.lock, "pmap");
 }
diff --git a/hal/armv8m/arch/pmap.h b/hal/armv8m/arch/pmap.h
index f68142162..5507118d3 100644
--- a/hal/armv8m/arch/pmap.h
+++ b/hal/armv8m/arch/pmap.h
@@ -17,6 +17,7 @@
 #define _PH_HAL_PMAP_ARMV8M_H_
 
 #include "hal/types.h"
+#include "syspage.h"
 
 #define PGHD_PRESENT    0x01U
 #define PGHD_USER       0x04U
@@ -54,7 +55,7 @@ typedef struct _page_t {
 typedef struct _pmap_t {
 	void *start;
 	void *end;
-	u32 regions;
+	const hal_syspage_prog_t *hal;
 } pmap_t;
 
 #endif
diff --git a/hal/armv8m/mcx/n94x/config.h b/hal/armv8m/mcx/n94x/config.h
index cd11e366e..4fe453911 100644
--- a/hal/armv8m/mcx/n94x/config.h
+++ b/hal/armv8m/mcx/n94x/config.h
@@ -20,7 +20,9 @@
 
 #ifndef __ASSEMBLY__
 
+#include "hal/types.h"
 #include "include/arch/armv8m/mcx/syspage.h"
+#include "include/syspage.h"
 #include "mcxn94x.h"
 
 #define HAL_NAME_PLATFORM "MCX N94x "
diff --git a/hal/armv8m/pmap.c b/hal/armv8m/pmap.c
index 4c76f2b50..6f53bedc6 100644
--- a/hal/armv8m/pmap.c
+++ b/hal/armv8m/pmap.c
@@ -15,6 +15,7 @@
 
 #include "hal/pmap.h"
 #include "config.h"
+#include "lib/lib.h"
 #include "syspage.h"
 #include "halsyspage.h"
 #include <arch/cpu.h>
@@ -43,13 +44,19 @@ static struct {
 	unsigned int kernelCodeRegion;
 	spinlock_t lock;
 	int mpu_enabled;
+	int last_mpu_count;
 } pmap_common;
 
 
 /* Function creates empty page table */
-int pmap_create(pmap_t *pmap, pmap_t *kpmap, page_t *p, void *vaddr)
+int pmap_create(pmap_t *pmap, pmap_t *kpmap, page_t *p, const syspage_prog_t *prog, void *vaddr)
 {
-	pmap->regions = pmap_common.kernelCodeRegion;
+	if (prog != NULL) {
+		pmap->hal = &prog->hal;
+	}
+	else {
+		pmap->hal = NULL;
+	}
 	return 0;
 }
 
@@ -60,67 +67,44 @@ addr_t pmap_destroy(pmap_t *pmap, int *i)
 }
 
 
-static unsigned int pmap_map2region(unsigned int map)
+void pmap_switch(pmap_t *pmap)
 {
-	int i;
-	unsigned int mask = 0;
+	static const volatile u32 *RBAR_ADDR = MPU_BASE + mpu_rbar;
+	unsigned int allocCnt;
+	spinlock_ctx_t sc;
+	unsigned int i;
+	const u32 *tableCurrent;
 
 	if (pmap_common.mpu_enabled == 0) {
-		return 1;
-	}
-
-	for (i = 0; i < sizeof(syspage->hs.mpu.map) / sizeof(*syspage->hs.mpu.map); ++i) {
-		if (map == syspage->hs.mpu.map[i]) {
-			mask |= (1 << i);
-		}
+		return;
 	}
 
-	return mask;
-}
-
+	if (pmap != NULL && pmap->hal != NULL) {
+		hal_spinlockSet(&pmap_common.lock, &sc);
 
-int pmap_addMap(pmap_t *pmap, unsigned int map)
-{
-	unsigned int rmask;
-	if (pmap_common.mpu_enabled == 0) {
-		return 0;
-	}
+		allocCnt = pmap->hal->mpu.allocCnt;
+		tableCurrent = &pmap->hal->mpu.table[0].rbar;
 
-	rmask = pmap_map2region(map);
-	if (rmask == 0) {
-		return -1;
-	}
+		/* Disable MPU */
+		hal_cpuDataMemoryBarrier();
+		*(pmap_common.mpu + mpu_ctrl) &= ~1;
 
-	pmap->regions |= rmask;
+		for (i = 0; i < max(allocCnt, pmap_common.last_mpu_count); i += 4) {
+			*(pmap_common.mpu + mpu_rnr) = i;
+			__asm__ volatile(
+					"ldmia %[tableCurrent]!, {r3-r8, r10, r11} \n\t" /* Load 4 regions (rbar/rlar pairs) from table, update table pointer */
+					"stmia %[mpu_rbar], {r3-r8, r10, r11}      \n\t" /* Write 4 regions via RBAR/RLAR and aliases */
+					: [tableCurrent] "+r"(tableCurrent)
+					: [mpu_rbar] "r"(RBAR_ADDR)
+					: "r3", "r4", "r5", "r6", "r7", "r8", "r10", "r11");
+		}
 
-	return 0;
-}
+		/* Enable MPU */
+		*(pmap_common.mpu + mpu_ctrl) |= 1;
+		hal_cpuDataSyncBarrier();
 
+		pmap_common.last_mpu_count = allocCnt;
 
-void pmap_switch(pmap_t *pmap)
-{
-	unsigned int i, cnt = syspage->hs.mpu.allocCnt;
-	spinlock_ctx_t sc;
-	if (pmap_common.mpu_enabled == 0) {
-		return;
-	}
-
-	if (pmap != NULL) {
-		hal_spinlockSet(&pmap_common.lock, &sc);
-		for (i = 0; i < cnt; ++i) {
-			/* Select region */
-			*(pmap_common.mpu + mpu_rnr) = i;
-			hal_cpuDataMemoryBarrier();
-
-			/* Enable/disable region according to the mask */
-			if ((pmap->regions & (1 << i)) != 0) {
-				*(pmap_common.mpu + mpu_rlar) |= 1U;
-			}
-			else {
-				*(pmap_common.mpu + mpu_rlar) &= ~1U;
-			}
-			hal_cpuDataMemoryBarrier();
-		}
 		hal_spinlockClear(&pmap_common.lock, &sc);
 	}
 }
@@ -147,7 +131,6 @@ addr_t pmap_resolve(pmap_t *pmap, void *vaddr)
 int pmap_isAllowed(pmap_t *pmap, const void *vaddr, size_t size)
 {
 	const syspage_map_t *map = syspage_mapAddrResolve((addr_t)vaddr);
-	unsigned int rmask;
 	addr_t addr_end = (addr_t)vaddr + size;
 	/* Check for potential arithmetic overflow. `addr_end` is allowed to be 0,
 	 * as it represents the top of memory. */
@@ -160,9 +143,17 @@ int pmap_isAllowed(pmap_t *pmap, const void *vaddr, size_t size)
 		return 1;
 	}
 
-	rmask = pmap_map2region(map->id);
+	if (pmap->hal == NULL) {
+		/* Kernel pmap has access to everything */
+		return 1;
+	}
 
-	return ((pmap->regions & rmask) != 0) ? 1 : 0;
+	for (int i = 0; i < pmap->hal->mpu.allocCnt; ++i) {
+		if (pmap->hal->mpu.map[i] == map->id) {
+			return 1;
+		}
+	}
+	return 0;
 }
 
 
@@ -200,9 +191,10 @@ int pmap_segment(unsigned int i, void **vaddr, size_t *size, vm_prot_t *prot, vo
 
 void _pmap_init(pmap_t *pmap, void **vstart, void **vend)
 {
-	const syspage_map_t *ikmap;
-	unsigned int ikregion;
-	unsigned int i, cnt = syspage->hs.mpu.allocCnt;
+	unsigned int cnt = min(
+			(syspage->hs.mpuType >> 8U) & 0xffU,
+			sizeof(pmap->hal->mpu.table) / sizeof(pmap->hal->mpu.table[0]));
+	int i;
 
 	(*vstart) = (void *)(((ptr_t)_init_vectors + 7) & ~7U);
 	(*vend) = (*((char **)vstart)) + SIZE_PAGE;
@@ -212,8 +204,8 @@ void _pmap_init(pmap_t *pmap, void **vstart, void **vend)
 	/* Initial size of kernel map */
 	pmap->end = (void *)((addr_t)&__bss_start + 32 * 1024);
 
-	/* Enable all regions for kernel */
-	pmap->regions = (1 << cnt) - 1;
+	pmap->hal = NULL;
+	pmap_common.last_mpu_count = cnt;
 
 	/* Configure MPU */
 	pmap_common.mpu = MPU_BASE;
@@ -239,42 +231,12 @@ void _pmap_init(pmap_t *pmap, void **vstart, void **vend)
 	for (i = 0; i < cnt; ++i) {
 		/* Select MPU region to configure */
 		*(pmap_common.mpu + mpu_rnr) = i;
-		hal_cpuDataMemoryBarrier();
-
-		*(pmap_common.mpu + mpu_rbar) = syspage->hs.mpu.table[i].rbar;
-		hal_cpuDataMemoryBarrier();
 
-		/* Disable regions for now */
-		*(pmap_common.mpu + mpu_rlar) = syspage->hs.mpu.table[i].rlar & ~1U;
-		hal_cpuDataMemoryBarrier();
+		/* Disable all regions for now */
+		*(pmap_common.mpu + mpu_rlar) = 0;
 	}
 
 	/* Enable MPU */
 	*(pmap_common.mpu + mpu_ctrl) |= 1;
-	hal_cpuDataMemoryBarrier();
-
-	/* FIXME HACK
-	 * allow all programs to execute (and read) kernel code map.
-	 * Needed because of hal_jmp, syscalls handler and signals handler.
-	 * In these functions we need to switch to the user mode when still
-	 * executing kernel code. This will cause memory management fault
-	 * if the application does not have access to the kernel instruction
-	 * map. Possible fix - place return to the user code in the separate
-	 * region and allow this region instead. */
-
-	/* Find kernel code region */
-	/* parasoft-suppress-next-line MISRAC2012-RULE_11_1 "We need address of this function in numeric type" */
-	ikmap = syspage_mapAddrResolve((addr_t)_pmap_init);
-	if (ikmap != NULL) {
-		ikregion = pmap_map2region(ikmap->id);
-	}
-
-	if ((ikmap == NULL) || (ikregion == 0)) {
-		hal_consolePrint(ATTR_BOLD, "pmap: Kernel code map not found or has no regions. Bad system config\n");
-		for (;;) {
-			hal_cpuHalt();
-		}
-	}
-
-	pmap_common.kernelCodeRegion = ikregion;
+	hal_cpuDataSyncBarrier();
 }
diff --git a/hal/armv8r/pmap.c b/hal/armv8r/pmap.c
index 04ad75598..948d8f088 100644
--- a/hal/armv8r/pmap.c
+++ b/hal/armv8r/pmap.c
@@ -26,7 +26,7 @@ u8 _init_stack[NUM_CPUS][SIZE_INITIAL_KSTACK] __attribute__((aligned(8)));
 
 
 /* Function creates empty page table */
-int pmap_create(pmap_t *pmap, pmap_t *kpmap, page_t *p, void *vaddr)
+int pmap_create(pmap_t *pmap, pmap_t *kpmap, page_t *p, const syspage_prog_t *prog, void *vaddr)
 {
 	return 0;
 }
diff --git a/hal/ia32/pmap.c b/hal/ia32/pmap.c
index f299d8dc5..4b0994627 100644
--- a/hal/ia32/pmap.c
+++ b/hal/ia32/pmap.c
@@ -38,7 +38,7 @@ struct {
 
 
 /* Function creates empty page table */
-int pmap_create(pmap_t *pmap, pmap_t *kpmap, page_t *p, void *vaddr)
+int pmap_create(pmap_t *pmap, pmap_t *kpmap, page_t *p, const syspage_prog_t *prog, void *vaddr)
 {
 	u32 i, pages;
 	pmap->pdir = vaddr;
diff --git a/hal/pmap.h b/hal/pmap.h
index bac98b19e..e3176a8de 100644
--- a/hal/pmap.h
+++ b/hal/pmap.h
@@ -19,6 +19,7 @@
 #include "vm/types.h"
 
 #include <arch/pmap.h>
+#include "syspage.h"
 
 
 #ifndef NOMMU
@@ -30,14 +31,12 @@ static inline int pmap_belongs(pmap_t *pmap, void *addr)
 
 #else
 
-int pmap_addMap(pmap_t *pmap, unsigned int map);
-
 int pmap_isAllowed(pmap_t *pmap, const void *vaddr, size_t size);
 
 #endif
 
 
-int pmap_create(pmap_t *pmap, pmap_t *kpmap, page_t *p, void *vaddr);
+int pmap_create(pmap_t *pmap, pmap_t *kpmap, page_t *p, const syspage_prog_t *prog, void *vaddr);
 
 
 addr_t pmap_destroy(pmap_t *pmap, int *i);
diff --git a/hal/riscv64/pmap.c b/hal/riscv64/pmap.c
index 3c679c569..1c0ff7278 100644
--- a/hal/riscv64/pmap.c
+++ b/hal/riscv64/pmap.c
@@ -98,7 +98,7 @@ addr_t pmap_getKernelStart(void)
 
 
 /* Function creates empty page table */
-int pmap_create(pmap_t *pmap, pmap_t *kpmap, page_t *p, void *vaddr)
+int pmap_create(pmap_t *pmap, pmap_t *kpmap, page_t *p, const syspage_prog_t *prog, void *vaddr)
 {
 	unsigned int i, pages;
 	ptr_t va;
diff --git a/hal/sparcv8leon/pmap-nommu.c b/hal/sparcv8leon/pmap-nommu.c
index 7f3c03269..1733b6719 100644
--- a/hal/sparcv8leon/pmap-nommu.c
+++ b/hal/sparcv8leon/pmap-nommu.c
@@ -25,7 +25,7 @@ extern void *_init_stack;
 
 
 /* Function creates empty page table */
-int pmap_create(pmap_t *pmap, pmap_t *kpmap, page_t *p, void *vaddr)
+int pmap_create(pmap_t *pmap, pmap_t *kpmap, page_t *p, const syspage_prog_t *prog, void *vaddr)
 {
 	return 0;
 }
@@ -37,12 +37,6 @@ addr_t pmap_destroy(pmap_t *pmap, int *i)
 }
 
 
-int pmap_addMap(pmap_t *pmap, unsigned int map)
-{
-	return 0;
-}
-
-
 void pmap_switch(pmap_t *pmap)
 {
 	return;
diff --git a/hal/sparcv8leon/pmap.c b/hal/sparcv8leon/pmap.c
index 2eb3506fa..40b57f29c 100644
--- a/hal/sparcv8leon/pmap.c
+++ b/hal/sparcv8leon/pmap.c
@@ -192,7 +192,7 @@ static void _pmap_contextDealloc(pmap_t *pmap)
 
 
 /* Function creates empty page table */
-int pmap_create(pmap_t *pmap, pmap_t *kpmap, page_t *p, void *vaddr)
+int pmap_create(pmap_t *pmap, pmap_t *kpmap, page_t *p, const syspage_prog_t *prog, void *vaddr)
 {
 	pmap->pdir1 = vaddr;
 	pmap->context = CONTEXT_INVALID;
diff --git a/include/arch/aarch64/zynqmp/syspage.h b/include/arch/aarch64/zynqmp/syspage.h
index 2abbc61be..11c3f04a3 100644
--- a/include/arch/aarch64/zynqmp/syspage.h
+++ b/include/arch/aarch64/zynqmp/syspage.h
@@ -21,4 +21,7 @@ typedef struct {
 } __attribute__((packed)) hal_syspage_t;
 
 
+typedef struct {
+} hal_syspage_prog_t;
+
 #endif
diff --git a/include/arch/armv7a/imx6ull/syspage.h b/include/arch/armv7a/imx6ull/syspage.h
index 1543fc8bc..e86ca6da6 100644
--- a/include/arch/armv7a/imx6ull/syspage.h
+++ b/include/arch/armv7a/imx6ull/syspage.h
@@ -21,4 +21,8 @@ typedef struct {
 	int dummy;
 } __attribute__((packed)) hal_syspage_t;
 
+
+typedef struct {
+} hal_syspage_prog_t;
+
 #endif
diff --git a/include/arch/armv7a/zynq7000/syspage.h b/include/arch/armv7a/zynq7000/syspage.h
index e312c7184..fba674a3e 100644
--- a/include/arch/armv7a/zynq7000/syspage.h
+++ b/include/arch/armv7a/zynq7000/syspage.h
@@ -21,4 +21,7 @@ typedef struct {
 } __attribute__((packed)) hal_syspage_t;
 
 
+typedef struct {
+} hal_syspage_prog_t;
+
 #endif
diff --git a/include/arch/armv7m/imxrt/syspage.h b/include/arch/armv7m/imxrt/syspage.h
index ae1dcee8f..52b20fc21 100644
--- a/include/arch/armv7m/imxrt/syspage.h
+++ b/include/arch/armv7m/imxrt/syspage.h
@@ -20,14 +20,18 @@
 
 typedef struct {
 	struct {
-		unsigned int type;
-		unsigned int allocCnt;
 		struct {
 			unsigned int rbar;
 			unsigned int rasr;
 		} table[16] __attribute__((aligned(8)));
 		unsigned int map[16]; /* ((unsigned int)-1) = map is not assigned */
-	} __attribute__((packed)) mpu;
+		unsigned int allocCnt;
+	} mpu;
+} hal_syspage_prog_t;
+
+
+typedef struct {
+	unsigned int mpuType;
 	unsigned int bootReason;
 } __attribute__((packed)) hal_syspage_t;
 
diff --git a/include/arch/armv7m/stm32/syspage.h b/include/arch/armv7m/stm32/syspage.h
index aaa8ef7cc..fcc04e3e5 100644
--- a/include/arch/armv7m/stm32/syspage.h
+++ b/include/arch/armv7m/stm32/syspage.h
@@ -20,14 +20,18 @@
 
 typedef struct {
 	struct {
-		unsigned int type;
-		unsigned int allocCnt;
 		struct {
 			unsigned int rbar;
 			unsigned int rasr;
 		} table[16] __attribute__((aligned(8)));
 		unsigned int map[16]; /* ((unsigned int)-1) = map is not assigned */
-	} __attribute__((packed)) mpu;
+		unsigned int allocCnt;
+	} mpu;
+} hal_syspage_prog_t;
+
+
+typedef struct {
+	unsigned int mpuType;
 	unsigned int bootReason;
 } __attribute__((packed)) hal_syspage_t;
 
diff --git a/include/arch/armv7r/tda4vm/syspage.h b/include/arch/armv7r/tda4vm/syspage.h
index eae556bb5..b9f86b837 100644
--- a/include/arch/armv7r/tda4vm/syspage.h
+++ b/include/arch/armv7r/tda4vm/syspage.h
@@ -18,16 +18,20 @@
 
 
 typedef struct {
-	int resetReason;
 	struct {
-		unsigned int type;
-		unsigned int allocCnt;
 		struct {
 			unsigned int rbar;
 			unsigned int rasr;
 		} table[16] __attribute__((aligned(8)));
 		unsigned int map[16]; /* ((unsigned int)-1) = map is not assigned */
+		unsigned int allocCnt;
 	} __attribute__((packed)) mpu;
+} __attribute__((packed)) hal_syspage_prog_t;
+
+
+typedef struct {
+	int resetReason;
+	unsigned int mpuType;
 } __attribute__((packed)) hal_syspage_t;
 
 
diff --git a/include/arch/armv7r/zynqmp/syspage.h b/include/arch/armv7r/zynqmp/syspage.h
index 31c94eecc..aa2ab0430 100644
--- a/include/arch/armv7r/zynqmp/syspage.h
+++ b/include/arch/armv7r/zynqmp/syspage.h
@@ -18,16 +18,20 @@
 
 
 typedef struct {
-	int resetReason;
 	struct {
-		unsigned int type;
-		unsigned int allocCnt;
 		struct {
 			unsigned int rbar;
 			unsigned int rasr;
 		} table[16] __attribute__((aligned(8)));
 		unsigned int map[16]; /* ((unsigned int)-1) = map is not assigned */
+		unsigned int allocCnt;
 	} __attribute__((packed)) mpu;
+} __attribute__((packed)) hal_syspage_prog_t;
+
+
+typedef struct {
+	int resetReason;
+	unsigned int mpuType;
 } __attribute__((packed)) hal_syspage_t;
 
 
diff --git a/include/arch/armv8m/mcx/syspage.h b/include/arch/armv8m/mcx/syspage.h
index 2f6721505..65e1f46f0 100644
--- a/include/arch/armv8m/mcx/syspage.h
+++ b/include/arch/armv8m/mcx/syspage.h
@@ -20,14 +20,18 @@
 
 typedef struct {
 	struct {
-		unsigned int type;
-		unsigned int allocCnt;
 		struct {
 			unsigned int rbar;
 			unsigned int rlar;
 		} table[16] __attribute__((aligned(8)));
 		unsigned int map[16]; /* ((unsigned int)-1) = map is not assigned */
-	} __attribute__((packed)) mpu;
+		unsigned int allocCnt;
+	} mpu;
+} hal_syspage_prog_t;
+
+
+typedef struct {
+	unsigned int mpuType;
 } __attribute__((packed)) hal_syspage_t;
 
 #endif
diff --git a/include/arch/armv8m/nrf/syspage.h b/include/arch/armv8m/nrf/syspage.h
index 6fc79e590..bcc048eb0 100644
--- a/include/arch/armv8m/nrf/syspage.h
+++ b/include/arch/armv8m/nrf/syspage.h
@@ -20,14 +20,18 @@
 
 typedef struct {
 	struct {
-		unsigned int type;
-		unsigned int allocCnt;
 		struct {
 			unsigned int rbar;
 			unsigned int rlar;
 		} table[16] __attribute__((aligned(8)));
 		unsigned int map[16]; /* ((unsigned int)-1) = map is not assigned */
-	} __attribute__((packed)) mpu;
+		unsigned int allocCnt;
+	} mpu;
+} hal_syspage_prog_t;
+
+
+typedef struct {
+	unsigned int mpuType;
 } __attribute__((packed)) hal_syspage_t;
 
 #endif
diff --git a/include/arch/armv8m/stm32/syspage.h b/include/arch/armv8m/stm32/syspage.h
index 1f1e50c64..e0fb32b48 100644
--- a/include/arch/armv8m/stm32/syspage.h
+++ b/include/arch/armv8m/stm32/syspage.h
@@ -20,15 +20,18 @@
 
 typedef struct {
 	struct {
-		unsigned int type;
-		unsigned int allocCnt;
-		unsigned int mair[2];
 		struct {
 			unsigned int rbar;
 			unsigned int rlar;
 		} table[16] __attribute__((aligned(8)));
 		unsigned int map[16]; /* ((unsigned int)-1) = map is not assigned */
-	} __attribute__((packed)) mpu;
+		unsigned int allocCnt;
+	} mpu;
+} hal_syspage_prog_t;
+
+
+typedef struct {
+	unsigned int mpuType;
 	unsigned int bootReason;
 } __attribute__((packed)) hal_syspage_t;
 
diff --git a/include/arch/armv8r/mps3an536/syspage.h b/include/arch/armv8r/mps3an536/syspage.h
index 1dce97769..430656cdd 100644
--- a/include/arch/armv8r/mps3an536/syspage.h
+++ b/include/arch/armv8r/mps3an536/syspage.h
@@ -22,4 +22,7 @@ typedef struct {
 } __attribute__((packed)) hal_syspage_t;
 
 
+typedef struct {
+} hal_syspage_prog_t;
+
 #endif
diff --git a/include/arch/ia32/syspage.h b/include/arch/ia32/syspage.h
index 9075b70dd..a94be6c6c 100644
--- a/include/arch/ia32/syspage.h
+++ b/include/arch/ia32/syspage.h
@@ -57,5 +57,7 @@ typedef struct {
 	} __attribute__((packed)) graphmode; /* Graphics mode info */
 } __attribute__((packed)) hal_syspage_t;
 
+typedef struct {
+} hal_syspage_prog_t;
 
 #endif
diff --git a/include/arch/riscv64/syspage.h b/include/arch/riscv64/syspage.h
index 5044f1eef..08c83f2ce 100644
--- a/include/arch/riscv64/syspage.h
+++ b/include/arch/riscv64/syspage.h
@@ -21,4 +21,8 @@ typedef struct {
 	unsigned int boothartId;
 } __attribute__((packed)) hal_syspage_t;
 
+
+typedef struct {
+} hal_syspage_prog_t;
+
 #endif
diff --git a/include/arch/sparcv8leon/syspage.h b/include/arch/sparcv8leon/syspage.h
index 020190ddb..4f0479c5d 100644
--- a/include/arch/sparcv8leon/syspage.h
+++ b/include/arch/sparcv8leon/syspage.h
@@ -21,4 +21,8 @@ typedef struct {
 	int dummy;
 } __attribute__((packed)) hal_syspage_t;
 
+
+typedef struct {
+} hal_syspage_prog_t;
+
 #endif
diff --git a/include/syspage.h b/include/syspage.h
index d9ce36cd8..a43ac6ea9 100644
--- a/include/syspage.h
+++ b/include/syspage.h
@@ -48,7 +48,9 @@ typedef struct _syspage_prog_t {
 
 	size_t dmapSz;
 	unsigned char *dmaps;
-} __attribute__((packed)) syspage_prog_t;
+
+	hal_syspage_prog_t hal;
+} syspage_prog_t;
 
 
 typedef struct _syspage_map_t {
diff --git a/proc/process.c b/proc/process.c
index 48324cdd7..e82d954f1 100644
--- a/proc/process.c
+++ b/proc/process.c
@@ -1069,7 +1069,6 @@ static void process_exec(thread_t *current, process_spawn_t *spawn)
 	void *stack, *entry = NULL;
 	int err = 0, count;
 	void *cleanupFn = NULL;
-	unsigned int i;
 	spinlock_ctx_t sc;
 	const struct stackArg args[] = {
 		{ &spawn->envp, sizeof(spawn->envp) },
@@ -1084,29 +1083,10 @@ static void process_exec(thread_t *current, process_spawn_t *spawn)
 #ifndef NOMMU
 	vm_mapCreate(&current->process->map, (void *)(VADDR_MIN + SIZE_PAGE), (void *)VADDR_USR_MAX);
 	proc_changeMap(current->process, &current->process->map, NULL, &current->process->map.pmap);
-	(void)i;
 #else
-	(void)pmap_create(&current->process->map.pmap, NULL, NULL, NULL);
+	(void)pmap_create(&current->process->map.pmap, NULL, NULL, spawn->prog, NULL);
 	proc_changeMap(current->process, (spawn->map != NULL) ? spawn->map : process_common.kmap, spawn->imap, &current->process->map.pmap);
 	current->process->entries = NULL;
-
-	if (spawn->prog != NULL) {
-		/* Add instruction maps */
-		for (i = 0; i < spawn->prog->imapSz; ++i) {
-			if (err != 0) {
-				break;
-			}
-			err = pmap_addMap(current->process->pmapp, spawn->prog->imaps[i]);
-		}
-
-		/* Add data/io maps */
-		for (i = 0; i < spawn->prog->dmapSz; ++i) {
-			if (err != 0) {
-				break;
-			}
-			err = pmap_addMap(current->process->pmapp, spawn->prog->dmaps[i]);
-		}
-	}
 #endif
 
 	pmap_switch(current->process->pmapp);
diff --git a/vm/map.c b/vm/map.c
index 3f07d87f3..f3c0eeeda 100644
--- a/vm/map.c
+++ b/vm/map.c
@@ -1006,9 +1006,9 @@ int vm_mapCreate(vm_map_t *map, void *start, void *stop)
 		return -ENOMEM;
 	}
 
-	pmap_create(&map->pmap, &map_common.kmap->pmap, map->pmap.pmapp, map->pmap.pmapv);
+	pmap_create(&map->pmap, &map_common.kmap->pmap, map->pmap.pmapp, NULL, map->pmap.pmapv);
 #else
-	(void)pmap_create(&map->pmap, &map_common.kmap->pmap, NULL, NULL);
+	(void)pmap_create(&map->pmap, &map_common.kmap->pmap, NULL, NULL, NULL);
 #endif
 
 	(void)proc_lockInit(&map->lock, &proc_lockAttrDefault, "map.map");