Add EnumerationTask and related classes

[ThomasHaas]

• EnumerationTask represents the task of enumerating final states. Currently, limited to litmus code.
• There is a new option --mode={verification, enumeration} to select the type of task to solve.

Possible TODOs:

• Add mode option to UI
• Maybe merge EnumerationSolver with AssumeSolver: they share a lot of code.
• Maybe some package refactoring.
• Unit tests?
• Make enumeration bound configurable (currently fixed at 10000 states)
• Add bounds checks to report incomplete enumeration
• Rename --mode=verification/enumeration to the shorter --mode=verify/enumerate?

[hernanponcedeleon]

• EnumerationTask represents the task of enumerating final states. Currently, limited to litmus code.
• There is a new option --mode={verification, enumeration} to select the type of task to solve.

I haven't test it, but seeing a new option and no changes to the relection file, it might be the case the options does not work in native. Also, if the option is in a new class, it will not be shown in the help. I will add (in another PR) some test so make sure we do not miss this situation anymore.

Possible TODOs:

• Unit tests?

Done.

Many of the tests will fail, but this does not necessarily mean the exploraiton is wrong. I generated the expected results using the cat files in herd's repo, thus there might be a missmatch with our cat models. But if this is the case, we should figure out how and why the models differ.

[github-actions]

Performance comparison

Linux x64

Benchmark details

Memory model: vmm

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/cna.c	10.006 ± 0.233 s	10.280 ± 0.472 s	➖ -2.8% [-36.8%, +31.2%]	UNKNOWN
benchmarks/locks/mutex_musl.c	21.349 ± 0.214 s	21.595 ± 0.328 s	➖ -1.2% [-6.3%, +4.0%]	UNKNOWN
benchmarks/lfds/dglm.c	22.471 ± 4.705 s	21.995 ± 4.258 s	➖ +0.0% [-122.2%, +122.2%]	UNKNOWN
benchmarks/lfds/ms.c	32.665 ± 0.568 s	33.220 ± 0.775 s	➖ -1.7% [-7.1%, +3.7%]	UNKNOWN
benchmarks/lfds/treiber.c	9.609 ± 0.279 s	9.349 ± 0.283 s	➖ +2.6% [-23.3%, +28.6%]	UNKNOWN
benchmarks/lfds/safe_stack.c	5.156 ± 0.348 s	5.184 ± 0.687 s	➖ -0.5% [-60.2%, +59.2%]	UNKNOWN
benchmarks/challenging/cna.c	36.732 ± 2.817 s	35.870 ± 0.317 s	➖ +2.0% [-40.5%, +44.5%]	UNKNOWN

Memory model: aarch64

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/linuxrwlock.c	5.668 ± 0.117 s	5.400 ± 0.249 s	➖ +4.7% [-16.3%, +25.8%]	UNKNOWN
benchmarks/challenging/cna.c	14.154 ± 1.252 s	13.111 ± 0.919 s	➖ +6.9% [-52.5%, +66.3%]	UNKNOWN
benchmarks/challenging/wsq.c	5.545 ± 0.053 s	5.468 ± 0.113 s	➖ +1.4% [-8.6%, +11.3%]	UNKNOWN

Memory model: power

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/linuxrwlock.c	13.372 ± 0.165 s	13.641 ± 0.279 s	➖ -2.0% [-21.0%, +16.9%]	UNKNOWN
benchmarks/locks/mutex_musl.c	12.235 ± 1.332 s	11.555 ± 1.170 s	➖ +5.0% [-60.8%, +70.8%]	UNKNOWN
benchmarks/lfds/ms.c	24.099 ± 4.272 s	22.955 ± 2.649 s	➖ +4.0% [-33.4%, +41.5%]	UNKNOWN
benchmarks/lfds/treiber.c	11.790 ± 0.799 s	11.495 ± 0.232 s	➖ +2.2% [-32.0%, +36.5%]	UNKNOWN

Total

Benchmarks	Base branch	PR branch	Improvement (99% CI)
All reported benchmarks	224.852 ± 6.381 s	221.119 ± 1.670 s	➖ +1.6% [-18.4%, +21.5%]

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

macOS ARM64

Benchmark details

Memory model: vmm

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/cna.c	17.605 ± 0.675 s	18.584 ± 0.467 s	➖ -5.7% [-38.5%, +27.2%]	UNKNOWN
benchmarks/locks/mutex_musl.c	42.353 ± 5.523 s	38.244 ± 3.378 s	➖ +9.0% [-53.8%, +71.8%]	UNKNOWN
benchmarks/lfds/dglm.c	47.453 ± 4.966 s	42.822 ± 4.767 s	➖ +9.8% [-4.2%, +23.7%]	UNKNOWN
benchmarks/lfds/ms.c	77.000 ± 7.810 s	67.000 ± 5.568 s	➖ +12.5% [-46.8%, +71.7%]	UNKNOWN
benchmarks/lfds/treiber.c	16.715 ± 1.439 s	15.572 ± 1.113 s	➖ +6.5% [-43.8%, +56.8%]	UNKNOWN
benchmarks/lfds/safe_stack.c	13.745 ± 1.045 s	11.528 ± 0.429 s	➖ +15.7% [-38.1%, +69.4%]	UNKNOWN
benchmarks/challenging/cna.c	46.901 ± 6.995 s	47.942 ± 6.051 s	➖ -2.5% [-32.9%, +27.9%]	UNKNOWN

Memory model: aarch64

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/linuxrwlock.c	18.491 ± 0.951 s	19.893 ± 1.469 s	➖ -7.7% [-52.4%, +37.1%]	UNKNOWN
benchmarks/locks/mutex_musl.c	14.100 ± 2.389 s	14.596 ± 0.248 s	➖ -5.8% [-122.4%, +110.8%]	UNKNOWN
benchmarks/lfds/dglm.c	14.610 ± 2.705 s	12.517 ± 0.865 s	➖ +12.7% [-65.0%, +90.5%]	PASS
benchmarks/lfds/ms.c	15.963 ± 0.221 s	15.580 ± 1.300 s	➖ +2.3% [-50.9%, +55.5%]	UNKNOWN
benchmarks/challenging/cna.c	33.163 ± 2.126 s	37.305 ± 2.370 s	➖ -12.6% [-39.5%, +14.4%]	UNKNOWN
benchmarks/challenging/wsq.c	17.316 ± 2.762 s	14.947 ± 0.937 s	➖ +12.1% [-74.8%, +99.0%]	UNKNOWN

Memory model: power

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/linuxrwlock.c	81.000 ± 12.767 s	59.281 ± 15.102 s	➖ +27.6% [-25.9%, +81.1%]	UNKNOWN
benchmarks/locks/mutex_musl.c	38.116 ± 0.813 s	37.354 ± 1.314 s	➖ +2.0% [-15.9%, +19.9%]	UNKNOWN
benchmarks/lfds/dglm.c	8.956 ± 1.621 s	10.595 ± 0.394 s	➖ -20.2% [-112.2%, +71.7%]	UNKNOWN
benchmarks/lfds/ms.c	51.434 ± 7.251 s	56.948 ± 4.953 s	➖ -11.3% [-47.7%, +25.1%]	UNKNOWN
benchmarks/lfds/treiber.c	22.604 ± 2.710 s	21.499 ± 0.161 s	➖ +4.1% [-56.3%, +64.4%]	UNKNOWN

Total

Benchmarks	Base branch	PR branch	Improvement (99% CI)
All reported benchmarks	577.526 ± 14.147 s	542.208 ± 17.793 s	✅ +6.1% [+1.3%, +11.0%]

[ThomasHaas]

From local testing, we still have 41 test failures. One of them times out due to OOTA.
Most of them have a spec and still list locations which causes a mismatch where Dartagnan enumerates less than intended. However, for the C11 litmus test ../litmus/C11/manual/imm-R2-alt.litmus, we enumerate 13 instead of 12 states. This one might be the only genuine discrepancy between Dartagnan and herd7.

[ThomasHaas]

I extracted a litmus test on which herd7 and Dartagnan disagree under c11.cat:

C imm-R2

(*
 * Bridging the Gap between Programming Languages and Hardware Weak Memory Models
 *)

{}

P0 (atomic_int* x, atomic_int* y) {
    atomic_store_explicit(y, 1, memory_order_relaxed);
    atomic_store_explicit(x, 1, memory_order_release);
}

P1 (atomic_int* x) {
    atomic_thread_fence(memory_order_release);
    int r0 = atomic_fetch_add_explicit(x, 1, memory_order_acquire);
    atomic_store_explicit(x, 3, memory_order_relaxed);
}

P2 (atomic_int* x, atomic_int* y) {
    int r0 = atomic_load_explicit(x, memory_order_acquire);
    int r1 = atomic_load_explicit(y, memory_order_relaxed);
}

exists (1:r0=1 /\ 2:r0=2 /\ 2:r1=0) // Reachable in Dartagnan, unreachable in Herd7

It looks like a release-acquire chain interrupted by an RMW. Looking at the c11.cat memory model, it does not seem to have a construct like (rf;rmw)* to extend release-acquire chains like other models do.

[xeren]

Dartagnan's c11.cat does feature a term R & W, which might rather be RMW. The above litmus test fails with this change.

[ThomasHaas]

That's a good point. R & W is clearly wrong in our model.

EDIT: Replacing R & W with RMW fixed the problem without breaking anything else in the litmus tests.

[ThomasHaas]

@hernanponcedeleon Except for the one timeout due to OOTA, I think all remaining failing tests are due to the explicitly mentioned locations inside the tests that cause herd7 to enumerate more.
I think we have the following options:

• Remove the locations bit from those tests and let herd7 generate new expected values
• Skip those tests only for enumeration but not for verification (requires a separate skip list)
• Add support for locations in litmus tests (probably the hardest solution to implement).

[ThomasHaas]

The verdict on linuxrwlock under c11.cat has changed from FAIL to UNKNOWN which looks reasonable to me.