diff --git a/kernel/microkernel/idle.c b/kernel/microkernel/idle.c
index b8992e95ae4..8d8dbc2dd24 100644
--- a/kernel/microkernel/idle.c
+++ b/kernel/microkernel/idle.c
@@ -134,10 +134,29 @@ void workload_monitor_calibrate(void)
 	_k_workload_ticks = 100;
 }
 
-#endif /* CONFIG_WORKLOAD_MONITOR */
+/*******************************************************************************
+*
+* _k_workload_monitor_update - workload monitor tick handler
+*
+* If workload monitor is configured this routine updates the global variables
+* it uses to record the passage of time.
+*
+* RETURNS: N/A
+*
+* \NOMANUAL
+*/
 
+void _k_workload_monitor_update(void)
+{
+	if (--_k_workload_ticks == 0) {
+		_k_workload_t0 = _k_workload_t1;
+		_k_workload_t1 = timer_read();
+		_k_workload_n0 = _k_workload_n1;
+		_k_workload_n1 = _k_workload_i - 1;
+		_k_workload_ticks = _k_workload_slice;
+	}
+}
 
-#ifdef CONFIG_WORKLOAD_MONITOR
 void _k_workload_get(struct k_args *P)
 {
 	unsigned int k, t;
@@ -168,7 +187,8 @@ void _k_workload_get(struct k_args *P)
 {
 	P->Args.u1.rval = 0;
 }
-#endif
+
+#endif /* CONFIG_WORKLOAD_MONITOR */
 
 /*******************************************************************************
 *
diff --git a/kernel/microkernel/include/kticks.h b/kernel/microkernel/include/kticks.h
index 8e3d68e77ef..4e28b4df394 100644
--- a/kernel/microkernel/include/kticks.h
+++ b/kernel/microkernel/include/kticks.h
@@ -39,18 +39,6 @@
 extern K_TIMER *_k_timer_list_head;
 extern K_TIMER *_k_timer_list_tail;
 extern int64_t _k_sys_clock_tick_count;
-extern unsigned int _k_workload_slice;
-extern unsigned int _k_workload_ticks;
-extern unsigned int _k_workload_ref_time;
-extern unsigned int _k_workload_t0;
-extern unsigned int _k_workload_t1;
-extern volatile unsigned int _k_workload_n0;
-extern volatile unsigned int _k_workload_n1;
-extern volatile unsigned int _k_workload_i;
-extern volatile unsigned int _k_workload_i0;
-extern volatile unsigned int _k_workload_delta;
-extern volatile unsigned int _k_workload_start_time;
-extern volatile unsigned int _k_workload_end_time;
 
 extern void enlist_timer(K_TIMER *T);
 extern void delist_timer(K_TIMER *T);
diff --git a/kernel/microkernel/include/minik.h b/kernel/microkernel/include/minik.h
index 03393c8e3ea..c778a902a46 100644
--- a/kernel/microkernel/include/minik.h
+++ b/kernel/microkernel/include/minik.h
@@ -151,6 +151,9 @@ extern const int _k_monitor_mask;
 
 #ifdef CONFIG_WORKLOAD_MONITOR
 extern void workload_monitor_calibrate(void);
+extern void _k_workload_monitor_update(void);
+#else
+#define _k_workload_monitor_update()	do { /* nothing */ } while (0)
 #endif
 
 #define INSERT_ELM(L, E)                              \
diff --git a/kernel/microkernel/ticker.c b/kernel/microkernel/ticker.c
index 6a574d4ff83..aef34b35e38 100644
--- a/kernel/microkernel/ticker.c
+++ b/kernel/microkernel/ticker.c
@@ -145,33 +145,6 @@ static void sys_clock_increment(int inc)
 	irq_unlock_inline(key);
 }
 
-/*******************************************************************************
-*
-* _WlMonitorUpdate - workload monitor tick handler
-*
-* If workload monitor is configured this routine updates the global variables
-* it uses to record the passage of time.
-*
-* RETURNS: N/A
-*
-* \NOMANUAL
-*/
-
-static inline void _WlMonitorUpdate(void)
-{
-#ifdef CONFIG_WORKLOAD_MONITOR
-	if (--_k_workload_ticks == 0) {
-		_k_workload_t0 = _k_workload_t1;
-		_k_workload_t1 = timer_read();
-		_k_workload_n0 = _k_workload_n1;
-		_k_workload_n1 = _k_workload_i - 1;
-		_k_workload_ticks = _k_workload_slice;
-	}
-#else
-/* do nothing */
-#endif
-}
-
 /*******************************************************************************
 *
 * _TlDebugUpdate - task level debugging tick handler
@@ -272,7 +245,7 @@ int K_ticker(int event)
 
 	ticks = _SysIdleElapsedTicksGet();
 
-	_WlMonitorUpdate();
+	_k_workload_monitor_update();
 
 	if (_TlDebugUpdate(ticks)) {
 		_TimeSliceUpdate();