-
-
Notifications
You must be signed in to change notification settings - Fork 187
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
WIP: Purge UniqueString #716
base: master
Are you sure you want to change the base?
WIP: Purge UniqueString #716
Conversation
Thanks, let's find out if this makes TLC faster: |
Performance test failed with:
https://github.com/tlaplus/tlaplus/runs/5239664920?check_suite_focus=true |
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. |
For a version of the CMs without This alone will probably not fix the issue though since the |
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 |
…backward compatibility
…m and its implementations
…changed perf.yml to not download them. changed measurement script
Amongst other things, I added the workflow hack and CM jar. However, when I ran |
Macro-benchmark now running at https://github.com/tlaplus/tlaplus/runs/5291716413 |
Btw. feel free to share constructive criticism, but please don't call other people's work "sick". |
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. |
Results from the performance benchmark:
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) |
I assume the column |
Yes, negative is bad. Re `PaxosMadeSimple: 69c931f |
bd71c07
to
0a543cc
Compare
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 ofUniqueString
withString
and all instances of==
involvingUniqueString
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 ofUniqueString
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