// divine-cflags: -std=c++11 // -*- C++ -*- (c) 2015 Vladimír Štill #define __STORE_BUFFER_SIZE 2 #include #include #include enum APs { w0in, w0out, w1in, w1out }; LTL( exclusion, G( w0in -> ((!w1in) W w0out ) ) && G( w1in -> ((!w0in) W w1out )) ); bool flag[2] = { false, false }; int turn; constexpr int other( int x ) { return x == 0 ? 1 : 0; } const APs in[] = { w0in, w1in }; const APs out[] = { w0out, w1out }; std::atomic< int > critical; template< int tid > void *worker( void * ) { lart::weakmem::store< lart::weakmem::TSO >( &flag[ tid ], true ); lart::weakmem::store< lart::weakmem::TSO >( &turn, other( tid ) ); while ( lart::weakmem::load< lart::weakmem::TSO >( &flag[ other( tid ) ] ) && lart::weakmem::load< lart::weakmem::TSO >( &turn ) == other( tid ) ) { } // critical start AP( in[ tid ] ); ++critical; --critical; AP( out[ tid ] ); // end lart::weakmem::store< lart::weakmem::TSO >( &flag[ tid ], false ); return nullptr; } int main() { pthread_t t1, t2; pthread_create( &t1, nullptr, &worker< 0 >, nullptr ); pthread_create( &t2, nullptr, &worker< 1 >, nullptr ); while ( true ) assert( critical <= 1 ); pthread_join( t1, nullptr ); pthread_join( t2, nullptr ); return 0; }