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.
 	 */