mcs: Remove domain time check from preemptionPoint

This removes the operations that trigger a reschedule or reprogram the
timer from `preemptionPoint` to ensure the relevant state updates in
the proof occur where they are easier to verify.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

include/kernel/thread.h

@@ -229,20 +229,26 @@ static inline void updateTimestamp(void)
     time_t consumed = (NODE_STATE(ksCurTime) - prev);
     NODE_STATE(ksConsumed) += consumed;
     if (CONFIG_NUM_DOMAINS > 1) {
-
         if ((consumed + MIN_BUDGET) >= ksDomainTime) {
             ksDomainTime = 0;
         } else {
             ksDomainTime -= consumed;
         }
-        if (unlikely(isCurDomainExpired())) {
-            NODE_STATE(ksReprogram) = true;
-            rescheduleRequired();
-        }
     }
 
 }
 
+/*
+ * Check if domain time has expired
+ */
+static inline void checkDomainTime(void)
+{
+    if (unlikely(isCurDomainExpired())) {
+        NODE_STATE(ksReprogram) = true;
+        rescheduleRequired();
+    }
+}
+
 /* Check if the current thread/domain budget has expired.
  * if it has, bill the thread, add it to the scheduler and
  * set up a reschedule.

src/kernel/thread.c

@@ -352,6 +352,7 @@ void schedule(void)
 {
 #ifdef CONFIG_KERNEL_MCS
     awaken();
+    checkDomainTime();
 #endif
 
     if (NODE_STATE(ksSchedulerAction) != SchedulerAction_ResumeCurrentThread) {