From 4768465027ae3f6adb7be732a2f14145cc14a540 Mon Sep 17 00:00:00 2001
From: Adrian Danis <Adrian.Danis@data61.csiro.au>
Date: Wed, 23 Aug 2017 16:48:31 +1000
Subject: [PATCH] mcs: allow kernel WCET estimate to be scaled

This configuration option allows for building images destined for
simulators, which may not simulate as fast as hardware, to still be
used.
---
 config.cmake              | 12 ++++++++++++
 include/config.h          |  4 ++++
 include/kernel/sporadic.h |  5 +++--
 3 files changed, 19 insertions(+), 2 deletions(-)

diff --git a/config.cmake b/config.cmake
index 7fefcf0a1..0bcc77d25 100644
--- a/config.cmake
+++ b/config.cmake
@@ -442,4 +442,16 @@ config_option(
 # of the currently running thread without a capability.
 config_set(KernelSetTLSBaseSelf SET_TLS_BASE_SELF ${KernelSetTLSBaseSelf})
 
+config_string(
+    KernelWcetScale KERNEL_WCET_SCALE
+    "Multiplier to scale kernel WCET estimate by: the kernel WCET estimate  \
+     is used to ensure a thread has enough budget to get in and out of the  \
+     kernel. When running in a simulator the WCET estimate, which is tuned  \
+     for hardware, may not be sufficient. This option provides a hacky knob \
+     that can be fiddled with when running inside a simulator."
+    DEFAULT 1
+    UNQUOTE
+    DEPENDS "KernelIsMCS" UNDEF_DISABLED
+)
+
 add_config_library(kernel "${configure_string}")
diff --git a/include/config.h b/include/config.h
index 56c738657..1bfeb0c6d 100644
--- a/include/config.h
+++ b/include/config.h
@@ -33,6 +33,10 @@
 #ifndef CONFIG_BOOT_THREAD_TIME_SLICE
 #define CONFIG_BOOT_THREAD_TIME_SLICE 5
 #endif
+
+#ifndef CONFIG_KERNEL_WCET_SCALE
+#define CONFIG_KERNEL_WCET_SCALE 1
+#endif
 #endif
 
 /* the number of scheduler domains */
diff --git a/include/kernel/sporadic.h b/include/kernel/sporadic.h
index d556aa116..81d80e96d 100644
--- a/include/kernel/sporadic.h
+++ b/include/kernel/sporadic.h
@@ -28,6 +28,7 @@
  * minimum size is 2, and can be configured by the user per scheduling context
  * above this) the next refill is merged.
  */
+#include <config.h>
 #include <types.h>
 #include <util.h>
 #include <object/structures.h>
@@ -36,8 +37,8 @@
 
 /* To do an operation in the kernel, the thread must have
  * at least this much budget - see comment on refill_sufficient */
-#define MIN_BUDGET_US (2u * getKernelWcetUs())
-#define MIN_BUDGET    (2u * getKernelWcetTicks())
+#define MIN_BUDGET_US (2u * getKernelWcetUs() * CONFIG_KERNEL_WCET_SCALE)
+#define MIN_BUDGET    (2u * getKernelWcetTicks() * CONFIG_KERNEL_WCET_SCALE)
 
 /* Short hand for accessing refill queue items */
 #define REFILL_INDEX(sc, index) (((refill_t *) (SC_REF(sc) + sizeof(sched_context_t)))[index])