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