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

Monadic system for compute & memory cost metering #45

Open
cwgoes opened this issue Aug 10, 2019 · 7 comments
Open

Monadic system for compute & memory cost metering #45

cwgoes opened this issue Aug 10, 2019 · 7 comments

Comments

@cwgoes
Copy link
Collaborator

@cwgoes cwgoes commented Aug 10, 2019

It seems like we should be able to use some sort of built-in monadic type, which is erased at runtime, to assign evaluation costs to terms, and then to functions (as functions of the evaluation costs & values of their arguments), which then will allow us to typecheck (once) the "gas calculation function" for a smart contract call as a function of the values of the arguments to that call, and then charge the user that amount of gas prior to executing the call - thus we won't need to track gas during evaluation.

In certain cases (e.g. where the result of a function call determines the cost of another function call, and we don't perform the first calculation until runtime) bounds or a bit of extra prior computation will be necessary.

We should be able to encode cost reductions for parallelisation into the cost functions for particular functions, e.g. map_reduce.

I believe ZF* may do something like this, so we might find inspiration there.

@cwgoes

This comment has been minimized.

Copy link
Collaborator Author

@cwgoes cwgoes commented Aug 16, 2019

References w.r.t. Zen Protocol's system: one, two, three.

@cwgoes cwgoes changed the title Dependent effects system for gas pricing Dependent effect / monadic system for gas pricing Sep 7, 2019
@cwgoes

This comment has been minimized.

Copy link
Collaborator Author

@cwgoes cwgoes commented Sep 7, 2019

I think we can utilize the basic monadic system in Danielsson's paper, adding in costs to particular rewrite rules in the evaluation semantics and ensuring that the reduction of an encapsulated term (the cost monad being erased) is bounded by the associated cost.

Some outstanding questions:

  • Base primitives & functions will need to have non-unit costs
  • How does optimal sharing change the necessary accounting (maybe not much, it already assumes call-by-need, but we need to think about what happens when thunks are copied)
  • Can we add in discounts for parallelism (this would need to be understood by the compiler)?
  • Can we automate or infer costs? The programmer overhead seems high.
  • This doesn't really account for memory usage, which we may need to consider as well.
@cwgoes cwgoes changed the title Dependent effect / monadic system for gas pricing monadic system for gas pricing Sep 8, 2019
@cwgoes cwgoes changed the title monadic system for gas pricing Monadic system for gas pricing Sep 8, 2019
@cwgoes

This comment has been minimized.

Copy link
Collaborator Author

@cwgoes cwgoes commented Sep 8, 2019

Additional thoughts after reading McCarthy 2016:

  1. Propositional approach is neater, though we could also return 0-usage naturals in QTT.
  2. It would be preferable to tie the monadic cost calculations directly to the cost semantics of the evaluator (ref #17) - in particular, we need to capture memory allocations, possibly bound the total graph size, and differentiate between sequential & parallel rewrite steps in some suitable fashion.
  3. Allocations may not be unit cost
    1. For primitive data types, cost will depend on the size of the data type
  4. Rewrite steps will not be unit cost
    1. Some may have primitive costs (built-in functions), bespoke-encoded rule costs must be calculated according to the term encoded into the bespoke rule
  5. Costs assigned to computation & memory allocation must be sufficiently accurate, as a lower bound, to serve as a cost model for a contract on a public blockchain.
  6. Cost inference would be nice in the future (the Coq library could perform some transforms, but I think it would be preferable to have explicit costs - just infer them where possible)
  7. How best to deal with runtime fusion (e.g. not . not . not . not)? Not sure yet.
@cwgoes cwgoes changed the title Monadic system for gas pricing Monadic system for compute & memory cost metering Sep 8, 2019
@cwgoes

This comment has been minimized.

Copy link
Collaborator Author

@cwgoes cwgoes commented Sep 10, 2019

Example of the runtime fusion case:

true = \t . \f . t

false = \t . \f . f

not = \b . \t . \f . b f t

not . not = \b . \t . \f . (\b' . \t . \f . b' f t) b f t
-> \b . \t . \f . b t f

not . not . not . not fuses like this twice in parallel, then once.

log n in the general case.

whereas not itself, naively applied n times, would be linear complexity.

Another example: fast exponentiation by squaring.

@cwgoes

This comment has been minimized.

Copy link
Collaborator Author

@cwgoes cwgoes commented Sep 10, 2019

Conclusions (tentative):

  • Elaborator-based approach a la ZF*, with eventual editor support or the like for ergonomics.
  • Parameterised costs for flexible machine targeting and easier upgrades.
  • Think more about how to deal with runtime fusion, as it results from semantics, not syntax.
  • Think more about explicit parallelism and how that will interact with the cost model.
  • Think more about how QTT will interact with the cost model or could render inference easier.
@cwgoes

This comment has been minimized.

Copy link
Collaborator Author

@cwgoes cwgoes commented Sep 11, 2019

A unique concern for optimal reduction via the abstract algorithm is the cost of sharing overhead.

This paper bounds it quadratically to the cost of proof-net reduction, but I think we will want a tighter bound - unlike Asperti & Guerrini, we are not interested in complexity relative to the size (or depth) of the term, but rather merely require a method for annotating terms with their complexity - so we need to reason about the costs of sharing overhead as a function of a particular lambda term.

@cwgoes

This comment has been minimized.

Copy link
Collaborator Author

@cwgoes cwgoes commented Nov 19, 2019

Notes from discussion:

rv1

rv2

rv3

rv4

Also:

  • We can have a zero-usage unsafeCoerce :: Cost a -> a which can be used in proofs
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
1 participant
You can’t perform that action at this time.