yanntm
commented
6 years ago I found some unitialized fields see PR, but the problem is still unsolved.
Closed yanntm closed 6 years ago
yanntm
commented
6 years ago I found some unitialized fields see PR, but the problem is still unsolved.
yanntm
commented
6 years ago More diagnosis traces, playing around with --strategy=, 5 runs per strat,
Out of 5 runs, how many times was a witness found ?
With --procs=1 / --procs=4
bfs : 0 / 0
sbfs : 0 / 0
dfs : 0 / 0
cndfs : 0 / 4
lndfs : 5 / 5
endfs : 0 / crash file hre_malloc.c, line 147: assertion "RTgetMallocRegion() == NULL" failed
renault : 5 / 5
ufscc : 5 / 5
ndfs : 5 / 5 renault, ufscc, ndfs, and lndfs are well behaved in these runs.
many strategies miss the counter-example (same root cause ?) There's an issue with endfs overallocating on my machine too.
cndfs behaves better with --procs=4 ; It still missed the trace in one out of 5 runs. This led to my original report of non-deterministic behavior (it's the default I believe)
bfs, sbfs, dfs, and endfs behave really bad (always miss the cex).
Maybe knowing the history of which of these strats share some root features you can debug more easily.
yanntm
commented
6 years ago Ok,
oops, mea culpa !
so the issue was due to malformed read dependency matrices apparently. Some algorithms must use this information more heavily, despite not activating POR.
I had trouble tracking the problem, since the tests for some (non deterministic) reason still passed after the change that broke my read matrices. So it wasn't obvious which commit should be incriminated. But after trying several versions of LTSmin it became obvious that the problem was on the input side (my files are broken).
In the end,
--check --por
was able to diagnose correctly and help me debug, I should run it in my test suite I guess/try that first when I have problems.
So, sorry for posting the issue here when the problem's on my side,
I'm closing this issue, apologies again.
alaarman
commented
6 years ago The bug reports close themselves :) The tree compression uses the dependency matrix. Was --check (alone) also able to find this incorrect dependency? It should be pretty thorough on checking only read/write matrices.
alaarman
commented
6 years ago What about report #109 ?
yanntm
commented
6 years ago yes,
--check was finding it even without --por
my post on #109 is about the same model, that regression was indeed patched by this fix of my generator code.
Hi,
this is related to the post in issue 109
Trying to trace the fact that an accepting cycle is not found, I get non determinisitic results with more than one thread ; The source files are on my other post.
The more threads, the more often it seems to find an accepted trace in my experiments. Running with -procs=1 is the worst, I have'nt had a run where the trace was found
I still get some variation in the trace with procs=1,
[Blue]reports diffferent values for both "levels" and "transition" metrics in each run, but idk if that's normal or not.With more procs, an accepting trace is often found, though the depth at which it is found varies greatly between runs (and sometimes it is not found), I guess it's normal in this case to have variation though since we interrupt on first accepted trace.
A trace with 2 procs below, run twice (in a row), finds an accepted run in one but not the other.