/* TAGS: big */
/* VERIFY_OPTS: -o nofail:malloc -o nofail:spurious-wakeup */
/* CC_OPTS: -Dgmtime_r=gmtime -Dlocaltime_r=localtime -DBOOST_HAS_PTHREADS -DBOOST_THREAD_POSIX -DPOSIX_THREADS -D__linux -D_SC_PAGESIZE -I $BOOST/libs/thread/include/ -I test/termination -I $BOOST/libs/config/include/ -I $BOOST/libs/throw_exception/include -I $BOOST/libs/assert/include/ -I $BOOST/libs/core/include/ -I $BOOST/libs/system/include/ -I $BOOST/libs/type_traits/include/ -I $BOOST/libs/static_assert/include/ -I $BOOST/libs/move/include/ -I $BOOST/libs/date_time/include/ -I $BOOST/libs/smart_ptr/include/ -I $BOOST/libs/predef/include -I $BOOST/libs/utility/include/ -I $BOOST/libs/mpl/include/ -I$BOOST/libs/preprocessor/include/ -I $BOOST/libs/numeric/conversion/include/ -I $BOOST/libs/chrono/include/ -I $BOOST/libs/ratio/include/ -I $BOOST/libs/integer/include/ -I $BOOST/libs/bind/include/ -I $BOOST/libs/io/include/ -I $BOOST/libs/container_hash/include/ -I $BOOST/libs/detail/include/ -I $BOOST/libs/atomic/include/ -I $BOOST/libs/tuple/include/ -I $BOOST/libs/exception/include/ -I $BOOST/libs/iterator/include/ -I $BOOST/libs/optional/include/ -I $BOOST/libs/function/include/ -I $BOOST/libs/type_index/include/ -I $BOOST/libs/algorithm/include -I $BOOST/libs/range/include -I $BOOST/libs/concept_check/include/ -I $BOOST/libs/lexical_cast/include/ -I $BOOST/libs/array/include/ -I $BOOST/libs/container/include/ -I $BOOST/libs/math/include */
/* EXTRA_SRCS: $BOOST/libs/thread/src/pthread/thread.cpp $BOOST/libs/thread/src/pthread/once_atomic.cpp */

#include <boost/thread/sync_bounded_queue.hpp>
#include <rst/termsec.h>
#include <thread>
#include <list>
#include <dios.h>

// V: fin.2.4@safety
// V: fin.5.10@safety                                   CC_OPT: -DNVALS=10
// V: inf.2.4@safety                                    CC_OPT: -DINF
// V: inf.5.10@safety                                   CC_OPT: -DNVALS=10 -DINF

// V: fin.2.4@local     V_OPT: --nontermination local
// V: fin.5.10@local    V_OPT: --nontermination local   CC_OPT: -DNVALS=10 -DCAPA=5
// V: inf.2.4@local     V_OPT: --nontermination local   CC_OPT: -DINF
// V: inf.5.10@local    V_OPT: --nontermination local   CC_OPT: -DNVALS=10 -DINF -DCAPA=5

// V: fin.2.4@global    V_OPT: --nontermination global
// V: fin.5.10@global   V_OPT: --nontermination global  CC_OPT: -DNVALS=10 -DCAPA=5
// V: inf.2.4@global    V_OPT: --nontermination global  CC_OPT: -DINF                     ERR: .*
// V: inf.5.10@global   V_OPT: --nontermination global  CC_OPT: -DNVALS=10 -DINF-DCAPA=5  ERR: .*

#ifdef NVALS
constexpr int nvals = NVALS;
#else
constexpr int nvals = 4;
#endif

#ifdef CAPA
constexpr int capa = CAPA;
#else
constexpr int capa = 2;
#endif

int main() {
    boost::sync_bounded_queue< int > queue( capa );

    std::thread writer( [&] {
#ifdef INF
        while ( true )
#endif
            for ( int i = 0; i < nvals; ++i ) {
                termsec::CheckFunction c;
                queue.push_back( i );
            }
    } );

    int last = -1;
#ifdef INF
    while ( true ) {
#else
    for ( int i = 0; i < nvals; ++i ) {
#endif
        int v;
        {
            termsec::CheckFunction c;
            v = queue.pull_front();
        }
        __dios_trace_f( "last = %d, v = %d", last, v );
#ifdef INF
        if ( last == nvals - 1 )
            assert( v == 0 );
        else
#endif
            assert( last + 1 == v );
        last = v;
    }
    __dios_trace_f( "last = %d", last );
    assert( last + 1 == nvals );

    writer.join();
}