/* TAGS: min */
/* VERIFY_OPTS: -o nofail:malloc */

// V: safety
// V: local   V_OPT: --nontermination local
// V: global  V_OPT: --nontermination global

#include <pthread.h>
#include <thread>
#include <dios.h>
#include <atomic>

int main() {
    pthread_barrier_t bar;
    int r = pthread_barrier_init( &bar, nullptr, 3 );
    assert( r == 0 );
    std::atomic< int > cnt{ 0 };

    std::thread ta( [&] {
        ++cnt;
        int r = pthread_barrier_wait( &bar );
        assert( r == 0 || r == PTHREAD_BARRIER_SERIAL_THREAD );
        assert( cnt == 3 );
    } );
    std::thread tb( [&] {
        ++cnt;
        int r = pthread_barrier_wait( &bar );
        assert( r == 0 || r == PTHREAD_BARRIER_SERIAL_THREAD );
        assert( cnt == 3 );
    } );

    ++cnt;
    r = pthread_barrier_wait( &bar );
    assert( r == 0 || r == PTHREAD_BARRIER_SERIAL_THREAD );
    assert( cnt == 3 );

    ta.join();
    tb.join();
}