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

Multiple lookups, simpler rec environment #996

Merged
merged 6 commits into from
Jan 8, 2024

Conversation

gabriel-barrett
Copy link
Member

@gabriel-barrett gabriel-barrett commented Dec 21, 2023

This PR simplifies recursive environments. Now, instead of it taking an environment itself, the tag for the symbol is changed to denote a recursive variable. Although we can't get mutual recursion like this, there's a possible fix:

(letrec ((f A) (g B))
  C)

can be transformed into

(letrec ((f (letrec ((g B)) A)))
  (letrec ((g B)) C))

while reducing, which will achieve mutual recursion. This will, however, add some overhead to non-mutually recursive functions. But again, this can be mitigated if we take the memoset approach to letrec.

Now, because of the simplification, it is possible to do 3 lookups per step without adding any slots. This greatly increases performance. (fib 20) goes from 613 iterations to 390, almost half the number of iterations

Copy link
Member

@huitseeker huitseeker left a comment

Choose a reason for hiding this comment

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

The better use of tags is great, I left a question, mostly geared at maintenability.

src/lem/eval.rs Outdated
Comment on lines 839 to 840
// This is a hack to signal that the binding came from a letrec
Expr::Thunk => {
Copy link
Member

Choose a reason for hiding this comment

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

  1. How much more expensive would it be to add a proper case in the environment?
  2. If the answer is "quite a bit", could we document this special meaning in the definition of the Thunk variant in the enum declaration?

I also wouldn't mind removing the mention of "hack" here, and renaming the "Thunk" variant to ThunkOrRecSym (or something more evocative).

Copy link
Member Author

Choose a reason for hiding this comment

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

@huitseeker not expensive at all, I think it would just add 1 constraint and 1 auxiliary. I just didn't do it because I'd have to add a bunch of cases in a bunch of files. I think I will add a new tag "FrozenVar", since it is a frozen computation that the variable refers to. I'll replace the comment as well

huitseeker
huitseeker previously approved these changes Jan 6, 2024
Copy link
Member

@huitseeker huitseeker left a comment

Choose a reason for hiding this comment

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

The specialized RecVar looks great, the cycle counts going down also looks nice. I'd love for @arthurpaulino and / or @porcuquine to have quick look, but this LGTM

@arthurpaulino
Copy link
Member

My review is summarized in this Zulip thread. The first bullet point is solved with the specialized RecVar tag.

On the second bullet point, I'd like us to, at least, plan for a solution for mutual recursion which makes us all content, as the syntactical manipulation mentioned in the PR description doesn't satisfy me completely (at least not yet).

@gabriel-barrett gabriel-barrett added this pull request to the merge queue Jan 7, 2024
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Jan 7, 2024
github-actions bot pushed a commit that referenced this pull request Jan 7, 2024
@gabriel-barrett
Copy link
Member Author

!gpu-benchmark

Copy link
Contributor

github-actions bot commented Jan 8, 2024

Benchmark for 753bf71

Click to view benchmark
Test Base PR %
LEM Fibonacci Prove - rc = 100/fib/num-100 2.4±0.00s 1732.1±1.67ms -27.83%
LEM Fibonacci Prove - rc = 100/fib/num-200 4.6±0.01s 3.3±0.00s -28.26%
LEM Fibonacci Prove - rc = 600/fib/num-100 1983.5±4.36ms 1956.5±5.37ms -1.36%
LEM Fibonacci Prove - rc = 600/fib/num-200 4.5±0.01s 3.3±0.01s -26.67%

@gabriel-barrett gabriel-barrett added this pull request to the merge queue Jan 8, 2024
github-actions bot pushed a commit that referenced this pull request Jan 8, 2024
Merged via the queue into lurk-lab:main with commit 2efe6ec Jan 8, 2024
12 checks passed
@gabriel-barrett gabriel-barrett deleted the better-rec-env branch January 8, 2024 20:45
huitseeker added a commit to huitseeker/lurk-rs that referenced this pull request Jan 8, 2024
This reverts commit 2efe6ec for a suspected perf regression.
@gabriel-barrett gabriel-barrett restored the better-rec-env branch January 9, 2024 13:55
gabriel-barrett added a commit to gabriel-barrett/lurk-rs that referenced this pull request Jan 10, 2024
* two lookups per step

* let/letrec refactor

* recursive enviroments simplified

* fixed eval/proof iterations

* New tag for recursive variables

* fixed lurk-lib and demo tests
gabriel-barrett added a commit to gabriel-barrett/lurk-rs that referenced this pull request Jan 10, 2024
* two lookups per step

* let/letrec refactor

* recursive enviroments simplified

* fixed eval/proof iterations

* New tag for recursive variables

* fixed lurk-lib and demo tests
gabriel-barrett added a commit to gabriel-barrett/lurk-rs that referenced this pull request Jan 11, 2024
* two lookups per step

* let/letrec refactor

* recursive enviroments simplified

* fixed eval/proof iterations

* New tag for recursive variables

* fixed lurk-lib and demo tests
@gabriel-barrett gabriel-barrett deleted the better-rec-env branch February 21, 2024 00:24
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.

None yet

3 participants