Environment optimization #1035
Environment optimization #1035
Conversation
|
|
||
| // Allocate the image tag if it hasn't been allocated before, | ||
| // create the full image pointer and add it to bound allocations | ||
| let img_tag = ctx.global_allocator.alloc_tag_cloned(&mut cs, &Env); |
There was a problem hiding this comment.
Is this 'maybe' allocation deterministic within the circuit, or does it depend on the dynamic data? If the latter, then we risk inconsistent circuits. For this to be okay, the calls to alloc_tag_cloned need to always happen in the same order, with the same arguments. This is a larger question than just this usage.
I assume it's okay, since the design of the global allocator (and these lazy-allocating methods) assumes the above. I'm just mentioning so you can tell me it's fine everywhere. If in any doubt, we should convince ourselves.
There was a problem hiding this comment.
I believe that all constants, including tags, are allocated before, so when you call this, it only amounts to getting the previously allocated constant. This does not depend on dynamic data, so it's fine
|
!gpu-benchmark |
|
!gpu-bench |
gabriel-barrett
force-pushed
the
new-env
branch
from
ad82b4b to
55128a3
Compare
|
!gpu-benchmark |
Benchmark for 73badc6Click to view benchmark
|
There was a problem hiding this comment.
Excellent. I'm obviously in favor of this change in principle. I looked at the code, and everything looks good. I would say that some LEM details are unfamiliar enough (have not stayed entirely up to speed on all internals) that having another set of eyes on the 'code review' rather than 'design review' would be useful.
gabriel-barrett
force-pushed
the
new-env
branch
from
55128a3 to
540d07a
Compare
letrec will now add thunk expressions which adds themselves to the environment before evaluating
This is so that we can delay hashing, much like `Ptr`s delay hashing
Now `letrec` works as before, but updated to the new, changed, environment. The reason for reverting is that the iteration count increased in a bunch of tests. For thunks to work properly, we will need the memoset implementation of eval
gabriel-barrett
force-pushed
the
new-env
branch
from
719ce89 to
55b5baa
Compare
This PR optimizes environments. Now, they're specialized data structures with its own tag
Env. Empty environments are 0 valued environments, and otherwise they are a hash of size 4, the first element being the symbol payload, the second and third elements being the corresponding value's tag and payload, and the fourth element, the tail environment's payload. Doing this means lookups now take a single hash4, which allows us to do 8 lookups per step!In the earlier PR, we simplified recursive envs by tagging symbols with a special tag to signal it came from a letrec. Now, because we don't have tags in symbols, some other strategy is needed. This is why I'm now tagging functions with a special recursive tag. It's important to note that this tag only appears in functions inside environment, as when you fetch them, it becomes a normal function with an extended environment. This is effectively the same behaviour as Lurk, although the internal representation is different
In earlier commits I gave another solution to letrecs which would solve issue #434 and actually give a proper letrec semantics, but the issue is that it would recompute recursive values and you'd end up with more iterations. This can only be solved with memoization, which will give the proper operational semantics to thunks, and can be solved after we've integrated the memoset into Lurk. Until then, we will have to settle on the other solution