Hi!
Sorry that I joined the convo so late! These measurements and the preparation is world class, especially the annotated charts! Well done! I’m raising some technical issues here, but that shouldn’t take away from the work or the actual achievements.
We noticed lately that our jobs became severely non-deterministic. My measurements show that even on very small projects, clang reliably produces different result sets with the same configuration.
This is a diff in between two identical runs, all configs are set to their default values, yet there are differences in results:
https://codechecker-demo.eastus.cloudapp.azure.com/Default/reports?run=qtbase_v6.2.0_determinism_check9A_1&run=libwebm_libwebm-1.0.0.27_determinism_check9A_1&run=vim_v8.2.1920_determinism_check9A_1&newcheck=qtbase_v6.2.0_determinism_check9B_1&newcheck=libwebm_libwebm-1.0.0.27_determinism_check9B_1&newcheck=vim_v8.2.1920_determinism_check9B_1
This is a diff in between two identical runs with the two timeout Z3 configs set to 0, the rlimit config is left unchanged, still, different result sets:
https://codechecker-demo.eastus.cloudapp.azure.com/Default/reports?run=qtbase_v6.2.0_determinism_check12A_1&run=libwebm_libwebm-1.0.0.27_determinism_check12A_1&run=vim_v8.2.1920_determinism_check12A_1&newcheck=qtbase_v6.2.0_determinism_check12B_1&newcheck=libwebm_libwebm-1.0.0.27_determinism_check12B_1&newcheck=vim_v8.2.1920_determinism_check12B_1
This is a diff in between two identical runs with only the “crosscheck-with-z3-rlimit-threshold” set to 0, other configs are unchanged, result sets aren’t identical, even though this is supposed to be a deterministic cutoff:
https://codechecker-demo.eastus.cloudapp.azure.com/Default/reports?run=qtbase_v6.2.0_determinism_check13A_3&run=libwebm_libwebm-1.0.0.27_determinism_check13A_3&run=vim_v8.2.1920_determinism_check13A_3&newcheck=qtbase_v6.2.0_determinism_check13B_3&newcheck=libwebm_libwebm-1.0.0.27_determinism_check13B_3&newcheck=vim_v8.2.1920_determinism_check13B_3
This is a diff in between two identical runs with ALL new Z3 configs set to 0, finally seems deterministic, but of course, catching non-determinism is easy as long as find a mismatch, not so much the other way around:
https://codechecker-demo.eastus.cloudapp.azure.com/Default/reports?run=qtbase_v6.2.0_determinism_check13A_2&run=libwebm_libwebm-1.0.0.27_determinism_check13A_2&run=vim_v8.2.1920_determinism_check13A_2&newcheck=qtbase_v6.2.0_determinism_check13B_2&newcheck=libwebm_libwebm-1.0.0.27_determinism_check13B_2&newcheck=vim_v8.2.1920_determinism_check13B_2
To us, nondeterminism is a major dealbreaker, and we issued an emergency fix for our downstream branch. I’m writing this comment to discuss whether we should set these configs to 0 by default, because my gut feeling is that we shouldn’t release an analyzer version with so much (any, really) non-determinism, certainly not by default.
Can I suggest that we offer a frontend, or even driver level flag like ‘-analyzer-quick’ that sets these to their appropriate values, but is off by default?
Again, big respect for the real advantages introduced by the patch and the thorough work to back it up!