Add new JumpForwarding pass

[ThomasHaas]

I added a jump forwarding pass that simplifies some ugly branching code like this:

goto L1  // This can directly jump to L2
L1:        // This label and the following jump can be deleted once all jumps are forwarded to L2
goto L2:
L2:

Oddly, this consistently yielded slower runtimes for challenging/cna.c under SC with B=2 (UNKNOWN).
Looking more into this, I noticed that the simplified code has less equivalence classes according to BranchEquivalence.
This yields stronger merging of cf-variables in the encoding stage.
This seems to be able to have negative impact for UNKNOWN programs, possibly because the solver cannot reason so easily about only the branch that contains the reachable bound event if that branch is merged with others (not sure though).
So I also added an option to BranchEquivalence that puts every branch into its own class (which leads to less aggressive merging of cf-variables). With this option enabled, the jump forwarding seems beneficial again.
Interestingly, for the B=3 (PASS) version of cna.c the stronger merging enabled by jump forwarding also seems to be beneficial. Maybe this is because the solver has to reason about all branches anyhow (since it is PASS) and so it is better to have them merged.

So overall my impression is this:

• More aggressive merging of cf-variables, whether due to the jump forwarding or aggressive BranchEquivalence, is good for PASS programs
• Less aggressive merging of cf-variables might be better for FAIL/UNKNOWN programs. No merging at all is still quite bad though.
• The sweet spot might be the following: merging cf-variables only of same-branch events (the new option of BranchEquivalence) but reducing the total number of branches (the new pass).
• The above claims are just from observing cna.c and might be different across different benchmarks.

[ThomasHaas]

Looking at the CI, it seems this PR has a very bad negative impact, especially on safe_stack.

[ThomasHaas]

With two successive runs showing bad performance, I guess we shouldn't merge this.
It's unfortunate, because this pass removes 10+% of unnecessary events and makes the resulting code quite a bit easier to read. At the same time, the bad performance suggests that adding more intermediary variables might be helpful (as eliminating them seems to be bad).
My best guess is that the pass can flatten the control-flow hierarchy in a bad way:

if (...) goto L1
if (...) goto L1
L1: // Two incoming jumps
goto L3 
...
if (...) goto L2
if (...) goto L2
L2: // Two incoming jumps
goto L3:
...
L3: // Has two incoming jumps

In the above version, L3 has 2 incoming jumps each of which has themselves 2 ways to be reached for a total of 2x2=4 paths to L3.
In the optimised version, L3 still has 4 reaching paths but via 4 different jumps instead of 2x2 combinations.
Maybe the solver now needs to reason about all 4 paths separately and cannot reason in groups of 2 anymore?

[hernanponcedeleon]

Why do the changes affect the RA tests?

[ThomasHaas]

It's a very good question. I don't know. The only reason can be that ExecutionAnalysis.isImplied/areMutuallyExclusive is affected by the option and that for some reason LazyRA and NativeRA use this information differently?
It is certainly odd.

[hernanponcedeleon]

Ran locks and lfds benchmarks five times per configuration with --bound=2 using vmm.cat.

PR improvement = (disabled − default) / disabled; positive means the PR default (true) is faster.

Benchmark	Default (true)	Disabled (false)	PR improvement
chase-lev	1.145 s	1.167 s	+1.8%
dglm	24.678 s	20.358 s	-21.2%
hash_table	0.500 s	0.493 s	-1.4%
ms	30.074 s	28.854 s	-4.2%
treiber	3.045 s	2.707 s	-12.5%
clh_mutex	0.564 s	0.569 s	+0.9%
cna	9.744 s	9.258 s	-5.3%
deadlock	0.282 s	0.261 s	-8.0%
linuxrwlock	1.074 s	1.138 s	+5.6%
mutex	2.398 s	2.455 s	+2.3%
mutex_musl	4.029 s	3.987 s	-1.1%
pthread_mutex	0.278 s	0.245 s	-13.4%
seqlock	0.567 s	0.550 s	-3.2%
spinlock	0.378 s	0.392 s	+3.5%
ticket_awnsb_mutex	2.334 s	2.386 s	+2.2%
ticketlock	0.293 s	0.343 s	+14.5%
ttas	0.447 s	0.484 s	+7.6%
Total	81.832 s	75.646 s	-8.2%

Overall it seems the current default option is bad. I would use false by default. Othern than that the changes LGTM.

[ThomasHaas]

Did you only compare the two configurations with each other? Btw. false was the default, but you changed it to true :P.
The important question is whether this PR (either option) is better than development. So far, this didn't seem to be the case

[hernanponcedeleon]

The history says "you changed, I committed" :D.

Yes, I compared only the configurations based on the code of this branch. Can also make comparison with development.

What I compared with development was "visually": I printed the IR on a few examples and I agree that it looks a bit better with the jump forwarding.

[hernanponcedeleon]

• Development: no JumpForwarding; original branch-equivalence behavior.
• Disabled: JumpForwarding enabled, but simpleBranchEquivalence=false; original branch-equivalence behavior.
• Default: JumpForwarding enabled and simpleBranchEquivalence=true.

Benchmark	Development	Disabled	Default	JumpForwarding improvement	Simple-BE improvement
chase-lev	1.197 s	1.167 s	1.145 s	+2.5%	+1.9%
dglm	21.457 s	20.358 s	24.678 s	+5.1%	-21.2%
hash_table	0.494 s	0.493 s	0.500 s	+0.2%	-1.4%
ms	31.288 s	28.854 s	30.074 s	+7.8%	-4.2%
treiber	2.684 s	2.707 s	3.045 s	-0.9%	-12.5%
clh_mutex	0.613 s	0.569 s	0.564 s	+7.2%	+0.9%
cna	8.794 s	9.258 s	9.744 s	-5.3%	-5.2%
deadlock	0.279 s	0.261 s	0.282 s	+6.5%	-8.0%
linuxrwlock	1.444 s	1.138 s	1.074 s	+21.2%	+5.6%
mutex	2.362 s	2.455 s	2.398 s	-3.9%	+2.3%
mutex_musl	3.696 s	3.987 s	4.029 s	-7.9%	-1.1%
pthread_mutex	0.306 s	0.245 s	0.278 s	+20.0%	-13.5%
seqlock	0.662 s	0.550 s	0.567 s	+17.0%	-3.1%
spinlock	0.477 s	0.392 s	0.378 s	+17.8%	+3.6%
ticket_awnsb_mutex	2.242 s	2.386 s	2.334 s	-6.4%	+2.2%
ticketlock	0.368 s	0.343 s	0.293 s	+6.9%	+14.6%
ttas	0.538 s	0.484 s	0.447 s	+10.0%	+7.6%
Total	78.903 s	75.647 s	81.830 s	+4.1%	-8.2%

I would say once we change the default option, we can merge.

[ThomasHaas]

Can you check the larger benchmarks like safe_stack, maybe qspinlock (if you have it), wsq and the more complex cna (in the challenging folder)? Especially safe_stack often showed over 100% overhead (sometimes even like 400%?).

[hernanponcedeleon]

I intentionally skip safe_stack because it unsafe and there is too much variance from run to run. I can run the benchmarking on the challenging folder

[hernanponcedeleon]

Benchmark	Development	Disabled	Default	JumpForwarding improvement	Simple-BE improvement
cna	22.766 s ± 0.621 s	19.608 s ± 0.801 s	23.039 s ± 1.466 s	+13.9%	-17.5%
harris-3	5.047 s ± 0.047 s	5.110 s ± 0.058 s	5.262 s ± 0.031 s	-1.2%	-3.0%
wsq	105.800 s ± 0.837 s	110.400 s ± 6.841 s	139.000 s ± 1.581 s	-4.3%	-25.9%

I would consider the regression in harris as noise. In wsq is more problematic, but also the std-dev from run to run is high, so I do not think this regression posses much problem. The speed-up in cna is quite good.

[ThomasHaas]

I intentionally skip safe_stack because it unsafe and there is too much variance from run to run. I can run the benchmarking on the challenging folder

Well yes, but IIRC the CI failed twice on safe_stack with a 15 minute timeout. And when I ran it locally, I got extremely high runtimes quite consistently. I think it was slower than usual every single time. Overall, the CI failed I think 3 times in a row: twice on safe_stack and once I think on a litmus test?! So I really want to be sure about the impact of this PR.
Granted, some negative impact might have been due to the bug in BranchEquivalence which is fixed now,

I also said this in my initial post:

Oddly, this consistently yielded slower runtimes for challenging/cna.c under SC with B=2 (UNKNOWN).

So there was a discrepancy between the performance on PASS and FAIL/UNKNOWN instances. I also think I tested this branch with the IDL encoding since we did not change the default yet IIRC. The SAT encoding might show less variance due to the generally smaller runtimes.

[hernanponcedeleon]

I made 20 runs per branch on safe_stack with B=2.

Target	Branch (simpleBranchEquivalence=false)	Development	Branch vs. development
TSO	16.825 ± 4.009 s	9.610 ± 4.519 s	75.1% slower
ARM8	17.027 ± 7.389 s	34.948 ± 13.408 s	51.3% faster

BTW, I do not see safe_stack timing out on the previous runs of this PR ... the faling cases where

[ERROR] com.dat3m.dartagnan.llvm.MiscellaneousTest.testAssume[56: floats_14, target=IMM] -- Time elapsed: 20.01 s <<< ERROR!

[ThomasHaas]

BTW, I do not see safe_stack timing out on the previous runs of this PR ... the faling cases where

[ERROR] com.dat3m.dartagnan.llvm.MiscellaneousTest.testAssume[56: floats_14, target=IMM] -- Time elapsed: 20.01 s <<< ERROR!

Hmm, I feel like I did more runs than the history shows. Maybe I did some locally? But I was certainly wrong about the litmus test: as you said, the floats test was failing (which was super surprising).

It's interesting that ARM is a lot faster and TSO is a lot slower in your tests. With the old IDL setting where solving times are much larger, I saw differences of over 100%. I remember that my machine usually needed 2-3 minutes for safe_stack but needed like 8-10 minutes on this branch. Anyways, if you are fine with the performance differences, we can merge I guess.
Feel free to change the defaul value of the option. I can also remove the option again, if you don't want to experiment with it anymore. I only added it because of weird performance degradations with the optimizations, but your evaluation shows that the option is almost always worse.

[hernanponcedeleon]

I think we can delete that option completely.

BTW: Im working on a PR that will add a CI job to do this performance evaluation in every PR. Maybe it makes sense to wait until that one is merged and let the CI do a final (maybe even larger) performance run.

[ThomasHaas]

That's up to you. We can also wait. This PR is totally orthogonal to every other change we do, so it doesn't block or unblock other PRs.

[github-actions]

Performance comparison

Linux x64

Memory model: vmm

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/cna.c	9.900 ± 0.662 s	9.291 ± 0.062 s	➖ +5.9% [-31.3%, +43.0%]	UNKNOWN
benchmarks/locks/mutex_musl.c	22.145 ± 0.805 s	22.655 ± 0.680 s	➖ -2.4% [-37.6%, +32.7%]	UNKNOWN
benchmarks/lfds/dglm.c	17.476 ± 1.006 s	16.206 ± 1.209 s	➖ +7.2% [-27.3%, +41.7%]	UNKNOWN
benchmarks/lfds/ms.c	38.789 ± 6.841 s	40.960 ± 4.022 s	➖ -7.4% [-111.1%, +96.4%]	UNKNOWN
benchmarks/lfds/treiber.c	8.904 ± 0.565 s	7.060 ± 0.170 s	✅ +20.6% [+3.1%, +38.1%]	UNKNOWN
benchmarks/lfds/safe_stack.c	5.506 ± 0.162 s	6.262 ± 0.023 s	➖ -13.8% [-35.8%, +8.1%]	UNKNOWN
benchmarks/challenging/cna.c	30.489 ± 3.527 s	32.869 ± 2.535 s	➖ -8.3% [-62.6%, +46.0%]	UNKNOWN

Memory model: aarch64

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/linuxrwlock.c	5.723 ± 0.030 s	5.737 ± 0.037 s	➖ -0.2% [-3.2%, +2.7%]	UNKNOWN
benchmarks/challenging/cna.c	9.742 ± 0.539 s	10.205 ± 0.202 s	➖ -5.0% [-48.6%, +38.5%]	UNKNOWN
benchmarks/challenging/wsq.c	5.170 ± 0.127 s	5.887 ± 0.009 s	➖ -13.9% [-29.3%, +1.5%]	UNKNOWN

Memory model: power

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/linuxrwlock.c	12.474 ± 0.264 s	12.374 ± 0.178 s	➖ +0.8% [-3.8%, +5.4%]	UNKNOWN
benchmarks/locks/mutex_musl.c	13.971 ± 0.301 s	13.275 ± 1.221 s	➖ +4.9% [-51.1%, +60.9%]	UNKNOWN
benchmarks/lfds/ms.c	20.075 ± 1.232 s	18.974 ± 1.220 s	➖ +5.3% [-42.2%, +52.7%]	UNKNOWN
benchmarks/lfds/treiber.c	11.858 ± 0.597 s	10.758 ± 0.285 s	➖ +9.2% [-6.6%, +25.0%]	UNKNOWN

Total

Benchmarks	Base branch	PR branch	Improvement (99% CI)
All reported benchmarks	212.221 ± 6.385 s	212.512 ± 3.975 s	➖ -0.2% [-13.4%, +13.0%]

4 benchmark(s) omitted because both averages were below 5 seconds.

macOS ARM64

Memory model: vmm

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/cna.c	24.276 ± 0.923 s	24.593 ± 0.349 s	➖ -1.4% [-27.3%, +24.5%]	UNKNOWN
benchmarks/locks/mutex_musl.c	35.748 ± 0.494 s	34.084 ± 3.076 s	➖ +4.6% [-50.5%, +59.7%]	UNKNOWN
benchmarks/lfds/dglm.c	46.225 ± 5.628 s	66.667 ± 3.055 s	➖ -45.8% [-160.8%, +69.2%]	UNKNOWN
benchmarks/lfds/ms.c	75.000 ± 3.606 s	73.000 ± 4.583 s	➖ +2.4% [-53.6%, +58.4%]	UNKNOWN
benchmarks/lfds/treiber.c	19.855 ± 0.973 s	20.169 ± 2.415 s	➖ -1.4% [-44.6%, +41.8%]	UNKNOWN
benchmarks/lfds/safe_stack.c	15.893 ± 3.303 s	14.477 ± 3.222 s	➖ +9.1% [-12.3%, +30.5%]	UNKNOWN
benchmarks/challenging/cna.c	44.662 ± 4.732 s	45.625 ± 8.496 s	➖ -2.0% [-79.8%, +75.7%]	UNKNOWN

Memory model: aarch64

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/linuxrwlock.c	19.541 ± 1.257 s	20.380 ± 1.964 s	➖ -4.2% [-23.0%, +14.7%]	UNKNOWN
benchmarks/locks/mutex_musl.c	16.184 ± 0.429 s	15.584 ± 2.015 s	➖ +3.7% [-68.7%, +76.0%]	UNKNOWN
benchmarks/lfds/dglm.c	12.194 ± 0.149 s	11.407 ± 0.154 s	➖ +6.4% [-5.4%, +18.3%]	PASS
benchmarks/lfds/ms.c	16.530 ± 1.019 s	18.652 ± 3.390 s	➖ -13.6% [-156.9%, +129.7%]	UNKNOWN
benchmarks/challenging/cna.c	38.875 ± 2.717 s	37.566 ± 2.532 s	➖ +2.9% [-64.0%, +69.8%]	UNKNOWN
benchmarks/challenging/wsq.c	20.028 ± 1.489 s	18.391 ± 0.732 s	➖ +7.7% [-48.6%, +64.0%]	UNKNOWN

Memory model: power

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/linuxrwlock.c	57.459 ± 2.639 s	47.756 ± 3.725 s	✅ +17.0% [+1.4%, +32.5%]	UNKNOWN
benchmarks/locks/mutex_musl.c	36.091 ± 4.708 s	35.961 ± 1.882 s	➖ -0.4% [-55.0%, +54.1%]	UNKNOWN
benchmarks/lfds/dglm.c	11.630 ± 1.890 s	10.476 ± 0.171 s	➖ +8.3% [-76.6%, +93.3%]	UNKNOWN
benchmarks/lfds/ms.c	57.982 ± 5.545 s	49.258 ± 4.727 s	✅ +15.0% [+12.2%, +17.8%]	UNKNOWN
benchmarks/lfds/treiber.c	25.861 ± 2.239 s	27.945 ± 2.542 s	➖ -8.1% [-29.8%, +13.7%]	UNKNOWN

Total

Benchmarks	Base branch	PR branch	Improvement (99% CI)
All reported benchmarks	574.033 ± 12.338 s	571.991 ± 15.282 s	➖ +0.3% [-26.8%, +27.4%]

[hernanponcedeleon]

Performance remains unchanged overall, thus I think we can merge.