Skip to content

feat(Python): Support caching const variables #6134

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

Open
wants to merge 11 commits into
base: master
Choose a base branch
from

Conversation

lucasmcdonald3
Copy link
Contributor

@lucasmcdonald3 lucasmcdonald3 commented Feb 28, 2025

What was changed?

  • Python code generator writes a cache decorator on variables declared as const

This is a proposal / proof of concept, not a ready-to-merge PR.
If the Dafny team likes this approach, I'll add a CLI argument to enable writing cache decorators on const variables.

Problem:

I'm seeing slow performance in Python when accessing complex const variables: example.

Some code that takes ~5-10 minutes in other languages takes ~40 minutes in Python.

I suspect other languages have some cache-like optimization for frequently-called methods, while Python is recomputing the value each time.
Since these variables are const, their values don't need to be recomputed every time they're accessed.

How has this been tested?

I tested code compiled with this change and its performance was now on-par with other languages.

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

Copy link
Collaborator

@fabiomadge fabiomadge left a comment

Choose a reason for hiding this comment

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

We could also generate code that does the caching for every const individually. That might save some runtime overhead, but I'm not sure it really does, thus justifying the cruft in the generated code.

if (!createBody) { return null; }
methodWriter.WriteLine(isStatic ? $"@{DafnyRuntimeModule}.classproperty" : "@property");
// if (isConst and cacheConstVariablesCliFlag)
Copy link
Collaborator

Choose a reason for hiding this comment

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

I think always caching is ok, so let's remove the remains of the flag everywhere.

// Setting this to 1 means that only 1 input/output pair is cached.
// Since const methods only take `self` or `instance` and no other parameters, there is only 1 input/output pair.
// maxsize can be fixed to 1.
methodWriter.WriteLine("@lru_cache(maxsize=1)");
Copy link
Collaborator

Choose a reason for hiding this comment

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

Did you test this with inheritance?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

A child class accessing an inherited cached property results in a cache miss. It overwrites the cached value from the parent class.

@lucasmcdonald3
Copy link
Contributor Author

We could also generate code that does the caching for every const individually.

Do you mean something like creating a global/class-level variable, then storing the cached value there?
That's also good. That would also make the inheritance story better.
I'll leave it up to you / Dafny team to decide which approach to take.

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.

3 participants