Is there someting wrong with sync_cv_broadcast_release in condition_var.h

[lydmcu]

hi
In sync_cv_broadcast_release it will call sync_bin_sem_post before seL4_Signal.
But In sync_cv_wait, sync_bin_sem_wait(lock) is called after seL4_Wait,
when call sync_bin_sem_post in sync_cv_broadcast_release, it will make "lock->value == 2", it will make sync_bin_sem_bare_post trigger assert " assert(*value <= 1)"

static inline int sync_bin_sem_bare_post(seL4_CPtr notification, volatile int *value) { /* We can do an "unsafe" increment here because we know we are the only * lock holder. */ int val = sync_atomic_increment(value, __ATOMIC_RELEASE); assert(*value <= 1); // if (val <= 0) { seL4_Signal(notification); } return 0; }
I do not this function can work for performance reasons