From: Brian Norris <banorris@uci.edu>
Date: Thu, 1 Nov 2012 19:08:53 +0000 (-0700)
Subject: nodestack: improve bounds-checking assertion
X-Git-Tag: pldi2013~31
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=fe7b400edb33255770fb47ad520afbd05d13a231;hp=fe7b400edb33255770fb47ad520afbd05d13a231;p=model-checker.git

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