Index: kernel/generic/src/mm/as.c
===================================================================
--- kernel/generic/src/mm/as.c	(revision d0c82c531ddd91c5c32e571f69768c044cf234b2)
+++ kernel/generic/src/mm/as.c	(revision fdaad75dff1d0aada7a6e1825ce65314be2ff3c2)
@@ -239,4 +239,6 @@
 	
 	spinlock_unlock(&asidlock);
+	interrupts_restore(ipl);
+
 	
 	/*
@@ -265,6 +267,4 @@
 	page_table_destroy(NULL);
 #endif
-	
-	interrupts_restore(ipl);
 	
 	slab_free(as_slab, as);
@@ -327,10 +327,8 @@
 		return NULL;
 	
-	ipl_t ipl = interrupts_disable();
 	mutex_lock(&as->lock);
 	
 	if (!check_area_conflicts(as, base, size, NULL)) {
 		mutex_unlock(&as->lock);
-		interrupts_restore(ipl);
 		return NULL;
 	}
@@ -357,5 +355,4 @@
 	
 	mutex_unlock(&as->lock);
-	interrupts_restore(ipl);
 	
 	return area;
@@ -376,5 +373,4 @@
 int as_area_resize(as_t *as, uintptr_t address, size_t size, unsigned int flags)
 {
-	ipl_t ipl = interrupts_disable();
 	mutex_lock(&as->lock);
 	
@@ -386,5 +382,4 @@
 	if (!area) {
 		mutex_unlock(&as->lock);
-		interrupts_restore(ipl);
 		return ENOENT;
 	}
@@ -398,5 +393,4 @@
 		mutex_unlock(&area->lock);
 		mutex_unlock(&as->lock);
-		interrupts_restore(ipl);
 		return ENOTSUP;
 	}
@@ -410,5 +404,4 @@
 		mutex_unlock(&area->lock);
 		mutex_unlock(&as->lock);
-		interrupts_restore(ipl);
 		return ENOTSUP;
 	}
@@ -422,5 +415,4 @@
 		mutex_unlock(&area->lock);
 		mutex_unlock(&as->lock);
-		interrupts_restore(ipl);
 		return EPERM;
 	}
@@ -549,5 +541,4 @@
 			mutex_unlock(&area->lock);
 			mutex_unlock(&as->lock);
-			interrupts_restore(ipl);
 			return EADDRNOTAVAIL;
 		}
@@ -558,5 +549,4 @@
 	mutex_unlock(&area->lock);
 	mutex_unlock(&as->lock);
-	interrupts_restore(ipl);
 	
 	return 0;
@@ -573,5 +563,4 @@
 int as_area_destroy(as_t *as, uintptr_t address)
 {
-	ipl_t ipl = interrupts_disable();
 	mutex_lock(&as->lock);
 	
@@ -579,5 +568,4 @@
 	if (!area) {
 		mutex_unlock(&as->lock);
-		interrupts_restore(ipl);
 		return ENOENT;
 	}
@@ -659,5 +647,4 @@
 	
 	mutex_unlock(&as->lock);
-	interrupts_restore(ipl);
 	return 0;
 }
@@ -690,5 +677,4 @@
     as_t *dst_as, uintptr_t dst_base, unsigned int dst_flags_mask)
 {
-	ipl_t ipl = interrupts_disable();
 	mutex_lock(&src_as->lock);
 	as_area_t *src_area = find_area_and_lock(src_as, src_base);
@@ -699,5 +685,4 @@
 		 */
 		mutex_unlock(&src_as->lock);
-		interrupts_restore(ipl);
 		return ENOENT;
 	}
@@ -711,5 +696,4 @@
 		mutex_unlock(&src_area->lock);
 		mutex_unlock(&src_as->lock);
-		interrupts_restore(ipl);
 		return ENOTSUP;
 	}
@@ -728,5 +712,4 @@
 		mutex_unlock(&src_area->lock);
 		mutex_unlock(&src_as->lock);
-		interrupts_restore(ipl);
 		return EPERM;
 	}
@@ -777,5 +760,4 @@
 		sh_info_remove_reference(sh_info);
 		
-		interrupts_restore(ipl);
 		return ENOMEM;
 	}
@@ -794,6 +776,4 @@
 	mutex_unlock(&dst_as->lock);
 	
-	interrupts_restore(ipl);
-	
 	return 0;
 }
@@ -816,5 +796,4 @@
 	};
 
-	ASSERT(interrupts_disabled());
 	ASSERT(mutex_locked(&area->lock));
 	
@@ -844,5 +823,4 @@
 	unsigned int page_flags = area_flags_to_page_flags(flags);
 	
-	ipl_t ipl = interrupts_disable();
 	mutex_lock(&as->lock);
 	
@@ -850,5 +828,4 @@
 	if (!area) {
 		mutex_unlock(&as->lock);
-		interrupts_restore(ipl);
 		return ENOENT;
 	}
@@ -859,5 +836,4 @@
 		mutex_unlock(&area->lock);
 		mutex_unlock(&as->lock);
-		interrupts_restore(ipl);
 		return ENOTSUP;
 	}
@@ -978,5 +954,4 @@
 	mutex_unlock(&area->lock);
 	mutex_unlock(&as->lock);
-	interrupts_restore(ipl);
 	
 	return 0;
@@ -1219,5 +1194,4 @@
 unsigned int as_area_get_flags(as_area_t *area)
 {
-	ASSERT(interrupts_disabled());
 	ASSERT(mutex_locked(&area->lock));
 
@@ -1321,5 +1295,4 @@
 as_area_t *find_area_and_lock(as_t *as, uintptr_t va)
 {
-	ASSERT(interrupts_disabled());
 	ASSERT(mutex_locked(&as->lock));
 
@@ -1386,5 +1359,4 @@
     as_area_t *avoid_area)
 {
-	ASSERT(interrupts_disabled());
 	ASSERT(mutex_locked(&as->lock));
 
@@ -1486,5 +1458,4 @@
 	size_t size;
 	
-	ipl_t ipl = interrupts_disable();
 	page_table_lock(AS, true);
 	as_area_t *src_area = find_area_and_lock(AS, base);
@@ -1497,5 +1468,4 @@
 	
 	page_table_unlock(AS, true);
-	interrupts_restore(ipl);
 	return size;
 }
@@ -2070,5 +2040,4 @@
 void as_get_area_info(as_t *as, as_area_info_t **obuf, size_t *osize)
 {
-	ipl_t ipl = interrupts_disable();
 	mutex_lock(&as->lock);
 	
@@ -2114,5 +2083,4 @@
 	
 	mutex_unlock(&as->lock);
-	interrupts_restore(ipl);
 	
 	*obuf = info;
@@ -2127,5 +2095,4 @@
 void as_print(as_t *as)
 {
-	ipl_t ipl = interrupts_disable();
 	mutex_lock(&as->lock);
 	
@@ -2150,5 +2117,4 @@
 	
 	mutex_unlock(&as->lock);
-	interrupts_restore(ipl);
 }
 
Index: kernel/generic/src/mm/page.c
===================================================================
--- kernel/generic/src/mm/page.c	(revision d0c82c531ddd91c5c32e571f69768c044cf234b2)
+++ kernel/generic/src/mm/page.c	(revision fdaad75dff1d0aada7a6e1825ce65314be2ff3c2)
@@ -118,5 +118,4 @@
     unsigned int flags)
 {
-	ASSERT(interrupts_disabled());
 	ASSERT(page_table_locked(as));
 	
@@ -142,5 +141,4 @@
 void page_mapping_remove(as_t *as, uintptr_t page)
 {
-	ASSERT(interrupts_disabled());
 	ASSERT(page_table_locked(as));
 	
@@ -167,5 +165,4 @@
 pte_t *page_mapping_find(as_t *as, uintptr_t page)
 {
-	ASSERT(interrupts_disabled());
 	ASSERT(page_table_locked(as));
 	
Index: kernel/generic/src/mm/tlb.c
===================================================================
--- kernel/generic/src/mm/tlb.c	(revision d0c82c531ddd91c5c32e571f69768c044cf234b2)
+++ kernel/generic/src/mm/tlb.c	(revision fdaad75dff1d0aada7a6e1825ce65314be2ff3c2)
@@ -73,6 +73,4 @@
  * to all other processors.
  *
- * This function must be called with interrupts disabled.
- *
  * @param type Type describing scope of shootdown.
  * @param asid Address space, if required by type.
@@ -85,5 +83,5 @@
 {
 	CPU->tlb_active = false;
-	irq_spinlock_lock(&tlblock, false);
+	irq_spinlock_lock(&tlblock, true);
 	
 	size_t i;
@@ -132,5 +130,5 @@
 void tlb_shootdown_finalize(void)
 {
-	irq_spinlock_unlock(&tlblock, false);
+	irq_spinlock_unlock(&tlblock, true);
 	CPU->tlb_active = true;
 }
Index: kernel/generic/src/synch/futex.c
===================================================================
--- kernel/generic/src/synch/futex.c	(revision d0c82c531ddd91c5c32e571f69768c044cf234b2)
+++ kernel/generic/src/synch/futex.c	(revision fdaad75dff1d0aada7a6e1825ce65314be2ff3c2)
@@ -113,9 +113,6 @@
 	uintptr_t paddr;
 	pte_t *t;
-	ipl_t ipl;
 	int rc;
 	
-	ipl = interrupts_disable();
-
 	/*
 	 * Find physical address of futex counter.
@@ -125,5 +122,4 @@
 	if (!t || !PTE_VALID(t) || !PTE_PRESENT(t)) {
 		page_table_unlock(AS, true);
-		interrupts_restore(ipl);
 		return (unative_t) ENOENT;
 	}
@@ -131,6 +127,4 @@
 	page_table_unlock(AS, true);
 	
-	interrupts_restore(ipl);	
-
 	futex = futex_find(paddr);