moves-rwth / storm

A Modern Probabilistic Model Checker
https://www.stormchecker.org
GNU General Public License v3.0
138 stars 75 forks source link

Memory errors in Bit Vector Hashmap #607

Closed landonjefftaylor closed 2 months ago

landonjefftaylor commented 2 months ago

While storing states in storm::storage::BitVectorHashMap<uint32_t>, we are seeing the error munmap_chunk(): invalid pointer. When running identical code several months ago, we didn't see this error, but we are now able to produce it on at least two machines.

OS Info

The machines that produce this error are running Debian Bookworm and Ubuntu 24. The error was not present on either machine several months ago, but now it is, so we are curious if this might actually be caused by an update to one of Storm's dependencies.

Steps to Reproduce

I've put together a minimal working example along with steps to reproduce the error at https://github.com/landonjefftaylor/storm-mwe

Error Information

We tested this on several different sizes of state spaces, with the following results:

In the minimal working example, we have instructions to run the example on different numbers of states.

volkm commented 2 months ago

Thanks for the detailed bug report and for creating the minimal working example. This help is really appreciated.

I could reproduce the issue using several Docker images of different Storm versions. For me, all Storm versions I tested (1.6.0, 1.6.4, 1.7.0, 1.8.1, 1.9.0) had this issue.

Do you know for which Storm it worked at some point?

Dockerfile:

# Test Dockerfile
# A different tag can be set from the commandline with:
# --build-arg TAG=<new_base_image>

# Set base image
ARG TAG=stable
FROM movesrwth/storm:$TAG

WORKDIR /opt/
RUN git clone https://github.com/landonjefftaylor/storm-mwe
RUN mkdir build
WORKDIR /opt/storm-mwe/build
RUN cmake .. && make

Command:

docker build -t test --build-arg TAG=1.8.1 . && docker run --rm -w /opt/storm-mwe/ test "./build/errormwe" && docker rmi test
volkm commented 2 months ago

In Debug mode, I get a mismatch for the bucket size:

ERROR (BitVectorHashMap.cpp:163): Size of bit vector and size of buckets do not match
errormwe: /opt/storm/src/storm/storage/BitVectorHashMap.cpp:163: std::pair<bool, long unsigned int> storm::storage::BitVectorHashMap<ValueType, Hash>::findBucket(const storm::storage::BitVector&) const [with ValueType = unsigned int; Hash = storm::storage::Murmur3BitVectorHash<unsigned int>]: Assertion `key.size() == bucketSize' failed.
landonjefftaylor commented 2 months ago

I tested it on the most recent 3 releases, so 1.8.0, 1.8.1, and 1.9.0 and got the error on all three. We originally tested (without the error) on 1.8.1 a few months ago.

sjunges commented 2 months ago

Hey,

If I understand the situation correctly (in particular Matthias message) this thus either is a bug in the MWE and/or it is due to changed behavior in the compilers?

Which compilers are you using?

Sebastian

landonjefftaylor commented 2 months ago

Apologies for the delay; it looks like the issue was indeed in our code. We forgot to give an explicit bucket size in line 53 (https://github.com/landonjefftaylor/storm-mwe/blob/b6d5d6b82b2e9f4c2d98518d0da1b8f038ed4ec1/src/main.cpp#L53). We have no idea why we didn't see this issue in previous tests, but we've got it working now.

In case someone sees this issue in the future, it was resolved with the following line:

storm::storage::BitVectorHashMap<uint32_t> stateStorage(generator->getStateSize());

Thank you so much for your help.

volkm commented 2 months ago

Would it maybe be a good idea to remove the default bucket size in the BitVectorHashMap constructor to avoid such issues in the future?

landonjefftaylor commented 2 months ago

That would have been helpful to us; that way we'd get a more visible error if we forgot that step.

sjunges commented 2 months ago

I would also agree with removing that, but it may break some code?