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