Termination Model
- Former user (Deleted)
The RChain termination model serves to reconcile the following facts:
- Rholang programs may reduce infinitely.
- An agent may deploy an infinitely reducing program for free.
TL;DR - jump to "Termination Semantics" if you're already familiar with notion of "phlogiston" (phlo).
Termination Proofs
If replication were eliminated, infinitely reducing programs would cease to be a problem because Rholang would cease to be Turing-complete. That, however, would eliminate a large class of generally useful programs from ever being deployed to the blockchain. Instead, we desire a method for transforming infinitely reducing Rholang programs into finitely reducing Rholang programs, i.e., a method for constructing termination proofs.
In general, a termination proof can be constructed from the following definitions (Turing, 1949):
(Termination argument search) a function Φ : Σ → W that maps program states Σ to elements of a well-founded set.
(Validity check) a transition invariant P ➝ P’∧ Φ(P) ≥ min W ⇒ Φ(P) > Φ(P’) to verify that Φ decreases for all P, P' ∈ Σ.
If the validity check holds for a given program, then evaluating the program verifies a termination proof. Moreover, if we have a well-defined operation domain ➝ ∈ Ω, we can tune Φ to capture the complexity of each operation by defining a third function
(Cost model) a function M : Ω ➝ W that maps operations to elements of a well-founded set.
and amending the validity check to become P ➝ P’ ∧ Φ(P) ≥ min W ⇒ Φ(P) > Φ(P) - M(➝) = Φ(P’). This adds the additional constraint that performing an operation decreases the value of Φ by the operation's complexity - effectively making Φ a complexity bound.
Termination Semantics
Rholang's operational semantics is extended with the following "phlo-based" operational rules.
(P | Q, ph)
------------------- (P, ph) | (Q, ph) (P, ph) => (P', ph') ph' ≥ 0-----------------------------------------
(P, ph) | (Q, ph) => (P', ph') | (Q, ph') (P, ph) => (P', ph') ph' < 0-----------------------------------------
(P, ph) | (Q, ph) => Nil
The first rule requires that phlo is shared between the sub-terms of a process; this prevents linearization of execution around a single phlo balance. The second requires that concurrent phlo modifications be witnessed by all processes that share phlo; this is a necessary condition for the third rule which requires that all sub-terms of a process halt if any one of the sub-terms tries to yield a negative phlo balance.
Out of Phlogiston Error (OOPE)
Suppose Alice wants to deploy a program that evaluates two arithmetic expressions in parallel. She deploys the program with two units of phlo.
(1+1 | 1+1, ph = 2) => (1+1, ph = 2) | (1+1, ph = 2) => (2, ph = 1) | (1+1, ph = 1) => (2, ph = 0) | (2, ph = 0)
Assuming that each addition operation costs one unit of phlo, and seeing that there are two addition operations, the final phlo balance for this deployment should be zero.
What would happen if Alice's program included another arithmetic process, but was allocated the same amount of phlo?
(1+1 | 1+1 | 1+1, ph = 2) => (1+1, ph = 2) | (1+1, ph = 2) | (1+1, ph = 2) => (2, ph = 1) | (1+1, ph = 1) | (1+1, ph = 1) => (2, ph = 0) | (2, ph = 0) | (1+1, ph = 0) => Nil //OutOfPhloError
This time, the initial phlo balance is replicated over three processes. Evaluating the third arithmetic process would produce a negative ph balance, so Alice's program throws an OutOfPhloError. It's easy to verify that any evaluation order would throw the same error.
Sending and Receiving
To get a better idea of how phlo behaves with programs that send and receive messages, we'll need a small language to describe the tuplespace.
C := [S1, ..., SN]
S := (!@Q, ph) // Ephemeral Write
(!!@Q, ph) // Persistent Write
(?z.P, ph) // Ephemeral Read
(??z.P, ph) // Persistent Read
T := { x1 -> C1, ..., xN -> CN }
where C represents the contents of a channel, i.e. a list of readers/writers, and T (for tuplespace) is a mapping from channels to their contents.
In a "deployer pays" model, one indicates their intent to pay for a process by deploying that process. If both sub-terms of a redex (reducible expression) are deployed separately, each deployer pays only for their portion of the reduction. Conversly, if both sub-terms are deployed together, the deployer pays for the entire reduction.
(x!Q, phA) | (for( z <- x ){ P }, phB) T := { x -> [] }
=> (x!Q, phA) T := { x -> [(?z.P, phB')] }
=> (P{@Q/z}, phB') T := { x -> [] }
In the above, notice first that both sub-terms of the redex were deployed separately. Second, notice that the agent who deployed the receive is responsible not only for paying for "reading" from x, but also for the continuation, P. This remains true even for persistent processes.
Let's examine a reduction where the read is persistent.
(x!Q, phA) | (for( z <= x ){ P }, phB) T := { x -> [] }
=> (x!Q, phA) T := { x -> [(??z.P, phB')] }
=> (P{@Q/z}, phB'') T := { x -> [(??z.P, phB'')] }
phB is decremented when the persistent receive is first evaluated. Evaluating the send decrements phA, removes the receive from the tuplespace, and evaluates the receive's continuation. Since the receive is persistent, it must be evaluated again to be placed back in the store, bringing phB' to phB''.
Conversely, examine a reduction where the send is persistent:
(x!!Q, phA) | (for( z <- x ){ P }, phB)
=> (for( z <- x ){ P }, phB) T := { x -> [(!!@Q, phA')] }
=> (P{@Q/z}, phB') T := { x -> [(!!@Q, phA'')
Just as with the persistent receive, the agent who deployed the persistent send is responsible for all computational costs incurred by deploying it.
When a persistent receive and a persistent send meet, the terms are evaluated until their respective phlo balances are depleted.
(x!!Q, phA) | (for( z <= x ){ P }, phB) T := { x -> [] }
=> (x!!Q, phA) T := { x -> [(??z.P, phB')] }
=> (x!!Q, phA') | (P{@Q/z}, phB'') T := { x -> [(??z.P, phB'')] }
Contracts
The only semantic difference between a persistent receive and a contract definition is in who pays for the continuation. Contract definition syntax indicates that the contract invoker will pay for the continuation, while receive syntax indicates that the deployer will pay for the continuation. In the following, the contract call X(Q) links the invoker's phlo supply to P.
contract X(z) = { P } | X(Q)
This allows users to define public contracts that use an Ethereum-style payment paradigm. Contract definitions must be supplied enough phlo to cover the cost of being added to the tuplespace (effectively the cost of a receive).
= (contract @"Foo"(z) = { P }, phA) | (@"Foo"(Q), phB) T := { @"Foo" -> [] }
=> (@"Foo"(Q), phB) T := { @"Foo" -> [(??z.P,_)] }
=> (P{@Q/z}, phB') T := { @"Foo" -> [(??z.P,_)] }
Since the contract definition and invocation have different phlo balances, we can infer that they were deployed separately. The phlo associated with the invocation, phB, is decreased by the cost of the invocation (effectively the cost of a send) and the remainder, phB'is passed to the continuation, P.