search

runtimeverification / rv-predict

Code for improved rv-predict and installer
BSD 3-Clause "New" or "Revised" License
2 stars 3 forks source link

Memcached bug - start / shutdown #649

Open edgar-pek opened 8 years ago

edgar-pek commented 8 years ago

@traiansf, @ericpts this one is deterministic -- can you please take a look when you get a chance? thank you.

memcached-bug.zip

[RV-Predict] Error: Maximum number of variables allowed (131072) exceeded.
Exception in thread "main" java.lang.AssertionError
    at com.runtimeverification.rvpredict.metadata.Metadata.setLocationSig(Metadata.java:97)
    at com.runtimeverification.rvpredict.trace.LLVMTraceCache$3.log(LLVMTraceCache.java:64)
    at com.runtimeverification.rvpredict.trace.LLVMTraceCache.parseInfo(LLVMTraceCache.java:42)
    at com.runtimeverification.rvpredict.trace.LLVMTraceCache.parseLocInfo(LLVMTraceCache.java:61)
    at com.runtimeverification.rvpredict.trace.LLVMTraceCache.readMetadata(LLVMTraceCache.java:98)
    at com.runtimeverification.rvpredict.trace.LLVMTraceCache.setup(LLVMTraceCache.java:111)
    at com.runtimeverification.rvpredict.engine.main.RVPredict.start(RVPredict.java:74)
    at com.runtimeverification.rvpredict.engine.main.Main.main(Main.java:47)
traiansf commented 8 years ago

Apparently the same location id is generated twice. This should not happen in general. Is it possible that the test you're running uses fork? I've taken a look to the sources for memcached-1.4.15 and a couple of files use fork:

daemon.c:    switch (fork()) {
testapp.c:    pid_t pid = fork();
testapp.c:    child = fork();
timedrun.c:    pid_t pid = fork();
timedrun.c:        perror("fork");
edgar-pek commented 8 years ago

I see, yes it could be that. Is there a simple way to generate a warning message if the program calls fork? That way we can rule out tests we know are out of scope.

traiansf commented 8 years ago

Yes, I think I can do that easily... Let me try

edgar-pek commented 8 years ago

re-test after PR #660 gets in master