Detected non-deterministic results when --jobs is not set to 1

[AnnabellaM]

Hi, I have recently been using Infer for an empirical study to detect non-deterministic behaviors in static analyzers. The experiments resulted in discovering some nondeterministic analysis results across multiple runs under various configurations of Infer.

• [ ] The version of Infer I used isv1.1.0.
• [ ] The operating system is ubuntu:20.04and I am using Docker.
• [ ] I ran Infer on 20 sampling configurations. The base command I used is infer --compilation-database compile_commands.json with following checkers on --annotation-reachability --bufferoverrun --cost --loop-hoisting --pulse, as well as these options used--dump-duplicate-symbols --headers --max-nesting --jobs --reactive --scheduler.
• [ ] I ran Infer on each program-configuration combination 5 times and compared the results across 5 runs for detecting non-deterministic behaviors. The program I used is openssl. And the nondeterministic results are found under the configurations shown below. As observed, these nondeterminism all happen when the --jobs option is not set to 1.

For example, here are some different results from the running Infer under the same configuration --headers --max-nesting 1 --jobs 5 --reactive --scheduler callgraph . result 1:

result 2:

result 3:

Could you please offer some insights into this issue and suggest ways to mitigate the non-deterministic behavior when running Infer with multiple jobs? Thank you.

[AnnabellaM]

Hello Infer team, I'm following up on this issue and would greatly appreciate any insights you could provide. Thank you!

[ngorogiannis]

Hi, it is indeed a known issue. Several fixes have landed on master since the 1.1 release (we ought to do one soon), so I would suggest:

• trying master
• disabling biabduction (if not already)
• using the restart scheduler
• code with recursive functions may still exhibit non-determinism.