Share bodies instead of copying them #9
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This fixes a major problem with the previous version: there exist pathological programs that lead to an exponential amount of copying. This improvement comes with the small cost that non-pathological programs take longer to compile. Sharing is observed by first converting the program into an interaction net, which is then reduced into the output program. The reduction algorithm used is that of the Lambdascope implementation extended with FFI nodes and the necessary rules to reduce them. https://web.archive.org/web/20170706084403/http://www.phil.uu.nl/~oostrom/publication/pdf/lambdascope.pdf For ease of debugging, a generic backend language was also introduced to decouple most of the compiler from LLVM. This may also, in future, allow alternative backends to be developed.
Owner
Author
|
Failing case: I think the cause is a bug in the oracle. Edit: Fixed. |
Previously, sharing would generate as many arguments as there were references. Often, most of them are duplicates.
I can't remember where it came from. Probably an old test case that has since been renamed or removed?
Unlike Lambdascope's strategy, this new strategy I've come up with does not require propagating book-keeping metadata through the interaction net. Consequently, it performs significantly better. Also unlike Lambdascope's strategy, it does not yet have a proof of correctness. :(
Owner
Author
There was a problem hiding this comment.
Counterexample (unsimplified)
foreign export "expOdd" c_expOdd
: (∀ ((∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → 0) → 0)
→ (∀ ((∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → 0) → 0)
→ IO (∀ 0 → 0 → 0)
foreign primitive pureIO : ∀ 0 → IO 0
foreign primitive bindIO : ∀ IO 0 → ∀ (1 → IO 0) → IO 0
zero = Λ λ((∀ 0 → (1 → 0) → 0) → 0) 0 (nothing @0)
succ = λ(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) Λ λ((∀ 0 → (1 → 0) → 0) → 0) 0 (just @0 (1 @0 0))
nothing = Λ Λ λ0 λ(1 → 0) 1
just = Λ λ0 Λ λ0 λ(1 → 0) 0 2
f = Λ λ0 λ0 0
t = Λ λ0 λ0 1
add = λ(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) λ(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0)
1 @(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) (λ(∀ 0 → ((∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) → 0) → 0)
0 @(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) 1 succ)
mul = λ(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) λ(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0)
1 @(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) (λ(∀ 0 → ((∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) → 0) → 0)
0 @(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) zero (add 1))
exp = λ(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) λ(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0)
0 @(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) (λ(∀ 0 → ((∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) → 0) → 0)
0 @(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) (succ zero) (mul 2))
isOdd = λ(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0)
0 @(∀ 0 → 0 → 0) (λ(∀ 0 → ((∀ 0 → 0 → 0) → 0) → 0)
0 @(∀ 0 → 0 → 0) f not)
not = λ(∀ 0 → 0 → 0) Λ λ0 λ0 2 @0 0 1
from8 = λ(∀ ((∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → 0) → 0)
0 @(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0)
(λ(∀ 0 → 0 → 0) λ(∀ 0 → 0 → 0) λ(∀ 0 → 0 → 0) λ(∀ 0 → 0 → 0) λ(∀ 0 → 0 → 0) λ(∀ 0 → 0 → 0) λ(∀ 0 → 0 → 0) λ(∀ 0 → 0 → 0)
add (from1 0) (mul (succ (succ zero)) (add (from1 1) (mul (succ (succ zero)) (
add (from1 2) (mul (succ (succ zero)) (add (from1 3) (mul (succ (succ zero)) (
add (from1 4) (mul (succ (succ zero)) (add (from1 5) (mul (succ (succ zero)) (
add (from1 6) (mul (succ (succ zero)) (from1 7)))))))))))))))
from1 = λ(∀ 0 → 0 → 0) 0 @(∀ ((∀ 0 → (1 → 0) → 0) → 0) → 0) (succ zero) zero
c_expOdd = λ(∀ ((∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → 0) → 0)
λ(∀ ((∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → (∀ 0 → 0 → 0) → 0) → 0)
pureIO @(∀ 0 → 0 → 0) (isOdd (exp (from8 1) (from8 0)))
Edit: Fixed.
This reverts commit 3073a06. The change doesn't always work and gets in the way of improving other aspects.
Switch to a CPS ruleset where branches can be applied directly to the IO continuation. Perform all marshalling in IO, as required by the new rewrite rules. Change the backend representation to use labelled blocks instead of nested blocks. Avoid collisions between user-defined exported functions and compiler-generated private functions used for sharing IO.
Remove the Branch0 node and inline its rules into where it was previously used.
Don't rebox tunnel output or PReduce's output, as there can be no duplication there. Add the second argument to Bind0C and Bind0F, as it is always known when they are produced. Remove the redundant Branch1 node by inlining its reduction into anything that would produce it.
Replace TBuild with TCross when in a tunnel.
Decide the name and pass the operand to the continuation before reducing the instruction.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This fixes a major problem with the previous version: there exist
pathological programs that lead to an exponential amount of copying.
This improvement comes with the small cost that non-pathological
programs take longer to compile.
Sharing is observed by first converting the program into an interaction
net, which is then reduced into the output program.
The reduction algorithm used is that of the Lambdascope implementation
extended with FFI nodes and the necessary rules to reduce them.
https://web.archive.org/web/20170706084403/http://www.phil.uu.nl/~oostrom/publication/pdf/lambdascope.pdf
For ease of debugging, a generic backend language was also introduced to
decouple most of the compiler from LLVM. This may also, in future, allow
alternative backends to be developed.