Index: arch/mips32/src/mm/tlb.c
===================================================================
--- arch/mips32/src/mm/tlb.c	(revision 20d50a15ee7f195ac1e5a2da974bef0722bb9d60)
+++ arch/mips32/src/mm/tlb.c	(revision 13fded3cce867db5468e1ff56db5579e305d2120)
@@ -400,6 +400,8 @@
 	page_mask_t mask;
 	entry_lo_t lo0, lo1;
-	entry_hi_t hi;
+	entry_hi_t hi, hi_save;
 	int i;
+
+	hi_save.value = cp0_entry_hi_read();
 
 	printf("TLB:\n");
@@ -418,4 +420,6 @@
 		       lo1.g, lo1.v, lo1.d, lo1.c, lo1.pfn);
 	}
+	
+	cp0_entry_hi_write(hi_save.value);
 }
 
@@ -425,6 +429,8 @@
 	ipl_t ipl;
 	entry_lo_t lo0, lo1;
+	entry_hi_t hi_save;
 	int i;
 
+	hi_save.value = cp0_entry_hi_read();
 	ipl = interrupts_disable();
 
@@ -446,4 +452,5 @@
 	
 	interrupts_restore(ipl);
+	cp0_entry_hi_write(hi_save.value);
 }
 
@@ -456,9 +463,10 @@
 	ipl_t ipl;
 	entry_lo_t lo0, lo1;
-	entry_hi_t hi;
+	entry_hi_t hi, hi_save;
 	int i;
 
 	ASSERT(asid != ASID_INVALID);
 
+	hi_save.value = cp0_entry_hi_read();
 	ipl = interrupts_disable();
 	
@@ -484,4 +492,5 @@
 	
 	interrupts_restore(ipl);
+	cp0_entry_hi_write(hi_save.value);
 }
 
@@ -495,9 +504,10 @@
 	ipl_t ipl;
 	entry_lo_t lo0, lo1;
-	entry_hi_t hi;
+	entry_hi_t hi, hi_save;
 	tlb_index_t index;
 
 	ASSERT(asid != ASID_INVALID);
 
+	hi_save.value = cp0_entry_hi_read();
 	ipl = interrupts_disable();
 
@@ -526,3 +536,4 @@
 	
 	interrupts_restore(ipl);
-}
+	cp0_entry_hi_write(hi_save.value);
+}