SV-COMP requires functional atomic sections for some benchmarks:
functions with prefix __VERIFIER_atomic_ are considered as atomic
atomic section can be entered via calling __VERIFIER_atomic_start() and be leaved via __VERIFIER_atomic_end()
Implementation:
Control structure contains stack of threads idx in atomic sections. Note: There will be only one thread in the stack - anything else means error. However the stack or counter is necessary because of nested calls to the atomic functions.
When the stack is not empty, only one thread is advanced from the current state.
SV-COMP requires functional atomic sections for some benchmarks:
__VERIFIER_atomic_are considered as atomic__VERIFIER_atomic_start()and be leaved via__VERIFIER_atomic_end()Implementation:
Controlstructure contains stack of threads idx in atomic sections. Note: There will be only one thread in the stack - anything else means error. However the stack or counter is necessary because of nested calls to the atomic functions.