1/*
2 * Copyright 2018, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 */
6
7#include <camkes.h>
8#include <stdio.h>
9#include <stdlib.h>
10#include <inttypes.h>
11
12#define IPRINT(format, ...) printf("%s: " format, get_instance_name(), ##__VA_ARGS__);
13
14#define MAX_VALUE  100000llu
15#define RATE  10000llu
16
17uint64_t acc = 0;
18
19int run() {
20
21    IPRINT("--- Starting ---\n");
22
23    while (acc < MAX_VALUE) {
24        /* do calculations to waste time */
25        acc *= 17;
26        acc++;
27        acc /= 17;
28        acc++;
29        if (acc % RATE == 0) {
30            IPRINT("acc = %"PRIuPTR"\n", acc);
31            seL4_Yield();
32        }
33    }
34
35    IPRINT("*** DONE %"PRIuPTR" ***\n", acc);
36
37    return 0;
38}
39