[RFC] Program extensions

[ThomasHaas]

This is a quick implementation of an idea I had.

Some program formats like Litmus specify extended information such as filters and specs that go beyond the program itself.
To capture this, I added a ProgramExtension member to Program which can be instantiated to a ProgramExtension.Litmus object containing all the extra information. I also used this for SPIR-V which uses the same filter/spec structure as litmus.
As noted in #1086, the litmus format can also specify "locations" for the purpose of enumeration. Supporting this would be straightforward by adding a new member to ProgramExtension.Litmus.

I'm not sure if this is the best way to go about it and if there are any pitfalls, but the idea seems reasonable to me.

[ThomasHaas]

If the only goal is to handle litmus locations, we can also use the cheap solution of just adding another member to Program. The question is whether we want throw everything into the Program class. An imaginable advantage is that we could reuse this even for non-litmus programs.

A different perspective would be to just consider all of this a "program spec" rather than a "program extension" and therefore use a less general ProgramSpecification class instead.

[github-actions]

Performance comparison

Linux x64

Benchmark details

Memory model: vmm

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/cna.c	13.973 ± 0.268 s	13.966 ± 0.069 s	➖ +0.0% [-13.8%, +13.9%]	UNKNOWN
benchmarks/locks/mutex_musl.c	30.146 ± 4.335 s	33.981 ± 1.045 s	➖ -14.0% [-93.9%, +65.9%]	UNKNOWN
benchmarks/lfds/dglm.c	22.812 ± 0.910 s	21.561 ± 2.076 s	➖ +5.6% [-30.1%, +41.2%]	UNKNOWN
benchmarks/lfds/ms.c	36.232 ± 4.960 s	36.273 ± 3.983 s	➖ -2.0% [-132.9%, +128.8%]	UNKNOWN
benchmarks/lfds/treiber.c	9.145 ± 0.432 s	8.848 ± 0.413 s	➖ +3.0% [-49.9%, +55.9%]	UNKNOWN
benchmarks/lfds/safe_stack.c	7.249 ± 0.167 s	6.807 ± 0.122 s	➖ +6.1% [-1.1%, +13.3%]	UNKNOWN
benchmarks/challenging/cna.c	36.177 ± 2.634 s	35.319 ± 1.146 s	➖ +2.0% [-43.0%, +47.1%]	UNKNOWN

Memory model: aarch64

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/linuxrwlock.c	6.638 ± 0.199 s	6.781 ± 0.245 s	➖ -2.3% [-39.4%, +34.8%]	UNKNOWN
benchmarks/locks/mutex_musl.c	5.089 ± 0.480 s	5.348 ± 0.600 s	➖ -6.5% [-131.2%, +118.3%]	UNKNOWN
benchmarks/challenging/cna.c	13.674 ± 1.253 s	14.116 ± 0.261 s	➖ -3.9% [-65.6%, +57.8%]	UNKNOWN
benchmarks/challenging/wsq.c	6.023 ± 0.268 s	6.105 ± 0.149 s	➖ -1.6% [-40.1%, +37.0%]	UNKNOWN

Memory model: power

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/linuxrwlock.c	18.244 ± 0.474 s	17.659 ± 0.694 s	➖ +3.2% [-12.3%, +18.7%]	UNKNOWN
benchmarks/locks/mutex_musl.c	20.286 ± 1.816 s	21.345 ± 0.954 s	➖ -5.5% [-31.7%, +20.7%]	UNKNOWN
benchmarks/lfds/dglm.c	5.728 ± 0.270 s	5.864 ± 0.058 s	➖ -2.5% [-32.0%, +26.9%]	UNKNOWN
benchmarks/lfds/ms.c	25.514 ± 3.150 s	24.325 ± 2.273 s	➖ +3.6% [-84.0%, +91.1%]	UNKNOWN
benchmarks/lfds/treiber.c	17.162 ± 0.158 s	17.133 ± 0.296 s	➖ +0.2% [-4.5%, +4.8%]	UNKNOWN

Total

Benchmarks	Base branch	PR branch	Improvement (99% CI)
All reported benchmarks	274.092 ± 7.097 s	275.431 ± 2.570 s	➖ -0.5% [-12.9%, +11.9%]

2 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	22.101 ± 1.457 s	21.582 ± 2.429 s	➖ +2.5% [-36.1%, +41.1%]	UNKNOWN
benchmarks/locks/mutex_musl.c	31.655 ± 0.819 s	30.662 ± 0.952 s	➖ +3.1% [-25.2%, +31.4%]	UNKNOWN
benchmarks/lfds/dglm.c	59.608 ± 5.635 s	63.667 ± 3.786 s	➖ -7.1% [-33.2%, +19.0%]	UNKNOWN
benchmarks/lfds/ms.c	80.667 ± 3.786 s	79.000 ± 2.646 s	➖ +2.0% [-15.3%, +19.3%]	UNKNOWN
benchmarks/lfds/treiber.c	24.163 ± 0.563 s	22.655 ± 0.390 s	➖ +6.2% [-7.3%, +19.7%]	UNKNOWN
benchmarks/lfds/safe_stack.c	15.514 ± 0.458 s	16.118 ± 0.566 s	➖ -4.0% [-43.0%, +35.0%]	UNKNOWN
benchmarks/challenging/cna.c	54.407 ± 1.953 s	56.895 ± 2.716 s	➖ -4.5% [-11.7%, +2.6%]	UNKNOWN

Memory model: aarch64

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/linuxrwlock.c	20.851 ± 0.727 s	22.003 ± 0.818 s	➖ -5.5% [-13.4%, +2.3%]	UNKNOWN
benchmarks/locks/mutex_musl.c	17.026 ± 1.021 s	17.020 ± 1.124 s	➖ -0.1% [-34.7%, +34.6%]	UNKNOWN
benchmarks/lfds/dglm.c	15.030 ± 2.539 s	14.656 ± 0.658 s	➖ -0.0% [-129.6%, +129.5%]	PASS
benchmarks/lfds/ms.c	13.613 ± 0.497 s	14.489 ± 0.502 s	➖ -6.5% [-27.8%, +14.8%]	UNKNOWN
benchmarks/challenging/cna.c	41.220 ± 1.736 s	43.634 ± 1.373 s	➖ -6.1% [-48.0%, +35.9%]	UNKNOWN
benchmarks/challenging/wsq.c	20.452 ± 0.762 s	19.544 ± 0.528 s	➖ +4.4% [-5.2%, +14.0%]	UNKNOWN

Memory model: power

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/linuxrwlock.c	65.194 ± 13.689 s	52.572 ± 4.662 s	➖ +18.1% [-34.0%, +70.2%]	UNKNOWN
benchmarks/locks/mutex_musl.c	50.488 ± 9.221 s	44.911 ± 4.451 s	➖ +10.0% [-45.9%, +65.9%]	UNKNOWN
benchmarks/lfds/dglm.c	10.947 ± 1.959 s	10.438 ± 0.793 s	➖ +3.4% [-60.3%, +67.1%]	UNKNOWN
benchmarks/lfds/ms.c	55.473 ± 3.798 s	50.597 ± 4.918 s	➖ +8.9% [-10.6%, +28.4%]	UNKNOWN
benchmarks/lfds/treiber.c	35.354 ± 5.451 s	35.465 ± 3.969 s	➖ -0.8% [-27.9%, +26.3%]	UNKNOWN

Total

Benchmarks	Base branch	PR branch	Improvement (99% CI)
All reported benchmarks	633.761 ± 13.350 s	615.909 ± 10.183 s	➖ +2.8% [-10.0%, +15.6%]

[hernanponcedeleon]

What does the "extension" in ProgramExtension refers to? the format (*.litmus, *.c, ...) or something "extra" that we attach to the program.

I like the idea of having a way to attached extra stuff to a program. In this view, the extension would be similar to the metadata but we would allow it to affect semantics.

However, I see two problems with the current proposal (assuming the "view" of above):

• the filter and the specification are more related to the verification goal than to the program per se (i.e., they do not affect the semantics of the program).
• I would use more fine grained extensions (e.g., one per each item below; at least those that we want to implement this way).

I see all the following could be extensions in the view above (I am not saying we might really want to implemented them all as this)

1. locations
2. aliases as used in PTX/Vulkan
3. which thread synchronize via kernel launch (model via ssw annotation in Vulkan)
4. the thread grid
5. the forward progress guarantees
6. the entry point

2-5 kind of represent the environment where the program executes.

5,6 is probable something we would still want to control from options rather than "mark it" in the source code as we do the others.

[ThomasHaas]

What does the "extension" in ProgramExtension refers to? the format (*.litmus, *.c, ...) or something "extra" that we attach to the program.

The latter: "something extra".

I like the idea of having a way to attached extra stuff to a program. In this view, the extension would be similar to the metadata but we would allow it to affect semantics.

Yes, that was the idea.

However, I see two problems with the current proposal (assuming the "view" of above):

the filter and the specification are more related to the verification goal than to the program per se (i.e., they do not affect the semantics of the program).

I thought about this too. The issue is that all this verification goal information is inside the program's syntax and as such, the ProgramParser has to extract that information somehow. Note that this information is there even if it is irrelevant for our verification goal.
I was also contemplating about restricting this feature only to spec information and call it ProgramSpec instead.
Either way, the first (and maybe only?) goal was to somehow capture the additional information/spec in the source language that goes beyond the program itself.

I would use more fine grained extensions (e.g., one per each item below; at least those that we want to implement this way).
I see all the following could be extensions in the view above (I am not saying we might really want to implemented them all as this)

1. locations

2. aliases as used in PTX/Vulkan

3. which thread synchronize via kernel launch (model via `ssw` annotation in Vulkan)

4. the thread grid

5. the forward progress guarantees

6. the entry point

I think if we can add features that make sense directly on our internal language, we probably do not need a generic extension mechanism.
For example, forward progress guarantees make sense on every program and "not having this extension" is equivalent to simply having fair progress. A similar point holds for entry points I think.
Even the thread grid makes sense generically, something I tried to capture a while ago in #882. Regular CPU programs can also be understood as arranged in a thread grid/hierarchy but that hierarchy has only a single thread layer below the root node.

The biggest outlier among those points is really the locations bit since it tells nothing about the program itself and only the spec, and only when doing enumeration. So I think there are two natural ways to go about it:

1. Change ProgramExtension to a generic ProgramSpec (in principle the specs do not need to relate to the source language). It has the ugly point to it that the spec may not actually be checked for, i.e., it can be ignored.
2. Rename ProgramExtension to something (I don't know what to call it yet) that represents extra data extracted from parsing the source program like embedded specs without conveying the idea that it is more than that. It has the benefit that the parser can just dump all filter/spec clauses/locations/whatever into this and it is not necessarily weird that parts of the information are ignored in Dartagnan (depending on the verification goal). This is basically what I implemented right now.

[hernanponcedeleon]

My main issue with the current proposal is its lack of modularity. I think the PR should introduce a mechanism through which a program can carry multiple independent attachments.

The common interface could be called SourceProgramAttachment, ProgramAttachment, or ParsedAttachment; all of these seem clearer than ProgramExtension to me.

Initially, we would add two implementations:

• ProgramSpecification, containing SpecificationType specType and Expression spec.
• ExecutionFilter, containing Expression filter.

Both attachments would be produced when parsing Litmus and SPIR-V programs.

Then, as part of #1086, we could add:

• ProgramLocations, containing the locations that should be considered during state enumeration.

We can then separately discuss whether any of the other information mentioned above (aliases, grid, etc) should also use this mechanism.

[ThomasHaas]

My main issue with the current proposal is its lack of modularity. I think the PR should introduce a mechanism through which a program can carry multiple independent attachments.

If you fully modularize it like this, I think it will boil down to exactly what we have right now: a single (optional) member per extension (e.g., spec and filter). The only difference is that we would wrap all the members in wrapper classes and maybe use a map to store all attachments.

ProgramLocations, containing the locations that should be considered during state enumeration.

Then I would just add a List<Expression> locations directly to Program and avoid the wrapper classes / extension mechanism. In that sense, we can close the PR and just use the easiest solution.

[ThomasHaas]

I will close this for now