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