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

// V: safety
// V: local=!crit,!join    V_OPT: --nontermination local,~critical,~thread-join       ERR: error trace: condition variable
// V: local=!crit,!cwait   V_OPT: --nontermination local,~critical,~condition-wait    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: .*
// note: libc++ rwlock is base on plain mutexes + condition variables

#include <mutex>
#include <shared_mutex>
#include <thread>
#include <dios.h>

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

    {
        std::unique_lock g( mtx );
        x = 42;
    }
    reader_a.join();
    reader_b.join();
}