pins2lts-mc --threads=1 : bad option

[yanntm]

Despite the current documentation stating this flag exists, it is not recognized.

Doc (googled it): http://fmt.cs.utwente.nl/tools/ltsmin/pins2lts-mc.html

Current/latest "next" doc : https://github.com/utwente-fmt/ltsmin/blob/next/doc/inc/pins2lts-mc-options.txt

Run trace : [ythierry@localhost Eratosthenes-PT-010 (master)]$ ../../../ITS-Tools-Dependencies/ltsmin/src/pins2lts-mc/pins2lts-mc gal.so --threads=1 -i EratosthenesPT010ReachabilityCardinality0==true pins2lts-mc: ============================================================================= pins2lts-mc: Runtime environment could only preallocate 31 GB while requesting 502 GB. pins2lts-mc: Configure your system limits to exploit all memory. pins2lts-mc: ============================================================================= pins2lts-mc( 0/ 8), error : bad option: --threads=1 (use --help for help)

(except --help crashes, see other submitted issue)

[yanntm]

Actually digging into the source : --procs=1 works

[alaarman]

The underlying threading library supports threads and processes. Some frontends are not thread-safe, we run those with processes. The pins2 frontend could be such a case, so conservatively we assume it only works with threads. If this is not required for GAL, I recommend that you set SPEC_MT_SAFE to 1 in src/pins-lib/pins-impl.h. Unfortunately we cannot make this optional, but we can make a second pins2 frontend that assume thread-safety.

We should also document the --threads / --procs difference as you mention. Noted.

[yanntm]

So If I set that SPEC_MT_SAFE flag at compile time, the multi-core engine supposes that my gal.so is reentrant is that right ? It is reentrant, it's very static and read only precomputed stuff, I can do that.

But mostly I'm trying to run pins2lts with only one thread (so the issue is not reentrance), -seq crashes, so I thought to use -mc with 1 thread limit, hence my digging into the option. The problem is just that is is misnamed in the doc, so I couldn't immediately find it.

If only one of procs or threads is applicable for a given tool, maybe one single option would suffice from the user point of view, it specifies how much parallelism we allow the tool.

[alaarman]

PINS next-state calls are never assumed to be re-entrant. However, if --threads is used (as opposed to --procs), then the frontend should be thread-safe, i.e. no static variables, no races.

[alaarman]

The issue is that the toolset supports having MPI workers, processes and threads (at the same time). I doubt there is a combination for the latter two, so perhaps we should fix that.

[Meijuh]

Fixed.