From a9d3d683c04ecab5a1a4f4b00238044f24c72b24 Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Date: Fri, 20 Aug 2021 18:36:00 +1000
Subject: [PATCH] switch off tests that are flaky under simulation

These are currently BREAKPOINT_002 and SCHED0021. The corresponding
issues #43 and #42 remain open, and when resolved positively, these
tests should be enabled again for simulation runs.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
---
 apps/sel4test-driver/CMakeLists.txt         | 2 ++
 apps/sel4test-tests/src/tests/breakpoints.c | 6 +++++-
 apps/sel4test-tests/src/tests/scheduler.c   | 4 +++-
 settings.cmake                              | 2 ++
 4 files changed, 12 insertions(+), 2 deletions(-)

diff --git a/apps/sel4test-driver/CMakeLists.txt b/apps/sel4test-driver/CMakeLists.txt
index b5003b13..4b2b9386 100644
--- a/apps/sel4test-driver/CMakeLists.txt
+++ b/apps/sel4test-driver/CMakeLists.txt
@@ -12,6 +12,8 @@ set(configure_string "")
 
 config_option(Sel4testHaveTimer HAVE_TIMER "Enable tests that require a timer driver" DEFAULT ON)
 
+config_option(Sel4testSimulation SIMULATION "Disable tests not suitable for simulation" DEFAULT OFF)
+
 config_option(
     Sel4testHaveCache
     HAVE_CACHE
diff --git a/apps/sel4test-tests/src/tests/breakpoints.c b/apps/sel4test-tests/src/tests/breakpoints.c
index 5c53ea6e..93efe0eb 100644
--- a/apps/sel4test-tests/src/tests/breakpoints.c
+++ b/apps/sel4test-tests/src/tests/breakpoints.c
@@ -4,6 +4,7 @@
  * SPDX-License-Identifier: BSD-2-Clause
  */
 #include <autoconf.h>
+#include <sel4test-driver/gen_config.h>
 
 #ifdef CONFIG_HARDWARE_DEBUG_API
 
@@ -263,8 +264,11 @@ test_debug_set_data_breakpoint(struct env *env)
     }
     return sel4test_get_result();
 }
+/* This test is flaky under simulation. See also #43  */
 DEFINE_TEST(BREAKPOINT_002, "Attempt to set and trigger a data breakpoint",
-            test_debug_set_data_breakpoint, config_set(CONFIG_HARDWARE_DEBUG_API))
+            test_debug_set_data_breakpoint,
+            config_set(CONFIG_HARDWARE_DEBUG_API) &&
+            !config_set(CONFIG_SIMULATION))
 
 static int
 test_debug_get_instruction_breakpoint(struct env *env)
diff --git a/apps/sel4test-tests/src/tests/scheduler.c b/apps/sel4test-tests/src/tests/scheduler.c
index 4c39c3dd..d07ee003 100644
--- a/apps/sel4test-tests/src/tests/scheduler.c
+++ b/apps/sel4test-tests/src/tests/scheduler.c
@@ -1624,8 +1624,10 @@ static int test_simple_preempt(struct env *env)
 
     return sel4test_get_result();
 }
+/* This test is flaky under simulation. Probably a race condition that only
+   comes out under simulator timing conditions. See also #42  */
 DEFINE_TEST(SCHED0021, "Test for pre-emption during running of many threads with equal prio", test_simple_preempt,
-            true);
+            !config_set(CONFIG_SIMULATION));
 
 int sched0022_to_fn(struct env *env, helper_thread_t *thread, seL4_CPtr ep)
 {
diff --git a/settings.cmake b/settings.cmake
index 896efb12..f64b1e72 100644
--- a/settings.cmake
+++ b/settings.cmake
@@ -63,8 +63,10 @@ if(NOT Sel4testAllowSettingsOverride)
     # sel4test specific config settings.
 
     if(SIMULATION)
+        set(Sel4testSimulation ON CACHE BOOL "" FORCE)
         set(Sel4testHaveCache OFF CACHE BOOL "" FORCE)
     else()
+        set(Sel4testSimulation OFF CACHE BOOL "" FORCE)
         set(Sel4testHaveCache ON CACHE BOOL "" FORCE)
     endif()