From de831ca7103ef117dc510e93d1f67bf857cb9a99 Mon Sep 17 00:00:00 2001 From: Indan Zupancic Date: Tue, 30 Nov 2021 13:56:53 +0100 Subject: [PATCH] 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 Signed-off-by: Indan Zupancic --- apps/sel4test-tests/src/tests/schedcontext.c | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/apps/sel4test-tests/src/tests/schedcontext.c b/apps/sel4test-tests/src/tests/schedcontext.c index 3d1ed2b4..dc08da95 100644 --- 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) {