From 68671dbc2f0db7be0bdb7066234e6c82ded43877 Mon Sep 17 00:00:00 2001
From: Norman Feske <norman.feske@genode-labs.com>
Date: Wed, 29 Oct 2014 16:38:28 +0100
Subject: [PATCH] sel4: preemptive scheduling

---
 repos/base-sel4/doc/notes.txt         | 43 +++++++++++++++++++++++++++
 repos/base-sel4/src/test/sel4/main.cc | 10 ++++++-
 2 files changed, 52 insertions(+), 1 deletion(-)

diff --git a/repos/base-sel4/doc/notes.txt b/repos/base-sel4/doc/notes.txt
index 96de86b99e..e81b90abe8 100644
--- a/repos/base-sel4/doc/notes.txt
+++ b/repos/base-sel4/doc/notes.txt
@@ -1097,3 +1097,46 @@ When executing the code, we get the desired result:
 
 From these messages, we can see that both the main thread and the second
 thread are faulting at their designated fault addresses.
+
+Now, with two threads in place, we can test-drive the preemptive scheduling of
+the kernel by changing the 'second_thread_entry' function to:
+
+! static int volatile cnt = 0;
+!
+! void second_thread_entry()
+! {
+!   for (;;)
+!     cnt++;
+! }
+
+At the end of the main function, we repeatedly print the counter value:
+
+! for (;;)
+!   PDBG("cnt = %d", cnt);
+
+When executing the code, the counter values surprisingly stays at the value
+0. This is because the just-created new thread has a lower priority than the
+main thread. By explicitly assigning the maximum priority to the second
+thread, we can enable the preemptive round-robin scheduling:
+
+! seL4_TCB_SetPriority(SECOND_THREAD_CAP, 0xff);
+
+Now, we can see the counter value nicely increasing:
+
+! int main(): cnt = 0
+! ...
+! int main(): cnt = 0
+! int main(): cnt = 2908738
+! ...
+! int main(): cnt = 2908738
+! int main(): cnt = 5876191
+! ...
+! int main(): cnt = 5876191
+! ...
+
+Each thread consumes its entire time slice. This way, the second thread has
+the chance to increment the counter circa 3 million times per time slice after
+which the main thread has the chance to print the counter about 50 times
+before being preempted again.
+
+
diff --git a/repos/base-sel4/src/test/sel4/main.cc b/repos/base-sel4/src/test/sel4/main.cc
index 0e916252dd..590ebd2f6f 100644
--- a/repos/base-sel4/src/test/sel4/main.cc
+++ b/repos/base-sel4/src/test/sel4/main.cc
@@ -68,9 +68,13 @@ static inline void init_ipc_buffer()
 }
 
 
+static int volatile cnt = 0;
+
+
 void second_thread_entry()
 {
-	*(int *)0x2244 = 0;
+	for (;;)
+		cnt++;
 }
 
 
@@ -137,6 +141,10 @@ int main()
 
 	seL4_TCB_Resume(SECOND_THREAD_CAP);
 
+	seL4_TCB_SetPriority(SECOND_THREAD_CAP, 0xff);
+
+	for (;;)
+		PDBG("cnt = %d", cnt);
 
 	*(int *)0x1122 = 0;
 	return 0;