Metadata refactor & guidelines

[ThomasHaas]

As discussed in #1105, I moved the basic metadata classes to a top-level package.
I made all Event-specific metadata inner classes of Event.
I moved SourceLocation to the top-level package, seeing that is could (and probably should) be reused for programs (#1105).

[ThomasHaas]

We wanted to discuss some guidelines about the usage of metadata. I will bring up some points/questions (not exhaustive) that we should talk about with tentative answers.

(1) Q: Is metadata always optional or can it be mandatory?
A: Preferred optional?
Current state: metadata is generally optional. However, there is a UnrollingBound metadata used to remember unrolling bounds at bound events which is unconditionally used in Dartagnan's loop bound dumping (though it probably could be made optional).
Maybe metadata that we are guaranteed to internally generate can be made mandatory?

(2) Q: Should metadata be able to modify the semantics of, e.g., events?
A: No. Semantic-defining information should always be explicit.

(3) Q: Can the presence of metadata affect the tools outcome?
A: Yes? While metadata should not directly affect the ground semantics (and hence the expected verdict), it could be allowed to affect precision of the tool. For example, type-based alias analysis (TBAA) using source language types can be implemented via Metadata (see #617). Similarly, one could imagine value range metadata attached to, e.g., loads.
If the metadata is sound it can change UNKNOWN to PASS, but if it is unsound, it could change FAIL to PASS.

(4) Q: How complex can metadata be?
A: Simple? Metadata should likely consist of simple types (ints, strings, paths, etc.) and not refer to IR-specific types (events, functions, registers, etc.). Furthermore, metadata classes should be immutable.

(5) Q: Where should metadata classes be located?
A: Depends. Metadata that is widely usable (e.g., source locations) should be in the general metadata package, but metadata that is specific to one type of class (e.g., event-specific metadata) should be an inner class.
The decision may not be clear: #1104 adds CutAnnotation metadata used for both Relation and Constraint which have no common superclass (maybe they should?) for CutAnnotation to live in. Maybe it could be put into the Wmm class?
An alternative would be to put all metadata into the metadata package, possibly within a subpackage for division (metadata.program, metadata.wmm, etc.). There should only be one layer of subpackages (no deep nesting) and the subdivision should be coarse (e.g. metadata.program instead of metadata.event, metadata.memory, etc.).

[github-actions]

Performance comparison

Linux x64

Benchmark details

Memory model: vmm

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/cna.c	12.895 ± 0.547 s	13.195 ± 0.699 s	➖ -2.3% [-14.2%, +9.5%]	UNKNOWN
benchmarks/locks/mutex_musl.c	24.573 ± 1.308 s	28.015 ± 3.358 s	➖ -14.1% [-91.9%, +63.8%]	UNKNOWN
benchmarks/lfds/dglm.c	19.308 ± 1.093 s	18.285 ± 2.116 s	➖ +5.4% [-34.5%, +45.4%]	UNKNOWN
benchmarks/lfds/ms.c	31.979 ± 6.842 s	31.220 ± 4.692 s	➖ -0.9% [-158.3%, +156.6%]	UNKNOWN
benchmarks/lfds/treiber.c	8.314 ± 0.161 s	8.809 ± 0.238 s	➖ -6.0% [-21.4%, +9.4%]	UNKNOWN
benchmarks/lfds/safe_stack.c	6.239 ± 0.184 s	6.749 ± 0.548 s	➖ -8.4% [-74.9%, +58.1%]	UNKNOWN
benchmarks/challenging/cna.c	31.958 ± 1.440 s	32.821 ± 1.851 s	➖ -3.0% [-57.9%, +51.9%]	UNKNOWN

Memory model: aarch64

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/linuxrwlock.c	6.544 ± 0.082 s	6.613 ± 0.055 s	➖ -1.0% [-5.8%, +3.7%]	UNKNOWN
benchmarks/challenging/cna.c	13.636 ± 1.432 s	11.285 ± 1.100 s	➖ +16.0% [-85.1%, +117.1%]	UNKNOWN
benchmarks/challenging/wsq.c	5.753 ± 0.032 s	5.731 ± 0.027 s	➖ +0.4% [-2.2%, +2.9%]	UNKNOWN

Memory model: power

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/linuxrwlock.c	16.791 ± 0.343 s	17.141 ± 0.258 s	➖ -2.1% [-20.9%, +16.6%]	UNKNOWN
benchmarks/locks/mutex_musl.c	17.573 ± 0.281 s	17.145 ± 0.820 s	➖ +2.4% [-21.0%, +25.8%]	UNKNOWN
benchmarks/lfds/dglm.c	5.382 ± 0.294 s	5.320 ± 0.196 s	➖ +1.0% [-26.6%, +28.6%]	UNKNOWN
benchmarks/lfds/ms.c	21.358 ± 3.186 s	20.751 ± 1.573 s	➖ +1.3% [-96.2%, +98.9%]	UNKNOWN
benchmarks/lfds/treiber.c	13.974 ± 0.268 s	13.276 ± 0.074 s	➖ +5.0% [-4.2%, +14.1%]	UNKNOWN

Total

Benchmarks	Base branch	PR branch	Improvement (99% CI)
All reported benchmarks	236.276 ± 8.062 s	236.356 ± 4.109 s	➖ -0.1% [-28.5%, +28.2%]

3 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.774 ± 1.392 s	18.991 ± 1.383 s	➖ -7.0% [-49.3%, +35.2%]	UNKNOWN
benchmarks/locks/mutex_musl.c	29.301 ± 0.207 s	30.013 ± 1.026 s	➖ -2.4% [-25.8%, +20.9%]	UNKNOWN
benchmarks/lfds/dglm.c	45.618 ± 1.574 s	47.580 ± 0.925 s	➖ -4.3% [-17.6%, +8.9%]	UNKNOWN
benchmarks/lfds/ms.c	68.000 ± 7.000 s	62.663 ± 7.101 s	➖ +7.8% [-19.5%, +35.2%]	UNKNOWN
benchmarks/lfds/treiber.c	17.340 ± 1.430 s	17.855 ± 1.005 s	➖ -3.7% [-79.3%, +72.0%]	UNKNOWN
benchmarks/lfds/safe_stack.c	11.112 ± 0.857 s	13.353 ± 0.770 s	➖ -20.9% [-107.5%, +65.7%]	UNKNOWN
benchmarks/challenging/cna.c	48.055 ± 10.703 s	40.609 ± 5.778 s	➖ +14.2% [-35.5%, +64.0%]	UNKNOWN

Memory model: aarch64

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/linuxrwlock.c	14.503 ± 1.325 s	15.296 ± 2.892 s	➖ -5.0% [-80.3%, +70.3%]	UNKNOWN
benchmarks/locks/mutex_musl.c	10.957 ± 0.257 s	10.987 ± 0.348 s	➖ -0.3% [-25.1%, +24.5%]	UNKNOWN
benchmarks/lfds/dglm.c	12.146 ± 0.633 s	12.579 ± 0.327 s	➖ -3.7% [-25.6%, +18.2%]	PASS
benchmarks/lfds/ms.c	13.283 ± 1.341 s	13.342 ± 0.400 s	➖ -0.9% [-41.6%, +39.8%]	UNKNOWN
benchmarks/challenging/cna.c	30.965 ± 1.689 s	35.351 ± 6.389 s	➖ -13.8% [-108.0%, +80.5%]	UNKNOWN
benchmarks/challenging/wsq.c	17.878 ± 3.074 s	18.582 ± 2.319 s	➖ -4.7% [-60.8%, +51.5%]	UNKNOWN

Memory model: power

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/linuxrwlock.c	29.427 ± 0.199 s	31.943 ± 0.363 s	❌ -8.6% [-14.7%, -2.4%]	UNKNOWN
benchmarks/locks/mutex_musl.c	34.036 ± 0.130 s	29.393 ± 0.939 s	➖ +13.6% [-3.6%, +30.9%]	UNKNOWN
benchmarks/lfds/dglm.c	10.649 ± 0.030 s	9.641 ± 0.131 s	✅ +9.5% [+3.7%, +15.2%]	UNKNOWN
benchmarks/lfds/ms.c	49.387 ± 3.217 s	57.388 ± 3.129 s	➖ -16.6% [-82.1%, +48.9%]	UNKNOWN
benchmarks/lfds/treiber.c	21.174 ± 2.312 s	22.219 ± 3.215 s	➖ -5.0% [-65.4%, +55.4%]	UNKNOWN

Total

Benchmarks	Base branch	PR branch	Improvement (99% CI)
All reported benchmarks	481.604 ± 5.665 s	487.785 ± 10.463 s	➖ -1.3% [-7.9%, +5.4%]

[hernanponcedeleon]

I moved SourceLocation to the top-level package, seeing that is could (and probably should) be reused for programs (#1105).

I think SourceLocation is more specific (e.g., it contains a line number) than what we would need for programs. I think We could have Source as general metadata (maybe useful for witnesses too (?)) and maybe change the string in SourceLocation.Generic to Source.

[ThomasHaas]

I think there are different possible ways to go about it. We can try with a basic Source metadata and have SourceLocation enrich Source with Location data.

[hernanponcedeleon]

We wanted to discuss some guidelines about the usage of metadata. I will bring up some points/questions (not exhaustive) that we should talk about with tentative answers.

(1) Q: Is metadata always optional or can it be mandatory? A: Preferred optional? Current state: metadata is generally optional. However, there is a UnrollingBound metadata used to remember unrolling bounds at bound events which is unconditionally used in Dartagnan's loop bound dumping (though it probably could be made optional). Maybe metadata that we are guaranteed to internally generate can be made mandatory?

I think the "if its presence can be guaranteed by us, making it mandatory is ok" is a good trade-off.

(2) Q: Should metadata be able to modify the semantics of, e.g., events? A: No. Semantic-defining information should always be explicit.

Agree.

(3) Q: Can the presence of metadata affect the tools outcome? A: Yes? While metadata should not directly affect the ground semantics (and hence the expected verdict), it could be allowed to affect precision of the tool. For example, type-based alias analysis (TBAA) using source language types can be implemented via Metadata (see #617). Similarly, one could imagine value range metadata attached to, e.g., loads. If the metadata is sound it can change UNKNOWN to PASS, but if it is unsound, it could change FAIL to PASS.

I think the following would fit in this Q. Imagine we would implement support for the locations annotations in litmus needed in #1086 as metadata. On the one side, I can see this would make sense if you think of it as "lets add a zoom filter to no notion of state"; one the other side, it will definitely affect the results of the exploration mode.

(4) Q: How complex can metadata be? A: Simple? Metadata should likely consist of simple types (ints, strings, paths, etc.) and not refer to IR-specific types (events, functions, registers, etc.). Furthermore, metadata classes should be immutable.

I cannot envision any use case where we would require IR-specific things. I would go for "just simple" and we can revise if the day comes.

(5) Q: Where should metadata classes be located? A: Depends. Metadata that is widely usable (e.g., source locations) should be in the general metadata package, but metadata that is specific to one type of class (e.g., event-specific metadata) should be an inner class. The decision may not be clear: #1104 adds CutAnnotation metadata used for both Relation and Constraint which have no common superclass (maybe they should?) for CutAnnotation to live in. Maybe it could be put into the Wmm class? An alternative would be to put all metadata into the metadata package, possibly within a subpackage for division (metadata.program, metadata.wmm, etc.). There should only be one layer of subpackages (no deep nesting) and the subdivision should be coarse (e.g. metadata.program instead of metadata.event, metadata.memory, etc.).

As we already discussed offine, I am in favor of keeping it class-internal as we already did in #1104.

BTW, I think we should add this documentation as part of the Metadata interface (e.g., this would help agents to spot wrong usages of it).

[hernanponcedeleon]

You mean Path.of(source).getFileName().toString() == source if the path does not exists? If so I would explicitly say so to avoid confusion.

EDIT: it seems Path.of("/").getFileName() would return null

[ThomasHaas]

It's not about path existence but rather path shape: not/a/path/to/a/file would still yield file.
Technically, Path.of() can throw an exception if there are invalid symbols in the path though. I can also revert it back to the old which used explicit substring manipulation, but now that I think about it, the old code expected / as separator which may fail under Windows... I guess we should just use a proper Path.

it seems Path.of("/").getFileName() would return null

Interesting, I expected it to return the empty string.

[ThomasHaas]

(3) Q: Can the presence of metadata affect the tools outcome? A: Yes? While metadata should not directly affect the ground semantics (and hence the expected verdict), it could be allowed to affect precision of the tool. For example, type-based alias analysis (TBAA) using source language types can be implemented via Metadata (see #617). Similarly, one could imagine value range metadata attached to, e.g., loads. If the metadata is sound it can change UNKNOWN to PASS, but if it is unsound, it could change FAIL to PASS.

I think the following would fit in this Q. Imagine we would implement support for the locations annotations in litmus needed in #1086 as metadata. On the one side, I can see this would make sense if you think of it as "lets add a zoom filter to no notion of state"; one the other side, it will definitely affect the results of the exploration mode.

(4) Q: How complex can metadata be? A: Simple? Metadata should likely consist of simple types (ints, strings, paths, etc.) and not refer to IR-specific types (events, functions, registers, etc.). Furthermore, metadata classes should be immutable.

I cannot envision any use case where we would require IR-specific things. I would go for "just simple" and we can revise if the day comes.

You just mentioned one in point (3) though. The locations annotations refer to registers and memory locations in the IR and so if it was Metadata, it would refer to IR objects. You can, of course, try to use only names in the metadata and later connect them back to the IR to avoid direct references. But I don't think this circumvents the actual problem, namely, that anything that refers to IR (directly or indirectly) can get easily broken by processing passes.

Given these arguments, I think locations should not be metadata. That doesn't mean we have to make every non-metadata piece a field in Program though. I could imagine to have something like a modular ProgramExtension member which can be LitmusExtension = {Specification, Locations, Filter} for litmus code and None for plain LLVM/SPIRV.

EDIT: If the location metadata would be a LocationAnnotation directly attached to the relevant registers and memory objects, I could imagine it as a sort of metadata (its a bit in the gray zone :)). However, I still would prefer the above sketched solution.

BTW, I think we should add this documentation as part of the Metadata interface (e.g., this would help agents to spot wrong usages of it).

Sure, but first we need to have some consensus :). I didn't want to put my proposed rules into the text before anyone showed agreement :)

[ThomasHaas]

[ERROR] com.dat3m.dartagnan.litmus.comparison.C11AndOpenCLRaceTest.testAssume[0: ../litmus/OPENCL/portedFromC11/manual/imm-E3.3.litmus]
java.lang.AssertionError: expected:<true> but was:<false>

This is a new one. Given how many CI runs we had without this error, debugging this one is going to be nightmare. I think RA and its reasoning over stratifications might be the most likely culprit here.

[hernanponcedeleon]

[ERROR] com.dat3m.dartagnan.litmus.comparison.C11AndOpenCLRaceTest.testAssume[0: ../litmus/OPENCL/portedFromC11/manual/imm-E3.3.litmus]
java.lang.AssertionError: expected:<true> but was:<false>

This is a new one. Given how many CI runs we had without this error, debugging this one is going to be nightmare. I think RA and its reasoning over stratifications might be the most likely culprit here.

I asked an agent to reproduced and it could not. This plus the fact that I never seen that test fail (not only in this PR history, but any any previous run) suggests the chances to hit it again are extremely low.

[ThomasHaas]

I couldn't reproduce it either and it is orthogonal to this PR. However, if you wanna debug it, I don't think you should just run the code until the error occurs but instead check the may/must sets in every run. If the error is due to RA, then maybe there are fluctuations in RA that do not immediately affect the verdict but still show the presence of a bug. Apart from RA, I cannot imagine what else could be wrong.

[hernanponcedeleon]

A few comments about the current state of the metadata following the proposed guidelines:

• CustomPrinting provides a stringify method that refers to our IR (thus violating (1)). Can we move the metadata to AbstractEvent (which makes use of stringify via this) and remove the Event parameter from the method?
• MemoryOrder is used by VisitorC11to decide whether an access is atomic, thus affecting semantics and violating (2).

I also think this pattern is currently allowed and can cause problems

setMetadata(new SourceLocation.Litmus(...));
setMetadata(new SourceLocation.Generic(...));
getMetadata(SourceLocation.class);

We should probably have some guidelines (and maybe even automatic checks that these are followed) about which kind of metadata can be combined.

About the guidelines: should we maybe split the matadata into different "sub-types"? Something like

• provenance: source locations, original names, original IDs. It may affect output but not accepted programs or verification results.
• optimization hints: TBAA, ranges. Absence must use a conservative fallback; consuming the hint must be sound.
• internally generated: unrolling/compilation IDs. The producer and consumer must be documented.

[hernanponcedeleon]

Using Path here may cause problems. This metadata is populated using debug information from LLVM/SPIRV. If the file was generated by Windows, but we are running the code now from Linux, the incompatibility between systems will results in something like "null#line"

[ThomasHaas]

I don't understand. The point of Path is that it is OS-agnostic, no? Why would we have issues there?
Is it because the LLVM visitor constructs the path via directory + "/" + file and so the separator is inconsistent (we should use Path.of(directory, file) though)? Even then, / is a valid separator on Windows I think.

[hernanponcedeleon]

Suppose you are given a *.ll file generated from Windows. The debug information contains C:\projects\demo\test.c.

Dartagnan later parses that LLVM file on Linux:

Path sourcePath = Path.of("C:\\projects\\demo\\test.c");
sourcePath.getFileName();

Because \ is not a path separator on Linux, the result is the entire string C:\projects\demo\test.c instead of test.c.

To be fair, I think we have the same problem on development. Also, since debug information is probably less useful when we are dealing with the compiled code rather than the source, this is not much of a real problem.

[ThomasHaas]

Ok, from Windows to Linux there are problems (the other way around is fine). It does not result in null#line though but rather an overly verbose source location. The same problem does not exist on development because we explicitly use directory + "/" + file which will result in a path like C:\\projects\\demo/test.c with mixed separators. We then do the split on "/" to extract the file name.
I guess we need to add a utility that replaces "\\" by "/" in paths to normalize them.

[ThomasHaas]

Hmm, I think there is a different underlying problem. If the source path was specified as C:\\projects\\demo\\test.c and we verify this on Linux/MacOS, the source path we track should still be the windows path, right? I mean, are we allowed to represent the path differently at all? I wouldn't be so strict about it and allow the path to be tracked as C:/projects/demo/test.c instead, but it certainly is something to consider.

[ThomasHaas]

A few comments about the current state of the metadata following the proposed guidelines:

• CustomPrinting provides a stringify method that refers to our IR (thus violating (1)). Can we move the metadata to AbstractEvent (which makes use of stringify via this) and remove the Event parameter from the method?

The point of (1) was about state referring to IR because passes can invalidate IR breaking the metadata. Methods referring to IR are no problem and CustomPrinting is stateless.

• MemoryOrder is used by VisitorC11to decide whether an access is atomic, thus affecting semantics and violating (2).

Yeah, that sucks a bit. For the most part, the metadata is generated within VisitorC11 (as part of new event creation) and so its existence is guaranteed. But the cases of plain Load/Store events is different: those carry the metadata since the parser created them and there are plenty opportunities for the metadata to be dropped.
The best solution is for VisitorC11 to not use the metadata IMO. tagList probably needs to check for every memory-order-related tag (RLX/REL/ACQ/SC) and attach atomicity tags based on that.
Alternatively, maybe the frontend should be responsible for marking events as atomic/nonatomic (in some sense, the parser's output is "incorrectly tagged" and the compilation pass fixes this in hindsight). After all, the frontend is also responsible for putting the correct memory order tags.

I also think this pattern is currently allowed and can cause problems

setMetadata(new SourceLocation.Litmus(...));
setMetadata(new SourceLocation.Generic(...));
getMetadata(SourceLocation.class);

We should probably have some guidelines (and maybe even automatic checks that these are followed) about which kind of metadata can be combined.

I don't think this is a real issue to be honest. The frontend should be generating that metadata and it should know not to attach multiple types of source information to the same object. Trying to come up with a fix to a problem that will likely never arise is wasted effort IMO.

About the guidelines: should we maybe split the matadata into different "sub-types"? Something like

* provenance: source locations, original names, original IDs. It may affect output but not accepted programs or verification results.

* optimization hints: TBAA, ranges. Absence must use a conservative fallback; consuming the hint must be sound.

* internally generated: unrolling/compilation IDs. The producer and consumer must be documented.

I also thought about a more fine-granular distinction, but I'm not sure what distinctions are practically useful and if they are needed yet. I like the provenance category insofar as it captures the fact that the metadata should be preserved through modifications of the annotated object (in particular copies should keep that metadata).
In that sense, I also think UnrollingId and CompilationId are a kind of provenance (they are also optional btw.).
In contrast, other types of metadata may get invalidated by transformations. Currently, we blindly copy all metadata during processing but it has ugly consequences, for example, CustomPrinting of an ARM8 CAS is preserved during compilation and so the resulting subevents have a wrong printer attached (the printer is smart to realize this and fallback to the default printing).
As for optimization hints, I guess CutAnnotation falls into this category.
CustomPrinting and MemoryOrder do not quite fit anywhere though. Both were intended only for IR printing and should not affect Dartagnan's behaviour in any way (modulo the fact that VisitorC11 abuses MemoryOrder right now). I'm not sure if "internally generated" is a reasonable category and what consequences it has. I think it is rather the case that there is "uncategorized metadata" (no matter where it is generated) which requires more accurate documentation precisely because it lacks a category.

Btw. now that I think about it, maybe we should move UnrollingId and CompilationId into the classes that generate them? They have a unique producer after all. Generally, if metadata has a unique producer or a unique consumer, we should maybe put it into that class. If neither is unique, we place it into the annotated class as we do right now?
By "unique" I don't mean that we currently happen to have exactly one class producing/consuming the metadata but rather that there is no expectation to have any other class in the future that also produce/consume it.

[ThomasHaas]

I think we should avoid making the framework too rigorous: the guidelines are "soft constraints" and not hard rules.

[ThomasHaas]

Btw. we use several tags internally like __NOOPT and __SPINLOOP. I'm wondering if they could (and should?) be replaced by some form of metadata. I think some of those tags can actually influence the semantics. But maybe that just means that those should not be tags in the first place?