blob: e24ff065c8f833d30058300f70a0e35f6a6527a7 [file] [log] [blame]
/*
* Copyright 2017, Data61
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
* ABN 41 687 119 230.
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(DATA61_BSD)
*/
#pragma once
#include <autoconf.h>
#include <assert.h>
#include <sel4/sel4.h>
#include <vka/vka.h>
#include <vka/object.h>
#include <stddef.h>
#include <sync/bin_sem_bare.h>
typedef struct {
vka_object_t notification;
volatile int value;
} sync_bin_sem_t;
/* Initialise an unmanaged binary semaphore with a notification object
* @param sem A semaphore object to be initialised.
* @param notification A notification object to use for the lock.
* @param value The initial value for the semaphore. Must be 0 or 1.
* @return 0 on success, an error code on failure. */
static inline int sync_bin_sem_init(sync_bin_sem_t *sem, seL4_CPtr notification, int value)
{
if (sem == NULL) {
ZF_LOGE("Semaphore passed to sync_bin_sem_init was NULL");
return -1;
}
if (value != 0 && value != 1) {
ZF_LOGE("Binary semaphore initial value neither 0 nor 1");
return -1;
}
#ifdef CONFIG_DEBUG_BUILD
/* Check the cap actually is a notification. */
assert(seL4_DebugCapIdentify(notification) == 6);
#endif
sem->notification.cptr = notification;
sem->value = value;
return 0;
}
/* Wait on a binary semaphore
* @param sem An initialised semaphore to acquire.
* @return 0 on success, an error code on failure. */
static inline int sync_bin_sem_wait(sync_bin_sem_t *sem)
{
if (sem == NULL) {
ZF_LOGE("Semaphore passed to sync_bin_sem_wait was NULL");
return -1;
}
return sync_bin_sem_bare_wait(sem->notification.cptr, &sem->value);
}
/* Signal a binary semaphore
* @param sem An initialised semaphore to release.
* @return 0 on success, an error code on failure. */
static inline int sync_bin_sem_post(sync_bin_sem_t *sem)
{
if (sem == NULL) {
ZF_LOGE("Semaphore passed to sync_bin_sem_post was NULL");
return -1;
}
return sync_bin_sem_bare_post(sem->notification.cptr, &sem->value);
}
/* Allocate and initialise a managed binary semaphore
* @param vka A VKA instance used to allocate a notification object.
* @param sem A semaphore object to initialise.
* @param value The initial value for the semaphore. Must be 0 or 1.
* @return 0 on success, an error code on failure. */
static inline int sync_bin_sem_new(vka_t *vka, sync_bin_sem_t *sem, int value)
{
if (sem == NULL) {
ZF_LOGE("Semaphore passed to sync_bin_sem_new was NULL");
return -1;
}
if (value != 0 && value != 1) {
ZF_LOGE("Binary semaphore initial value neither 0 nor 1");
return -1;
}
int error = vka_alloc_notification(vka, &(sem->notification));
if (error != 0) {
return error;
} else {
return sync_bin_sem_init(sem, sem->notification.cptr, value);
}
}
/* Deallocate a managed binary semaphore (do not use with sync_bin_sem_init)
* @param vka A VKA instance used to deallocate the notification object.
* @param sem A semaphore object initialised by sync_bin_sem_new.
* @return 0 on success, an error code on failure. */
static inline int sync_bin_sem_destroy(vka_t *vka, sync_bin_sem_t *sem)
{
if (sem == NULL) {
ZF_LOGE("Semaphore passed to sync_bin_sem_destroy was NULL");
return -1;
}
vka_free_object(vka, &(sem->notification));
return 0;
}