I have a test case where future_index == -1 in get_future_value(). It
passes the ASSERT() and instead triggers a fault when accessing the
vector.
With the benchmarks at this commit:
commit
40b27f40998eed81640b016094bacf79df96d377
mpmc-queue: run more producer/consumer threads
I can trigger a model-checker bug by running:
# ./run.sh mpmc-queue/mpmc-queue -f 4 -m 1
...
Error: assertion failed in nodestack.cc at line 319
stack trace:
../libmodel.so : Node::get_future_value()+0x56
../libmodel.so : ModelChecker::process_read(ModelAction*, bool)+0x141
../libmodel.so :
ModelChecker::check_current_action(ModelAction*)+0x2ff
../libmodel.so : ModelChecker::take_step()+0x6c
../libmodel.so : ModelChecker::finish_execution()+0x10
../libmodel.so : ()+0x16a8a
../libmodel.so : main()+0x37
/lib/x86_64-linux-gnu/libc.so.6 : __libc_start_main()+0xed
mpmc-queue/mpmc-queue() [0x400f59]
...
* @return The first element in future_values
*/
uint64_t Node::get_future_value() {
- ASSERT(future_index<((int)future_values.size()));
+ ASSERT(future_index >= 0 && future_index<((int)future_values.size()));
return future_values[future_index].value;
}
modelclock_t Node::get_future_value_expiration() {
- ASSERT(future_index<((int)future_values.size()));
+ ASSERT(future_index >= 0 && future_index<((int)future_values.size()));
return future_values[future_index].expiration;
}