Index: kernel/arch/ia32/include/cpu.h
===================================================================
--- kernel/arch/ia32/include/cpu.h	(revision c00589d744b4c2f8becc2dd1223b865d10f1e238)
+++ kernel/arch/ia32/include/cpu.h	(revision 99272a380ff885480a8f252b2e013a3ef7216b14)
@@ -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 99272a380ff885480a8f252b2e013a3ef7216b14)
@@ -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 99272a380ff885480a8f252b2e013a3ef7216b14)
@@ -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 99272a380ff885480a8f252b2e013a3ef7216b14)
@@ -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 99272a380ff885480a8f252b2e013a3ef7216b14)
@@ -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 99272a380ff885480a8f252b2e013a3ef7216b14)
@@ -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 99272a380ff885480a8f252b2e013a3ef7216b14)
@@ -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 99272a380ff885480a8f252b2e013a3ef7216b14)
@@ -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 99272a380ff885480a8f252b2e013a3ef7216b14)
@@ -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 99272a380ff885480a8f252b2e013a3ef7216b14)
@@ -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);