11556Srgrimes/* 250471Speter * Copyright 2016, General Dynamics C4 Systems 31556Srgrimes * 4298107Sgjb * This software may be distributed and modified according to the terms of 51556Srgrimes * the GNU General Public License version 2. Note that NO WARRANTY is provided. 61556Srgrimes * See "LICENSE_GPLv2.txt" for details. 71556Srgrimes * 8 * @TAG(GD_GPL) 9 */ 10 11#include <config.h> 12#include <benchmark/benchmark_track.h> 13#include <model/statedata.h> 14 15#ifdef CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES 16 17timestamp_t ksEnter; 18seL4_Word ksLogIndex; 19seL4_Word ksLogIndexFinalized; 20 21void benchmark_track_exit(void) 22{ 23 timestamp_t duration = 0; 24 timestamp_t ksExit = timestamp(); 25 benchmark_track_kernel_entry_t *ksLog = (benchmark_track_kernel_entry_t *) KS_LOG_PPTR; 26 27 if (likely(ksUserLogBuffer != 0)) { 28 /* If Log buffer is filled, do nothing */ 29 if (likely(ksLogIndex < MAX_LOG_SIZE)) { 30 duration = ksExit - ksEnter; 31 ksLog[ksLogIndex].entry = ksKernelEntry; 32 ksLog[ksLogIndex].start_time = ksEnter; 33 ksLog[ksLogIndex].duration = duration; 34 ksLogIndex++; 35 } 36 } 37} 38#endif /* CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES */ 39