[ 0:01] + tee fairness.cpp [ 0:01] #include [ 0:01] #include [ 0:01] #include [ 0:01] #include [ 0:01] #include [ 0:01] [ 0:01] bool checkX(); [ 0:01] [ 0:01] void __buchi_accept(); [ 0:01] void __buchi_cancel(); [ 0:01] unsigned __buchi_choose(unsigned); [ 0:01] [ 0:01] struct BuchiAutomaton : public __dios::Monitor [ 0:01] { [ 0:01] BuchiAutomaton() : state(0) {} [ 0:01] void step() [ 0:01] { [ 0:01] switch(state) [ 0:01] { [ 0:01] case 0: { [ 0:01] unsigned nd0 = __buchi_choose(2); [ 0:01] if ((nd0 == 0) && true) [ 0:01] { [ 0:01] state = 0; [ 0:01] } [ 0:01] else if ((nd0 == 1) && !checkX()) [ 0:01] { [ 0:01] state = 1; [ 0:01] } [ 0:01] break; [ 0:01] } [ 0:01] case 1: { [ 0:01] if (!checkX()) [ 0:01] { [ 0:01] __buchi_accept(); [ 0:01] state = 1; [ 0:01] } [ 0:01] else [ 0:01] { [ 0:01] __buchi_cancel(); [ 0:01] } [ 0:01] break; [ 0:01] } [ 0:01] } [ 0:01] } [ 0:01] [ 0:01] unsigned state; [ 0:01] }; [ 0:01] [ 0:01] void __buchi_accept() { [ 0:01] __vm_control( _VM_CA_Bit, _VM_CR_Flags, _VM_CF_Accepting, _VM_CF_Accepting ); [ 0:01] } [ 0:01] [ 0:01] void __buchi_cancel() { [ 0:01] __vm_control( _VM_CA_Bit, _VM_CR_Flags, _VM_CF_Cancel, _VM_CF_Cancel ); [ 0:01] } [ 0:01] [ 0:01] unsigned __buchi_choose( unsigned n ) { [ 0:01] return __vm_choose( n ); [ 0:01] } [ 0:01] [ 0:01] std::atomic_int x; [ 0:01] [ 0:01] bool checkX() { return x == 1; } [ 0:01] [ 0:01] int main() { [ 0:01] __dios::register_monitor( new BuchiAutomaton() ); [ 0:01] [ 0:01] __dios_trace_t( "Monitor registered" ); [ 0:01] [ 0:01] auto t = std::thread( [&]{ [ 0:01] while ( true ) { [ 0:01] __dios_trace_t( "Set 1" ); [ 0:01] x = 1; [ 0:01] __vmutil_interrupt(); [ 0:01] } [ 0:01] } ); [ 0:01] [ 0:01] __dios_trace_t( "Thread started" ); [ 0:01] [ 0:01] while ( true ) { [ 0:01] __dios_trace_t( "Set 0" ); [ 0:01] x = 0; [ 0:01] __vmutil_interrupt(); [ 0:01] } [ 0:01] } [ 0:01] + divine verify --liveness -std=c++1z -onofail:malloc fairness.cpp [ 0:01] compiling fairness.cpp [ 0:01] a report was written to fairness.report [ 0:12] + grep 'error found: yes' trace1.out [ 0:13] error found: yes [ 0:13] + divine verify --liveness -std=c++1z -onofail:malloc -oconfig:fair fairness.cpp [ 0:13] compiling fairness.cpp [ 0:13] a report was written to fairness.report [ 0:25] + grep 'error found: no' trace2.out [ 0:26] error found: no [ 0:26] + exit [ 0:26] + check debris