1/*
2 * Copyright 2016, 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(D61_BSD)
11 */
12
13#ifndef _TIMER_SERVER_DISPATCHER_DSPACE_TIMER_H_
14#define _TIMER_SERVER_DISPATCHER_DSPACE_TIMER_H_
15
16#include "../../badge.h"
17
18/*! @file
19    @brief Timer dataspace interface functions. */
20
21/*! @brief Similar to data_open_handler, for timer dataspaces. */
22seL4_CPtr timer_open_handler(void *rpc_userptr , char* rpc_name , int rpc_flags , int rpc_mode ,
23                              int rpc_size , int* rpc_errno);
24
25/*! @brief Similar to data_write_handler, for timer dataspaces.
26
27    Writing a uint64_t to the timer dspace will be interpreted as sleeping for that many nanoseconds
28    akin to a nanosleep() syscall, before returning.
29*/
30int timer_write_handler(void *rpc_userptr , seL4_CPtr rpc_dspace_fd , uint32_t rpc_offset ,
31                         rpc_buffer_t rpc_buf , uint32_t rpc_count);
32
33/*! @brief Similar to data_read_handler, for timer dataspaces.
34
35    Reading a uint64_t from the timer dspace will be interpreted as reading the current time in
36    nanoseconds.
37*/
38int timer_read_handler(void *rpc_userptr , seL4_CPtr rpc_dspace_fd , uint32_t rpc_offset ,
39                        rpc_buffer_t rpc_buf , uint32_t rpc_count);
40
41#endif /* _TIMER_SERVER_DISPATCHER_DSPACE_TIMER_H_ */