--------------------------------------- 3 Threads and Region size 3 ----------------------------------------- Scenario of data race: Dynamic data races; depending on which memory cell each thread is accessing at run-time Case 1: (Lines 87 and 68 could cause a race where thread 0 is writing in 87 and thread 1 is reading t[base-1] in 68) Case 2: thread i is writing t[base] in line 76 and thread i-1 is reading t[base+MAXN]) in line 81 for thread i > 0 Mem. unit is in MB and Time is in Sec. Property Result Depth State vector Total time Total Act. memory -------- ------ ----- ------------ ---------- ----------------- []!(read_t[0] && write_t[0]) Success 877 84 0.734 17.735 []!(read_t[1] && write_t[1]) S 877 84 0.734 17.735 []!(read_t[2] && write_t[2]) Failure 877 84 0.046 2.598 []!(read_t[3] && write_t[3]) F 877 84 0.046 2.598 []!(read_t[4] && write_t[4]) S 877 84 0.765 17.735 []!(read_t[5] && write_t[5]) F 877 84 0.171 5.430 []!(read_t[6] && write_t[6]) F 877 84 0.046 2.891 []!(read_t[7] && write_t[7]) S 877 84 0.734 17.735 []!(read_t[8] && write_t[8]) S 877 84 0.796 17.735 --------------------------------------- 4 Threads and Region size 3 ----------------------------------------- Property Result Depth State vector Total time Total Act. memory -------- ------ ----- ------------ ---------- ----------------- []!(read_t[0] && write_t[0]) Success 1201 108 58.1 504.169 with compression []!(read_t[0] && write_t[0]) Success 1201 108 20.5 437.567 with Hash-Compact []!(read_t[1] && write_t[1]) Success 1201 108 20.5 437.567 with Hash-Compact []!(read_t[2] && write_t[2]) F 1201 108 0.078 259.345 with Hash-Compact []!(read_t[5] && write_t[5]) F 1201 108 0.171 260.419 with Hash-Compact --------------------------------------- 5 Threads and Region size 3 ----------------------------------------- Got out of memory! Now, we check the cases where we have three threads but the region size is increased --------------------------------------- 3 Threads and Region size 4 ----------------------------------------- Property Result Depth State vector Total time Total Act. memory -------- ------ ----- ------------ ---------- ----------------- []!(read_t[0] && write_t[0]) Success 1381 92 2.11 46.251 []!(read_t[1] && write_t[1]) S 1381 92 2.09 46.251 []!(read_t[2] && write_t[2]) S 1381 92 2.12 46.251 []!(read_t[3] && write_t[3]) F 1381 92 0.062 2.696 []!(read_t[4] && write_t[4]) F 1381 92 0.046 2.696 []!(read_t[5] && write_t[5]) S 1381 92 2.14 46.251 []!(read_t[6] && write_t[6]) S 1381 92 2.11 46.251 []!(read_t[7] && write_t[7]) F 1381 92 0.406 9.727 --------------------------------------- 3 Threads and Region size 5 ----------------------------------------- Property Result Depth State vector Total time Total Act. memory -------- ------ ----- ------------ ---------- ----------------- []!(read_t[0] && write_t[0]) Success 2005 96 4.88 101.329 []!(read_t[1] && write_t[1]) S 2005 96 4.86 101.329 []!(read_t[2] && write_t[2]) S 2005 96 4.86 101.329 []!(read_t[3] && write_t[3]) S 2005 96 4.83 101.329 []!(read_t[4] && write_t[4]) F 2005 96 0.078 2.891 []!(read_t[5] && write_t[5]) F 2005 96 0.093 2.794 []!(read_t[6] && write_t[6]) S 2005 96 4.86 101.329 []!(read_t[7] && write_t[7]) S 2005 96 4.84 101.329 []!(read_t[8] && write_t[8]) S 2005 96 4.84 101.329 []!(read_t[9] && write_t[9]) F 2005 96 0.734 16.661 []!(read_t[10] && write_t[10]) F 2005 96 0.406 9.922 []!(read_t[11] && write_t[11]) S 2005 96 4.84 101.329 960248 states stored --------------------------------------- 3 Threads and Region size 6 ---------------------------------------- 1838224 states stored --------------------------------------- 3 Threads and Region size 7 ---------------------------------------- 3209852 states, stored --------------------------------------- 3 Threads and Region size 8 ---------------------------------------- 5231708 states, stored --------------------------------------- 3 Threads and Region size 9 ---------------------------------------- 8081872 states, stored --------------------------------------- 3 Threads and Region size 10 ---------------------------------------- verified for []!(read_t[0] && write_t[0]) 11959928 states, stored --------------------------------------- 3 Threads and Region size 11 ---------------------------------------- 17086964 states, stored --------------------------------------- 3 Threads and Region size 14 ---------------------------------------- out of memory! Property Result Depth State vector Total time Total Act. memory -------- ------ ----- ------------ ---------- ----------------- []!(read_t[0] && write_t[0]) []!(read_t[10] && write_t[10]) F 6925 128 0.265 259.540 with hash-compact