Index: kernel/arch/amd64/include/cpu.h
===================================================================
--- kernel/arch/amd64/include/cpu.h	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/amd64/include/cpu.h	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -65,5 +65,5 @@
 	tss_t *tss;
 	
-	count_t iomapver_copy;  /** Copy of TASK's I/O Permission bitmap generation count. */
+	size_t iomapver_copy;  /** Copy of TASK's I/O Permission bitmap generation count. */
 } cpu_arch_t;
 
Index: kernel/arch/amd64/include/mm/page.h
===================================================================
--- kernel/arch/amd64/include/mm/page.h	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/amd64/include/mm/page.h	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -113,31 +113,31 @@
 	(write_cr3((uintptr_t) (ptl0)))
 #define SET_PTL1_ADDRESS_ARCH(ptl0, i, a) \
-	set_pt_addr((pte_t *) (ptl0), (index_t) (i), a)
+	set_pt_addr((pte_t *) (ptl0), (size_t) (i), a)
 #define SET_PTL2_ADDRESS_ARCH(ptl1, i, a) \
-	set_pt_addr((pte_t *) (ptl1), (index_t) (i), a)
+	set_pt_addr((pte_t *) (ptl1), (size_t) (i), a)
 #define SET_PTL3_ADDRESS_ARCH(ptl2, i, a) \
-	set_pt_addr((pte_t *) (ptl2), (index_t) (i), a)
+	set_pt_addr((pte_t *) (ptl2), (size_t) (i), a)
 #define SET_FRAME_ADDRESS_ARCH(ptl3, i, a) \
-	set_pt_addr((pte_t *) (ptl3), (index_t) (i), a)
+	set_pt_addr((pte_t *) (ptl3), (size_t) (i), a)
 
 /* Get PTE flags accessors for each level. */
 #define GET_PTL1_FLAGS_ARCH(ptl0, i) \
-	get_pt_flags((pte_t *) (ptl0), (index_t) (i))
+	get_pt_flags((pte_t *) (ptl0), (size_t) (i))
 #define GET_PTL2_FLAGS_ARCH(ptl1, i) \
-	get_pt_flags((pte_t *) (ptl1), (index_t) (i))
+	get_pt_flags((pte_t *) (ptl1), (size_t) (i))
 #define GET_PTL3_FLAGS_ARCH(ptl2, i) \
-	get_pt_flags((pte_t *) (ptl2), (index_t) (i))
+	get_pt_flags((pte_t *) (ptl2), (size_t) (i))
 #define GET_FRAME_FLAGS_ARCH(ptl3, i) \
-	get_pt_flags((pte_t *) (ptl3), (index_t) (i))
+	get_pt_flags((pte_t *) (ptl3), (size_t) (i))
 
 /* Set PTE flags accessors for each level. */
 #define SET_PTL1_FLAGS_ARCH(ptl0, i, x) \
-	set_pt_flags((pte_t *) (ptl0), (index_t) (i), (x))
+	set_pt_flags((pte_t *) (ptl0), (size_t) (i), (x))
 #define SET_PTL2_FLAGS_ARCH(ptl1, i, x) \
-	set_pt_flags((pte_t *) (ptl1), (index_t) (i), (x))
+	set_pt_flags((pte_t *) (ptl1), (size_t) (i), (x))
 #define SET_PTL3_FLAGS_ARCH(ptl2, i, x) \
-	set_pt_flags((pte_t *) (ptl2), (index_t) (i), (x))
+	set_pt_flags((pte_t *) (ptl2), (size_t) (i), (x))
 #define SET_FRAME_FLAGS_ARCH(ptl3, i, x) \
-	set_pt_flags((pte_t *) (ptl3), (index_t) (i), (x))
+	set_pt_flags((pte_t *) (ptl3), (size_t) (i), (x))
 
 /* Macros for querying the last-level PTE entries. */
@@ -177,5 +177,5 @@
 #define PFERR_CODE_ID		(1 << 4)
 
-static inline int get_pt_flags(pte_t *pt, index_t i)
+static inline int get_pt_flags(pte_t *pt, size_t i)
 {
 	pte_t *p = &pt[i];
@@ -190,5 +190,5 @@
 }
 
-static inline void set_pt_addr(pte_t *pt, index_t i, uintptr_t a)
+static inline void set_pt_addr(pte_t *pt, size_t i, uintptr_t a)
 {
 	pte_t *p = &pt[i];
@@ -198,5 +198,5 @@
 }
 
-static inline void set_pt_flags(pte_t *pt, index_t i, int flags)
+static inline void set_pt_flags(pte_t *pt, size_t i, int flags)
 {
 	pte_t *p = &pt[i];
Index: kernel/arch/amd64/include/proc/task.h
===================================================================
--- kernel/arch/amd64/include/proc/task.h	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/amd64/include/proc/task.h	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -41,5 +41,5 @@
 typedef struct {
 	/** I/O Permission bitmap Generation counter. */
-	count_t iomapver;
+	size_t iomapver;
 	/** I/O Permission bitmap. */
 	bitmap_t iomap;
Index: kernel/arch/amd64/include/types.h
===================================================================
--- kernel/arch/amd64/include/types.h	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/amd64/include/types.h	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -47,6 +47,4 @@
 
 typedef uint64_t size_t;
-typedef uint64_t count_t;
-typedef uint64_t index_t;
 
 typedef uint64_t uintptr_t;
@@ -61,9 +59,7 @@
 } fncptr_t;
 
-/**< Formats for uintptr_t, size_t, count_t and index_t */
+/**< Formats for uintptr_t, size_t */
 #define PRIp "llx"
 #define PRIs "llu"
-#define PRIc "llu"
-#define PRIi "llu"
 
 /**< Formats for (u)int8_t, (u)int16_t, (u)int32_t, (u)int64_t and (u)native_t */
Index: kernel/arch/amd64/src/ddi/ddi.c
===================================================================
--- kernel/arch/amd64/src/ddi/ddi.c	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/amd64/src/ddi/ddi.c	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -57,5 +57,5 @@
 int ddi_iospace_enable_arch(task_t *task, uintptr_t ioaddr, size_t size)
 {
-	count_t bits;
+	size_t bits;
 	
 	bits = ioaddr + size;
@@ -99,5 +99,5 @@
 	 * Enable the range and we are done.
 	 */
-	bitmap_clear_range(&task->arch.iomap, (index_t) ioaddr, (count_t) size);
+	bitmap_clear_range(&task->arch.iomap, (size_t) ioaddr, (size_t) size);
 	
 	/*
@@ -118,9 +118,9 @@
 void io_perm_bitmap_install(void)
 {
-	count_t bits;
+	size_t bits;
 	ptr_16_64_t cpugdtr;
 	descriptor_t *gdt_p;
 	tss_descriptor_t *tss_desc;
-	count_t ver;
+	size_t ver;
 	
 	/* First, copy the I/O Permission Bitmap. */
Index: kernel/arch/amd64/src/interrupt.c
===================================================================
--- kernel/arch/amd64/src/interrupt.c	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/amd64/src/interrupt.c	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -102,5 +102,5 @@
 {
 	if (TASK) {
-		count_t ver;
+		size_t ver;
 
 		spinlock_lock(&TASK->lock);
Index: kernel/arch/arm32/include/mm/page.h
===================================================================
--- kernel/arch/arm32/include/mm/page.h	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/arm32/include/mm/page.h	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -95,5 +95,5 @@
 /* Get PTE flags accessors for each level. */
 #define GET_PTL1_FLAGS_ARCH(ptl0, i) \
-	get_pt_level0_flags((pte_level0_t *) (ptl0), (index_t) (i))
+	get_pt_level0_flags((pte_level0_t *) (ptl0), (size_t) (i))
 #define GET_PTL2_FLAGS_ARCH(ptl1, i) \
 	PAGE_PRESENT
@@ -101,13 +101,13 @@
 	PAGE_PRESENT
 #define GET_FRAME_FLAGS_ARCH(ptl3, i) \
-	get_pt_level1_flags((pte_level1_t *) (ptl3), (index_t) (i))
+	get_pt_level1_flags((pte_level1_t *) (ptl3), (size_t) (i))
 
 /* Set PTE flags accessors for each level. */
 #define SET_PTL1_FLAGS_ARCH(ptl0, i, x) \
-	set_pt_level0_flags((pte_level0_t *) (ptl0), (index_t) (i), (x))
+	set_pt_level0_flags((pte_level0_t *) (ptl0), (size_t) (i), (x))
 #define SET_PTL2_FLAGS_ARCH(ptl1, i, x)
 #define SET_PTL3_FLAGS_ARCH(ptl2, i, x)
 #define SET_FRAME_FLAGS_ARCH(ptl3, i, x) \
-	set_pt_level1_flags((pte_level1_t *) (ptl3), (index_t) (i), (x))
+	set_pt_level1_flags((pte_level1_t *) (ptl3), (size_t) (i), (x))
 
 /* Macros for querying the last-level PTE entries. */
@@ -205,5 +205,5 @@
  *  @param i      Index of the entry to return.
  */
-static inline int get_pt_level0_flags(pte_level0_t *pt, index_t i)
+static inline int get_pt_level0_flags(pte_level0_t *pt, size_t i)
 {
 	pte_level0_t *p = &pt[i];
@@ -220,5 +220,5 @@
  *  @param i      Index of the entry to return.
  */
-static inline int get_pt_level1_flags(pte_level1_t *pt, index_t i)
+static inline int get_pt_level1_flags(pte_level1_t *pt, size_t i)
 {
 	pte_level1_t *p = &pt[i];
@@ -245,5 +245,5 @@
  *  @param flags  new flags
  */
-static inline void set_pt_level0_flags(pte_level0_t *pt, index_t i, int flags)
+static inline void set_pt_level0_flags(pte_level0_t *pt, size_t i, int flags)
 {
 	pte_level0_t *p = &pt[i];
@@ -273,5 +273,5 @@
  *  @param flags  New flags.
  */  
-static inline void set_pt_level1_flags(pte_level1_t *pt, index_t i, int flags)
+static inline void set_pt_level1_flags(pte_level1_t *pt, size_t i, int flags)
 {
 	pte_level1_t *p = &pt[i];
Index: kernel/arch/arm32/include/types.h
===================================================================
--- kernel/arch/arm32/include/types.h	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/arm32/include/types.h	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -54,6 +54,4 @@
 
 typedef uint32_t size_t;
-typedef uint32_t count_t;
-typedef uint32_t index_t;
 
 typedef uint32_t uintptr_t;
@@ -70,6 +68,4 @@
 #define PRIp "x"	/**< Format for uintptr_t. */
 #define PRIs "u"	/**< Format for size_t. */
-#define PRIc "u"	/**< Format for count_t. */
-#define PRIi "u"	/**< Format for index_t. */
 
 #define PRId8 "d"	/**< Format for int8_t. */
Index: kernel/arch/arm32/src/mm/tlb.c
===================================================================
--- kernel/arch/arm32/src/mm/tlb.c	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/arm32/src/mm/tlb.c	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -81,5 +81,5 @@
  * @param cnt Number of entries to invalidate.
  */
-void tlb_invalidate_pages(asid_t asid __attribute__((unused)), uintptr_t page, count_t cnt)
+void tlb_invalidate_pages(asid_t asid __attribute__((unused)), uintptr_t page, size_t cnt)
 {
 	unsigned int i;
Index: kernel/arch/ia32/include/cpu.h
===================================================================
--- kernel/arch/ia32/include/cpu.h	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/ia32/include/cpu.h	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -58,5 +58,5 @@
 	tss_t *tss;
 	
-	count_t iomapver_copy;  /** Copy of TASK's I/O Permission bitmap generation count. */
+	size_t iomapver_copy;  /** Copy of TASK's I/O Permission bitmap generation count. */
 } cpu_arch_t;
 
Index: kernel/arch/ia32/include/mm/page.h
===================================================================
--- kernel/arch/ia32/include/mm/page.h	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/ia32/include/mm/page.h	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -96,5 +96,5 @@
 /* Get PTE flags accessors for each level. */
 #define GET_PTL1_FLAGS_ARCH(ptl0, i) \
-	get_pt_flags((pte_t *) (ptl0), (index_t) (i))
+	get_pt_flags((pte_t *) (ptl0), (size_t) (i))
 #define GET_PTL2_FLAGS_ARCH(ptl1, i) \
 	PAGE_PRESENT
@@ -102,13 +102,13 @@
 	PAGE_PRESENT
 #define GET_FRAME_FLAGS_ARCH(ptl3, i) \
-	get_pt_flags((pte_t *) (ptl3), (index_t) (i))
+	get_pt_flags((pte_t *) (ptl3), (size_t) (i))
 
 /* Set PTE flags accessors for each level. */
 #define SET_PTL1_FLAGS_ARCH(ptl0, i, x)	\
-	set_pt_flags((pte_t *) (ptl0), (index_t) (i), (x))
+	set_pt_flags((pte_t *) (ptl0), (size_t) (i), (x))
 #define SET_PTL2_FLAGS_ARCH(ptl1, i, x)
 #define SET_PTL3_FLAGS_ARCH(ptl2, i, x)
 #define SET_FRAME_FLAGS_ARCH(ptl3, i, x) \
-	set_pt_flags((pte_t *) (ptl3), (index_t) (i), (x))
+	set_pt_flags((pte_t *) (ptl3), (size_t) (i), (x))
 
 /* Macros for querying the last level entries. */
@@ -146,5 +146,5 @@
 #define PFERR_CODE_RSVD		(1 << 3)	
 
-static inline int get_pt_flags(pte_t *pt, index_t i)
+static inline int get_pt_flags(pte_t *pt, size_t i)
 {
 	pte_t *p = &pt[i];
@@ -159,5 +159,5 @@
 }
 
-static inline void set_pt_flags(pte_t *pt, index_t i, int flags)
+static inline void set_pt_flags(pte_t *pt, size_t i, int flags)
 {
 	pte_t *p = &pt[i];
Index: kernel/arch/ia32/include/proc/task.h
===================================================================
--- kernel/arch/ia32/include/proc/task.h	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/ia32/include/proc/task.h	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -41,5 +41,5 @@
 typedef struct {
 	/** I/O Permission bitmap Generation counter. */
-	count_t iomapver;
+	size_t iomapver;
 	/** I/O Permission bitmap. */
 	bitmap_t iomap;
Index: kernel/arch/ia32/include/smp/smp.h
===================================================================
--- kernel/arch/ia32/include/smp/smp.h	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/ia32/include/smp/smp.h	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -40,8 +40,8 @@
 /** SMP config opertaions interface. */
 struct smp_config_operations {
-	count_t (* cpu_count)(void);		/**< Return number of detected processors. */
-	bool (* cpu_enabled)(index_t i);	/**< Check whether the processor of index i is enabled. */
-	bool (*cpu_bootstrap)(index_t i);	/**< Check whether the processor of index i is BSP. */
-	uint8_t (*cpu_apic_id)(index_t i);		/**< Return APIC ID of the processor of index i. */
+	size_t (* cpu_count)(void);		/**< Return number of detected processors. */
+	bool (* cpu_enabled)(size_t i);	/**< Check whether the processor of index i is enabled. */
+	bool (*cpu_bootstrap)(size_t i);	/**< Check whether the processor of index i is BSP. */
+	uint8_t (*cpu_apic_id)(size_t i);		/**< Return APIC ID of the processor of index i. */
 	int (*irq_to_pin)(unsigned int irq);		/**< Return mapping between irq and APIC pin. */
 };
Index: kernel/arch/ia32/include/types.h
===================================================================
--- kernel/arch/ia32/include/types.h	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/ia32/include/types.h	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -47,6 +47,4 @@
 
 typedef uint32_t size_t;
-typedef uint32_t count_t;
-typedef uint32_t index_t;
 
 typedef uint32_t uintptr_t;
@@ -63,6 +61,4 @@
 #define PRIp "x"	/**< Format for uintptr_t. */
 #define PRIs "u"	/**< Format for size_t. */
-#define PRIc "u"	/**< Format for count_t. */
-#define PRIi "u"	/**< Format for index_t. */
 
 #define PRId8 "d"	/**< Format for int8_t. */
Index: kernel/arch/ia32/src/ddi/ddi.c
===================================================================
--- kernel/arch/ia32/src/ddi/ddi.c	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/ia32/src/ddi/ddi.c	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -58,5 +58,5 @@
 int ddi_iospace_enable_arch(task_t *task, uintptr_t ioaddr, size_t size)
 {
-	count_t bits;
+	size_t bits;
 
 	bits = ioaddr + size;
@@ -100,5 +100,5 @@
 	 * Enable the range and we are done.
 	 */
-	bitmap_clear_range(&task->arch.iomap, (index_t) ioaddr, (count_t) size);
+	bitmap_clear_range(&task->arch.iomap, (size_t) ioaddr, (size_t) size);
 
 	/*
@@ -119,8 +119,8 @@
 void io_perm_bitmap_install(void)
 {
-	count_t bits;
+	size_t bits;
 	ptr_16_32_t cpugdtr;
 	descriptor_t *gdt_p;
-	count_t ver;
+	size_t ver;
 
 	/* First, copy the I/O Permission Bitmap. */
Index: kernel/arch/ia32/src/interrupt.c
===================================================================
--- kernel/arch/ia32/src/interrupt.c	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/ia32/src/interrupt.c	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -102,5 +102,5 @@
 {
 	if (TASK) {
-		count_t ver;
+		size_t ver;
 		
 		spinlock_lock(&TASK->lock);
Index: kernel/arch/ia32/src/mm/frame.c
===================================================================
--- kernel/arch/ia32/src/mm/frame.c	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/ia32/src/mm/frame.c	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -71,5 +71,5 @@
 #endif
 		pfn_t pfn;
-		count_t count;
+		size_t count;
 		
 		if (e820table[i].type == MEMMAP_MEMORY_AVAILABLE) {
Index: kernel/arch/ia32/src/mm/tlb.c
===================================================================
--- kernel/arch/ia32/src/mm/tlb.c	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/ia32/src/mm/tlb.c	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -60,5 +60,5 @@
  * @param cnt Number of entries to invalidate.
  */
-void tlb_invalidate_pages(asid_t asid __attribute__((unused)), uintptr_t page, count_t cnt)
+void tlb_invalidate_pages(asid_t asid __attribute__((unused)), uintptr_t page, size_t cnt)
 {
 	unsigned int i;
Index: kernel/arch/ia32/src/smp/mps.c
===================================================================
--- kernel/arch/ia32/src/smp/mps.c	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/ia32/src/smp/mps.c	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -87,8 +87,8 @@
  * Implementation of IA-32 SMP configuration interface.
  */
-static count_t get_cpu_count(void);
-static bool is_cpu_enabled(index_t i);
-static bool is_bsp(index_t i);
-static uint8_t get_cpu_apic_id(index_t i);
+static size_t get_cpu_count(void);
+static bool is_cpu_enabled(size_t i);
+static bool is_bsp(size_t i);
+static uint8_t get_cpu_apic_id(size_t i);
 static int mps_irq_to_pin(unsigned int irq);
 
@@ -101,10 +101,10 @@
 };
 
-count_t get_cpu_count(void)
+size_t get_cpu_count(void)
 {
 	return processor_entry_cnt;
 }
 
-bool is_cpu_enabled(index_t i)
+bool is_cpu_enabled(size_t i)
 {
 	ASSERT(i < processor_entry_cnt);
@@ -112,5 +112,5 @@
 }
 
-bool is_bsp(index_t i)
+bool is_bsp(size_t i)
 {
 	ASSERT(i < processor_entry_cnt);
@@ -118,5 +118,5 @@
 }
 
-uint8_t get_cpu_apic_id(index_t i)
+uint8_t get_cpu_apic_id(size_t i)
 {
 	ASSERT(i < processor_entry_cnt);
Index: kernel/arch/ia64/include/mm/page.h
===================================================================
--- kernel/arch/ia64/include/mm/page.h	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/ia64/include/mm/page.h	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -241,5 +241,5 @@
  * @return Current contents of rr[i].
  */
-static inline uint64_t rr_read(index_t i)
+static inline uint64_t rr_read(size_t i)
 {
 	uint64_t ret;
@@ -254,5 +254,5 @@
  * @param v Value to be written to rr[i].
  */
-static inline void rr_write(index_t i, uint64_t v)
+static inline void rr_write(size_t i, uint64_t v)
 {
 	ASSERT(i < REGION_REGISTERS);
Index: kernel/arch/ia64/include/mm/tlb.h
===================================================================
--- kernel/arch/ia64/include/mm/tlb.h	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/ia64/include/mm/tlb.h	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -77,10 +77,10 @@
 extern void itc_mapping_insert(uintptr_t va, asid_t asid, tlb_entry_t entry);
 
-extern void tr_mapping_insert(uintptr_t va, asid_t asid, tlb_entry_t entry, bool dtr, index_t tr);
-extern void dtr_mapping_insert(uintptr_t va, asid_t asid, tlb_entry_t entry, index_t tr);
-extern void itr_mapping_insert(uintptr_t va, asid_t asid, tlb_entry_t entry, index_t tr);
+extern void tr_mapping_insert(uintptr_t va, asid_t asid, tlb_entry_t entry, bool dtr, size_t tr);
+extern void dtr_mapping_insert(uintptr_t va, asid_t asid, tlb_entry_t entry, size_t tr);
+extern void itr_mapping_insert(uintptr_t va, asid_t asid, tlb_entry_t entry, size_t tr);
 
-extern void dtlb_kernel_mapping_insert(uintptr_t page, uintptr_t frame, bool dtr, index_t tr);
-extern void dtr_purge(uintptr_t page, count_t width);
+extern void dtlb_kernel_mapping_insert(uintptr_t page, uintptr_t frame, bool dtr, size_t tr);
+extern void dtr_purge(uintptr_t page, size_t width);
 
 extern void dtc_pte_copy(pte_t *t);
Index: kernel/arch/ia64/include/types.h
===================================================================
--- kernel/arch/ia64/include/types.h	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/ia64/include/types.h	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -55,6 +55,4 @@
 
 typedef uint64_t size_t;
-typedef uint64_t count_t;
-typedef uint64_t index_t;
 
 typedef uint64_t uintptr_t;
@@ -73,6 +71,4 @@
 #define PRIp "lx"	/**< Format for uintptr_t. */
 #define PRIs "lu"	/**< Format for size_t. */
-#define PRIc "lu"	/**< Format for count_t. */
-#define PRIi "lu"	/**< Format for index_t. */
 
 #define PRId8 "d"	/**< Format for int8_t. */
Index: kernel/arch/ia64/src/mm/page.c
===================================================================
--- kernel/arch/ia64/src/mm/page.c	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/ia64/src/mm/page.c	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -132,5 +132,5 @@
 {
 	region_register rr_save, rr;
-	index_t vrn;
+	size_t vrn;
 	rid_t rid;
 	vhpt_entry_t *v;
@@ -177,5 +177,5 @@
 {
 	region_register rr_save, rr;	
-	index_t vrn;
+	size_t vrn;
 	rid_t rid;
 	bool match;
@@ -224,5 +224,5 @@
 {
 	region_register rr_save, rr;	
-	index_t vrn;
+	size_t vrn;
 	rid_t rid;
 	uint64_t tag;
Index: kernel/arch/ia64/src/mm/tlb.c
===================================================================
--- kernel/arch/ia64/src/mm/tlb.c	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/ia64/src/mm/tlb.c	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -101,5 +101,5 @@
 
 
-void tlb_invalidate_pages(asid_t asid, uintptr_t page, count_t cnt)
+void tlb_invalidate_pages(asid_t asid, uintptr_t page, size_t cnt)
 {
 	region_register rr;
@@ -268,5 +268,5 @@
  */
 void
-itr_mapping_insert(uintptr_t va, asid_t asid, tlb_entry_t entry, index_t tr)
+itr_mapping_insert(uintptr_t va, asid_t asid, tlb_entry_t entry, size_t tr)
 {
 	tr_mapping_insert(va, asid, entry, false, tr);
@@ -282,5 +282,5 @@
  */
 void
-dtr_mapping_insert(uintptr_t va, asid_t asid, tlb_entry_t entry, index_t tr)
+dtr_mapping_insert(uintptr_t va, asid_t asid, tlb_entry_t entry, size_t tr)
 {
 	tr_mapping_insert(va, asid, entry, true, tr);
@@ -299,5 +299,5 @@
 void
 tr_mapping_insert(uintptr_t va, asid_t asid, tlb_entry_t entry, bool dtr,
-    index_t tr)
+    size_t tr)
 {
 	region_register rr;
@@ -354,5 +354,5 @@
 void
 dtlb_kernel_mapping_insert(uintptr_t page, uintptr_t frame, bool dtr,
-    index_t tr)
+    size_t tr)
 {
 	tlb_entry_t entry;
@@ -383,5 +383,5 @@
  * @param width		Width of the purge in bits.
  */
-void dtr_purge(uintptr_t page, count_t width)
+void dtr_purge(uintptr_t page, size_t width)
 {
 	asm volatile ("ptr.d %0, %1\n" : : "r" (page), "r" (width << 2));
Index: kernel/arch/ia64/src/mm/vhpt.c
===================================================================
--- kernel/arch/ia64/src/mm/vhpt.c	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/ia64/src/mm/vhpt.c	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -54,5 +54,5 @@
 {
 	region_register rr_save, rr;
-	index_t vrn;
+	size_t vrn;
 	rid_t rid;
 	uint64_t tag;
Index: kernel/arch/mips32/include/arch.h
===================================================================
--- kernel/arch/mips32/include/arch.h	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/mips32/include/arch.h	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -43,5 +43,5 @@
 #include <typedefs.h>
 
-extern count_t cpu_count;
+extern size_t cpu_count;
 
 typedef struct {
Index: kernel/arch/mips32/include/debugger.h
===================================================================
--- kernel/arch/mips32/include/debugger.h	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/mips32/include/debugger.h	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -54,5 +54,5 @@
 	unative_t nextinstruction;  /**< Original instruction following break */
 	int flags;        /**< Flags regarding breakpoint */
-	count_t counter;
+	size_t counter;
 	void (*bkfunc)(void *b, istate_t *istate);
 } bpinfo_t;
Index: kernel/arch/mips32/include/mm/page.h
===================================================================
--- kernel/arch/mips32/include/mm/page.h	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/mips32/include/mm/page.h	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -113,5 +113,5 @@
 /* Get PTE flags accessors for each level. */
 #define GET_PTL1_FLAGS_ARCH(ptl0, i) \
-	get_pt_flags((pte_t *) (ptl0), (index_t) (i))
+	get_pt_flags((pte_t *) (ptl0), (size_t) (i))
 #define GET_PTL2_FLAGS_ARCH(ptl1, i) \
 	PAGE_PRESENT
@@ -119,13 +119,13 @@
 	PAGE_PRESENT
 #define GET_FRAME_FLAGS_ARCH(ptl3, i) \
-	get_pt_flags((pte_t *) (ptl3), (index_t) (i))
+	get_pt_flags((pte_t *) (ptl3), (size_t) (i))
 
 /* Set PTE flags accessors for each level. */
 #define SET_PTL1_FLAGS_ARCH(ptl0, i, x) \
-	set_pt_flags((pte_t *) (ptl0), (index_t) (i), (x))
+	set_pt_flags((pte_t *) (ptl0), (size_t) (i), (x))
 #define SET_PTL2_FLAGS_ARCH(ptl1, i, x)
 #define SET_PTL3_FLAGS_ARCH(ptl2, i, x)
 #define SET_FRAME_FLAGS_ARCH(ptl3, i, x) \
-	set_pt_flags((pte_t *) (ptl3), (index_t) (i), (x))
+	set_pt_flags((pte_t *) (ptl3), (size_t) (i), (x))
 
 /* Last-level info macros. */
@@ -141,5 +141,5 @@
 #include <arch/exception.h>
 
-static inline int get_pt_flags(pte_t *pt, index_t i)
+static inline int get_pt_flags(pte_t *pt, size_t i)
 {
 	pte_t *p = &pt[i];
@@ -154,5 +154,5 @@
 }
 
-static inline void set_pt_flags(pte_t *pt, index_t i, int flags)
+static inline void set_pt_flags(pte_t *pt, size_t i, int flags)
 {
 	pte_t *p = &pt[i];
Index: kernel/arch/mips32/include/types.h
===================================================================
--- kernel/arch/mips32/include/types.h	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/mips32/include/types.h	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -47,6 +47,4 @@
 
 typedef uint32_t size_t;
-typedef uint32_t count_t;
-typedef uint32_t index_t;
 
 typedef uint32_t uintptr_t;
@@ -63,6 +61,4 @@
 #define PRIp "x"	/**< Format for uintptr_t. */
 #define PRIs "u"	/**< Format for size_t. */
-#define PRIc "u"	/**< Format for count_t. */
-#define PRIi "u"	/**< Format for index_t. */
 
 #define PRId8 "d"	/**< Format for int8_t. */
Index: kernel/arch/mips32/src/mips32.c
===================================================================
--- kernel/arch/mips32/src/mips32.c	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/mips32/src/mips32.c	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -77,5 +77,5 @@
 uintptr_t supervisor_sp __attribute__ ((section (".text")));
 
-count_t cpu_count = 0;
+size_t cpu_count = 0;
 
 /** Performs mips32-specific initialization before main_bsp() is called. */
@@ -85,5 +85,5 @@
 	init.cnt = bootinfo->cnt;
 	
-	count_t i;
+	size_t i;
 	for (i = 0; i < min3(bootinfo->cnt, TASKMAP_MAX_RECORDS, CONFIG_INIT_TASKS); i++) {
 		init.tasks[i].addr = bootinfo->tasks[i].addr;
Index: kernel/arch/mips32/src/mm/frame.c
===================================================================
--- kernel/arch/mips32/src/mm/frame.c	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/mips32/src/mm/frame.c	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -63,5 +63,5 @@
 } phys_region_t;
 
-static count_t phys_regions_count = 0;
+static size_t phys_regions_count = 0;
 static phys_region_t phys_regions[MAX_REGIONS];
 
@@ -120,5 +120,5 @@
 	/* Init tasks */
 	bool safe = true;
-	count_t i;
+	size_t i;
 	for (i = 0; i < init.cnt; i++)
 		if (overlaps(frame << ZERO_PAGE_WIDTH, ZERO_PAGE_SIZE,
@@ -175,5 +175,5 @@
 	cp0_entry_hi_write(0);
 
-	count_t i;
+	size_t i;
 	for (i = 0; i < TLB_ENTRY_COUNT; i++) {
 		cp0_index_write(i);
@@ -252,5 +252,5 @@
 	printf("---------- ----------\n");
 	
-	count_t i;
+	size_t i;
 	for (i = 0; i < phys_regions_count; i++) {
 		printf("%#010x %10u\n",
Index: kernel/arch/mips32/src/mm/tlb.c
===================================================================
--- kernel/arch/mips32/src/mm/tlb.c	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/mips32/src/mm/tlb.c	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -561,5 +561,5 @@
  * @param cnt		Number of entries to invalidate.
  */
-void tlb_invalidate_pages(asid_t asid, uintptr_t page, count_t cnt)
+void tlb_invalidate_pages(asid_t asid, uintptr_t page, size_t cnt)
 {
 	unsigned int i;
Index: kernel/arch/ppc32/include/mm/page.h
===================================================================
--- kernel/arch/ppc32/include/mm/page.h	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/ppc32/include/mm/page.h	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -103,5 +103,5 @@
 /* Get PTE flags accessors for each level. */
 #define GET_PTL1_FLAGS_ARCH(ptl0, i) \
-	get_pt_flags((pte_t *) (ptl0), (index_t) (i))
+	get_pt_flags((pte_t *) (ptl0), (size_t) (i))
 #define GET_PTL2_FLAGS_ARCH(ptl1, i) \
 	PAGE_PRESENT
@@ -109,13 +109,13 @@
 	PAGE_PRESENT
 #define GET_FRAME_FLAGS_ARCH(ptl3, i) \
-	get_pt_flags((pte_t *) (ptl3), (index_t) (i))
+	get_pt_flags((pte_t *) (ptl3), (size_t) (i))
 
 /* Set PTE flags accessors for each level. */
 #define SET_PTL1_FLAGS_ARCH(ptl0, i, x)	\
-	set_pt_flags((pte_t *) (ptl0), (index_t) (i), (x))
+	set_pt_flags((pte_t *) (ptl0), (size_t) (i), (x))
 #define SET_PTL2_FLAGS_ARCH(ptl1, i, x)
 #define SET_PTL3_FLAGS_ARCH(ptl2, i, x)
 #define SET_FRAME_FLAGS_ARCH(ptl3, i, x) \
-	set_pt_flags((pte_t *) (ptl3), (index_t) (i), (x))
+	set_pt_flags((pte_t *) (ptl3), (size_t) (i), (x))
 
 /* Macros for querying the last-level PTEs. */
@@ -131,5 +131,5 @@
 #include <arch/interrupt.h>
 
-static inline int get_pt_flags(pte_t *pt, index_t i)
+static inline int get_pt_flags(pte_t *pt, size_t i)
 {
 	pte_t *p = &pt[i];
@@ -144,5 +144,5 @@
 }
 
-static inline void set_pt_flags(pte_t *pt, index_t i, int flags)
+static inline void set_pt_flags(pte_t *pt, size_t i, int flags)
 {
 	pte_t *p = &pt[i];
Index: kernel/arch/ppc32/include/types.h
===================================================================
--- kernel/arch/ppc32/include/types.h	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/ppc32/include/types.h	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -47,6 +47,4 @@
 
 typedef uint32_t size_t;
-typedef uint32_t count_t;
-typedef uint32_t index_t;
 
 typedef uint32_t uintptr_t;
@@ -61,9 +59,7 @@
 } fncptr_t;
 
-/**< Formats for uintptr_t, size_t, count_t and index_t */
+/**< Formats for uintptr_t, size_t */
 #define PRIp "x"
 #define PRIs "u"
-#define PRIc "u"
-#define PRIi "u"
 
 /**< Formats for (u)int8_t, (u)int16_t, (u)int32_t, (u)int64_t and (u)native_t */
Index: kernel/arch/ppc32/src/mm/frame.c
===================================================================
--- kernel/arch/ppc32/src/mm/frame.c	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/ppc32/src/mm/frame.c	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -58,5 +58,5 @@
 {
 	pfn_t minconf = 2;
-	count_t i;
+	size_t i;
 	pfn_t start, conf;
 	size_t size;
Index: kernel/arch/ppc32/src/mm/tlb.c
===================================================================
--- kernel/arch/ppc32/src/mm/tlb.c	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/ppc32/src/mm/tlb.c	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -550,5 +550,5 @@
 
 
-void tlb_invalidate_pages(asid_t asid, uintptr_t page, count_t cnt)
+void tlb_invalidate_pages(asid_t asid, uintptr_t page, size_t cnt)
 {
 	// TODO
Index: kernel/arch/sparc64/include/mm/tlb.h
===================================================================
--- kernel/arch/sparc64/include/mm/tlb.h	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/sparc64/include/mm/tlb.h	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -323,5 +323,5 @@
  * 			Register.
  */
-static inline uint64_t itlb_data_access_read(index_t entry)
+static inline uint64_t itlb_data_access_read(size_t entry)
 {
 	itlb_data_access_addr_t reg;
@@ -337,5 +337,5 @@
  * @param value		Value to be written.
  */
-static inline void itlb_data_access_write(index_t entry, uint64_t value)
+static inline void itlb_data_access_write(size_t entry, uint64_t value)
 {
 	itlb_data_access_addr_t reg;
@@ -354,5 +354,5 @@
  * 			Register.
  */
-static inline uint64_t dtlb_data_access_read(index_t entry)
+static inline uint64_t dtlb_data_access_read(size_t entry)
 {
 	dtlb_data_access_addr_t reg;
@@ -368,5 +368,5 @@
  * @param value		Value to be written.
  */
-static inline void dtlb_data_access_write(index_t entry, uint64_t value)
+static inline void dtlb_data_access_write(size_t entry, uint64_t value)
 {
 	dtlb_data_access_addr_t reg;
@@ -384,5 +384,5 @@
  * @return		Current value of specified IMMU TLB Tag Read Register.
  */
-static inline uint64_t itlb_tag_read_read(index_t entry)
+static inline uint64_t itlb_tag_read_read(size_t entry)
 {
 	itlb_tag_read_addr_t tag;
@@ -399,5 +399,5 @@
  * @return		Current value of specified DMMU TLB Tag Read Register.
  */
-static inline uint64_t dtlb_tag_read_read(index_t entry)
+static inline uint64_t dtlb_tag_read_read(size_t entry)
 {
 	dtlb_tag_read_addr_t tag;
@@ -419,5 +419,5 @@
  * 			Register.
  */
-static inline uint64_t itlb_data_access_read(int tlb, index_t entry)
+static inline uint64_t itlb_data_access_read(int tlb, size_t entry)
 {
 	itlb_data_access_addr_t reg;
@@ -434,5 +434,5 @@
  * @param value		Value to be written.
  */
-static inline void itlb_data_access_write(int tlb, index_t entry,
+static inline void itlb_data_access_write(int tlb, size_t entry,
 	uint64_t value)
 {
@@ -454,5 +454,5 @@
  * 			Register.
  */
-static inline uint64_t dtlb_data_access_read(int tlb, index_t entry)
+static inline uint64_t dtlb_data_access_read(int tlb, size_t entry)
 {
 	dtlb_data_access_addr_t reg;
@@ -470,5 +470,5 @@
  * @param value		Value to be written.
  */
-static inline void dtlb_data_access_write(int tlb, index_t entry,
+static inline void dtlb_data_access_write(int tlb, size_t entry,
 	uint64_t value)
 {
@@ -489,5 +489,5 @@
  * @return		Current value of specified IMMU TLB Tag Read Register.
  */
-static inline uint64_t itlb_tag_read_read(int tlb, index_t entry)
+static inline uint64_t itlb_tag_read_read(int tlb, size_t entry)
 {
 	itlb_tag_read_addr_t tag;
@@ -506,5 +506,5 @@
  * @return		Current value of specified DMMU TLB Tag Read Register.
  */
-static inline uint64_t dtlb_tag_read_read(int tlb, index_t entry)
+static inline uint64_t dtlb_tag_read_read(int tlb, size_t entry)
 {
 	dtlb_tag_read_addr_t tag;
Index: kernel/arch/sparc64/include/mm/tsb.h
===================================================================
--- kernel/arch/sparc64/include/mm/tsb.h	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/sparc64/include/mm/tsb.h	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -161,7 +161,7 @@
 struct pte;
 
-extern void tsb_invalidate(struct as *as, uintptr_t page, count_t pages);
-extern void itsb_pte_copy(struct pte *t, index_t index);
-extern void dtsb_pte_copy(struct pte *t, index_t index, bool ro);
+extern void tsb_invalidate(struct as *as, uintptr_t page, size_t pages);
+extern void itsb_pte_copy(struct pte *t, size_t index);
+extern void dtsb_pte_copy(struct pte *t, size_t index, bool ro);
 
 #endif /* !def __ASM__ */
Index: kernel/arch/sparc64/include/types.h
===================================================================
--- kernel/arch/sparc64/include/types.h	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/sparc64/include/types.h	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -47,6 +47,4 @@
 
 typedef uint64_t size_t;
-typedef uint64_t count_t;
-typedef uint64_t index_t;
 
 typedef uint64_t uintptr_t;
@@ -61,9 +59,7 @@
 } fncptr_t;
 
-/**< Formats for uintptr_t, size_t, count_t and index_t */
+/**< Formats for uintptr_t, size_t */
 #define PRIp "llx"
 #define PRIs "llu"
-#define PRIc "llu"
-#define PRIi "llu"
 
 /**< Formats for (u)int8_t, (u)int16_t, (u)int32_t, (u)int64_t and (u)native_t */
Index: kernel/arch/sparc64/src/drivers/fhc.c
===================================================================
--- kernel/arch/sparc64/src/drivers/fhc.c	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/sparc64/src/drivers/fhc.c	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -72,5 +72,5 @@
 		return NULL;
 		
-	count_t regs = prop->size / sizeof(ofw_central_reg_t);
+	size_t regs = prop->size / sizeof(ofw_central_reg_t);
 	if (regs + 1 < UART_IMAP_REG)
 		return NULL;
Index: kernel/arch/sparc64/src/drivers/pci.c
===================================================================
--- kernel/arch/sparc64/src/drivers/pci.c	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/sparc64/src/drivers/pci.c	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -92,5 +92,5 @@
 
 	ofw_upa_reg_t *reg = prop->value;
-	count_t regs = prop->size / sizeof(ofw_upa_reg_t);
+	size_t regs = prop->size / sizeof(ofw_upa_reg_t);
 
 	if (regs < SABRE_INTERNAL_REG + 1)
@@ -139,5 +139,5 @@
 
 	ofw_upa_reg_t *reg = prop->value;
-	count_t regs = prop->size / sizeof(ofw_upa_reg_t);
+	size_t regs = prop->size / sizeof(ofw_upa_reg_t);
 
 	if (regs < PSYCHO_INTERNAL_REG + 1)
Index: kernel/arch/sparc64/src/mm/as.c
===================================================================
--- kernel/arch/sparc64/src/mm/as.c	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/sparc64/src/mm/as.c	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -90,5 +90,5 @@
 	 * size.
 	 */
-	count_t cnt = ((ITSB_ENTRY_COUNT + DTSB_ENTRY_COUNT) *
+	size_t cnt = ((ITSB_ENTRY_COUNT + DTSB_ENTRY_COUNT) *
 	    sizeof(tsb_entry_t)) >> FRAME_WIDTH;
 	frame_free(KA2PA((uintptr_t) as->arch.itsb));
@@ -102,5 +102,5 @@
 {
 #ifdef CONFIG_TSB
-	tsb_invalidate(as, 0, (count_t) -1);
+	tsb_invalidate(as, 0, (size_t) -1);
 #endif
 	return 0;
Index: kernel/arch/sparc64/src/mm/tlb.c
===================================================================
--- kernel/arch/sparc64/src/mm/tlb.c	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/sparc64/src/mm/tlb.c	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -55,6 +55,6 @@
 #endif
 
-static void dtlb_pte_copy(pte_t *, index_t, bool);
-static void itlb_pte_copy(pte_t *, index_t);
+static void dtlb_pte_copy(pte_t *, size_t, bool);
+static void itlb_pte_copy(pte_t *, size_t);
 static void do_fast_instruction_access_mmu_miss_fault(istate_t *, const char *);
 static void do_fast_data_access_mmu_miss_fault(istate_t *, tlb_tag_access_reg_t,
@@ -131,5 +131,5 @@
  * 			of its w field.
  */
-void dtlb_pte_copy(pte_t *t, index_t index, bool ro)
+void dtlb_pte_copy(pte_t *t, size_t index, bool ro)
 {
 	tlb_tag_access_reg_t tag;
@@ -168,5 +168,5 @@
  * @param index		Zero if lower 8K-subpage, one if higher 8K-subpage.
  */
-void itlb_pte_copy(pte_t *t, index_t index)
+void itlb_pte_copy(pte_t *t, size_t index)
 {
 	tlb_tag_access_reg_t tag;
@@ -201,5 +201,5 @@
 {
 	uintptr_t page_16k = ALIGN_DOWN(istate->tpc, PAGE_SIZE);
-	index_t index = (istate->tpc >> MMU_PAGE_WIDTH) % MMU_PAGES_PER_PAGE;
+	size_t index = (istate->tpc >> MMU_PAGE_WIDTH) % MMU_PAGES_PER_PAGE;
 	pte_t *t;
 
@@ -246,5 +246,5 @@
 	uintptr_t page_8k;
 	uintptr_t page_16k;
-	index_t index;
+	size_t index;
 	pte_t *t;
 
@@ -310,5 +310,5 @@
 {
 	uintptr_t page_16k;
-	index_t index;
+	size_t index;
 	pte_t *t;
 
@@ -580,5 +580,5 @@
  * @param cnt		Number of ITLB and DTLB entries to invalidate.
  */
-void tlb_invalidate_pages(asid_t asid, uintptr_t page, count_t cnt)
+void tlb_invalidate_pages(asid_t asid, uintptr_t page, size_t cnt)
 {
 	unsigned int i;
Index: kernel/arch/sparc64/src/mm/tsb.c
===================================================================
--- kernel/arch/sparc64/src/mm/tsb.c	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/sparc64/src/mm/tsb.c	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -51,11 +51,12 @@
  * @param as Address space.
  * @param page First page to invalidate in TSB.
- * @param pages Number of pages to invalidate. Value of (count_t) -1 means the
+ * @param pages Number of pages to invalidate. Value of (size_t) -1 means the
  * 	whole TSB.
  */
-void tsb_invalidate(as_t *as, uintptr_t page, count_t pages)
+void tsb_invalidate(as_t *as, uintptr_t page, size_t pages)
 {
-	index_t i0, i;
-	count_t cnt;
+	size_t i0;
+	size_t i;
+	size_t cnt;
 	
 	ASSERT(as->arch.itsb && as->arch.dtsb);
@@ -64,5 +65,5 @@
 	ASSERT(i0 < ITSB_ENTRY_COUNT && i0 < DTSB_ENTRY_COUNT);
 
-	if (pages == (count_t) -1 || (pages * 2) > ITSB_ENTRY_COUNT)
+	if (pages == (size_t) -1 || (pages * 2) > ITSB_ENTRY_COUNT)
 		cnt = ITSB_ENTRY_COUNT;
 	else
@@ -82,9 +83,9 @@
  * @param index	Zero if lower 8K-subpage, one if higher 8K subpage.
  */
-void itsb_pte_copy(pte_t *t, index_t index)
+void itsb_pte_copy(pte_t *t, size_t index)
 {
 	as_t *as;
 	tsb_entry_t *tsb;
-	index_t entry;
+	size_t entry;
 
 	ASSERT(index <= 1);
@@ -128,9 +129,9 @@
  * @param ro	If true, the mapping is copied read-only.
  */
-void dtsb_pte_copy(pte_t *t, index_t index, bool ro)
+void dtsb_pte_copy(pte_t *t, size_t index, bool ro)
 {
 	as_t *as;
 	tsb_entry_t *tsb;
-	index_t entry;
+	size_t entry;
 	
 	ASSERT(index <= 1);
Index: kernel/arch/sparc64/src/smp/smp.c
===================================================================
--- kernel/arch/sparc64/src/smp/smp.c	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/sparc64/src/smp/smp.c	(revision 080ad7fcf59dd514b2dceeb65a63f76c705addac)
@@ -62,5 +62,5 @@
 {
 	ofw_tree_node_t *node;
-	count_t cnt = 0;
+	size_t cnt = 0;
 	
 	if (is_us() || is_us_iii()) {