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

Cache parsing #4085

Merged
merged 96 commits into from
May 31, 2023
Merged

Conversation

keyboardDrummer
Copy link
Member

@keyboardDrummer keyboardDrummer commented May 26, 2023

Changes

  • Let the Dafny language server use a cache for parsing. The cache stores items as long as they were used in the previous compilation. This means that commenting out an include can cause a large piece of cache to be pruned, leading to a possibly unexpected slowdown when it's uncommented again.
  • Fix the cloner so it clones the RangeToken property of Expression objects. This is required for parse caching since we need to clone the AST before further processing since it is mutable.
  • Many fixes to the cloner code
  • Add telemetry that records how long parsing a particular compilation took
  • Add test for included file has error message for indirect includes, something that was still missing from Pure parse function #4083

Caveats

I've decided not to add an option to turn off caching, since I don't see the use-case. Of course caching is a computation vs storage trade-off, and we could provide many options to configure the caching behavior, but I think the current caching is cheap enough (at most storing two sets of parse results at a time) that there is no reason to want to turn it off.

Please carefully review the code that determines the cache key, since a bug in that would lead to outdated compilation results.

Testing

  • Add a test that checks if parsing is cached, and that the cache prunes entries when they're not hit.
  • Add a test that checks that for larger files, the start and end of the file is taken into account for computing the caching hash, so presumably the rest of the file as well. Also check that the Uri changes the hash.
  • There are many existing tests that make changes to a file which will trigger the new hashing code.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

Copy link
Contributor

@alex-chew alex-chew left a comment

Choose a reason for hiding this comment

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

I've reviewed the first 30 files (as they appear in the diff view) - that's up to and including Source/DafnyLanguageServer/Caching/TextReaderFromCharArrays.cs. I'll continue reviewing the rest.

Source/DafnyCore/AST/Grammar/ProgramParser.cs Show resolved Hide resolved
Source/DafnyLanguageServer/Caching/ByteArrayEquality.cs Outdated Show resolved Hide resolved
Comment on lines 44 to 53
var array = arrays[arrayIndex];
if (elementIndex == array.Length) {
return -1;
}
var result = array[elementIndex++];
if (array.Length == elementIndex) {
arrayIndex++;
elementIndex = 0;
}
return result;
Copy link
Contributor

Choose a reason for hiding this comment

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

I think this Read implementation won't work as expected if there's an empty char[] anywhere in arrays (except perhaps at the end). Is that intentional, and if so can we document that?

Source/DafnyLanguageServer/Caching/ByteArrayEquality.cs Outdated Show resolved Hide resolved
Source/DafnyLanguageServer/Caching/ByteArrayEquality.cs Outdated Show resolved Hide resolved
Copy link
Contributor

@alex-chew alex-chew left a comment

Choose a reason for hiding this comment

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

Another batch of comments. Just TickingCache and CachingParser left to review.

Source/DafnyPipeline.Test/TranslatorTest.cs Outdated Show resolved Hide resolved
docs/dev/news/4083.feat Outdated Show resolved Hide resolved
docs/dev/news/4085.feat Outdated Show resolved Hide resolved
keyboardDrummer and others added 5 commits May 31, 2023 23:00
Co-authored-by: Alex Chew <alex-chew@users.noreply.github.com>
Co-authored-by: Alex Chew <alex-chew@users.noreply.github.com>
@alex-chew
Copy link
Contributor

Most of the changes LGTM. The remaining blocking issues are:

  • adding a bounds check in TextReaderFromCharArrays.Peek
  • checking that empty char[]s are handled correctly in TextReaderFromCharArrays.Read (it looks to me like they shouldn't, but the added unit test will tell)
  • preventing trivial collisions in the cache key hashing function

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants