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

// V: safety
// V: local=!join   V_OPT: --nontermination local,~thread-join ERR: error trace: critical section
// V: local=!crit   V_OPT: --nontermination local,~critical    ERR: error trace: thread join
// V: local=all     V_OPT: --nontermination local              ERR: error trace: termsec check begin
// V: global        V_OPT: --nontermination global             ERR: error trace: .*

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

int main() {
    pthread_rwlock_t mtx = PTHREAD_RWLOCK_INITIALIZER;
    int x = 0;
    std::thread reader_a( [&] {
        while ( true ) {
            pthread_rwlock_rdlock( &mtx );
            __dios_trace_f( "read a: x = %d", x );
            pthread_rwlock_unlock( &mtx );
        }
    } );
    std::thread reader_b( [&] {
        pthread_rwlock_rdlock( &mtx );
        while ( true ) {
            __dios_trace_f( "read b: x = %d", x );
        }
        pthread_rwlock_unlock( &mtx );
    } );

    {
        pthread_rwlock_wrlock( &mtx );
        x = 42;
        pthread_rwlock_unlock( &mtx );
    }
    reader_a.join();
    reader_b.join();
}