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