1/* 2 * Copyright 2016, General Dynamics C4 Systems 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 */ 6 7#include <config.h> 8#include <benchmark/benchmark_track.h> 9#include <model/statedata.h> 10 11#ifdef CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES 12 13timestamp_t ksEnter; 14seL4_Word ksLogIndex; 15seL4_Word ksLogIndexFinalized; 16 17void benchmark_track_exit(void) 18{ 19 timestamp_t duration = 0; 20 timestamp_t ksExit = timestamp(); 21 benchmark_track_kernel_entry_t *ksLog = (benchmark_track_kernel_entry_t *) KS_LOG_PPTR; 22 23 if (likely(ksUserLogBuffer != 0)) { 24 /* If Log buffer is filled, do nothing */ 25 if (likely(ksLogIndex < MAX_LOG_SIZE)) { 26 duration = ksExit - ksEnter; 27 ksLog[ksLogIndex].entry = ksKernelEntry; 28 ksLog[ksLogIndex].start_time = ksEnter; 29 ksLog[ksLogIndex].duration = duration; 30 ksLogIndex++; 31 } 32 } 33} 34#endif /* CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES */ 35