LART: Relaxed memory verification is not relaxed enough
In the following code there should be assertion failure (even under TSO), but our relaxed memory instrumentation does not enable it since it respects program order of each of the threads.
// divine-cflags: -std=c++11
#include <pthread.h>
#include <atomic>
#include <cassert>
std::atomic< int > x( 0 );
std::atomic< int > y( 0 );
int main() {
pthread_t t1, t2;
pthread_create( &t1, nullptr, []( void * ) -> void * {
while ( !x.load( std::memory_order_acquire ) ) { } // the load and store could be reordered
y.store( 1, std::memory_order_release );
return nullptr;
}, nullptr );
pthread_create( &t2, nullptr, []( void * ) -> void * {
while ( !y.load( std::memory_order_acquire ) ) { }
assert( x.load( std::memory_order_acquire ) == 1 ); // this assert should fail
return nullptr;
}, nullptr );
x.store( 1, std::memory_order_release );
pthread_join( t1, nullptr );
pthread_join( t2, nullptr );
}