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 
13 timestamp_t ksEnter;
14 seL4_Word ksLogIndex;
15 seL4_Word ksLogIndexFinalized;
16 
benchmark_track_exit(void)17 void 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