sv-benchmarks
sv-benchmarks copied to clipboard
Reachable error in pthread-ext/41_FreeBSD_abd_kbd_sliced
The program pthread-ext/41_FreeBSD_abd_kbd_sliced
is labeled as true
. However there should be a feasible counterexample trace (which Ultimate Automizer also found).
One thread can simply call akbd_read_char(1)
and therefore execute the trace:
__VERIFIER_atomic_acquire();
COND = 0;
__VERIFIER_atomic_release();
assume_abort_if_not(COND);
__VERIFIER_atomic_acquire();
if(!(COND)) { goto ERROR; }
For this error trace to be feasible we need to set COND
to 1 before the assume_abort_if_not and back to 0 after it. This can be achieved, if other threads call adb_kbd_receive_packet()
and akbd_read_char(1)
respectivitely (since the mutex is not locked there).
Therefore it seems that this example should be labeled as false (unreach-call)
.