/* MODEX Version 1.0 - 20 January 2003; extended for Unified Parallel C (UPC) in February 2011 */ /* extracted from sigupc_racefree.c */ #define SIZE 15 #define THREADS 3 int barr = THREADS; int proc = 0; bit read_hist[15]; bit write_hist[15]; #define race (read_hist[0] && write_hist[0]) active [THREADS] proctype main() { int cnt = 3; int i; /* mapped */ int s; /* mapped */ int trial; /* mapped */ /* 95: D: int trial; */ /* 98: D: int i,s; */ c_code { Pmain->trial=1; }; /* line 111 */ L_1: do /* do-while */ :: /* for-loop: */ c_code { Pmain->i=0; }; /* line 121 */ L_2: do :: c_expr { (Pmain->i<2) }; /* line 121 */ if :: c_expr { (Pmain->_pid==(Pmain->i%THREADS)) }; /* line 121 */ if :: {true -> s = 0;} :: {true -> s = 1;} :: {true -> s = 2;} :: {true -> s = 3;} :: {true -> s = 4;} :: {true -> s = 5;} :: {true -> s = 6;} :: {true -> s = 7;} :: {true -> s = 8;} :: {true -> s = 9;} :: {true -> s = 10;} :: {true -> s = 11;} :: {true -> s = 12;} :: {true -> s = 13;} :: {true -> s = 14;} fi ; /* line 124 */ read_hist[s] = 1; read_hist[s] = 0; write_hist[s] = 1; write_hist[s] = 0; /* line 124 */ :: else; /* line 124 */ fi; c_code { ++Pmain->i; }; /* line 124 */ :: else; /* line 124 */ -> break od; atomic{ barr = barr -1; proc=0;} (barr == 0) || (proc == 1) -> proc = 1; barr = barr + 1 ; (barr == THREADS) || (proc == 0) -> proc = 0; ; /* line 135 */ c_code { ++Pmain->trial; }; /* line 135 */ /* This 'if statement' is manually abstracted away as it does not have an impact on concurrency failures if :: c_expr { (error>0.001) }; line 135 :: else; line 135 break fi */ if :: (cnt >= 0) -> cnt = cnt -1; skip; :: else; break; fi od; /* function-calls: foo() 124 */ }