For every process P there exists a companion "resource" ph, resource ph which defines a limit on the number of computational actions that P can take. Before P can take an action, it must reduce the value of ph by the cost of the action. When ph reaches 0, P halts.
To side-step issues with consistency and safety, we assign to every P, with resources a resource ph, a behavioral type φB that enforces invariants on the conditions under which ph may be accessed. In particular:
- ph is an exclusively owned resource.; and
- ph is a linear resource.
In addition, every P ∈ [[φB]](v) defines two has two names, get and set, by which it can modify the value of ph. To enforce linearity, we require that get and set are only used in alternation. To enforce exclusivity, we require that ph is viewable only by its "owner" process, P. This constraint is necessary to ensure that, for any given P1 | P2, ph1 is not siphoned off by a greedy P2.
Formulae, our logical interpretation of types, are The formulae generated by the following grammargrammar below introduce a spatial-behavioral logic for processes:
φ, ψ ::= true verity verity
| 0 nullity nullity
| ¬ negation¬ negation
| φ & ψ conjunction
| φ | ψ separation
| *b descent
| a!φ . elevation
| a?b.φ activity
| rec X . φ greatest greatest fix point
| ∀n : ψ . φ quantification quantification
a ::= @φ indication@φ indication
| b ...
b ::= @P nomination nomination
| n ...
Below each of the following formulae is an interpretation of the bounded process type φB. Where no especially interesting interpretation is apparent, the type semantic of the existing interpretation is translated into English. Formulae are assigned semantics by the two mutually recursive functions
...
in addition to the valuation function v : V → ( Proc ), where V is the set of propositional variables used in the rec production. Below, we give an interpretation of the "bounded" behavioral type φB for each formulae generated by the production above. Where there exists no exceptionally interesting interpretation for φB, a description is given of the formula's semantic.
[[ true ]](v) = Proc
A process P satisfies true if ph is accessed according to the linearity and exclusivity constraints defined by the bounded type φB.
[[ 0 ]](v) = { P : P ≡ 0 }
...
A resource P satisfies the negation type P : ¬φB if either linearity or exclusivity are broken during the execution of P.
...
A process P satisfies the conjunction type P : φ & ψ if it satisfies both P : φ and P : ψ.
[[ φ | ψ ]](v) = { P : ∃P0, P1.P ≡ P0 | P1, P0 ∈ [[φ]](v), P1 ∈ [[ψ]](v) }
A process P satisfies P : φB | ψB if P is the parallel composition of two separate, yet bounded, processes, P1 : φB and P2 : ψB, respectively. Thus, ph can be thought of as the composition of two mutually-exclusive sub-resources, ph1 and ph2 belonging to P1 and P2.
...
A process P satisfies the elevation type P : a!(φB) if it exports a bounded process P' : φB with resources ph. Note that, because φB is a least relation, P' maintains ownership of its resource even as its communicated. If P' is not an owner, but a resource such as*ph, the process P : a!(*b) is still well-typed. It represents an owner which is transferring ownership of ph to the receiving process.
[[ a?b.φ ]](v) = { P : ∃Q, P' .P ≡ Q | x(y).P' , x ∈ ((a))(v), ∀c.∃z.P' {z/y} ∈ [[φ{c/b}]](v) }
...
[[ rec X . φ ]](v) = ∪ { S ⊆ Proc : S ⊆ [[φ]](v{S/X}) }
A process P satisfies the greatest fix point if all future recursive calls preserve the satisfiability of φB. This effectively guarantees exclusivity and linearity of phX under recursion.
[[ ∀n : ψ . φ ]](v) = ∩x∈((@ψ))(v) [[φ{x/n}]](v)
Similar to elevation, quantification has two interesting cases. In the first case, quantification expresses the conditions necessary to substitute an owner x : @ψB into the environment φ. If [[φ{x/n}]](v) := true{x/n} and [[*x]](v) ⊆ true{x/n}, we can infer that x is later expanded back into it's process form X : ψB. Furthermore, true{x/n} asserts that, if phX is later accessed, linearity and exclusivity are respected.
...