Resource Types
For every process P there exists a 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 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) 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.
The formulae generated by the grammar below introduce a spatial-behavioral logic for processes:
φ, ψ ::= true verity
| 0 nullity
| ¬ negation
| φ & ψ conjunction
| φ | ψ separation
| *b descent
| a!φ . elevation
| a?b.φ activity
| rec X . φ greatest fix point
| ∀n : ψ . φ quantification
a ::= @φ indication
| b ...
b ::= @P nomination
| n ...
Formulae are assigned semantics by the two mutually recursive functions
[[ − ]]( − ) : PForm A x [ V → (Proc )] → (Proc)
(( − ))( − ) : QForm A x [ V → (Proc )] → (Proc)
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 process P satisfies the null type P : 0 when the valuation of ph is zero.
[[ ¬φ ]](v) = Proc/[[φ]](v)
A resource P satisfies the negation type P : ¬φB if either linearity or exclusivity are broken during the execution of P.
[[ φ & ψ ]](v) = [[φ]](v) ∩ [[ψ]](v)
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.
[[ *b ]](v) = { P : ∃Q, P0 .P ≡ Q | *x, x ∈ ((b))(v) }
A process P satisfies the drop type P : *b if it dereferences a quoted process x ∈ ((b))(v).
[[ a!(φ) ]](v) = { P : ∃Q, P'. P ≡ Q | x!P', x ∈ ((a))(v), P' ∈ [[φ]](v) }
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) }
The activity type defines the set of processes which receive a message on some x ∈ ((a))(v), then behave according to φ, where every occurance of c being substituted into φ is matched by some z being substituted into P' such that P' {z/y} : φ{c/b}.
[[ 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.
In the second case, where the resource x ∈ @*b, is being substituted into φ, if [[φ{x/n}]](v) := true{x/n}, we can infer that linearity and exclusivity of x is preserved under substitution.
(( @φ ))(v) = { x : x ≡N @P, P ∈ [[φ]](v) }
A name x satisfies the indication type x : @φ if x is name equivalent to @P and P : φ.
(( @P ))(v) = { x : x ≡N @P }
A name x satisfies the nomination type x : @P if x is name equivalent to @P.