/* TAGS: cpp big hashset */
/* VERIFY_OPTS: -o nofail:malloc */
/* CC_OPTS: -I$SRC_ROOT/test/weakmem/lockfree/ -I$SRC_ROOT/bricks/ */

#include "brick-hashset"
#include <pthread.h>
#include <cassert>

// V: sc.t2c2o0@safety                                                             CC_OPT: -DTHRS=2 -DCNT=2 -DOVERLAP=0
// v: tso4.t2c2o0@safety   V_OPT: --relaxed-memory tso:4                           CC_OPT: -DTHRS=2 -DCNT=2 -DOVERLAP=0
// v: tso16.t2c2o0@safety  V_OPT: --relaxed-memory tso:16                          CC_OPT: -DTHRS=2 -DCNT=2 -DOVERLAP=0
// V: sc.t2c4o2@safety                                                             CC_OPT: -DTHRS=2 -DCNT=4 -DOVERLAP=4
// v: tso4.t2c4o2@safety   V_OPT: --relaxed-memory tso:4                           CC_OPT: -DTHRS=2 -DCNT=4 -DOVERLAP=4
// v: tso16.t2c4o2@safety  V_OPT: --relaxed-memory tso:16                          CC_OPT: -DTHRS=2 -DCNT=4 -DOVERLAP=4
// V: sc.t3c1o2@safety                                                             CC_OPT: -DTHRS=3 -DCNT=1 -DOVERLAP=2
// v: tso4.t3c1o2@safety   V_OPT: --relaxed-memory tso:4                           CC_OPT: -DTHRS=3 -DCNT=1 -DOVERLAP=2
// v: tso16.t3c1o2@safety  V_OPT: --relaxed-memory tso:16                          CC_OPT: -DTHRS=3 -DCNT=1 -DOVERLAP=2

// V: sc.t2c2o0@local      V_OPT: --nontermination local                           CC_OPT: -DTHRS=2 -DCNT=2 -DOVERLAP=0
// v: tso4.t2c2o0@local    V_OPT: --nontermination local --relaxed-memory tso:4    CC_OPT: -DTHRS=2 -DCNT=2 -DOVERLAP=0
// v: tso16.t2c2o0@local   V_OPT: --nontermination local --relaxed-memory tso:16   CC_OPT: -DTHRS=2 -DCNT=2 -DOVERLAP=0
// V: sc.t2c4o2@local      V_OPT: --nontermination local                           CC_OPT: -DTHRS=2 -DCNT=4 -DOVERLAP=4
// v: tso4.t2c4o2@local    V_OPT: --nontermination local --relaxed-memory tso:4    CC_OPT: -DTHRS=2 -DCNT=4 -DOVERLAP=4
// v: tso16.t2c4o2@local   V_OPT: --nontermination local --relaxed-memory tso:16   CC_OPT: -DTHRS=2 -DCNT=4 -DOVERLAP=4
// V: sc.t3c1o2@local      V_OPT: --nontermination local                           CC_OPT: -DTHRS=3 -DCNT=1 -DOVERLAP=2
// v: tso4.t3c1o2@local    V_OPT: --nontermination local --relaxed-memory tso:4    CC_OPT: -DTHRS=3 -DCNT=1 -DOVERLAP=2
// v: tso16.t3c1o2@local   V_OPT: --nontermination local --relaxed-memory tso:16   CC_OPT: -DTHRS=3 -DCNT=1 -DOVERLAP=2

// V: sc.t2c2o0@global     V_OPT: --nontermination global                          CC_OPT: -DTHRS=2 -DCNT=2 -DOVERLAP=0
// v: tso4.t2c2o0@global   V_OPT: --nontermination global --relaxed-memory tso:4   CC_OPT: -DTHRS=2 -DCNT=2 -DOVERLAP=0
// v: tso16.t2c2o0@global  V_OPT: --nontermination global --relaxed-memory tso:16  CC_OPT: -DTHRS=2 -DCNT=2 -DOVERLAP=0
// V: sc.t2c4o2@global     V_OPT: --nontermination global                          CC_OPT: -DTHRS=2 -DCNT=4 -DOVERLAP=4
// v: tso4.t2c4o2@global   V_OPT: --nontermination global --relaxed-memory tso:4   CC_OPT: -DTHRS=2 -DCNT=4 -DOVERLAP=4
// v: tso16.t2c4o2@global  V_OPT: --nontermination global --relaxed-memory tso:16  CC_OPT: -DTHRS=2 -DCNT=4 -DOVERLAP=4
// V: sc.t3c1o2@global     V_OPT: --nontermination global                          CC_OPT: -DTHRS=3 -DCNT=1 -DOVERLAP=2
// v: tso4.t3c1o2@global   V_OPT: --nontermination global --relaxed-memory tso:4   CC_OPT: -DTHRS=3 -DCNT=1 -DOVERLAP=2
// v: tso16.t3c1o2@global  V_OPT: --nontermination global --relaxed-memory tso:16  CC_OPT: -DTHRS=3 -DCNT=1 -DOVERLAP=2

using namespace brick::hashset;
using brick::t_hashset::test_hasher;

using HashSet = CompactConcurrent< int, test_hasher< int > >;

void worker( int wid, HashSet hs ) {
    const int end = CNT + OVERLAP;
    for ( int i = 0; i < end; ++i ) {
        hs.insert( 1 + wid * CNT + i );
    }
}

__attribute__(( __annotate__( "divine.debugfn" ) ))
void dump( std::set< int > &seen ) noexcept {
    printf( "{ " );
    for ( int x : seen ) {
        printf( "%d ", x );
    }
    printf( "}" );
}

int main() {
    HashSet hs;
    pthread_t thrs[THRS - 1];
    for ( int i = 0; i < THRS - 1; ++i ) {
        std::pair< int, HashSet * > p( i + 1, &hs );
        pthread_create( &thrs[i], nullptr, []( void *hs ) -> void * {
                auto p = *reinterpret_cast< std::pair< int, HashSet * > * >( hs );
                worker( p.first, *p.second );
                return nullptr;
            }, &p );
    }
    worker( 0, hs );
    for ( int i = 0; i < THRS - 1; ++i ) {
        pthread_join( thrs[i], nullptr );
    }

    std::set< int > seen;
    for ( auto &c : hs.current() ) {
        if ( c.empty() )
            continue;
        auto r = seen.insert( c.copy() );
        assert( r.second );
    }
    dump( seen );
    auto total = CNT * THRS + OVERLAP;
    assert( seen.size() == total );
    for ( int i = 1; i <= total; ++i ) {
        assert( seen.find( i ) != seen.end() );
    }
}