Benchmarking

build_sdk.py

@@ -72,6 +72,20 @@ class ConfigInfo:
         examples = {
             "hello": Path("example/zcu102/hello")
         }
+    ),
+    BoardInfo(
+        name="imx8mm",
+        gcc_cpu="cortex-a53",
+        loader_link_address=0x41000000,
+        kernel_options = {
+            "KernelPlatform": "imx8mm-evk",
+            "KernelIsMCS": True,
+            "KernelArmExportPCNTUser": True,
+            "KernelArmExportPMUUser": True,
+        },
+        examples = {
+            "ethernet": Path("example/imx8mm/passive_server")
+        }
     )
 )
 
@@ -81,6 +95,14 @@ class ConfigInfo:
         debug=False,
         kernel_options = {},
     ),
+    ConfigInfo(
+        name="benchmark",
+        debug=False,
+        kernel_options = {
+            "KernelDebugBuild": False,
+            "KernelBenchmarks": "track_utilisation"
+        },
+    ),
     ConfigInfo(
         name="debug",
         debug=True,
@@ -89,7 +111,7 @@ class ConfigInfo:
             "KernelPrinting": True,
             "KernelVerificationBuild": False
         }
-    ),
+    )
 )
 
 

example/imx8mm/passive_server/Makefile

@@ -0,0 +1,59 @@
+#
+# Copyright 2021, Breakaway Consulting Pty. Ltd.
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+ifeq ($(strip $(BUILD_DIR)),)
+$(error BUILD_DIR must be specified)
+endif
+
+ifeq ($(strip $(SEL4CP_SDK)),)
+$(error SEL4CP_SDK must be specified)
+endif
+
+ifeq ($(strip $(SEL4CP_BOARD)),)
+$(error SEL4CP_BOARD must be specified)
+endif
+
+ifeq ($(strip $(SEL4CP_CONFIG)),)
+$(error SEL4CP_CONFIG must be specified)
+endif
+
+TOOLCHAIN := aarch64-unknown-linux-gnu
+
+CPU := cortex-a53
+
+CC := $(TOOLCHAIN)-gcc
+LD := $(TOOLCHAIN)-ld
+AS := $(TOOLCHAIN)-as
+SEL4CP_TOOL ?= $(SEL4CP_SDK)/bin/sel4cp
+
+SERVER_OBJS := server.o
+CLIENT_OBJS := client.o
+
+BOARD_DIR := $(SEL4CP_SDK)/board/$(SEL4CP_BOARD)/$(SEL4CP_CONFIG)
+
+IMAGES := server.elf client.elf
+CFLAGS := -mcpu=$(CPU) -mstrict-align -nostdlib -ffreestanding -g3 -O3 -Wall  -Wno-unused-function -Werror -I$(BOARD_DIR)/include
+LDFLAGS := -L$(BOARD_DIR)/lib
+LIBS := -lsel4cp -Tsel4cp.ld
+
+IMAGE_FILE = $(BUILD_DIR)/loader.img
+REPORT_FILE = $(BUILD_DIR)/report.txt
+
+all: $(IMAGE_FILE)
+
+$(BUILD_DIR)/%.o: %.c Makefile
+	$(CC) -c $(CFLAGS) $< -o $@
+
+$(BUILD_DIR)/%.o: %.s Makefile
+	$(AS) -g3 -mcpu=$(CPU) $< -o $@
+
+$(BUILD_DIR)/server.elf: $(addprefix $(BUILD_DIR)/, $(SERVER_OBJS))
+	$(LD) $(LDFLAGS) $^ $(LIBS) -o $@
+
+$(BUILD_DIR)/client.elf: $(addprefix $(BUILD_DIR)/, $(CLIENT_OBJS))
+	$(LD) $(LDFLAGS) $^ $(LIBS) -o $@
+
+$(IMAGE_FILE) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(IMAGES)) passive_server.system
+	$(SEL4CP_TOOL) passive_server.system --search-path $(BUILD_DIR) --board $(SEL4CP_BOARD) --config $(SEL4CP_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE)

example/imx8mm/passive_server/client.c

@@ -0,0 +1,24 @@
+/*
+ * Copyright 2022, UNSW
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+#include <sel4cp.h>
+
+#define SERVER_CH 0 
+
+void
+init(void)
+{
+    sel4cp_dbg_puts("client: client protection domain init function running\n");
+
+    /* message the server */
+    sel4cp_mr_set(0, 0);
+    (void) sel4cp_ppcall(SERVER_CH, sel4cp_msginfo_new(1, 1));
+}
+
+void
+notified(sel4cp_channel ch)
+{
+    sel4cp_dbg_puts("Client recieved a notification on an unexpected channel\n");
+}

example/imx8mm/passive_server/passive_server.system

@@ -0,0 +1,21 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2022, UNSW
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <protection_domain name="server" priority="100" pp="true" passive="true">
+        <program_image path="server.elf" />
+    </protection_domain>
+
+    <protection_domain name="client" priority="99">
+        <program_image path="client.elf" />
+    </protection_domain>
+
+    <channel>
+        <end pd="server" id="0" />
+        <end pd="client" id="0" />
+    </channel>
+
+</system>

example/imx8mm/passive_server/server.c

@@ -0,0 +1,33 @@
+/*
+ * Copyright 2022, UNSW
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+#include <sel4cp.h>
+
+sel4cp_msginfo 
+protected(sel4cp_channel ch, sel4cp_msginfo msginfo)
+{
+    switch (sel4cp_msginfo_get_label(msginfo)) {
+        case 0:
+            sel4cp_dbg_puts("Server is running on clients scheduling context\n");
+            break;
+        default:
+            sel4cp_dbg_puts("server received an unexpected message\n");
+    }
+
+    return seL4_MessageInfo_new(0, 0, 0, 0);
+}
+
+void
+init(void)
+{
+    sel4cp_dbg_puts("server: server protection domain init function running\n");
+    /* Nothing to initialise */
+}
+
+void
+notified(sel4cp_channel ch)
+{
+    sel4cp_dbg_puts("Server recieved a notification on an unexpected channel\n");
+}

libsel4cp/include/sel4cp.h

@@ -8,13 +8,16 @@
 #pragma once
 
 #include <stdint.h>
+#include <stdbool.h>
 
 #define __thread
 #include <sel4/sel4.h>
 
 typedef unsigned int sel4cp_channel;
 typedef seL4_MessageInfo_t sel4cp_msginfo;
 
+#define MONITOR_EP 5
+#define TCB_CAP 6
 #define BASE_OUTPUT_NOTIFICATION_CAP 10
 #define BASE_ENDPOINT_CAP 74
 #define BASE_IRQ_CAP 138
@@ -27,6 +30,10 @@ void notified(sel4cp_channel ch);
 sel4cp_msginfo protected(sel4cp_channel ch, sel4cp_msginfo msginfo);
 
 extern char sel4cp_name[16];
+/* These next three variables are so our PDs can combine a signal with the next Recv syscall */
+extern bool have_signal;
+extern seL4_CPtr signal;
+extern seL4_MessageInfo_t signal_msg;
 
 /*
  * Output a single character on the debug console.

libsel4cp/src/main.c

@@ -19,7 +19,11 @@
 
 char _stack[4096]  __attribute__((__aligned__(16)));
 
+bool passive;
 char sel4cp_name[16];
+bool have_signal = false;
+seL4_CPtr signal;
+seL4_MessageInfo_t signal_msg;
 
 extern seL4_IPCBuffer __sel4_ipc_buffer_obj;
 
@@ -54,6 +58,8 @@ handler_loop(void)
 
         if (have_reply) {
             tag = seL4_ReplyRecv(INPUT_CAP, reply_tag, &badge, REPLY_CAP);
+        } else if (have_signal) {
+            tag = seL4_NBSendRecv(signal, signal_msg, INPUT_CAP, &badge, REPLY_CAP);
         } else {
             tag = seL4_Recv(INPUT_CAP, &badge, REPLY_CAP);
         }
@@ -82,5 +88,19 @@ main(void)
 {
     run_init_funcs();
     init();
+
+    /* 
+     If we are passive, now our initialisation is complete we can
+     signal the monitor to unbind our scheduling context and bind
+     it to our notification object. 
+     We delay this signal so we are ready waiting on a recv() syscall
+    */
+    if (passive) {
+        have_signal = true;
+        signal_msg = seL4_MessageInfo_new(0, 0, 0, 1);
+        seL4_SetMR(0, 0);
+        signal = (MONITOR_EP);
+    }
+
     handler_loop();
 }

loader/src/loader.c

@@ -26,10 +26,6 @@ _Static_assert(sizeof(uintptr_t) == 8 || sizeof(uintptr_t) == 4, "Expect uintptr
 
 #define STACK_SIZE 4096
 
-#define UART_BASE 0x5a070000
-#define STAT 0x14
-#define TRANSMIT 0x1c
-#define STAT_TDRE (1 << 23)
 #define UART_REG(x) ((volatile uint32_t *)(UART_BASE + (x)))
 
 #if defined(BOARD_zcu102)
@@ -113,13 +109,35 @@ memcpy(void *dst, const void *src, size_t sz)
 }
 
 #if defined(BOARD_tqma8xqp1gb)
+#define UART_BASE 0x5a070000
+#define STAT 0x14
+#define TRANSMIT 0x1c
+#define STAT_TDRE (1 << 23)
+
+static void
+putc(uint8_t ch)
+{
+    while (!(*UART_REG(STAT) & STAT_TDRE)) { }
+    *UART_REG(TRANSMIT) = ch;
+}
+#elif defined(BOARD_imx8mm)
+#define UART_BASE 0x30890000
+#define STAT 0x98
+#define TRANSMIT 0x40
+#define STAT_TDRE (1 << 14)
+
 static void
 putc(uint8_t ch)
 {
     while (!(*UART_REG(STAT) & STAT_TDRE)) { }
     *UART_REG(TRANSMIT) = ch;
 }
 #elif defined(BOARD_zcu102)
+#define UART_BASE 0x5a070000
+#define STAT 0x14
+#define TRANSMIT 0x1c
+#define STAT_TDRE (1 << 23)
+
 static void
 putc(uint8_t ch)
 {

monitor/src/main.c

@@ -79,7 +79,7 @@
  *
  * FIXME: This can be smaller once compression is enabled.
  */
-#define BOOTSTRAP_INVOCATION_DATA_SIZE 90
+#define BOOTSTRAP_INVOCATION_DATA_SIZE 110
 
 seL4_IPCBuffer *__sel4_ipc_buffer;
 
@@ -90,6 +90,8 @@ static char pd_names[MAX_PDS][MAX_NAME_LEN];
 seL4_Word fault_ep;
 seL4_Word reply;
 seL4_Word tcbs[MAX_TCBS];
+seL4_Word scheduling_contexts[MAX_TCBS];
+seL4_Word notification_caps[MAX_TCBS];
 
 struct region {
     uintptr_t paddr;
@@ -369,6 +371,19 @@ monitor(void)
         puthex64(tcb_cap);
         puts("\n");
 
+        if (label == seL4_Fault_NullFault && badge < MAX_PDS) {
+            /* This is a request from our PD to become passive */ 
+            err = seL4_SchedContext_UnbindObject(scheduling_contexts[badge], tcb_cap);
+            err = seL4_SchedContext_Bind(scheduling_contexts[badge], notification_caps[badge]);
+            if (err != seL4_NoError) {
+                puts("error binding scheduling context to notification");
+            } else {
+                puts(pd_names[badge]);
+                puts(" is now passive!\n");
+            }
+            continue;
+        }
+
         if (badge < MAX_PDS && pd_names[badge][0] != 0) {
             puts("faulting PD: ");
             puts(pd_names[badge]);