nodestack: improve bounds-checking assertion
authorBrian Norris <banorris@uci.edu>
Thu, 1 Nov 2012 19:08:53 +0000 (12:08 -0700)
committerBrian Norris <banorris@uci.edu>
Thu, 1 Nov 2012 19:24:36 +0000 (12:24 -0700)
commitfe7b400edb33255770fb47ad520afbd05d13a231
tree13e6097a0ca843333f0e459d07e65fe77fbaa228
parent547377c72c02a7831b63f5c7aa2ac2559109907c
nodestack: improve bounds-checking assertion

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]
  ...
nodestack.cc