TK1 has KERNEL_WCET of 100 instead of 10

Proper fix is for seL4 to export MIN_BUDGET_US, but until then hardcode it here. Co-authored-by: Gerwin Klein <[email protected]> Signed-off-by: Indan Zupancic <[email protected]>
seL4 · Dec 2, 2021 · de831ca · de831ca
1 parent b572953
commit de831ca
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/apps/sel4test-tests/src/tests/schedcontext.c b/apps/sel4test-tests/src/tests/schedcontext.c
@@ -12,9 +12,14 @@
 
 #include "../helpers.h"
 
+/* FIXME: this is a temporary hack and MIN_BUDGET_US should be exported via libsel4 */
 #ifndef MIN_BUDGET_US
+#ifdef CONFIG_PLAT_TK1
+#define MIN_BUDGET_US (2 * 100)
+#else
 #define MIN_BUDGET_US (2 * 10)
 #endif
+#endif
 
 int test_sched_control_configure(env_t env)
 {