1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
|
#+TITLE: Roadmap
The work after the [[file:denial.org][denial]] rework, in the order it can be built. Each step
says why it comes where it does and what has to hold before the next
one starts. The design behind the steps is in [[file:modes.org][modes]], [[file:denial.org][denials]],
[[file:partial-bindings.org][partial bindings]] and [[file:maintenance.org][incremental maintenance]]. Each step lands with its
own tests.
* Done
- Programs are images that name their evaluator, and evaluators
=parse= and =eval= their own kinds. See [[file:evaluators.org][programs and evaluators]].
- Ephemeral relations wrap programs, and storage keeps a program as its
evaluator name and source.
- Every relation declares its modes, and =contains= decides by a test
or by reading, never by reading without end.
- Admission refuses to judge a denial that does not end, and stops at
one witness per denial.
- [[file:../lib/kernel/Merkle.ml][Merkle]] walks a range of keys, from a key and until a predicate.
- A substantial relation keeps an index on each attribute, declares
={a; Finite}= for each, and answers =lookup= through the [[file:../lib/protocols/Indexed.mli][Indexed]]
protocol. See [[file:partial-bindings.org::*What RNT has][partial bindings]].
- FOL restricts a plan with =Where=, pushes the restriction below the
projections that keep its attributes, and reads an index when its
input offers one. A denial can bind attributes, and admission judges
it through the index.
These two replace the binding-aware read this roadmap once planned for
every relation. A binding is a condition on tuples, and conditions
belong to a query language, as [[file:partial-bindings.org::*Where a binding belongs][partial bindings]] explains.
* 1. Read sets
RNT cannot tell which denials a commit can break, because a relation
does not say what it reads. It also cannot turn an inserted tuple into
bindings on a denial, because it does not know how the denial's
attributes line up with those of the relations it reads.
The step has every derived relation state the relations it reads and
where each of its attributes comes from. The =provenance= field of an
attribute description is the natural place to start, and a FOL plan
knows both from its terms.
It is done when, given the relations a commit changed, RNT lists the
denials that read them, and for each one the binding an inserted tuple
puts on it.
* 2. Tuple deltas
The checks in the next steps start from the tuples a commit inserted and
deleted. [[file:../lib/kernel/Path.mli][Path.diff]] names the relations that changed between two states,
and stops at subtrees with equal addresses. The same walk over the two
tuple sets of a relation finds the tuples that changed inside it, since
a prolly tree shares every unchanged subtree.
A commit should also be able to carry such a change rather than a whole
relation. Today [[file:../lib/kernel/Scope.mli][Scope.publish]] binds whole relations, so adding one
tuple means reading the relation into a literal first. A [[file:partial-bindings.org::*Delta relations][delta
relation]], a stored base with tuples to insert and delete, would let
admission apply the change to the base's tuple set and indexes alone.
It is done when RNT gives the inserted and deleted tuples of each
relation a commit changed, at a cost proportional to the change, and a
commit that changes one tuple writes only the paths to it.
* 3. Incremental denial checking
Every commit judges every denial over the whole state. With the two
steps above, a commit can judge only what it can break. For each tuple
it inserted, each denial that reads that tuple's relation is restricted
by the binding the tuple implies, and the first tuple found refuses the
commit. Deletions never matter, because every denial was empty before
the commit.
The kernel knows no rule language and cannot derive that restriction
for a program it cannot read, so the evaluator offers the check. For a
FOL denial it is a =Where= over the denial's plan, which FOL already
pushes down to the stored relations and answers from their indexes. A
denial whose evaluator offers no such check keeps the full check, and
so does a commit that installs a denial, since a new denial has no
earlier emptiness to rely on.
Most rules worth checking this way join two relations, so FOL needs
joins for the step to reach them. A restriction through a join binds
both sides on the join attributes.
It is done when a commit that touches one relation reads only the
restricted denials that read it, and its verdict equals the full
check's on the same states.
* 4. Incremental maintenance
A materialized ephemeral relation would cost what a substantial one
costs to read, but every commit that changes its inputs has to change
it as well. Incremental denial checking is the insertion half of that
work. Maintenance adds the rest.
- Materialization, so that a derived relation is stored with its tuples
and its indexes.
- Deletion rules, and a count per tuple of how many input tuples
produce it.
- An order for each commit: apply the change, maintain every
materialized relation that reads it, judge the denials, then move the
head.
It is done when a maintained relation holds the same tuples as the same
relation recomputed from scratch, after every commit in the tests.
* 5. Builds that do not fit in memory
A substantial relation builds its tuple set and each index by inserting
one entry at a time inside =with_batch=, which keeps every version of
every node until it flushes. A build holds about =N × depth= nodes, more
than the tuples it stores. Tuple deltas remove the rebuild from ordinary
commits, but an import, a first materialization, or a relation stored
before indexes still builds from nothing.
The step sorts the entries of each tree, on disk when they do not fit,
builds the tree bottom-up from the sorted stream, and writes its nodes
in short transactions. [[file:partial-bindings.org::*Builds that do not fit][Partial bindings]] gives the details. A tree
built bottom-up must equal the tree inserting the same keys would make,
or a relation's address would depend on how it was built.
It is done when building a relation holds a bounded number of nodes,
whatever its size, and yields the same address as building it by
insertion.
* Alongside
These do not block the steps above.
- =Relation.read= reads a relation whole, and a multigroup stores a
relation that wraps no program by reading it whole. Both hang on a
=Countable= relation and should check its modes first, as admission
does.
- A relation that declares ={all; Bounded 1}= promises a membership
test, and nothing checks that it gives one. A program that declares
=Finite= and never ends still hangs any reader.
- A tuple's =type_= is part of its hash and not of its heading, so
={all; Bounded 1}= holds only while the tuples of a relation share one
=type_=.
- FOL detects cycles only among its own programs. A cycle across
languages recurses without end.
- Denials do not protect themselves. Removing one is judged on a state
where it is gone. This needs the access checks the [[file:../README.org][README]] plans.
- Evaluators should declare capability tags, such as =dml=, and the
registry should index them.
- Programs that change state have no result protocol.
- Once [[file:../lib/kernel/Merkle.ml][Merkle]] chunking depends only on the tuples a tree holds,
maintenance can be checked by comparing addresses instead of tuples.
- A leaked handle's finalizer can dereference a handle that was already
invalidated, so tests fail with =Attempt to dereference an invalid
handle!= in whichever test the collector happens to run, depending on
the size of the minor heap.
- The signatures in [[file:object-system.org][the object system]] predate the code.
|
