1/* 2 * Copyright 2017, Data61 3 * Commonwealth Scientific and Industrial Research Organisation (CSIRO) 4 * ABN 41 687 119 230. 5 * 6 * This software may be distributed and modified according to the terms of 7 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 8 * See "LICENSE_BSD2.txt" for details. 9 * 10 * @TAG(DATA61_BSD) 11 */ 12 13#pragma once 14#include <autoconf.h> 15#include <sel4utils/gen_config.h> 16#ifdef CONFIG_BENCHMARK_TRACEPOINTS 17#include <inttypes.h> 18#include <stdio.h> 19 20#include <sel4/simple_types.h> 21#include <sel4/benchmark_tracepoints_types.h> 22 23/** 24 * Dump the benchmark log. The kernel must be compiled with CONFIG_MAX_NUM_TRACE_POINTS > 0, 25 * either edit .config manually or add it using "make menuconfig" by selecting 26 * "Kernel" -> "seL4 System Parameters" -> "Adds a log buffer to the kernel for instrumentation." 27 */ 28static inline void seL4_BenchmarkTraceDumpFullLog(benchmark_tracepoint_log_entry_t *logBuffer, size_t logSize) 29{ 30 seL4_Word index = 0; 31 FILE *fd = stdout; 32 33 while ((index * sizeof(benchmark_tracepoint_log_entry_t)) < logSize) { 34 if (logBuffer[index].duration != 0) { 35 fprintf(fd, "tracepoint id = %u \tduration = %u\n", logBuffer[index].id, logBuffer[index].duration); 36 } 37 index++; 38 } 39 40 fprintf(fd, "Dumped entire log, size %" PRIu32 "\n", index); 41} 42#endif /* CONFIG_BENCHMARK_TRACEPOINTS */ 43