/* TAGS: min c tso divine-internal */ /* VERIFY_OPTS: --relaxed-memory tso:2 */ /* this is a regression test demonstrating error in an early version of lazy * x86-TSO in DIVINE */ #include #include #include #include #define REACH( X ) assert( !(X) ) volatile int x, y, z; volatile int bypass_sig; void *t1( void *_ ) { x = 1; y = 1; __vm_ctl_flag( 0, _LART_CF_RelaxedMemRuntime ); bypass_sig = 1; while ( bypass_sig != 2 ) { } __vm_ctl_flag( _LART_CF_RelaxedMemRuntime, 0 ); __sync_synchronize(); return NULL; } int main() { pthread_t t1t; pthread_create( &t1t, NULL, &t1, NULL ); /* wait for the other thread to put everything to SB */ __vm_ctl_flag( 0, _LART_CF_RelaxedMemRuntime ); while ( bypass_sig != 1 ) { } __vm_ctl_flag( _LART_CF_RelaxedMemRuntime, 0 ); x = 2; y = 2; y = 3; /* forces flush of x = 2 while x = 1 is still in SB of t1 */ /* let the other thread flush its SB */ __vm_ctl_flag( 0, _LART_CF_RelaxedMemRuntime ); bypass_sig = 2; __vm_ctl_flag( _LART_CF_RelaxedMemRuntime, 0 ); pthread_join( t1t, NULL ); REACH( y == 3 && x == 2 ); /* ERROR */ }