1/*
2 * Copyright 2017, Data61
3 * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
4 * ABN 41 687 119 230.
5 *
6 * This software may be distributed and modified according to the terms of
7 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
8 * See "LICENSE_BSD2.txt" for details.
9 *
10 * @TAG(DATA61_BSD)
11 */
12
13#include <autoconf.h>
14#include <sel4test-driver/gen_config.h>
15
16#ifdef CONFIG_BENCHMARK_TRACK_UTILISATION
17#include <sel4/sel4.h>
18#include <vka/object.h>
19
20#include <utils/util.h>
21#include <sel4/benchmark_utilisation_types.h>
22#include "../helpers.h"
23
24static int test_benchmark_utilisation(env_t env)
25{
26
27    uint64_t *__attribute__((__may_alias__)) ipcbuffer = (uint64_t *) & (seL4_GetIPCBuffer()->msg[0]);
28
29    seL4_BenchmarkResetThreadUtilisation(simple_get_tcb(&env->simple));
30
31    seL4_BenchmarkResetLog();
32
33    /* Sleep, and allow Idle thread to run */
34    sel4test_sleep(env, NS_IN_S);
35
36    seL4_BenchmarkFinalizeLog();
37
38    seL4_BenchmarkGetThreadUtilisation(simple_get_tcb(&env->simple));
39
40    THREAD_MEMORY_FENCE();
41
42    /* Idle thread should run and get us a non-zero value */
43    test_neq(ipcbuffer[BENCHMARK_IDLE_LOCALCPU_UTILISATION], (uint64_t) 0);
44
45    /* Current thread should run (overhead of loop and calling ltimer functions) */
46    test_neq(ipcbuffer[BENCHMARK_TOTAL_UTILISATION], (uint64_t) 0);
47
48    /* Idle thread should be less than the overall utilisation */
49    test_lt(ipcbuffer[BENCHMARK_IDLE_LOCALCPU_UTILISATION], ipcbuffer[BENCHMARK_TOTAL_UTILISATION]);
50
51    /*
52     * We slept/blocked for 1 second, so idle thread should get scheduled at least 75% of this time.
53     * It's assumed (and how sel4test works currently) that THIS thread is the highest
54     * priority running thread, and all other threads are blocked, in order for the idle thread to run.
55     */
56    test_gt(((ipcbuffer[BENCHMARK_IDLE_LOCALCPU_UTILISATION] * 100) /
57             ipcbuffer[BENCHMARK_TOTAL_UTILISATION]), (uint64_t) 50);
58
59    return sel4test_get_result();
60}
61DEFINE_TEST(BENCHMARK_0001, "Test seL4 Benchmarking API - Utilisation", test_benchmark_utilisation,
62            config_set(CONFIG_HAVE_TIMER));
63#endif /* CONFIG_BENCHMARK_TRACK_UTILISATION */
64