Index: kernel/arch/mips32/src/mm/tlb.c
===================================================================
--- kernel/arch/mips32/src/mm/tlb.c	(revision 3a2b6364ba3983a631bdcfe110037871ba380b25)
+++ kernel/arch/mips32/src/mm/tlb.c	(revision 1d432f9b3f6833cb86d4ee1903d5cdc12a99f6aa)
@@ -369,4 +369,6 @@
 	entry_hi_t hi;
 	pte_t *pte;
+
+	ASSERT(mutex_locked(&AS->lock));
 
 	hi.value = cp0_entry_hi_read();
Index: kernel/arch/ppc32/src/mm/tlb.c
===================================================================
--- kernel/arch/ppc32/src/mm/tlb.c	(revision 3a2b6364ba3983a631bdcfe110037871ba380b25)
+++ kernel/arch/ppc32/src/mm/tlb.c	(revision 1d432f9b3f6833cb86d4ee1903d5cdc12a99f6aa)
@@ -67,4 +67,6 @@
     istate_t *istate, int *pfrc)
 {
+	ASSERT(mutex_locked(&as->lock));
+
 	/*
 	 * Check if the mapping exists in page tables.
Index: kernel/genarch/src/mm/asid.c
===================================================================
--- kernel/genarch/src/mm/asid.c	(revision 3a2b6364ba3983a631bdcfe110037871ba380b25)
+++ kernel/genarch/src/mm/asid.c	(revision 1d432f9b3f6833cb86d4ee1903d5cdc12a99f6aa)
@@ -70,6 +70,5 @@
 /** Allocate free address space identifier.
  *
- * Interrupts must be disabled and inactive_as_with_asid_lock must be held
- * prior to this call
+ * Interrupts must be disabled and asidlock must be held prior to this call
  *
  * @return New ASID.
@@ -80,4 +79,7 @@
 	link_t *tmp;
 	as_t *as;
+
+	ASSERT(interrupts_disabled());
+	ASSERT(spinlock_locked(&asidlock));
 
 	/*
Index: kernel/genarch/src/mm/page_ht.c
===================================================================
--- kernel/genarch/src/mm/page_ht.c	(revision 3a2b6364ba3983a631bdcfe110037871ba380b25)
+++ kernel/genarch/src/mm/page_ht.c	(revision 1d432f9b3f6833cb86d4ee1903d5cdc12a99f6aa)
@@ -186,4 +186,7 @@
 		page = ALIGN_DOWN(page, PAGE_SIZE)
 	};
+
+	ASSERT(interrupts_disabled());
+	ASSERT(page_table_locked(as));
 	
 	if (!hash_table_find(&page_ht, key)) {
@@ -226,4 +229,7 @@
 		page = ALIGN_DOWN(page, PAGE_SIZE)
 	};
+
+	ASSERT(interrupts_disabled());
+	ASSERT(page_table_locked(as));
 	
 	/*
@@ -253,4 +259,7 @@
 		page = ALIGN_DOWN(page, PAGE_SIZE)
 	};
+
+	ASSERT(interrupts_disabled());
+	ASSERT(page_table_locked(as));
 	
 	link_t *cur = hash_table_find(&page_ht, key);
Index: kernel/genarch/src/mm/page_pt.c
===================================================================
--- kernel/genarch/src/mm/page_pt.c	(revision 3a2b6364ba3983a631bdcfe110037871ba380b25)
+++ kernel/genarch/src/mm/page_pt.c	(revision 1d432f9b3f6833cb86d4ee1903d5cdc12a99f6aa)
@@ -73,4 +73,7 @@
 {
 	pte_t *ptl0 = (pte_t *) PA2KA((uintptr_t) as->genarch.page_table);
+
+	ASSERT(interrupts_disabled());
+	ASSERT(page_table_locked(as));
 	
 	if (GET_PTL1_FLAGS(ptl0, PTL0_INDEX(page)) & PAGE_NOT_PRESENT) {
@@ -121,4 +124,7 @@
 void pt_mapping_remove(as_t *as, uintptr_t page)
 {
+	ASSERT(interrupts_disabled());
+	ASSERT(page_table_locked(as));
+
 	/*
 	 * First, remove the mapping, if it exists.
@@ -251,4 +257,7 @@
 pte_t *pt_mapping_find(as_t *as, uintptr_t page)
 {
+	ASSERT(interrupts_disabled());
+	ASSERT(page_table_locked(as));
+
 	pte_t *ptl0 = (pte_t *) PA2KA((uintptr_t) as->genarch.page_table);
 	if (GET_PTL1_FLAGS(ptl0, PTL0_INDEX(page)) & PAGE_NOT_PRESENT)
Index: kernel/generic/src/ipc/irq.c
===================================================================
--- kernel/generic/src/ipc/irq.c	(revision 3a2b6364ba3983a631bdcfe110037871ba380b25)
+++ kernel/generic/src/ipc/irq.c	(revision 1d432f9b3f6833cb86d4ee1903d5cdc12a99f6aa)
@@ -430,4 +430,7 @@
 {
 	ASSERT(irq);
+
+	ASSERT(interrupts_disabled());
+	ASSERT(irq_spinlock_locked(&irq->lock));
 	
 	if (irq->notif_cfg.answerbox) {
Index: kernel/generic/src/mm/as.c
===================================================================
--- kernel/generic/src/mm/as.c	(revision 3a2b6364ba3983a631bdcfe110037871ba380b25)
+++ kernel/generic/src/mm/as.c	(revision 1d432f9b3f6833cb86d4ee1903d5cdc12a99f6aa)
@@ -817,4 +817,7 @@
 		[PF_ACCESS_EXEC] = AS_AREA_EXEC
 	};
+
+	ASSERT(interrupts_disabled());
+	ASSERT(mutex_locked(&area->lock));
 	
 	if (!(area->flags & flagmap[access]))
@@ -1221,4 +1224,7 @@
 unsigned int as_area_get_flags(as_area_t *area)
 {
+	ASSERT(interrupts_disabled());
+	ASSERT(mutex_locked(&area->lock));
+
 	return area_flags_to_page_flags(area->flags);
 }
@@ -1322,4 +1328,7 @@
 as_area_t *find_area_and_lock(as_t *as, uintptr_t va)
 {
+	ASSERT(interrupts_disabled());
+	ASSERT(mutex_locked(&as->lock));
+
 	btree_node_t *leaf;
 	as_area_t *area = (as_area_t *) btree_search(&as->as_area_btree, va, &leaf);
@@ -1386,4 +1395,7 @@
     as_area_t *avoid_area)
 {
+	ASSERT(interrupts_disabled());
+	ASSERT(mutex_locked(&as->lock));
+
 	/*
 	 * We don't want any area to have conflicts with NULL page.
@@ -1473,5 +1485,5 @@
 /** Return size of the address space area with given base.
  *
- * @param base Arbitrary address insede the address space area.
+ * @param base Arbitrary address inside the address space area.
  *
  * @return Size of the address space area in bytes or zero if it
@@ -1484,4 +1496,5 @@
 	
 	ipl_t ipl = interrupts_disable();
+	page_table_lock(AS, true);
 	as_area_t *src_area = find_area_and_lock(AS, base);
 	
@@ -1492,4 +1505,5 @@
 		size = 0;
 	
+	page_table_unlock(AS, true);
 	interrupts_restore(ipl);
 	return size;
@@ -1509,4 +1523,5 @@
 int used_space_insert(as_area_t *area, uintptr_t page, size_t count)
 {
+	ASSERT(mutex_locked(&area->lock));
 	ASSERT(page == ALIGN_DOWN(page, PAGE_SIZE));
 	ASSERT(count);
@@ -1815,4 +1830,5 @@
 int used_space_remove(as_area_t *area, uintptr_t page, size_t count)
 {
+	ASSERT(mutex_locked(&area->lock));
 	ASSERT(page == ALIGN_DOWN(page, PAGE_SIZE));
 	ASSERT(count);
Index: kernel/generic/src/mm/backend_anon.c
===================================================================
--- kernel/generic/src/mm/backend_anon.c	(revision 3a2b6364ba3983a631bdcfe110037871ba380b25)
+++ kernel/generic/src/mm/backend_anon.c	(revision 1d432f9b3f6833cb86d4ee1903d5cdc12a99f6aa)
@@ -79,4 +79,7 @@
 {
 	uintptr_t frame;
+
+	ASSERT(page_table_locked(AS));
+	ASSERT(mutex_locked(&area->lock));
 
 	if (!as_area_check_access(area, access))
@@ -168,4 +171,7 @@
 void anon_frame_free(as_area_t *area, uintptr_t page, uintptr_t frame)
 {
+	ASSERT(page_table_locked(area->as));
+	ASSERT(mutex_locked(&area->lock));
+
 	frame_free(frame);
 }
@@ -183,4 +189,7 @@
 {
 	link_t *cur;
+
+	ASSERT(mutex_locked(&area->as->lock));
+	ASSERT(mutex_locked(&area->lock));
 
 	/*
Index: kernel/generic/src/mm/backend_elf.c
===================================================================
--- kernel/generic/src/mm/backend_elf.c	(revision 3a2b6364ba3983a631bdcfe110037871ba380b25)
+++ kernel/generic/src/mm/backend_elf.c	(revision 1d432f9b3f6833cb86d4ee1903d5cdc12a99f6aa)
@@ -86,4 +86,7 @@
 	bool dirty = false;
 
+	ASSERT(page_table_locked(AS));
+	ASSERT(mutex_locked(&area->lock));
+
 	if (!as_area_check_access(area, access))
 		return AS_PF_FAULT;
@@ -235,6 +238,10 @@
 	uintptr_t start_anon;
 
-	ASSERT((page >= ALIGN_DOWN(entry->p_vaddr, PAGE_SIZE)) &&
-	    (page < entry->p_vaddr + entry->p_memsz));
+	ASSERT(page_table_locked(area->as));
+	ASSERT(mutex_locked(&area->lock));
+
+	ASSERT(page >= ALIGN_DOWN(entry->p_vaddr, PAGE_SIZE));
+	ASSERT(page < entry->p_vaddr + entry->p_memsz);
+
 	start_anon = entry->p_vaddr + entry->p_filesz;
 
@@ -273,4 +280,7 @@
 	btree_node_t *leaf, *node;
 	uintptr_t start_anon = entry->p_vaddr + entry->p_filesz;
+
+	ASSERT(mutex_locked(&area->as->lock));
+	ASSERT(mutex_locked(&area->lock));
 
 	/*
Index: kernel/generic/src/mm/backend_phys.c
===================================================================
--- kernel/generic/src/mm/backend_phys.c	(revision 3a2b6364ba3983a631bdcfe110037871ba380b25)
+++ kernel/generic/src/mm/backend_phys.c	(revision 1d432f9b3f6833cb86d4ee1903d5cdc12a99f6aa)
@@ -72,4 +72,7 @@
 	uintptr_t base = area->backend_data.base;
 
+	ASSERT(page_table_locked(AS));
+	ASSERT(mutex_locked(&area->lock));
+
 	if (!as_area_check_access(area, access))
 		return AS_PF_FAULT;
@@ -93,4 +96,6 @@
 void phys_share(as_area_t *area)
 {
+	ASSERT(mutex_locked(&area->as->lock));
+	ASSERT(mutex_locked(&area->lock));
 }
 
Index: kernel/generic/src/mm/page.c
===================================================================
--- kernel/generic/src/mm/page.c	(revision 3a2b6364ba3983a631bdcfe110037871ba380b25)
+++ kernel/generic/src/mm/page.c	(revision 1d432f9b3f6833cb86d4ee1903d5cdc12a99f6aa)
@@ -120,7 +120,10 @@
     unsigned int flags)
 {
+	ASSERT(interrupts_disabled());
+	ASSERT(page_table_locked(as));
+	
 	ASSERT(page_mapping_operations);
 	ASSERT(page_mapping_operations->mapping_insert);
-	
+
 	page_mapping_operations->mapping_insert(as, page, frame, flags);
 	
@@ -143,4 +146,7 @@
 void page_mapping_remove(as_t *as, uintptr_t page)
 {
+	ASSERT(interrupts_disabled());
+	ASSERT(page_table_locked(as));
+	
 	ASSERT(page_mapping_operations);
 	ASSERT(page_mapping_operations->mapping_remove);
@@ -167,4 +173,7 @@
 pte_t *page_mapping_find(as_t *as, uintptr_t page)
 {
+	ASSERT(interrupts_disabled());
+	ASSERT(page_table_locked(as));
+	
 	ASSERT(page_mapping_operations);
 	ASSERT(page_mapping_operations->mapping_find);
Index: kernel/generic/src/proc/task.c
===================================================================
--- kernel/generic/src/proc/task.c	(revision 3a2b6364ba3983a631bdcfe110037871ba380b25)
+++ kernel/generic/src/proc/task.c	(revision 1d432f9b3f6833cb86d4ee1903d5cdc12a99f6aa)
@@ -351,4 +351,7 @@
 task_t *task_find_by_id(task_id_t id)
 {
+	ASSERT(interrupts_disabled());
+	ASSERT(irq_spinlock_locked(&tasks_lock));
+
 	avltree_node_t *node =
 	    avltree_search(&tasks_tree, (avltree_key_t) id);
@@ -362,5 +365,5 @@
 /** Get accounting data of given task.
  *
- * Note that task lock of 't' must be already held and interrupts must be
+ * Note that task lock of 'task' must be already held and interrupts must be
  * already disabled.
  *
@@ -372,4 +375,7 @@
 void task_get_accounting(task_t *task, uint64_t *ucycles, uint64_t *kcycles)
 {
+	ASSERT(interrupts_disabled());
+	ASSERT(irq_spinlock_locked(&task->lock));
+
 	/* Accumulated values of task */
 	uint64_t uret = task->ucycles;
Index: kernel/generic/src/proc/thread.c
===================================================================
--- kernel/generic/src/proc/thread.c	(revision 3a2b6364ba3983a631bdcfe110037871ba380b25)
+++ kernel/generic/src/proc/thread.c	(revision 1d432f9b3f6833cb86d4ee1903d5cdc12a99f6aa)
@@ -683,4 +683,7 @@
 bool thread_exists(thread_t *thread)
 {
+	ASSERT(interrupts_disabled());
+	ASSERT(irq_spinlock_locked(&threads_lock));
+
 	avltree_node_t *node =
 	    avltree_search(&threads_tree, (avltree_key_t) ((uintptr_t) thread));
@@ -700,4 +703,7 @@
 {
 	uint64_t time = get_cycle();
+
+	ASSERT(interrupts_disabled());
+	ASSERT(irq_spinlock_locked(&THREAD->lock));
 	
 	if (user)
@@ -735,4 +741,7 @@
 thread_t *thread_find_by_id(thread_id_t thread_id)
 {
+	ASSERT(interrupts_disabled());
+	ASSERT(irq_spinlock_locked(&threads_lock));
+
 	thread_iterator_t iterator;
 	
Index: kernel/generic/src/synch/waitq.c
===================================================================
--- kernel/generic/src/synch/waitq.c	(revision 3a2b6364ba3983a631bdcfe110037871ba380b25)
+++ kernel/generic/src/synch/waitq.c	(revision 1d432f9b3f6833cb86d4ee1903d5cdc12a99f6aa)
@@ -459,4 +459,7 @@
 {
 	size_t count = 0;
+
+	ASSERT(interrupts_disabled());
+	ASSERT(irq_spinlock_locked(&wq->lock));
 	
 loop:
Index: kernel/generic/src/sysinfo/stats.c
===================================================================
--- kernel/generic/src/sysinfo/stats.c	(revision 3a2b6364ba3983a631bdcfe110037871ba380b25)
+++ kernel/generic/src/sysinfo/stats.c	(revision 1d432f9b3f6833cb86d4ee1903d5cdc12a99f6aa)
@@ -204,4 +204,7 @@
 static void produce_stats_task(task_t *task, stats_task_t *stats_task)
 {
+	ASSERT(interrupts_disabled());
+	ASSERT(irq_spinlock_locked(&task->lock));
+
 	stats_task->task_id = task->taskid;
 	str_cpy(stats_task->name, TASK_NAME_BUFLEN, task->name);
@@ -303,4 +306,7 @@
 static void produce_stats_thread(thread_t *thread, stats_thread_t *stats_thread)
 {
+	ASSERT(interrupts_disabled());
+	ASSERT(irq_spinlock_locked(&thread->lock));
+
 	stats_thread->thread_id = thread->tid;
 	stats_thread->task_id = thread->task->taskid;
Index: kernel/generic/src/udebug/udebug.c
===================================================================
--- kernel/generic/src/udebug/udebug.c	(revision 3a2b6364ba3983a631bdcfe110037871ba380b25)
+++ kernel/generic/src/udebug/udebug.c	(revision 1d432f9b3f6833cb86d4ee1903d5cdc12a99f6aa)
@@ -389,5 +389,5 @@
  * FINISHED event for each of them.
  *
- * @param task Task structure. ta->udebug.lock must be already locked.
+ * @param task Task structure. task->udebug.lock must be already locked.
  *
  * @return Zero on success or negative error code.
@@ -396,4 +396,6 @@
 int udebug_task_cleanup(struct task *task)
 {
+	ASSERT(mutex_locked(&task->udebug.lock));
+
 	if ((task->udebug.dt_state != UDEBUG_TS_BEGINNING) &&
 	    (task->udebug.dt_state != UDEBUG_TS_ACTIVE)) {