BLAS dot product kernel #413
Conversation
apps/blas/dot/dot.fil
Outdated
|
|
||
| // needed for typechecking | ||
| assume RA::L == log2(N); | ||
| assume M::II <= reuses; |
There was a problem hiding this comment.
This assumption is a little sketchy. What is the reason this would be safe?
There was a problem hiding this comment.
I agree it is sketchy because it wouldn't always be safe. But otherwise, the compiler throws errors that the invocation of M triggers too often since we want Dot's delay to be reuses
There was a problem hiding this comment.
I think one way to think about assume is that we should only use it if we know an algebraic fact is true but the compiler cannot prove it (log(2*n) = 1 + log(n)). Everything else is out of bounds for usage of assume and this doesn't quite seem like an algebraic property but more a "thing we want to be true but isn't".
There was a problem hiding this comment.
Totally makes sense. What should I do here, then? Because if we abstract over multiplier implementation, we need some way to reason about the multiplier's II in comparison to the entire module's II, and I'm not sure how else to do that
There was a problem hiding this comment.
If you look again, I was able to get rid of this assume; I was using <'G: II> in the signature of Multipliers. Now I changed that just to <G: 1> but kept II as an output parameter (so it can be accessed elsewhere)
apps/blas/dot/dot.fil
Outdated
| { | ||
|
|
||
| M := new Multipliers[W, N]; | ||
| RA := new RAdd[W, N]; |
There was a problem hiding this comment.
Use the instance borrow syntax to specify how long both of these components are reused for.
There was a problem hiding this comment.
Wouldn't the time over which I reuse them depend on the output parameters of the instances? For the multiplier specifically, I would imagine that the interval would look like ['G, 'G + reuses*M::II + M::L], which we can't express.
There was a problem hiding this comment.
Why can't we express that? Can't we write:
M := new Multipliers[W, N] in ['G, 'G + reuses*M::II + M::L];
There was a problem hiding this comment.
This is something that should be supported, right? As in we should be able to figure out what M:II and M::L are just from the instantiation, and then use them in the borrow interval.
|
@gabizon103 don't get blocked on my reviews for merging this. Push ahead and maybe add links to the tracker for things that need my review! |
Implements a dot product kernel that is parameterized over multiplier reuse, from #411