Added support for using multiple tracepoints at the same time.

Kconfig

@@ -276,10 +276,20 @@ menu "seL4 System Parameters"
         default n
         help    
             Enables a 1MB log buffer and functions for extracting data from it at user level.
-            Use TRACE_POINT_START and TRACE_POINT_STOP macros for recording data.
+            Use TRACE_POINT_START(k) and TRACE_POINT_STOP(k) macros for recording data, where k
+            is an integer used to identify log entries.
             NOTE this is only tested on the sabre and will not work on platforms with < 512mb memory.
             This is not fully implemented for x86.
 
+    config MAX_NUM_TRACE_POINTS
+        int "Maximum number of tracepoints"
+        depends on BENCHMARK
+        default 8
+        help
+            The maximum number of different trace point identifiers which can be used.
+            When using TRACE_POINT_START(k) and TRACE_POINT_STOP(k), the values of k must be from 0
+            to this value - 1. This value must be at most (2 ^ NUM_TRACE_POINT_ID_BITS).
+
 endmenu
 
 menu "Build Options"

include/api/syscall.xml

@@ -38,6 +38,7 @@
             <syscall name="BenchmarkResetLog" />
             <syscall name="BenchmarkDumpLog"  />
             <syscall name="BenchmarkLogSize"  />
+            <syscall name="BenchmarkFinalizeLog"  />
         </config>
     </debug>
 </syscalls>

include/arch/arm/arch/api/constants.h

@@ -0,0 +1,16 @@
+/*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ */
+
+#ifndef __ARCH_API_CONSTANTS_H
+#define __ARCH_API_CONSTANTS_H
+
+#define seL4_LogBufferSize (1<<20)
+
+#endif

include/arch/arm/arch/benchmark.h

@@ -15,14 +15,7 @@
 
 #include <armv/benchmark.h>
 
-/* We have 1MB of word sized entries */
-#define MAX_LOG_SIZE 262144
-
-extern word_t ksEntry;
-extern word_t ksExit;
-extern word_t ksLogIndex;
-extern word_t *ksLog;
-
+typedef uint32_t timestamp_t;
 
 void armv_init_ccnt(void);
 

include/arch/x86/arch/api/constants.h

@@ -0,0 +1,16 @@
+/*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ */
+
+#ifndef __ARCH_API_CONSTANTS_H
+#define __ARCH_API_CONSTANTS_H
+
+#define seL4_LogBufferSize (BIT(LARGE_PAGE_BITS))
+
+#endif

include/arch/x86/arch/benchmark.h

@@ -11,18 +11,9 @@
 #ifndef ARCH_BENCHMARK_H
 #define ARCH_BENCHMARK_H
 
-#include <config.h>
-#include <arch/object/structures.h>
-
 #ifdef CONFIG_BENCHMARK
 
-/* we have one large page of word sized entries */
-#define MAX_LOG_SIZE (BIT(LARGE_PAGE_BITS) / sizeof(word_t))
-
-extern uint64_t ksEntry;
-extern uint64_t ksExit;
-extern uint32_t ksLogIndex;
-extern uint32_t *ksLog;
+typedef uint64_t timestamp_t;
 
 #define IA32_KSLOG_IDX (BIT(PD_BITS + PDPT_BITS) - 2)
 

include/benchmark.h

@@ -13,32 +13,51 @@
 
 #include <arch/benchmark.h>
 #include <machine/io.h>
+#include <arch/api/constants.h>
 
 #ifdef CONFIG_BENCHMARK
-#define TRACE_POINT_START trace_point_start()
-#define TRACE_POINT_STOP   trace_point_stop()
+#define TRACE_POINT_START(x) trace_point_start(x)
+#define TRACE_POINT_STOP(x)   trace_point_stop(x)
+
+typedef struct ks_log_entry {
+    uint32_t key;
+    uint32_t data;
+} ks_log_entry_t;
+
+#define MAX_LOG_SIZE (seL4_LogBufferSize / sizeof(ks_log_entry_t))
+
+extern timestamp_t ksEntries[CONFIG_MAX_NUM_TRACE_POINTS];
+extern bool_t ksStarted[CONFIG_MAX_NUM_TRACE_POINTS];
+extern timestamp_t ksExit;
+extern uint32_t ksLogIndex;
+extern uint32_t ksLogIndexFinalized;
+extern ks_log_entry_t *ksLog;
 
 /* we can fill the entire IPC buffer except for word 0, which
  * the kernel overwrites with the message tag */
 #define MAX_IPC_BUFFER_STORAGE (1024 - 1)
 
 static inline void
-trace_point_start(void)
+trace_point_start(word_t id)
 {
-    ksEntry = timestamp();
+    ksEntries[id] = timestamp();
+    ksStarted[id] = true;
 }
 
 static inline void
-trace_point_stop(void)
+trace_point_stop(word_t id)
 {
     ksExit = timestamp();
 
-    if (likely(ksLogIndex < MAX_LOG_SIZE)) {
-        ksLog[ksLogIndex] = ksExit - ksEntry;
+    if (likely(ksStarted[id])) {
+        ksStarted[id] = false;
+        if (likely(ksLogIndex < MAX_LOG_SIZE)) {
+            ksLog[ksLogIndex] = (ks_log_entry_t) {id, ksExit - ksEntries[id]};
+        }
+        /* increment the log index even if we have exceeded the log size
+         * this is so we can tell if we need a bigger log */
+        ksLogIndex++;
     }
-    /* increment the log index even if we have exceeded the log size
-     * this is so we can tell if we need a bigger log */
-    ksLogIndex++;
 
     /* If this fails integer overflow has occured. */
     assert(ksLogIndex > 0);
@@ -46,8 +65,8 @@ trace_point_stop(void)
 
 #else
 
-#define TRACE_POINT_START
-#define TRACE_POINT_STOP
+#define TRACE_POINT_START(x)
+#define TRACE_POINT_STOP(x)
 
 #endif /* CONFIG_BENCHMARK */
 

include/config.h

@@ -70,6 +70,11 @@
 #define CONFIG_TIMER_TICK_MS 2
 #endif
 
+/* maximum number of different tracepoints which can be placed in the kernel */
+#ifndef CONFIG_MAX_NUM_TRACE_POINTS
+#define CONFIG_MAX_NUM_TRACE_POINTS 8
+#endif
+
 /* Configuration parameters below are for IA-32 only. */
 
 /* maximum number of nodes supported (if 1, a uniprocessor version is compiled) */

libsel4/arch_include/arm/sel4/arch/constants.h

@@ -13,4 +13,7 @@
 
 #include <sel4/arch/objecttype.h>
 
+/* size of kernel log buffer in bytes */
+#define seL4_LogBufferSize (1<<20)
+
 #endif

libsel4/arch_include/arm/sel4/arch/syscalls.h

@@ -597,6 +597,15 @@ seL4_BenchmarkLogSize(void)
 
 }
 
+static inline void
+seL4_BenchmarkFinalizeLog(void)
+{
+    register seL4_Word scno asm("r7") = seL4_SysBenchmarkFinalizeLog;
+    asm volatile ("swi %[swi_num]"
+                  : /* no outputs */
+                  : [swi_num] "i" __SWINUM(seL4_SysBenchmarkFinalizeLog), "r"(scno)
+                 );
+}
 
 #endif /* CONFIG_BENCHMARK */
 

libsel4/arch_include/x86/sel4/arch/constants.h

@@ -41,4 +41,7 @@
 #define MSI_MAX 0x1d
 #endif
 
+/* size of kernel log buffer in bytes */
+#define seL4_LogBufferSize (BIT(seL4_LargePageBits))
+
 #endif

libsel4/arch_include/x86/sel4/arch/syscalls.h

@@ -600,5 +600,21 @@ seL4_BenchmarkLogSize(void)
     return ret;
 }
 
+static inline void
+seL4_BenchmarkFinalizeLog(void)
+{
+    asm volatile (
+        "pushl %%ebp        \n"
+        "movl %%esp, %%ecx  \n"
+        "leal 1f, %%edx     \n"
+        "1:                 \n"
+        "sysenter           \n"
+        "popl %%ebp         \n"
+        :
+        : "a" (seL4_SysBenchmarkFinalizeLog)
+        : "%ecx", "%edx", "%edi", "memory"
+    );
+}
+
 #endif /* CONFIG_BENCHMARK */
 #endif

libsel4/include/api/syscall.xml

@@ -38,6 +38,7 @@
             <syscall name="BenchmarkResetLog" />
             <syscall name="BenchmarkDumpLog"  />
             <syscall name="BenchmarkLogSize"  />
+            <syscall name="BenchmarkFinalizeLog"  />
         </config>
     </debug>
 </syscalls>

libsel4/include/sel4/types.h

@@ -71,6 +71,11 @@ typedef seL4_CPtr seL4_DomainSet;
 
 #define seL4_NilData seL4_CapData_Badge_new(0)
 
+typedef struct {
+    seL4_Word key;
+    seL4_Word data;
+} seL4_LogEntry;
+
 #include <sel4/arch/constants.h>
 
 #endif

src/api/syscall.c

@@ -116,7 +116,7 @@ handleUnknownSyscall(word_t w)
         word_t *buffer = lookupIPCBuffer(true, ksCurThread);
         word_t start = getRegister(ksCurThread, capRegister);
         word_t size = getRegister(ksCurThread, msgInfoRegister);
-        word_t logSize = ksLogIndex > MAX_LOG_SIZE ? MAX_LOG_SIZE : ksLogIndex;
+        word_t logSize = ksLogIndexFinalized > MAX_LOG_SIZE ? MAX_LOG_SIZE : ksLogIndexFinalized;
 
         if (buffer == NULL) {
             userError("Cannot dump benchmarking log to a thread without an ipc buffer\n");
@@ -143,7 +143,10 @@ handleUnknownSyscall(word_t w)
 
         /* write to ipc buffer */
         for (i = 0; i < size; i++) {
-            buffer[i + 1] = ksLog[i + start];
+            int base_index = i * 2 + 1;
+            ks_log_entry_t *log = &ksLog[i + start];
+            buffer[base_index] = log->key;
+            buffer[base_index + 1] = log->data;
         }
 
         /* Return the amount written */
@@ -151,7 +154,10 @@ handleUnknownSyscall(word_t w)
         return EXCEPTION_NONE;
     } else if (w == SysBenchmarkLogSize) {
         /* Return the amount of log items we tried to log (may exceed max size) */
-        setRegister(ksCurThread, capRegister, ksLogIndex);
+        setRegister(ksCurThread, capRegister, ksLogIndexFinalized);
+        return EXCEPTION_NONE;
+    } else if (w == SysBenchmarkFinalizeLog) {
+        ksLogIndexFinalized = ksLogIndex;
         return EXCEPTION_NONE;
     }
 #endif /* CONFIG_BENCHMARK */

src/arch/arm/api/benchmark.c

@@ -12,11 +12,14 @@
 
 #include <benchmark.h>
 #include <arch/benchmark.h>
+#include <stdbool.h>
 
-uint32_t ksEntry;
-uint32_t ksExit;
+timestamp_t ksEntries[CONFIG_MAX_NUM_TRACE_POINTS];
+bool_t ksStarted[CONFIG_MAX_NUM_TRACE_POINTS];
+timestamp_t ksExit;
 uint32_t ksLogIndex = 0;
-uint32_t *ksLog;
+uint32_t ksLogIndexFinalized = 0;
+ks_log_entry_t *ksLog;
 
 #endif /* CONFIG_BENCHMARK */
 

src/arch/arm/kernel/vspace.c

@@ -233,7 +233,7 @@ map_kernel_window(void)
               0  /* Write-through to minimise perf hit */
           );
     armKSGlobalPD[idx] = pde;
-    ksLog = (word_t *) ptrFromPAddr(phys);
+    ksLog = (ks_log_entry_t *) ptrFromPAddr(phys);
 
     /* we remove the address PADDR_TOP - 1MB from the
      * available physical memory for the sabre.
@@ -241,7 +241,7 @@ map_kernel_window(void)
      * if you are using a different platform this may need
      * adjusting or you may need to do something completely different
      * to get a 1mb, write through buffer*/
-    assert(ksLog == ((word_t *) KS_LOG_PADDR));
+    assert(ksLog == ((ks_log_entry_t *) KS_LOG_PADDR));
     phys += BIT(pageBitsForSize(ARMSection));
     idx++;
 #endif /* CONFIG_BENCHMARK */

src/arch/x86/api/benchmark.c

@@ -13,11 +13,14 @@
 #include <benchmark.h>
 #include <arch/benchmark.h>
 #include <arch/machine/hardware.h>
+#include <stdbool.h>
 
-DATA_GLOB uint64_t ksEntry;
-DATA_GLOB uint64_t ksExit;
+DATA_GLOB timestamp_t ksEntries[CONFIG_MAX_NUM_TRACE_POINTS];
+DATA_GLOB bool_t ksStarted[CONFIG_MAX_NUM_TRACE_POINTS];
+DATA_GLOB timestamp_t ksExit;
 DATA_GLOB uint32_t ksLogIndex = 0;
-DATA_GLOB uint32_t *ksLog;
+DATA_GLOB uint32_t ksLogIndexFinalized = 0;
+DATA_GLOB ks_log_entry_t *ksLog;
 
 #endif /* CONFIG_BENCHMARK */
 

src/arch/x86/kernel/boot.c

@@ -397,9 +397,9 @@ init_node_state(
     /* if we crash here, the log isn't working */
 #ifdef CONFIG_DEBUG_BUILD
     printf("Testing log\n");
-    ksLog[0] = 0xdeadbeef;
-    printf("Wrote to ksLog %x\n", ksLog[0]);
-    assert(ksLog[0] == 0xdeadbeef);
+    ksLog[0].data = 0xdeadbeef;
+    printf("Wrote to ksLog %x\n", ksLog[0].data);
+    assert(ksLog[0].data == 0xdeadbeef);
 #endif /* CONFIG_DEBUG_BUILD */
 #endif /* CONFIG_BENCHMARK */
 

src/arch/x86/kernel/vspace.c

@@ -560,7 +560,7 @@ map_kernel_window(
     /* mark the address of the log. We will map it
         * in later with the correct attributes, but we need
         * to wait until we can call alloc_region. */
-    ksLog = (word_t *) paddr_to_pptr(phys);
+    ksLog = (ks_log_entry_t *) paddr_to_pptr(phys);
     phys += BIT(LARGE_PAGE_BITS);
     assert(idx == IA32_KSLOG_IDX);
     idx++;