Summary
- Reason for writing: The resources (CPU cycles, memory, storage, network access) available to a Rholang contract must be limited to those purchased by the message sender who triggers the contract. Since Rholang is Turing complete, a resource bound cannot be statically determined. Thus, we require means to bound resource consumption at runtime.
- Problem: In the following, the necessary definitions are given and implementation options explored. Essentially, I make the argument that a fair bound for Rholang requires a well-defined notion of state, of operations that transform the state, and a means to quantify resource consumption in a concurrent setting.
- Conclusion: A resource bound enforced at the Rosette VM level is trivial and granular w.r.t Rosette. A bound enforced at the Rholang source level is infeasible and imprecise. A resource bound for the Rholang interpreter is feasible and granular.
- Implications:
1. Considering the triviality of implementation, a bound at the Rosette VM level should be implemented and is in progress.
2. A bound for the Rholang Interpreter is not only feasible but superior to one for Rosette. Implementation is in progress.
...
We need a resource bound to ensure that the program doesn't exceed a certain complexity.
To do this, define a potential function Φ : Σ → Q+ that maps each program state to some non-negative rational number. Φ represents the resources available for consumption in a given state. If it can be shown that P → Ω(α) P' ∧ Φ(P) ≥ Ω(α) ⇒ Φ(P') = Φ(P) - Ω(α) is true for all program states, then Φ(P) is a valid resource bound. Clearly, the validity of Φ depends on the definition of T.
Implementing a resource bound for sequential programs is trivial. It basically amounts to maintaining a counter to represent consumable resources. The initial value of the counter equals the initial resources allocated to the program. With every operation, the counter is decremented by the cost of the operation.
For concurrent programs, matters are more complicated. For rholang in particular, two processes can transition independently (represented P | Q →α P' | Q). This implies the existence of multiple resource pools, one for P and one for Q. If P transitions independently of Q, then Φ(P) must be checked independently of Φ(Q), else the transitions are linearized around a single resource pool.
In addition, resource allocation must be fair. For example, the transition P | Q →α Nil | Q describes a program state P that transitions to a final state Nil. If the resources belonging to Nil are greater than zero, Φ(Nil) ≥ 0, and the resources of Q are less than the cost of a transition, Φ(Q) < Ω(α) for some transition Q →α Q', then Φ(Nil) should be relinquished to Q to enable the transition.
Basically, we have to answer three principle questions:
...