use LibSel4UseThreadLocals to disable TLS ipcbuf

.github/workflows/sdk.yaml

@@ -16,7 +16,7 @@ on:
     branches: [ "main" ]
 
 env:
-  SEL4_VERSION: c55f50b6e5e5c753ec9295d85ed5dff91a1e1562
+  SEL4_VERSION: efd9426e1771b6cdbcc7e58d3fd58d3df77c337e
 
 # To reduce the load we cancel any older runs of this workflow for the current
 # PR. For deployment to the main branch, the workflow will run on each push,

DEVELOPER.md

@@ -120,7 +120,7 @@ It should be noted that while Microkit uses mainline seL4, it is fairly tied to
 specific version used.
 
 For this version of Microkit please use the following commit:
-`c55f50b6e5e5c753ec9295d85ed5dff91a1e1562`.
+`efd9426e1771b6cdbcc7e58d3fd58d3df77c337e`.
 
 ## Building the SDK
 

build_sdk.py

@@ -45,6 +45,13 @@
 DEFAULT_KERNEL_OPTIONS = {
     "KernelIsMCS": True,
     "KernelRootCNodeSizeBits": "17",
+    # Thread local storage is painful and annoying to configure.
+    # We'd really rather NOT use thread local storage (especially
+    # considering we never have more than one thread in a VSpace)
+    #
+    # Turning off this feature removes the __thread attribute on
+    # __sel4_ipc_buffer and makes it a true global.
+    "LibSel4UseThreadLocals": False,
 }
 
 DEFAULT_KERNEL_OPTIONS_AARCH64 = {

libmicrokit/include/microkit.h

@@ -9,7 +9,6 @@
 
 #pragma once
 
-#define __thread
 #include <sel4/sel4.h>
 
 typedef unsigned int microkit_channel;

libmicrokit/src/dbg.c

@@ -5,7 +5,6 @@
  */
 #include <microkit.h>
 
-#define __thread
 #include <sel4/sel4.h>
 
 void microkit_dbg_putc(int c)

libmicrokit/src/main.c

@@ -7,7 +7,6 @@
 #include <stddef.h>
 #include <stdint.h>
 
-#define __thread
 #include <sel4/sel4.h>
 
 #include <microkit.h>

monitor/src/main.c

@@ -12,27 +12,6 @@
  *   Acting as the fault handler for protection domains.
  */
 
-/*
- * Why this you may ask? Well, the seL4 headers depend on
- * a global `__sel4_ipc_buffer` which is a pointer to the
- * thread's IPC buffer. Which is reasonable enough, passing
- * that explicitly to every function would be annoying.
- *
- * The seL4 headers make this global a thread-local global,
- * which is also reasonable, considering it applies to a
- * specific thread! But, for our purposes we don't have threads!
- *
- * Thread local storage is painful and annoying to configure.
- * We'd really rather NOT use thread local storage (especially
- * consider we never have more than one thread in a Vspace)
- *
- * So, by defining __thread to be empty it means the variable
- * becomes a true global rather than thread local storage
- * variable, which means, we don't need to waste a bunch
- * of effort and complexity on thread local storage implementation.
- */
-#define __thread
-
 #include <stdbool.h>
 #include <stdint.h>
 #include <sel4/sel4.h>