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/* An unmanaged binary semaphore; i.e. the caller stores the state related to
16 * the semaphore itself. This can be useful in scenarios such as CAmkES, where
17 * immediate concurrency means we have a race on initialising a managed
18 * semaphore.
19 */
20
21#include <assert.h>
22#include <sel4/sel4.h>
23#include <stddef.h>
24#include <platsupport/sync/atomic.h>
25
26static inline int sync_bin_sem_bare_wait(seL4_CPtr notification, volatile int *value) {
27    int oldval;
28    int result = sync_atomic_decrement_safe(value, &oldval, __ATOMIC_ACQUIRE);
29    if (result != 0) {
30        /* Failed decrement; too many outstanding lock holders. */
31        return -1;
32    }
33    if (oldval <= 0) {
34        seL4_Wait(notification, NULL);
35        /* Even though we performed an acquire barrier during the atomic
36         * decrement we did not actually have the lock yet, so we have
37         * to do another one now */
38        __atomic_thread_fence(__ATOMIC_ACQUIRE);
39    }
40    return 0;
41}
42
43static inline int sync_bin_sem_bare_post(seL4_CPtr notification, volatile int *value) {
44    /* We can do an "unsafe" increment here because we know we are the only
45     * lock holder.
46     */
47    int val = sync_atomic_increment(value, __ATOMIC_RELEASE);
48    assert(*value <= 1);
49    if (val <= 0) {
50        seL4_Signal(notification);
51    }
52    return 0;
53}
54
55