Index: kernel/arch/ia64/src/mm/as.c
===================================================================
--- kernel/arch/ia64/src/mm/as.c	(revision 563c2ddc4c2e228951de3522875152bb1cf8dc51)
+++ kernel/arch/ia64/src/mm/as.c	(revision 879585a3fd47daccb6ab751ad240297f65de5bae)
@@ -37,9 +37,8 @@
 #include <arch/mm/page.h>
 #include <genarch/mm/as_ht.h>
+#include <genarch/mm/page_ht.h>
 #include <genarch/mm/asid_fifo.h>
 #include <mm/asid.h>
-#include <arch.h>
 #include <arch/barrier.h>
-#include <synch/spinlock.h>
 
 /** Architecture dependent address space init. */
@@ -56,10 +55,6 @@
 void as_install_arch(as_t *as)
 {
-	ipl_t ipl;
 	region_register rr;
 	int i;
-	
-	ipl = interrupts_disable();
-	spinlock_lock(&as->lock);
 	
 	ASSERT(as->asid != ASID_INVALID);
@@ -81,7 +76,4 @@
 	srlz_d();
 	srlz_i();
-	
-	spinlock_unlock(&as->lock);
-	interrupts_restore(ipl);
 }
 
Index: kernel/arch/mips32/src/mm/as.c
===================================================================
--- kernel/arch/mips32/src/mm/as.c	(revision 563c2ddc4c2e228951de3522875152bb1cf8dc51)
+++ kernel/arch/mips32/src/mm/as.c	(revision 879585a3fd47daccb6ab751ad240297f65de5bae)
@@ -35,4 +35,5 @@
 #include <arch/mm/as.h>
 #include <genarch/mm/as_pt.h>
+#include <genarch/mm/page_pt.h>
 #include <genarch/mm/asid_fifo.h>
 #include <arch/mm/tlb.h>
@@ -40,5 +41,4 @@
 #include <mm/as.h>
 #include <arch/cp0.h>
-#include <arch.h>
 
 /** Architecture dependent address space init. */
@@ -58,5 +58,4 @@
 {
 	entry_hi_t hi;
-	ipl_t ipl;
 
 	/*
@@ -65,10 +64,6 @@
 	hi.value = cp0_entry_hi_read();
 
-	ipl = interrupts_disable();
-	spinlock_lock(&as->lock);
 	hi.asid = as->asid;
 	cp0_entry_hi_write(hi.value);	
-	spinlock_unlock(&as->lock);
-	interrupts_restore(ipl);
 }
 
Index: kernel/arch/ppc32/src/mm/as.c
===================================================================
--- kernel/arch/ppc32/src/mm/as.c	(revision 563c2ddc4c2e228951de3522875152bb1cf8dc51)
+++ kernel/arch/ppc32/src/mm/as.c	(revision 879585a3fd47daccb6ab751ad240297f65de5bae)
@@ -55,10 +55,6 @@
 {
 	asid_t asid;
-	ipl_t ipl;
 	uint32_t sr;
 
-	ipl = interrupts_disable();
-	spinlock_lock(&as->lock);
-	
 	asid = as->asid;
 	
@@ -80,7 +76,4 @@
 		);
 	}
-	
-	spinlock_unlock(&as->lock);
-	interrupts_restore(ipl);
 }
 
Index: kernel/arch/ppc64/src/mm/as.c
===================================================================
--- kernel/arch/ppc64/src/mm/as.c	(revision 563c2ddc4c2e228951de3522875152bb1cf8dc51)
+++ kernel/arch/ppc64/src/mm/as.c	(revision 879585a3fd47daccb6ab751ad240297f65de5bae)
@@ -27,5 +27,5 @@
  */
 
- /** @addtogroup ppc64mm
+/** @addtogroup ppc64mm
   * @{
  */
@@ -42,5 +42,5 @@
 }
 
- /** @}
+/** @}
  */
 
Index: kernel/arch/sparc64/src/mm/as.c
===================================================================
--- kernel/arch/sparc64/src/mm/as.c	(revision 563c2ddc4c2e228951de3522875152bb1cf8dc51)
+++ kernel/arch/sparc64/src/mm/as.c	(revision 879585a3fd47daccb6ab751ad240297f65de5bae)
@@ -43,5 +43,4 @@
 #include <arch/mm/tsb.h>
 #include <arch/memstr.h>
-#include <synch/mutex.h>
 #include <arch/asm.h>
 #include <mm/frame.h>
@@ -101,11 +100,5 @@
 {
 #ifdef CONFIG_TSB
-	ipl_t ipl;
-
-	ipl = interrupts_disable();
-	mutex_lock_active(&as->lock);	/* completely unnecessary, but polite */
 	tsb_invalidate(as, 0, (count_t) -1);
-	mutex_unlock(&as->lock);
-	interrupts_restore(ipl);
 #endif
 	return 0;
@@ -124,16 +117,15 @@
 	
 	/*
-	 * Note that we don't lock the address space.
-	 * That's correct - we can afford it here
-	 * because we only read members that are
-	 * currently read-only.
+	 * Note that we don't and may not lock the address space. That's ok
+	 * since we only read members that are currently read-only.
+	 *
+	 * Moreover, the as->asid is protected by asidlock, which is being held.
 	 */
 	
 	/*
-	 * Write ASID to secondary context register.
-	 * The primary context register has to be set
-	 * from TL>0 so it will be filled from the
-	 * secondary context register from the TL=1
-	 * code just before switch to userspace.
+	 * Write ASID to secondary context register. The primary context
+	 * register has to be set from TL>0 so it will be filled from the
+	 * secondary context register from the TL=1 code just before switch to
+	 * userspace.
 	 */
 	ctx.v = 0;
@@ -185,8 +177,8 @@
 
 	/*
-	 * Note that we don't lock the address space.
-	 * That's correct - we can afford it here
-	 * because we only read members that are
-	 * currently read-only.
+	 * Note that we don't and may not lock the address space. That's ok
+	 * since we only read members that are currently read-only.
+	 *
+	 * Moreover, the as->asid is protected by asidlock, which is being held.
 	 */