Inter-Definability
Some sorts of synergy can be constructed given other forms.
There are qualifications on such constructions.
One qualification is that the constructed form be efficient if the given form is.
Another qualification is that preemptive scheduling within a mutable name space is allowed.
The language, or the kernel design must decide what primitive synergy to provide.
Some extreme forms, such as displaying the cap bits, are seldom provided, except to highly trusted code.
We aspire to a partial ordering describing which of these forms can be define given others.
This will probably require more careful definitions of each.
I think that this can be done in a language independent form, even allowing machine language which is the native language of kernels.
I begin with a set of names and a brief description of each form:
- Amp
- Rights amplification
- eq?
- The name is from Scheme.
It tests for complete interchangeability of its two arguments.
The Keykos DISCRIM object provides the analogous service.
Predicate calculus assurance of conformance with predicate calculus axioms is required (including caps to malicious objects):
- For all x: x=x
- For all x, y (if x=y then φ → ψ) (where φ is like ψ except that x occurs freely in φ wherever y occurs freely in ψ.)
- Seal
- Section 6 in the 1973 Morris proposals.
There is a widely shared immutable object Createseal.
(Createseal) yields (seal unseal) such that:
For all x (unseal (seal x)) = x.
For all x {[(unseal x) = #f] or [there exists y (x = (seal y)]).
- WeakMap
- xx
- Safe
- xx
Keykos domain tool exceeds the safe.
- Yours?
- An order on a trusted class of creators.
Did you create this?
- Brand
- as available to Keykos programs lacking the domain tool.
Perhaps the same as ‘Yours?’.
- Stiegler
- Stiegler’s code;
Incompatible with preemptive scheduling of tasks which share access to mutable storage.
- Static
- Static compile time sibling access;
If a ref to an instance of class x is passed to another instance of class x,
The the latter instance can access private members of the first instance.
Here Mark Miller builds sealer-unsealer pairs from WeakMap.
Partial Ordering
A partial ordering of a finite set X may be defined as the transitive closure of a unique minimal subset of X×X.
We begin to collect this subset here.
“α ➾ β” means that β can be defined in terms of α.
- WeakMap ➾ Seal
- Mark Miller’s construction