WIP: Purge UniqueString

[zwergziege]

Took a comment (#685 (comment)) to heart and tried to get rid of UniqueString. If this is a refactoring that is too risky / too much work to be considered, just close the PR. If not, there are still some issues for which I could use some help / input.

I tried to carve out UniqueString step by step. In essence, I replaced all occurrences of UniqueString with String and all instances of == involving UniqueString with .equals (without null checks though). For the order of state variables, I created a static map. Ideally, this will be removed completely at some point in the future. The checkpoint code of UniqueString was removed without replacement since the order of the SVs is inferred while parsing the spec.

Edit: Checkpoint creation definitely needs another look. Distributed TLC probably as well.

Note: While I already found some bugs in the refactoring, I did not take the time to create a new history with patched commits instead of erroneous ones. For this sake, I use square brackets to denote checking out a commit and applying patches.

Intermediate bugs / patches

Description: ModelValue.fingerprint has an infinite loop
Introduced by: Changed ModelValue to use String internally c47f8d5
Fix: fixed infinite recursion in ModelValue 075a8b6

Description: Context.walkGraph casts a key of this.table to UniqueString. Keys have been changed to be String | ModuleName
Introduced by: make sany context use String internally and deprecate functions that use US 0ffc03a
Is resolved in: Removed deprecated functions and purged UniqueString from a few files c3bbb3e

Description: Location.name can be null which leads to problems on inclusion and equality checking
Introduced by: Purged from Location 67dda5e
Fix: Assure Location.name != null f7bf369

Description: Mixed up calls in OperatorStack.reducePostfix()
Introduced by: SyntaxTreeNode Filename 58fdb46
Fix: fixed wrong filename of SyntaxTreeNode 9c06db1 [1] for short

Failing Tests

I used the normal test suite for reference, but my master was also a bit outdated and thus the list of failing tests is probably incomplete.

The following failures are caused by: Let StringValue use String internally 4569d27 [2]
and can be further tracked to not every StringValue.val getting UniqueStringed and the different results on compare (convert to UniqueString in ctor, compareTo and equals (?) for a "fix", [2+fix])
tlc2.tool.liveness.CodePlexBug08EWD840FL1Test
tlc2.tool.liveness.CodePlexBug08EWD840FL2Tests
tlc2.tool.liveness.CodePlexBug08EWD840FL3Test
tlc2.tool.liveness.CodePlexBug08EWD840FL4Test
tlc2.tool.liveness.OneBitMutexNoSymmetryTest

the same holds for those, but I'm pretty positive that they are not indeed errors and can be fixed simply by changing the order of elements in the expected output (i.e. the order in which states are explored / values are printed has changed):
tlc2.tool.EvalExceptionTest
tlc2.tool.PrintTraceRaceTest
tlc2.tool.PrintTraceRaceTest_TTraceTest
tlc2.tool.liveness.CodePlexBug08AgentRingTest
tlc2.debug.EWD840DebuggerTest
tlc2.debug.EWD998TraceDebuggerTest

I'm guessing similar things happen for
pcal.SBBTest
but I'm not 100% sure because the number of generated states varies, which seems like a bug...

tlc2.tool.liveness.CodePlexBug08EWD840FL2FromCheckpointTest probably fails due to broken a broken checkpoint (which could be fixed) and then exhibits the same behavior as the tests above (i.e. works on [2+fix])

tlc2.debug.EWD840DebuggerSimTest
is first caused by SyntaxTreeNode Filename 58fdb46 which has been fixed but still shows problems similar to the tests above (i.e. works on [2+fix+1])

tlc2.debug.EWD998ChanDebuggerTest same as above but reordering is also a problem for records. those have been changed before Let StringValue use String internally 4569d27

For the following tests, I have not had the time to look for the root causes.

tlc2.tool.TLCExtTraceSimTest

pcal.SBBTest_TTraceTest
tlc2.tool.liveness.CodePlexBug08AgentRingTest_TTraceTest
tlc2.tool.liveness.CodePlexBug08EWD840FL1Test_TTraceTest
tlc2.tool.liveness.CodePlexBug08EWD840FL2Test_TTraceTest
tlc2.tool.liveness.CodePlexBug08EWD840FL3Test_TTraceTest
tlc2.tool.liveness.CodePlexBug08EWD840FL4Test_TTraceTest
tlc2.tool.liveness.OneBitMutexNoSymmetryTest_TTraceTest

[lemmy]

Thanks, let's find out if this makes TLC faster:
https://github.com/tlaplus/tlaplus/actions/runs/1861316670

[lemmy]

Performance test failed with:

Semantic processing of module Integers
Semantic processing of module IOUtils
Semantic processing of module measure
Starting... (2022-02-18 00:[33](https://github.com/tlaplus/tlaplus/runs/5239664920?check_suite_focus=true#step:7:33):25)
Error: TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.NoClassDefFoundError
: util/UniqueString
Finished in 00s at (2022-02-18 00:33:25)

https://github.com/tlaplus/tlaplus/runs/5239664920?check_suite_focus=true

[zwergziege]

I will have to take a closer look at this, but I suspect this to be due to references to UniqueString in the community modules.

[zwergziege]

For a version of the CMs without UniqueString see tlaplus/CommunityModules#69
Before you build this version of the CMs you have to create the tla2tools.jar from this repo and copy them to the tlc folder in the CM repo.
Testing this using CI will of course require some workflow changes.

This alone will probably not fix the issue though since the IValueStream code of strings changed which might break the IOUtils. I did this because I thought those methods were only used for checkpoints. I should probably maintain backward compatibility then. What do you think?

[lemmy]

I like that the CommunityModules look much cleaner and clearer without UniqueString; this makes implementing module overrides easier. That alone, however, doesn't justify this major refactoring. Thus, let's check the performance benefit or penalty of this change. For the moment, I suggest adding CommunityModules.jar and tla2tools.jar to this PR and hacking .github/workflows/perf.yml in this PR accordingly. Alternatively, we could add two optional inputs to perf.yml that override the location where perf.yml gets tla2tools.jar and CommunityModules-deps.jar.

[zwergziege]

Amongst other things, I added the workflow hack and CM jar. However, when I ran measure.tla the TLC instances created from within that spec (that's sick btw) all returned errors, but I also got them with the jars generated from master, so I don't know if that's an issue... Also, I have never worked with github workflows, so maybe I'm missing something.
I played around with the measurement script a little bit and found that the purged version tends to be slower. Sometimes by quite a heavy margin (~3 or smth). Thus, I'm not too confident that this is actually worth it. Maybe I can check where performance is lost with flame graphs or smth in the future. I assume it has smth to do with context lookups but am not entirely sure. Apparently, fast inequality is not enough.
Concerning the remaining errors in the standard tests: Are the liveness counterexamples guaranteed to be of minimal length? If not maybe there are only reorder issues left.

[lemmy]

Macro-benchmark now running at https://github.com/tlaplus/tlaplus/runs/5291716413

[lemmy]

Btw. feel free to share constructive criticism, but please don't call other people's work "sick".

[zwergziege]

Oh.. I'm sorry! I didn't mean to sound derogatory. I just forgot for a sec that the semantics of the word 'sick' are extremely context dependent. I actually love it :D I should have been more clear about that.

[lemmy]

Results from the performance benchmark:

Spec	Workers	increase
EWD840	4	0%
EWD840	8	0%
Grid5k	2	-25%
PaxosCommit	2	-41%
PaxosCommit	4	-43%
Bookkeeper	2	-47%
SwarmKit	2	-54%
SwarmKit	4	-55%
Bookkeeper	4	-58%
MongoRepl	2	-60%
SwarmKit	8	-79%
Grid5k	4	-86%
PaxosCommit	8	-88%
Bloemen	2	-123%
EWD840	2	-136%
MongoRepl	4	-170%
Bookkeeper	8	-259%
Ghostferry	2	-262%
Grid5k	8	-321%
Bloemen	4	-585%
MongoRepl	8	-737%
Bloemen	8	-1 066%
Ghostferry	4	-1 296%
Ghostferry	8	-1 949%

PaxosMadeSimple spec also crashes (with explains why wallclock time of benchmarks went down):

TLC2 Version 2.18 of Day Month 20?? (rev: 7d1c827)
Running breadth-first search Model-Checking with fp 67 and seed 6221033366766164042 with 2 workers on 16 cores with 7086MB heap and 64MB offheap memory [pid: 21069] (Linux 5.4.0-100-generic amd64, Azul Systems, Inc. 11.0.3 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /home/gh-runner/actions-runner/_work/tlaplus/tlaplus/general/performance/PaxosMadeSimple/MC.tla
Parsing file /home/gh-runner/actions-runner/_work/tlaplus/tlaplus/general/performance/PaxosMadeSimple/PaxosMadeSimple.tla
Parsing file /tmp/tlc-523841701504858182/TLC.tla (jar:file:/home/gh-runner/actions-runner/_work/tlaplus/tlaplus/tlatools/org.lamport.tlatools/dist/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /home/gh-runner/actions-runner/_work/tlaplus/tlaplus/general/performance/stats.tla
Parsing file /tmp/tlc-523841701504858182/Integers.tla (jar:file:/home/gh-runner/actions-runner/_work/tlaplus/tlaplus/tlatools/org.lamport.tlatools/dist/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /tmp/tlc-523841701504858182/FiniteSets.tla (jar:file:/home/gh-runner/actions-runner/_work/tlaplus/tlaplus/tlatools/org.lamport.tlatools/dist/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/tlc-523841701504858182/Naturals.tla (jar:file:/home/gh-runner/actions-runner/_work/tlaplus/tlaplus/tlatools/org.lamport.tlatools/dist/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-523841701504858182/Sequences.tla (jar:file:/home/gh-runner/actions-runner/_work/tlaplus/tlaplus/tlatools/org.lamport.tlatools/dist/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-523841701504858182/IOUtils.tla (jar:file:/home/gh-runner/actions-runner/_work/tlaplus/tlaplus/tlatools/org.lamport.tlatools/dist/CommunityModules-deps.jar!/IOUtils.tla)
Parsing file /tmp/tlc-523841701504858182/CSV.tla (jar:file:/home/gh-runner/actions-runner/_work/tlaplus/tlaplus/tlatools/org.lamport.tlatools/dist/CommunityModules-deps.jar!/CSV.tla)
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module PaxosMadeSimple
Semantic processing of module TLC
Semantic processing of module IOUtils
Semantic processing of module CSV
Semantic processing of module stats
Semantic processing of module MC
Starting... (2022-02-23 20:55:09)
Error: The configuration file substitutes constant Quorum with non-constant const_144139943713313000 - specifically: Attempted to apply the operator overridden by the Java method
public static tlc2.value.impl.Value tlc2.module.TLCEval.tlcEval(tlc2.tool.impl.Tool,tla2sany.semantic.ExprOrOpArgNode[],tlc2.util.Context,tlc2.tool.TLCState,tlc2.tool.TLCState,int,tlc2.tool.coverage.CostModel),
but it produced the following error:
class tlc2.tool.impl.WorkerValue cannot be cast to class tlc2.value.impl.Value (tlc2.tool.impl.WorkerValue and tlc2.value.impl.Value are in unnamed module of loader 'app')
Finished in 00s at (2022-02-23 20:55:09)

[zwergziege]

I assume the column increase gives the increase in performance and thus negative numbers are bad?
Correct me if I'm wrong, but I'm under the impression that PaxosMadeSimple also crashes in previous specs.

[lemmy]

Yes, negative is bad.

Re `PaxosMadeSimple: 69c931f