Issues with LTL traces in MT context

[yanntm]

Hi, So I'm trying to get traces out of ltl, but the results are a bit random, and the files tend to be broken.

Attached model, when run with 8 threads, typically produces a gcf file with incomplete or completely wrong information, or even a corrupt gcf that subsequently crashes ltsmin-printtrace. In particular resolution of edge labels seems bad, the states themselves are consistent.

I think the problem comes from this invocation : https://github.com/utwente-fmt/ltsmin/blob/3499bb5afb06c5e955d0df5bb3220eb7b654f3da/src/pins2lts-mc/algorithm/dfs-fifo.c#L104

We are coming from here : https://github.com/utwente-fmt/ltsmin/blob/3499bb5afb06c5e955d0df5bb3220eb7b654f3da/src/pins2lts-mc/algorithm/dfs-fifo.c#L123-L127 Where we did set LTSMIN exit to signal but the barrier is not strong to ensure only one thread is still working.

Most other invocations to trace are much more heavily protected or delayed as in this instance : https://github.com/utwente-fmt/ltsmin/blob/master/src/pins2lts-mc/algorithm/ltl.c#L77-L89

The call that was commented + the comment preceding it makes me think the issue has been met before. @alaarman Could we use the same kind of behavior for NonProgress cycles ? somehow print the trace with a single thread AFTER all threads have acknowledged the EXIT sign.

In other cases, there is also care taken, e.g. only master is working here https://github.com/utwente-fmt/ltsmin/blob/3499bb5afb06c5e955d0df5bb3220eb7b654f3da/src/pins2lts-mc/algorithm/ufscc.c#L725

---

Attached are a few test files example.zip

Compile with 'gcc' -g '-c' '-I/home/ythierry/git/ITSTools/ltsmin/fr.lip6.move.gal.ltsmin.binaries/bin/include/' '-I.' '-std=c99' '-fPIC' '-O0' 'model.c';'gcc' -g '-c' '-I/home/ythierry/git/ITSTools/ltsmin/fr.lip6.move.gal.ltsmin.binaries/bin/include/' '-I.' '-std=c99' '-fPIC' '-O0' 'strat.c';'gcc' -g '-shared' '-o' 'gal.so' 'model.o' strat.o

Then I'm running this: /home/ythierry/git/LTSmin-BinaryBuilds/ltsmin/src/pins2lts-mc/pins2lts-mc './gal.so' '--threads=1' '--when' '--ltl' '<>((LTLAPtower==true))' '--buchi-type=spotba' '-v' '--trace' 'trace.gcf'

So threads=1 works, threads=8 is mostly producing corrupt GCF file.

**

thanks for your insight, I'll keep investigating, but it's one of those subtle concurrency issues so not easy to fully diagnose, and I have the feeling that the solution has already been developed, just this call was not updated to honor it.