Index: kernel/generic/include/atomic.h
===================================================================
--- kernel/generic/include/atomic.h	(revision 22a28a696141d62f28e48ed72d1d255ff519795c)
+++ kernel/generic/include/atomic.h	(revision e3038b41e1f6e1ef905bbc80916933e18d3e3008)
@@ -41,4 +41,6 @@
 
 ATOMIC static inline void atomic_set(atomic_t *val, atomic_count_t i)
+    WRITES(&val->count)
+    REQUIRES_EXTENT_MUTABLE(val)
 {
 	val->count = i;
@@ -46,4 +48,5 @@
 
 ATOMIC static inline atomic_count_t atomic_get(atomic_t *val)
+    REQUIRES_EXTENT_MUTABLE(val)
 {
 	return val->count;
Index: kernel/generic/include/verify.h
===================================================================
--- kernel/generic/include/verify.h	(revision 22a28a696141d62f28e48ed72d1d255ff519795c)
+++ kernel/generic/include/verify.h	(revision e3038b41e1f6e1ef905bbc80916933e18d3e3008)
@@ -39,11 +39,32 @@
 #ifdef CONFIG_VERIFY_VCC
 
-#define ATOMIC         __spec_attr("atomic_inline", "")
-#define REQUIRES(...)  __requires(__VA_ARGS__)
+#define ATOMIC         __specification_attr("atomic_inline", "")
+
+#define READS(ptr)     __specification(reads(ptr))
+#define WRITES(ptr)    __specification(writes(ptr))
+#define REQUIRES(...)  __specification(requires __VA_ARGS__)
+
+#define EXTENT(ptr)              \extent(ptr)
+#define ARRAY_RANGE(ptr, nmemb)  \array_range(ptr, nmemb)
+
+#define REQUIRES_EXTENT_MUTABLE(ptr) \
+	REQUIRES(\extent_mutable(ptr))
+
+#define REQUIRES_ARRAY_MUTABLE(ptr, nmemb) \
+	REQUIRES(\mutable_array(ptr, nmemb))
 
 #else /* CONFIG_VERIFY_VCC */
 
 #define ATOMIC
+
+#define READS(ptr)
+#define WRITES(ptr)
 #define REQUIRES(...)
+
+#define EXTENT(ptr)
+#define ARRAY_RANGE(ptr, nmemb)
+
+#define REQUIRES_EXTENT_MUTABLE(ptr)
+#define REQUIRES_ARRAY_MUTABLE(ptr, nmemb)
 
 #endif /* CONFIG_VERIFY_VCC */
Index: kernel/generic/src/interrupt/interrupt.c
===================================================================
--- kernel/generic/src/interrupt/interrupt.c	(revision 22a28a696141d62f28e48ed72d1d255ff519795c)
+++ kernel/generic/src/interrupt/interrupt.c	(revision e3038b41e1f6e1ef905bbc80916933e18d3e3008)
@@ -143,6 +143,8 @@
 	uint64_t end_cycle = get_cycle();
 	
+	irq_spinlock_lock(&exctbl_lock, false);
 	exc_table[n].cycles += end_cycle - begin_cycle;
 	exc_table[n].count++;
+	irq_spinlock_unlock(&exctbl_lock, false);
 	
 	/* Do not charge THREAD for exception cycles */
Index: kernel/generic/src/mm/frame.c
===================================================================
--- kernel/generic/src/mm/frame.c	(revision 22a28a696141d62f28e48ed72d1d255ff519795c)
+++ kernel/generic/src/mm/frame.c	(revision e3038b41e1f6e1ef905bbc80916933e18d3e3008)
@@ -1234,9 +1234,9 @@
 {
 #ifdef __32_BITS__
-	printf("[nr] [base addr ] [frames    ] [flags ] [free frames ] [busy frames ]\n");
+	printf("[nr] [base addr] [frames    ] [flags ] [free frames ] [busy frames ]\n");
 #endif
 
 #ifdef __64_BITS__
-	printf("[nr] [base address      ] [frames    ] [flags ] [free frames ] [busy frames ]\n");
+	printf("[nr] [base address    ] [frames    ] [flags ] [free frames ] [busy frames ]\n");
 #endif
 	
@@ -1274,9 +1274,9 @@
 		
 #ifdef __32_BITS__
-		printf("   %10p", base);
+		printf("  %10p", base);
 #endif
 		
 #ifdef __64_BITS__
-		printf("   %18p", base);
+		printf(" %18p", base);
 #endif
 		
Index: kernel/generic/src/mm/tlb.c
===================================================================
--- kernel/generic/src/mm/tlb.c	(revision 22a28a696141d62f28e48ed72d1d255ff519795c)
+++ kernel/generic/src/mm/tlb.c	(revision e3038b41e1f6e1ef905bbc80916933e18d3e3008)
@@ -73,17 +73,16 @@
  * to all other processors.
  *
- * @param type		Type describing scope of shootdown.
- * @param asid		Address space, if required by type.
- * @param page		Virtual page address, if required by type.
- * @param count		Number of pages, if required by type.
+ * @param type  Type describing scope of shootdown.
+ * @param asid  Address space, if required by type.
+ * @param page  Virtual page address, if required by type.
+ * @param count Number of pages, if required by type.
  *
  * @return The interrupt priority level as it existed prior to this call.
+ *
  */
 ipl_t tlb_shootdown_start(tlb_invalidate_type_t type, asid_t asid,
     uintptr_t page, size_t count)
 {
-	ipl_t ipl;
-
-	ipl = interrupts_disable();
+	ipl_t ipl = interrupts_disable();
 	CPU->tlb_active = false;
 	irq_spinlock_lock(&tlblock, false);
@@ -91,10 +90,8 @@
 	size_t i;
 	for (i = 0; i < config.cpu_count; i++) {
-		cpu_t *cpu;
-		
 		if (i == CPU->id)
 			continue;
 		
-		cpu = &cpus[i];
+		cpu_t *cpu = &cpus[i];
 		irq_spinlock_lock(&cpu->lock, false);
 		if (cpu->tlb_messages_count == TLB_MESSAGE_QUEUE_LEN) {
@@ -127,5 +124,5 @@
 		if (cpus[i].tlb_active)
 			goto busy_wait;
-
+	
 	return ipl;
 }
@@ -133,5 +130,6 @@
 /** Finish TLB shootdown sequence.
  *
- * @param ipl		Previous interrupt priority level.
+ * @param ipl Previous interrupt priority level.
+ *
  */
 void tlb_shootdown_finalize(ipl_t ipl)