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