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.

[hernanponcedeleon]

• Add support for locations in litmus tests (probably the hardest solution to implement).

Implementing this should not be hard, right? We just need to parse the locations/registers in this list, store them in the program as some "metadata", and compute the notion of state not only based on the variables of the spec, but rather the union of those with the ones computed here.

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

can you explain me why the "bug" is gone?

[ThomasHaas]

• Add support for locations in litmus tests (probably the hardest solution to implement).

Implementing this should not be hard, right? We just need to parse the locations/registers in this list, store them in the program as some "metadata", and compute the notion of state not only based on the variables of the spec, but rather the union of those with the ones computed here.

Just as "metadata" is a bit problematic, but yeah, we need to store the list somewhere similar to how we store the spec.
However, we need to be careful that existing passes are updated, e.g., Tearing may also need to tear the stored expressions.

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

can you explain me why the "bug" is gone?

The c11.cat model had a place where it used R & W to refer to RMWs in the context of release-sequences. Clearly, that relation is always empty in our modeling, which broke release sequences. I assume the FADD chains that could form in linuxrwlock were affected by that. Replacing R & W by RMW restores the release sequences as intended.