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#pragma once
14
15#include <autoconf.h>
16#include <assert.h>
17#include <sel4/sel4.h>
18#ifdef CONFIG_DEBUG_BUILD
19#include <sel4debug/debug.h>
20#endif
21#include <vka/vka.h>
22#include <vka/object.h>
23#include <stddef.h>
24#include <sync/bin_sem_bare.h>
25
26typedef struct {
27    vka_object_t notification;
28    volatile int value;
29} sync_bin_sem_t;
30
31/* Initialise an unmanaged binary semaphore with a notification object
32 * @param sem           A semaphore object to be initialised.
33 * @param notification  A notification object to use for the lock.
34 * @param value         The initial value for the semaphore. Must be 0 or 1.
35 * @return              0 on success, an error code on failure. */
36static inline int sync_bin_sem_init(sync_bin_sem_t *sem, seL4_CPtr notification, int value)
37{
38    if (sem == NULL) {
39        ZF_LOGE("Semaphore passed to sync_bin_sem_init was NULL");
40        return -1;
41    }
42
43    if (value != 0 && value != 1) {
44        ZF_LOGE("Binary semaphore initial value neither 0 nor 1");
45        return -1;
46    }
47
48#ifdef CONFIG_DEBUG_BUILD
49    /* Check the cap actually is a notification. */
50    assert(debug_cap_is_notification(notification));
51#endif
52
53    sem->notification.cptr = notification;
54    sem->value = value;
55    return 0;
56}
57
58/* Wait on a binary semaphore
59 * @param sem           An initialised semaphore to acquire.
60 * @return              0 on success, an error code on failure. */
61static inline int sync_bin_sem_wait(sync_bin_sem_t *sem)
62{
63    if (sem == NULL) {
64        ZF_LOGE("Semaphore passed to sync_bin_sem_wait was NULL");
65        return -1;
66    }
67    return sync_bin_sem_bare_wait(sem->notification.cptr, &sem->value);
68}
69
70/* Signal a binary semaphore
71 * @param sem           An initialised semaphore to release.
72 * @return              0 on success, an error code on failure. */
73static inline int sync_bin_sem_post(sync_bin_sem_t *sem)
74{
75    if (sem == NULL) {
76        ZF_LOGE("Semaphore passed to sync_bin_sem_post was NULL");
77        return -1;
78    }
79    return sync_bin_sem_bare_post(sem->notification.cptr, &sem->value);
80}
81
82/* Allocate and initialise a managed binary semaphore
83 * @param vka           A VKA instance used to allocate a notification object.
84 * @param sem           A semaphore object to initialise.
85 * @param value         The initial value for the semaphore. Must be 0 or 1.
86 * @return              0 on success, an error code on failure. */
87static inline int sync_bin_sem_new(vka_t *vka, sync_bin_sem_t *sem, int value)
88{
89    if (sem == NULL) {
90        ZF_LOGE("Semaphore passed to sync_bin_sem_new was NULL");
91        return -1;
92    }
93    if (value != 0 && value != 1) {
94        ZF_LOGE("Binary semaphore initial value neither 0 nor 1");
95        return -1;
96    }
97    int error = vka_alloc_notification(vka, &(sem->notification));
98
99    if (error != 0) {
100        return error;
101    } else {
102        return sync_bin_sem_init(sem, sem->notification.cptr, value);
103    }
104}
105
106/* Deallocate a managed binary semaphore (do not use with sync_bin_sem_init)
107 * @param vka           A VKA instance used to deallocate the notification object.
108 * @param sem           A semaphore object initialised by sync_bin_sem_new.
109 * @return              0 on success, an error code on failure. */
110static inline int sync_bin_sem_destroy(vka_t *vka, sync_bin_sem_t *sem)
111{
112    if (sem == NULL) {
113        ZF_LOGE("Semaphore passed to sync_bin_sem_destroy was NULL");
114        return -1;
115    }
116    vka_free_object(vka, &(sem->notification));
117    return 0;
118}
119
120