diff --git a/arch/x86/kernel/cpu.c b/arch/x86/kernel/cpu.c
index c5857dea..1eaedd0c 100644
--- a/arch/x86/kernel/cpu.c
+++ b/arch/x86/kernel/cpu.c
@@ -443,14 +443,14 @@ void set_signal(int sig, void *regs, struct siginfo *info);
 void check_signal(unsigned long rc, void *regs);
 extern void tlb_flush_handler(int vector);
 
-void handle_interrupt(int vector, struct x86_regs *regs)
+void handle_interrupt(int vector, struct x86_user_context *regs)
 {
 	struct ihk_mc_interrupt_handler *h;
 
 	lapic_ack();
 
 	dkprintf("CPU[%d] got interrupt, vector: %d, RIP: 0x%lX\n", 
-	         ihk_mc_get_processor_id(), vector, regs->rip);
+	         ihk_mc_get_processor_id(), vector, regs->gpr.rip);
 
 	if (vector < 0 || vector > 255) {
 		panic("Invalid interrupt vector.");
@@ -462,7 +462,7 @@ void handle_interrupt(int vector, struct x86_regs *regs)
 			memset(&info, '\0', sizeof info);
 			info.si_signo = SIGFPE;
 			info.si_code = FPE_INTDIV;
-			info._sifields._sigfault.si_addr = (void *)regs->rip;
+			info._sifields._sigfault.si_addr = (void *)regs->gpr.rip;
 			set_signal(SIGFPE, regs, &info);
 			break;
 		    case 9:
@@ -478,7 +478,7 @@ void handle_interrupt(int vector, struct x86_regs *regs)
 			memset(&info, '\0', sizeof info);
 			info.si_signo = SIGILL;
 			info.si_code = ILL_ILLOPN;
-			info._sifields._sigfault.si_addr = (void *)regs->rip;
+			info._sifields._sigfault.si_addr = (void *)regs->gpr.rip;
 			set_signal(SIGILL, regs, &info);
 			break;
 		    case 10:
@@ -496,7 +496,7 @@ void handle_interrupt(int vector, struct x86_regs *regs)
 			break;
 		    default:
 			kprintf("Exception %d, rflags: 0x%lX CS: 0x%lX, RIP: 0x%lX\n",
-			        vector, regs->rflags, regs->cs, regs->rip);
+			        vector, regs->gpr.rflags, regs->gpr.cs, regs->gpr.rip);
 			arch_show_interrupt_context(regs);
 			panic("Unhandled exception");
 		}
@@ -518,10 +518,10 @@ void handle_interrupt(int vector, struct x86_regs *regs)
 	check_need_resched();
 }
 
-void gpe_handler(struct x86_regs *regs)
+void gpe_handler(struct x86_user_context *regs)
 {
 	kprintf("General protection fault (err: %lx, %lx:%lx)\n",
-	        regs->error, regs->cs, regs->rip);
+	        regs->gpr.error, regs->gpr.cs, regs->gpr.rip);
 	arch_show_interrupt_context(regs);
 	set_signal(SIGSEGV, regs, NULL);
 	check_signal(0, regs);
@@ -529,7 +529,7 @@ void gpe_handler(struct x86_regs *regs)
 	// panic("GPF");
 }
 
-void debug_handler(struct x86_regs *regs)
+void debug_handler(struct x86_user_context *regs)
 {
 	unsigned long db6;
 	int si_code = 0;
@@ -543,7 +543,7 @@ void debug_handler(struct x86_regs *regs)
 
 	asm("mov %%db6, %0" :"=r" (db6));
 	if (db6 & DB6_BS) {
-	        regs->rflags &= ~RFLAGS_TF;
+	        regs->gpr.rflags &= ~RFLAGS_TF;
 		si_code = TRAP_TRACE;
 	} else if (db6 & (DB6_B3|DB6_B2|DB6_B1|DB6_B0)) {
 		si_code = TRAP_HWBKPT;
@@ -556,7 +556,7 @@ void debug_handler(struct x86_regs *regs)
 	check_need_resched();
 }
 
-void int3_handler(struct x86_regs *regs)
+void int3_handler(struct x86_user_context *regs)
 {
 	struct siginfo info;
 
@@ -758,11 +758,11 @@ void ihk_mc_init_user_process(ihk_mc_kernel_context_t *ctx,
 	*puctx = uctx;
 
 	memset(uctx, 0, sizeof(ihk_mc_user_context_t));
-	uctx->cs = USER_CS;
-	uctx->rip = new_pc;
-	uctx->ss = USER_DS;
-	uctx->rsp = user_sp;
-	uctx->rflags = RFLAGS_IF;
+	uctx->gpr.cs = USER_CS;
+	uctx->gpr.rip = new_pc;
+	uctx->gpr.ss = USER_DS;
+	uctx->gpr.rsp = user_sp;
+	uctx->gpr.rflags = RFLAGS_IF;
 
 	ihk_mc_init_context(ctx, sp, (void (*)(void))enter_user_mode);
 	ctx->rsp0 = (unsigned long)stack_pointer;
@@ -773,18 +773,18 @@ void ihk_mc_modify_user_context(ihk_mc_user_context_t *uctx,
                                 unsigned long value)
 {
 	if (reg == IHK_UCR_STACK_POINTER) {
-		uctx->rsp = value;
+		uctx->gpr.rsp = value;
 	} else if (reg == IHK_UCR_PROGRAM_COUNTER) {
-		uctx->rip = value;
+		uctx->gpr.rip = value;
 	}
 }
 
 void ihk_mc_print_user_context(ihk_mc_user_context_t *uctx)
 {
-	kprintf("CS:RIP = %04lx:%16lx\n", uctx->cs, uctx->rip);
+	kprintf("CS:RIP = %04lx:%16lx\n", uctx->gpr.cs, uctx->gpr.rip);
 	kprintf("%16lx %16lx %16lx %16lx\n%16lx %16lx %16lx\n",
-	        uctx->rax, uctx->rbx, uctx->rcx, uctx->rdx,
-	        uctx->rsi, uctx->rdi, uctx->rsp);
+	        uctx->gpr.rax, uctx->gpr.rbx, uctx->gpr.rcx, uctx->gpr.rdx,
+	        uctx->gpr.rsi, uctx->gpr.rdi, uctx->gpr.rsp);
 }
 
 void ihk_mc_set_syscall_handler(long (*handler)(int, ihk_mc_user_context_t *))
@@ -823,7 +823,8 @@ void arch_show_extended_context(void)
 
 void arch_show_interrupt_context(const void *reg)
 {
-	const struct x86_regs *regs = reg;
+	const struct x86_user_context *uctx = reg;
+	const struct x86_basic_regs *regs = &uctx->gpr;
 	unsigned long irqflags;
 
 	irqflags = kprintf_lock();
diff --git a/arch/x86/kernel/gencore.c b/arch/x86/kernel/gencore.c
index 24a6a4f9..472b5844 100644
--- a/arch/x86/kernel/gencore.c
+++ b/arch/x86/kernel/gencore.c
@@ -86,7 +86,8 @@ void fill_prstatus(struct note *head, struct process *proc, void *regs0)
 {
 	void *name;
 	struct elf_prstatus64 *prstatus; 
-	struct x86_regs *regs = regs0;
+	struct x86_user_context *uctx = regs0;
+	struct x86_basic_regs *regs = &uctx->gpr;
         register unsigned long _r12 asm("r12");
         register unsigned long _r13 asm("r13");
         register unsigned long _r14 asm("r14");
diff --git a/arch/x86/kernel/include/ihk/context.h b/arch/x86/kernel/include/ihk/context.h
index ff51d7d6..22448e66 100644
--- a/arch/x86/kernel/include/ihk/context.h
+++ b/arch/x86/kernel/include/ihk/context.h
@@ -22,19 +22,23 @@ struct x86_kregs {
 };
 
 typedef struct x86_kregs ihk_mc_kernel_context_t;
+
 /* XXX: User context should contain floating point registers */
-typedef struct x86_regs ihk_mc_user_context_t;
+struct x86_user_context {
+	struct x86_basic_regs gpr;
+};
+typedef struct x86_user_context ihk_mc_user_context_t;
 
-#define ihk_mc_syscall_arg0(uc) (uc)->rdi
-#define ihk_mc_syscall_arg1(uc) (uc)->rsi
-#define ihk_mc_syscall_arg2(uc) (uc)->rdx
-#define ihk_mc_syscall_arg3(uc) (uc)->r10
-#define ihk_mc_syscall_arg4(uc) (uc)->r8
-#define ihk_mc_syscall_arg5(uc) (uc)->r9
+#define ihk_mc_syscall_arg0(uc) (uc)->gpr.rdi
+#define ihk_mc_syscall_arg1(uc) (uc)->gpr.rsi
+#define ihk_mc_syscall_arg2(uc) (uc)->gpr.rdx
+#define ihk_mc_syscall_arg3(uc) (uc)->gpr.r10
+#define ihk_mc_syscall_arg4(uc) (uc)->gpr.r8
+#define ihk_mc_syscall_arg5(uc) (uc)->gpr.r9
 
-#define ihk_mc_syscall_ret(uc)  (uc)->rax
+#define ihk_mc_syscall_ret(uc)  (uc)->gpr.rax
 
-#define ihk_mc_syscall_pc(uc)   (uc)->rip
-#define ihk_mc_syscall_sp(uc)   (uc)->rsp
+#define ihk_mc_syscall_pc(uc)   (uc)->gpr.rip
+#define ihk_mc_syscall_sp(uc)   (uc)->gpr.rsp
 
 #endif
diff --git a/arch/x86/kernel/include/registers.h b/arch/x86/kernel/include/registers.h
index 505c7592..461db363 100644
--- a/arch/x86/kernel/include/registers.h
+++ b/arch/x86/kernel/include/registers.h
@@ -178,7 +178,7 @@ struct tss64 {
         unsigned short iomap_address;
 } __attribute__((packed));
 
-struct x86_regs {
+struct x86_basic_regs {
 	unsigned long r15, r14, r13, r12, r11, r10, r9, r8;
 	unsigned long rdi, rsi, rdx, rcx, rbx, rax, rbp;
 	unsigned long error, rip, cs, rflags, rsp, ss;
diff --git a/arch/x86/kernel/syscall.c b/arch/x86/kernel/syscall.c
index d07305e9..a73b9a59 100644
--- a/arch/x86/kernel/syscall.c
+++ b/arch/x86/kernel/syscall.c
@@ -132,7 +132,7 @@ fault:
 }
 
 struct sigsp {
-	struct x86_regs regs;
+	struct x86_user_context regs;
 	unsigned long sigrc;
 	unsigned long sigmask;
 	int ssflags;
@@ -142,17 +142,17 @@ struct sigsp {
 SYSCALL_DECLARE(rt_sigreturn)
 {
 	struct process *proc = cpu_local_var(current);
-	struct x86_regs *regs;
+	struct x86_user_context *regs;
 	struct sigsp *sigsp;
 	long rc = -EFAULT;
 
 	asm("movq %%gs:132, %0" : "=r" (regs));
 	--regs;
 
-	sigsp = (struct sigsp *)regs->rsp;
+	sigsp = (struct sigsp *)regs->gpr.rsp;
 	proc->sigmask.__val[0] = sigsp->sigmask;
 	proc->sigstack.ss_flags = sigsp->ssflags;
-	if(copy_from_user(proc, regs, &sigsp->regs, sizeof(struct x86_regs)))
+	if(copy_from_user(proc, regs, &sigsp->regs, sizeof(struct x86_user_context)))
 		return rc;
 	copy_from_user(proc, &rc, &sigsp->sigrc, sizeof(long));
 	return rc;
@@ -193,7 +193,7 @@ do_setpgid(int pid, int pgid)
 
 static unsigned long *ptrace_get_regaddr(struct process *proc, long addr)
 {
-#define PTRACE_GET_REGADDR(regname) case offsetof(struct user_regs_struct, regname): return &(proc->uctx->regname)
+#define PTRACE_GET_REGADDR(regname) case offsetof(struct user_regs_struct, regname): return &(proc->uctx->gpr.regname)
 	switch (addr) {
 		PTRACE_GET_REGADDR(r15);
 		PTRACE_GET_REGADDR(r14);
@@ -240,7 +240,7 @@ ptrace_read_user(struct process *proc, long addr, unsigned long *value)
 	if (addr < sizeof(struct user_regs_struct)) {
 		if (addr & (sizeof(*value) - 1)) return -EIO;
 		if (addr == offsetof(struct user_regs_struct, eflags)) {
-			*value = proc->uctx->rflags;
+			*value = proc->uctx->gpr.rflags;
 			return 0;
 		}
 		if (addr == offsetof(struct user_regs_struct, fs_base)) {
@@ -282,8 +282,8 @@ ptrace_write_user(struct process *proc, long addr, unsigned long value)
 	if (addr < sizeof(struct user_regs_struct)) {
 		if (addr & (sizeof(value) - 1)) return -EIO;
 		if (addr == offsetof(struct user_regs_struct, eflags)) {
-			proc->uctx->rflags &= ~RFLAGS_MASK;
-			proc->uctx->rflags |= (value & RFLAGS_MASK);
+			proc->uctx->gpr.rflags &= ~RFLAGS_MASK;
+			proc->uctx->gpr.rflags |= (value & RFLAGS_MASK);
 			return 0;
 		}
 		if (addr == offsetof(struct user_regs_struct, fs_base)) {
@@ -382,12 +382,12 @@ clear_debugreg(void)
 
 void clear_single_step(struct process *proc)
 {
-	proc->uctx->rflags &= ~RFLAGS_TF;
+	proc->uctx->gpr.rflags &= ~RFLAGS_TF;
 }
 
 void set_single_step(struct process *proc)
 {
-	proc->uctx->rflags |= RFLAGS_TF;
+	proc->uctx->gpr.rflags |= RFLAGS_TF;
 }
 
 extern void coredump(struct process *proc, void *regs);
@@ -441,7 +441,7 @@ void ptrace_report_signal(struct process *proc, int sig)
 void
 do_signal(unsigned long rc, void *regs0, struct process *proc, struct sig_pending *pending)
 {
-	struct x86_regs *regs = regs0;
+	struct x86_user_context *regs = regs0;
 	struct k_sigaction *k;
 	int	sig;
 	__sigset_t w;
@@ -466,7 +466,7 @@ do_signal(unsigned long rc, void *regs0, struct process *proc, struct sig_pendin
 		--regs;
 	}
 	else{
-		rc = regs->rax;
+		rc = regs->gpr.rax;
 	}
 
 	irqstate = ihk_mc_spinlock_lock(&proc->sighandler->lock);
@@ -492,16 +492,16 @@ do_signal(unsigned long rc, void *regs0, struct process *proc, struct sig_pendin
 			proc->sigstack.ss_flags |= SS_ONSTACK;
 		}
 		else{
-			usp = (unsigned long *)regs->rsp;
+			usp = (unsigned long *)regs->gpr.rsp;
 		}
 		sigsp = ((struct sigsp *)usp) - 1;
 		sigsp = (struct sigsp *)((unsigned long)sigsp & 0xfffffffffffffff0UL);
-		if(copy_to_user(proc, &sigsp->regs, regs, sizeof(struct x86_regs)) ||
+		if(copy_to_user(proc, &sigsp->regs, regs, sizeof(struct x86_user_context)) ||
 		   copy_to_user(proc, &sigsp->sigrc, &rc, sizeof(long))){
 			kfree(pending);
 			ihk_mc_spinlock_unlock(&proc->sighandler->lock, irqstate);
 			kprintf("do_signal,copy_to_user failed\n");
-			terminate(0, sig, (ihk_mc_user_context_t *)regs->rsp);
+			terminate(0, sig, (ihk_mc_user_context_t *)regs->gpr.rsp);
 			return;
 		}
 		sigsp->sigmask = mask;
@@ -512,13 +512,13 @@ do_signal(unsigned long rc, void *regs0, struct process *proc, struct sig_pendin
 		usp--;
 		*usp = (unsigned long)k->sa.sa_restorer;
 
-		regs->rdi = (unsigned long)sig;
+		regs->gpr.rdi = (unsigned long)sig;
 		if(k->sa.sa_flags & SA_SIGINFO){
-			regs->rsi = (unsigned long)&sigsp->info;
-			regs->rdx = 0;
+			regs->gpr.rsi = (unsigned long)&sigsp->info;
+			regs->gpr.rdx = 0;
 		}
-		regs->rip = (unsigned long)k->sa.sa_handler;
-		regs->rsp = (unsigned long)usp;
+		regs->gpr.rip = (unsigned long)k->sa.sa_handler;
+		regs->gpr.rsp = (unsigned long)usp;
 
 		proc->sigmask.__val[0] |= pending->sigmask.__val[0];
 		kfree(pending);
@@ -609,14 +609,14 @@ do_signal(unsigned long rc, void *regs0, struct process *proc, struct sig_pendin
 			dkprintf("do_signal,default,core,sig=%d\n", sig);
 			coredump(proc, regs);
 			coredumped = 0x80;
-			terminate(0, sig | coredumped, (ihk_mc_user_context_t *)regs->rsp);
+			terminate(0, sig | coredumped, (ihk_mc_user_context_t *)regs->gpr.rsp);
 			break;
 		case SIGCHLD:
 		case SIGURG:
 			break;
 		default:
 			dkprintf("do_signal,default,terminate,sig=%d\n", sig);
-			terminate(0, sig, (ihk_mc_user_context_t *)regs->rsp);
+			terminate(0, sig, (ihk_mc_user_context_t *)regs->gpr.rsp);
 			break;
 		}
 	}
@@ -665,7 +665,7 @@ hassigpending(struct process *proc)
 void
 check_signal(unsigned long rc, void *regs0)
 {
-	struct x86_regs *regs = regs0;
+	struct x86_user_context *regs = regs0;
 	struct process *proc;
 	struct sig_pending *pending;
 	int	irqstate;
@@ -692,7 +692,7 @@ check_signal(unsigned long rc, void *regs0)
 		return;
 	}
 
-	if(regs != NULL && (regs->rsp & 0x8000000000000000)) {
+	if(regs != NULL && (regs->gpr.rsp & 0x8000000000000000)) {
 		return;
 	}
 
@@ -971,16 +971,16 @@ do_kill(int pid, int tid, int sig, siginfo_t *info, int ptracecont)
 void
 set_signal(int sig, void *regs0, siginfo_t *info)
 {
-	struct x86_regs *regs = regs0;
+	struct x86_user_context *regs = regs0;
 	struct process *proc = cpu_local_var(current);
 
 	if(proc == NULL || proc->ftn->pid == 0)
 		return;
 
 	if((__sigmask(sig) & proc->sigmask.__val[0]) ||
-	   (regs->rsp & 0x8000000000000000)){
+	   (regs->gpr.rsp & 0x8000000000000000)){
 		coredump(proc, regs0);
-		terminate(0, sig | 0x80, (ihk_mc_user_context_t *)regs->rsp);
+		terminate(0, sig | 0x80, (ihk_mc_user_context_t *)regs->gpr.rsp);
 	}
 		do_kill(proc->ftn->pid, proc->ftn->tid, sig, info, 0);
 }
diff --git a/kernel/mem.c b/kernel/mem.c
index 193a7d46..a9229fd4 100644
--- a/kernel/mem.c
+++ b/kernel/mem.c
@@ -214,7 +214,7 @@ static void unhandled_page_fault(struct process *proc, void *fault_addr, void *r
 	struct vm_range *range;
 	char found;
 	unsigned long irqflags;
-	unsigned long error = ((struct x86_regs *)regs)->error;
+	unsigned long error = ((struct x86_user_context *)regs)->gpr.error;
 
 	irqflags = kprintf_lock();
 	dkprintf("[%d] Page fault for 0x%lX\n",