Skip to content
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

Introduce parser memoization to avoid exponentional behavior #1799

Merged
merged 18 commits into from
Nov 11, 2022

Conversation

Kha
Copy link
Member

@Kha Kha commented Nov 3, 2022

Cache invocations of category, leading_parser and syntax := parsers using a mapping from parser name and current context & state to parse result. Abstract parser context and syntax stack to enforce correct use.

@Kha
Copy link
Member Author

Kha commented Nov 3, 2022

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit cf3b001.
There were significant changes against commit d0dc9a2:

  Benchmark          Metric            Change
  =====================================================
- stdlib             compilation new       2%  (49.1 σ)
- stdlib             task-clock            1% (214.0 σ)
- workspaceSymbols   task-clock            4%  (12.3 σ)
- workspaceSymbols   wall-clock            4%  (12.4 σ)

@Kha
Copy link
Member Author

Kha commented Nov 3, 2022

Instruction counts suggest these are random fluctuations. Which seem to have become more frequent recently.

@Kha
Copy link
Member Author

Kha commented Nov 5, 2022

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 2ee1eb9.
There were no significant changes.

@Kha
Copy link
Member Author

Kha commented Nov 5, 2022

Comparison with previous benchmark: http://speedcenter.informatik.kit.edu/velcom/compare/6b556c5e-941a-48e3-8f57-5457ee362ab8/to/30d3b0d6-b0c2-411e-af98-c57c0f36db58 +14% parsing, though variance is high

@Kha
Copy link
Member Author

Kha commented Nov 5, 2022

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 17dd678.
There were significant changes against commit d0dc9a2:

  Benchmark          Metric            Change
  =====================================================
- stdlib             compilation new       2%  (54.4 σ)
- stdlib             task-clock            2% (208.5 σ)
- workspaceSymbols   task-clock            3%  (10.0 σ)

@Kha
Copy link
Member Author

Kha commented Nov 6, 2022

@Kha
Copy link
Member Author

Kha commented Nov 7, 2022

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit a74b707.
There were significant changes against commit d0dc9a2:

  Benchmark   Metric       Change
  ========================================
- liasolver   task-clock       1% (10.8 σ)
- liasolver   wall-clock       1% (11.0 σ)
- stdlib      task-clock       2% (99.1 σ)

@Kha Kha force-pushed the packrat branch 3 times, most recently from 468b341 to 915bd1e Compare November 9, 2022 13:43
@Kha
Copy link
Member Author

Kha commented Nov 9, 2022

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 915bd1e.
There were no significant changes.

@Kha Kha changed the title perf: cache category parses perf: cache category and leading parsers Nov 9, 2022
src/Lean/Parser/Types.lean Outdated Show resolved Hide resolved
@Kha
Copy link
Member Author

Kha commented Nov 10, 2022

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit d0f2fe4.
There were significant changes against commit 2386c40:

  Benchmark   Metric       Change
  =========================================
+ stdlib      task-clock      -2% (-32.2 σ)
+ stdlib      wall-clock      -2% (-68.0 σ)

@Kha Kha marked this pull request as ready for review November 10, 2022 13:30
Comment on lines +369 to +371
As this excludes trailing parsers from being cached, we also reset `lhsPrec`, which is not read but set by leading parsers, to 0
in order to increase cache hits. Finally, `errorMsg` is also reset to `none` as a leading parser should not be called in the first
place if there was an error.
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sounds reasonable? Test suite says "yes". All ParserState fields are accounted for now.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think so. It is great you are documenting it.

@Kha Kha changed the title perf: cache category and leading parsers Introduce parser memoization to avoid exponentional behavior Nov 11, 2022
@Kha Kha added the changelog Automatically adds PR title linking to PR to changelog on merge label Nov 11, 2022
@Kha Kha merged commit 0dea086 into leanprover:master Nov 11, 2022
@Kha Kha deleted the packrat branch November 11, 2022 08:13
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
changelog Automatically adds PR title linking to PR to changelog on merge
Projects
None yet
Development

Successfully merging this pull request may close these issues.

square braces can cause exponential time/memory consumption
3 participants