diff options
Diffstat (limited to '')
| -rw-r--r-- | docs/denial.org | 194 | ||||
| -rw-r--r-- | docs/evaluators.org | 285 | ||||
| -rw-r--r-- | docs/lifecycle.org | 50 | ||||
| -rw-r--r-- | docs/maintenance.org | 104 | ||||
| -rw-r--r-- | docs/modes.org | 171 | ||||
| -rw-r--r-- | docs/object-system.org | 2 | ||||
| -rw-r--r-- | docs/object-taxonomy.org | 8 | ||||
| -rw-r--r-- | docs/roadmap.org | 137 |
8 files changed, 854 insertions, 97 deletions
diff --git a/docs/denial.org b/docs/denial.org new file mode 100644 index 0000000..d79a394 --- /dev/null +++ b/docs/denial.org @@ -0,0 +1,194 @@ +#+TITLE: Denials + +* Purpose +A denial is a relation that must be empty. Each tuple it holds is one +breach of a rule, so a state where every denial is empty is a state +where every rule holds. RNT knows no rule language. It knows only that +denials must be empty, and it refuses to move a branch head to a state +where one is not. Constraints across relations, the assertions SQL +names but rarely implements, become relations like any other. + +The idea is the denial form of integrity constraints, from Sadri and +Kowalski ("A theorem-proving approach to database integrity", 1988), +where a rule is written as a query for its own counterexamples. + +* Where denials live +Each multigroup holds its denials beside its schemas. + +#+begin_example +\system\branch\master\multigroup\library\schema\default\relation\book +\system\branch\master\multigroup\library\denial\no-books +#+end_example + +A multigroup stores a denial the way a schema stores a relation. An +[[file:../lib/kernel/EphemeralRelation.ml][ephemeral relation]] that wraps a [[file:../lib/kernel/Program.ml][program]] becomes the program's +evaluator name and source, and any other relation becomes its tuples. A +program is the usual case, because a rule has to be computed against +the state it judges. When a branch reads the denial back, the +[[file:evaluators.org][evaluator]] registered under that name parses the source, and reading +the denial invokes the program =within= the branch state it was read +through. The same denial therefore reads one state through the head +and another through =previous=. + +* Judging a state +[[file:../lib/protocols/Admission.mli][Admission]] is the protocol that judges a state. + +#+begin_src ocaml +type violations = (string * Concepts.Tuple.t) list + +class type implementation = object + method check : (violations, Concepts.Condition.condition) result +end +#+end_src + +=check= names every denial that holds a tuple, with one such tuple as +its witness. An empty list means the state is admitted. An error means +the state could not be judged, and an unjudged state is not admitted +either. + +A multigroup judges each of its denials in two steps. + +1. It asks the denial for its [[file:modes.org][modes]]. If the denial is not + exhaustible with nothing bound, the multigroup fails with + =unjudgeable-denial= and reads nothing. +2. Otherwise it reads the denial up to its first tuple. No tuple means + the denial holds. A first tuple is the witness, and the multigroup + reads no further. + +For a denial that wraps a program, the multigroup invokes the program +once, within the branch state it judges, and asks both questions of the +relation the program returns. + +A branch state asks each of its multigroups and names every violation +by its path, =\multigroup\[m]\denial\[d]=. Judging belongs to the +multigroup, the universe its relations describe. The branch only +versions states and collects the answers. A rule may still read +relations of any multigroup, because the branch asks all of them. + +One witness is enough to refuse a state, and asking for more would cost +a read of the whole denial, which never ends for a =Countable= one. + +* Trust +The guard rests on what a denial declares. A FOL denial over stored +relations derives its modes from theirs, so its claim to be finite +holds. A denial written in another language declares whatever its +evaluator returns. A program that declares =Finite= and then never ends +still hangs the check, and RNT cannot tell. The same holds when FOL +reads a relation from another evaluator, since FOL takes that +relation's modes as given. A cycle of programs across languages also +recurses without end. + +* Moving a head +=BranchManager= asks the proposed state for its admission before it +moves a head. If the state is not admitted, it refuses the move with a +=refused= condition that names each denial and its witness, and the +head stays where it was. It asks before taking the head, since a denial +may run a program that reads storage. + +#+begin_src plantuml :file ../images/denial-admission.svg +@startuml +participant "Scope.publish" as Publish +participant BranchManager +participant "proposed\nbranch state" as Branch +participant Multigroup +participant Denial + +Publish -> BranchManager : move the head +BranchManager -> Branch : check +loop each multigroup + Branch -> Multigroup : check + loop each denial + Multigroup -> Denial : modes + alt not exhaustible with nothing bound + Multigroup --> BranchManager : unjudgeable-denial + else exhaustible + Multigroup -> Denial : enumerate, read the first tuple + Denial --> Multigroup : a witness, or nothing + end + end + Multigroup --> Branch : violations +end +Branch --> BranchManager : violations, named by path +alt none + BranchManager -> BranchManager : move the head +else some + BranchManager --> Publish : refused, one witness per denial +end +@enduml +#+end_src + +#+RESULTS: +[[file:../images/denial-admission.svg]] + +The check judges the state itself, not a change to it. Every commit +lands only if the whole state it makes is admitted, whichever subsystem +made it, so a rule written in one language guards data written from +all of them. + +* Publishing denials +[[file:../lib/kernel/Scope.mli][Scope.publish]] binds denials with its relations, in the same state. + +#+begin_src ocaml +Scope.publish root ~branch:"master" ~home:library + ~denials:["no-books", Some no_books; "audit:shelved-twice", Some twice] + ["book", Some books] +#+end_src + +A name =d= binds in the home multigroup, and =m:d= binds in multigroup +=m=. A commit can install a rule and the data it guards together, and +the rule is judged with the data. If the state it makes already breaks +the rule, the commit is refused. A denial that cannot be judged cannot +be installed either, since the state that holds it cannot be admitted. + +* Judging a state without landing it +A subsystem that wants to know whether a change would be admitted builds +the state with [[file:../lib/kernel/Path.mli][Path.assoc_all]] and asks it. + +#+begin_src ocaml +let* next = Path.assoc_all head [Scope.relations library, "book", Some books] in +let* admission = Protocols.Admission.require next in +Protocols.Admission.check admission +#+end_src + +Nothing lands. A host can use this to preview a form, a move or an +import, and show which rule would refuse it. + +* Open problems +** Incremental checking +Every commit judges every denial of every multigroup over the whole +state. Decker ("Translating Advanced Integrity Checking Technology to +SQL", 2002) shows how to check only what a change can break. Take the +denial of a book shelved twice. + +#+begin_example +{(title, s1, s2) | shelved(title, s1) ∧ shelved(title, s2) ∧ s1 ≠ s2} +#+end_example + +A commit that inserts =shelved("Codd", "A")= can only add violations +where =title = "Codd"= and one shelf is ="A"=. Asking the denial for +those tuples, with the other shelf free, is the whole incremental check. +It is the insertion-only case of [[file:maintenance.org][incremental maintenance]], which covers +the delta rules it reuses. + +RNT cannot ask that today. The question binds some attributes of the +denial and leaves others free, and no operation produces the tuples of +a relation under a partial binding. This is the gap that [[file:modes.org::*Reachable bindings][reachable +bindings]] describes. Closing it takes three pieces. + +1. A binding-aware read, which every relation implements and FOL passes + through its plans. +2. Indexes, so that a substantial relation answers such a read by + lookup rather than by filtering a scan. +3. Read sets, so that RNT knows which relations a denial reads and how + their attributes line up with the denial's, and can turn an inserted + tuple into bindings on each denial it touches. + +** Denials do not protect themselves +A commit that removes a denial and breaks its rule is judged on the +state it makes, where the denial is gone, so it lands. Guarding +=\denial= needs the access checks the [[file:../README.org][README]] plans to keep apart +from lookup. + +** Multigroups from before denials +A multigroup stored before denials existed has no =denials= field and +does not load. diff --git a/docs/evaluators.org b/docs/evaluators.org index b7ce3b8..f1b4be5 100644 --- a/docs/evaluators.org +++ b/docs/evaluators.org @@ -1,108 +1,215 @@ -#+TITLE: Evaluators +#+TITLE: Programs and evaluators + +* Why the kernel has no language +RNT supplies objects, storage and the execution lifecycle, and leaves +languages to its clients. SQL puts retrieval, data manipulation and data +definition in one language, and the boundaries between them are hard to +draw. In RNT, a language =A= may serve retrieval, =B= may serve +manipulation and definition, and =C= may serve manipulation beside =B=. +Nothing arbitrates between =B= and =C=, and a client picks either. The +[[file:../lib/evaluators/FOL.ml][FOL]] evaluator is one such language, shipped with RNT for retrieval. + +That leaves the kernel two jobs. It has to run a program without +knowing its language, and it has to let programs in different languages +read each other's results. Programs and evaluators are how it does both. + +* Programs +The kernel holds, stores and runs programs whose structure it cannot +know. A [[file:../lib/kernel/Program.ml][program]] is therefore an image, in the manner of a Windows +[[https://en.wikipedia.org/wiki/Portable_Executable][Portable Executable]], whose header tells the loader which subsystem +runs it. -* Position -RNT should supply objects, storage, and execution -lifecycle, but not directly a sublanguage. That duty is then on the -clients to implement one and register it, using the kernel's -capabilities. +#+begin_src ocaml +type kind = .. +type image = {evaluator: string; kind: kind; source: string} +#+end_src -In this context, an evaluator is an RNT object, registered and -selected through the object interface, with a special "evaluator" -protocol. Unlike SQL where the boundaries between execution contexts -of the language is confusing and sometmes non-trivial, a sublanguage -=A= may serve retrieval, =B= may serve DML and DDL while =C= may serve -DML alongside =B=. Nothing arbitrates between B and C; making the -client free to opt for one. +=evaluator= names the evaluator that runs the program, as +=scope:language=. =kind= is the program as that evaluator understands +it. =source= is its text, for display and for storage. -The FOL evaluator is therefore, one of such evaluators that is shipped -alongside RNT for specifically Data Retrieval. +=kind= is an [[https://ocaml.org/manual/extensiblevariants.html][extensible variant]], extended the way [[file:object-system.org][protocols]] are. Each +evaluator adds its own constructor, as FOL adds =Fol of Path.t term=. +The tree keeps its OCaml type, and only the evaluator that defined the +constructor can match on it, so the kernel passes programs around with +no encoding in between. The evaluator name is the one string a program +carries, because the kernel looks evaluators up by name and storage can +keep a name but not a constructor. -* Capability tags -An evaluator object declares a set of opaque labels — =drl=, =dml=, -=ddl=, =vcs=, or anything a client invents. The registry stores and -indexes them so a client can ask which evaluators declare =dml= and -get back B and C. - -* Protocols -An evaluator is an object like any other, that can be used to execute -a program, exactly as an interpreter takes an expression and an -environment. The plan tree should already bear every value and handle -the program needs, so there is nothing left to bind. Each invocation -carries independent state based atop of the handles it was given -(being therefore hash dependent and isolated). +Every program speaks [[file:../lib/protocols/Executable.mli][Executable]], and a program built with a root can run. #+begin_src ocaml -module Make (P : PROGRAM) : sig - class type implementation = object - method invoke : P.t -> (Handle.t, condition) result - end -end +method invoke : Handle.t list -> within:Handle.t -> (Handle.t, condition) result #+end_src -The protocol is parameterized by the evaluator's own plan type, so a -plan is never encoded into values only to be decoded again. Each -application of the functor yields its own protocol constructor, which -is what keeps one evaluator from answering another's programs: a -client obtains the interface through the module of the evaluator it -intends to speak to. The FOL evaluator, which lives under -=lib/evaluators= alongside the evaluators shipped with RNT, currently -understands a single node: +Invoking a program looks up =\[scope]\evaluator\[language]= under its +root, and hands that evaluator the kind, the inputs and =within=. A bare +=language= names the =system= scope. The root is a capability, so a +program reaches only the evaluators of the root it was given. A program +built without a root can be stored but not run, and invoking it fails +with =unloaded-program=. A name with nothing registered under it fails with +=no-evaluator=. + +* Evaluators +An evaluator is an object with the [[file:../lib/protocols/Evaluator.mli][Evaluator]] protocol. #+begin_src ocaml -type plan = Base of Handle.t +method parse : string -> (kind, condition) result +method eval : kind -> Handle.t list -> within:Handle.t -> (Handle.t, condition) result #+end_src -=Base= carries the handle of a relation, which is enumerated to -exhaustion. The evaluator only invokes protocols on the handles it -receives, which keeps it free of storage and of name resolution. - -The returned handle carries a result protocol with =Protocols.Cursor=, -giving it incremental consumption. Since executing a plan node yields -a cursor, operators stack as cursors over cursors, in the manner of a -volcano iterator, and no intermediate result is materialized. A -successor state and a command completion are further result protocols, -added for DML and DDL later. It's important to notice that the kernel -enumerates result protocols; it thererfore does not enumerate -sublanguages. That is not to say however that we cannot have a builtin -catalog relation installed and configured by the client that -enumerates them (that's a concern for the future). - -* Handles -There is no evaluation context. Since we are a capability based -system, holding a handle is what authorizes its use, so the caller -obtains every handle a program needs beforehand (through the -directories it was granted) and passes them in. Evaluators reach -kernel resources *only* through those handles. A program that refers -to things by name carries the directory they are resolved in, as the -lambda evaluator does: - -#+begin_src ocaml -type program = Program of term * Directory.t Handle.interface +=eval= runs a kind, and fails for a kind that is not its own. =parse= +turns source back into a kind, which is how the kernel reloads a stored +program. A program built in code skips parsing. =FOL.program term= +builds one from a tree and prints the tree as its source, so a test can +build a plan without a syntax. FOL has no text syntax yet, and its +source is the [[https://en.wikipedia.org/wiki/Bencode][bencoded]] term. + +#+begin_src plantuml :file ../images/evaluators-classes.svg +@startuml +hide empty members +skinparam classAttributeIconSize 0 + +class Program <<image>> { + evaluator : string + kind : Program.kind + source : string +} +interface Executable { + invoke(inputs, within) : relation +} +interface Evaluator { + parse(source) : kind + eval(kind, inputs, within) : relation +} +class "FOL evaluator" as FOL +class EphemeralRelation +interface Relation { + contains(tuple) : bool + modes() : Mode.t +} +interface Enumerable { + enumerate() : cursor +} +interface Schematics { + describe() : heading +} + +Program ..|> Executable : runs when given a root +FOL ..|> Evaluator +Program --> Evaluator : names it as\nscope:language +EphemeralRelation ..|> Relation +EphemeralRelation ..|> Enumerable +EphemeralRelation ..|> Schematics +EphemeralRelation o--> "0..1" Program : wraps +Evaluator ..> EphemeralRelation : eval returns +@enduml #+end_src -Since every object is content addressed and prolly trees do not -depend on insertion order, equal state yields an equal hash, so the -relation behind a handle does not change under a running evaluation. -A successful evaluation and cursor exhaustion never commit. Commit -should be an explicit host operation. +#+RESULTS: +[[file:../images/evaluators-classes.svg]] + +* Within +In RNT, holding a handle is what authorizes its use, so an evaluator +gets no context beyond one directory. A program names relations by +path, and its evaluator resolves those paths in the directory the +program is invoked =within=. It can reach nothing else. + +Resolving paths at each invocation is what lets one program run against +any state. Read through +=\system\branch\master\multigroup\m\schema\s\relation\r=, a stored +program runs within that branch state. Read through +=\system\branch\master\previous\...=, it runs within the previous state +and reads what was there then. It can never read outside its branch. + +Evaluation never commits, and neither does exhausting a cursor. +Committing is an explicit host operation. Cancellation, budgets and +resource accounting are not implemented. + +* Results +Programs in different languages can read each other's results only if +those results share one interface. The result of every program is an +[[file:../lib/kernel/EphemeralRelation.ml][ephemeral relation]]. It describes its heading, declares its [[file:modes.org][modes]] and +answers membership. Enumerating it gives a cursor, so operators stack +as cursors over cursors, as in Graefe's Volcano iterator model +("Volcano, an Extensible and Parallel Query Evaluation System", 1994), +and nothing in between is materialized. + +An ephemeral relation can wrap a program, through +=EphemeralRelation.of_program=. Reading it invokes the program within +the state it was given. Asking its modes, or whether it holds a tuple, +invokes the program and asks the relation the program returns. For FOL +this is cheap, because FOL builds its result without reading a tuple. + +Programs that change state have no result protocol yet. + +* Storage +A multigroup stores an ephemeral relation that wraps a program as the +program's evaluator name and source, beside its heading. It stores any +other relation as its tuples. When a branch reads the relation back, +the evaluator registered under that name parses the source into a kind, +and the relation wraps the program that comes out. The parse happens at +lookup, so a missing evaluator or a malformed source fails at +=Path.lookup= rather than at the first read. + +#+begin_src plantuml :file ../images/evaluators-reading.svg +@startuml +actor Client +participant "Path.lookup" as Path +participant Multigroup +participant EphemeralRelation as E +participant Program +participant "evaluator under\nthe program's name" as Ev + +Client -> Path : lookup a relation in a branch state +Path -> Multigroup : find it +Multigroup -> E : load (evaluator name, source, heading) +E -> Program : Program.load root +Program -> Ev : parse source +Ev --> Program : kind +E --> Client : relation wrapping the program +Client -> E : enumerate +E -> Program : invoke ~within:branch state +Program -> Ev : eval kind ~within +Ev --> Program : result relation +Program --> E : result relation +E --> Client : cursor over the result +@enduml +#+end_src -Cancellation, budgets, and resource accounting are not implemented. +#+RESULTS: +[[file:../images/evaluators-reading.svg]] * Composition -Evaluators compose through invocation and result protocols alone. A -DML program written in B may invoke a retrieval program written in A, -consume its cursor, and build a successor state from the tuples. A -retrieval program in A may invoke a procedural relation implemented by -C. Neither evaluator however knows the other's representation. The -caller must establish that the callee's contract meets its needs, -obviously. +Evaluators compose through programs and results, and neither knows the +other's kind. When FOL resolves a path to a relation that wraps a +program, it checks the program's kind. + +- A FOL program is inlined into the plan. FOL then sees through it, and + refuses a program that reaches itself with =cyclic-program=. +- A program of any other kind is invoked within the same state, and its + result enters the plan like any other relation. + +A program in another language reads a FOL program the same way, by +resolving its path and reading the relation. The [[file:../test/unit/kernel/Branch.ml][branch tests]] do both, +with a toy language whose programs shout the titles of a FOL relation. + +FOL detects cycles only among its own programs. A cycle across +languages, where a FOL program reads a toy program that reads it back, +recurses without end. Nothing checks one evaluator's assumptions about +another's results either, so the caller has to establish that the +callee's results meet its needs. * Registration -Registration is made by the client, and in the case of builtins, -automatically at initialization, just as =Relation= and =Schematics=, -for example. A foreign registration path is a later concern and is not -designed for here. - -Only =Protocols.Cursor= exists as a result protocol (at least for now), -so a successor state, completion, plan persistence, and cross-evaluator -optimizations are absent by design. +The system's evaluators are registered at initialization, under +=\system\evaluator=. A subsystem mounts its own root with +[[file:../lib/kernel/Initialization.mli][Initialization.mount]], which holds =\[name]\evaluator=, and registers +its evaluators there. Its programs then name them as =name:language=. A +foreign registration path is a later concern. + +* Capability tags +A client should be able to ask which evaluators serve manipulation, and +get =B= and =C= back. The intent is that each evaluator declares a set +of opaque labels, such as =drl=, =dml=, =ddl=, =vcs= or any a client +invents, and that the registry indexes them. None of this is +implemented. diff --git a/docs/lifecycle.org b/docs/lifecycle.org index 80b387d..c23e9a1 100644 --- a/docs/lifecycle.org +++ b/docs/lifecycle.org @@ -7,6 +7,9 @@ operates purely on the object tree and never touches storage. "Collection" here means dropping the in-memory registry entry, not deleting anything on disk. +The manager is a design and is not built. [[*What exists today][What exists today]] describes the +mechanism the code has now. + * Three independent facts per object Each registry entry keeps three separate pieces of state, deliberately not @@ -42,12 +45,11 @@ the =reference_count= of each edge target; unregistration drops it. The edge set is a per-kind property and lives next to the registry, because the object knows its own shape. -Only ephemeral relations carry edges today. An ephemeral relation is a stored -plan that reads other relations, so those inputs must not be collected while -the plan can still be replayed. The edges are branch-local symlink paths, not -version-pinned paths: as the branch head advances the inputs move with it, and -=Namespace.resolve= turns the symlink into whatever object is current on this -branch hash. This is what lets an ephemeral relation behave like a view. +Only ephemeral relations carry edges today. An ephemeral relation wraps a +[[file:evaluators.org][program]] that reads other relations, so those inputs must not be collected +while the program can still run. Its inputs are paths resolved in the branch +state it is read through, not pinned versions. Read through the head, it reads +the inputs as they are. Read through =previous=, it reads them as they were. * Teardown order @@ -80,3 +82,39 @@ collectable like anything else. Separate from collection. An exclusive object with an open handle, such as a branch head being read, cannot be modified until the handle closes. =contention= reports this so writers can be gated. + +* What exists today +Each object carries its own lifecycle, one of the classes in +[[file:../lib/kernel/Lifecycle.mli][Lifecycle]], and every handle to it calls into that lifecycle when it is +copied or released. + +- =null= is for objects with nothing to release, either because storage + can rebuild them or because they hold no resources. Substantial + relations, multigroups, branch states, programs and evaluators are + =null=. +- =counted= is for objects that hold resources. It counts handles and runs + the object's destructor when the last one is released. Namespaces, + sessions, generated cursors and ephemeral relations are counted, and an + ephemeral relation releases its inputs when it is destroyed. +- =exclusive= admits one handle at a time. Nothing uses it since sessions + became counted. +- =retaining= stands in for a handle while it holds a reference to an + owner, so that what the handle reads outlives the object that produced + it. A cursor over a program's result keeps the result alive this way. + +A namespace owns the handles registered in it. =Namespace.update= moves the +handle in, which invalidates the caller's handle, and releases the handle +it replaces. A destroyed namespace releases every entry. A caller that +still needs a handle after registering it registers a =Handle.copy=. + +Walking a path opens a handle at every step, and the walk has to release +all of them except the last. [[file:../lib/kernel/Path.ml][Path]] does this with an autorelease pool, +named after the [[https://developer.apple.com/library/archive/documentation/Cocoa/Conceptual/MemoryMgmt/Articles/mmAutoreleasePools.html][Cocoa]] mechanism. Each handle found along the way goes +into the pool, and the pool releases them when the walk ends. =Handle.keep= +takes the handle the walk returns back out of the pool, and the caller +releases it. The pool is an OCaml [[https://ocaml.org/manual/effects.html][effect handler]], so the code inside the +walk adds handles to it without being passed the pool. + +A handle to a managed object that the garbage collector reaches while it +is still valid has leaked. Its finalizer logs a warning with the backtrace +of where the handle was made, and releases it. diff --git a/docs/maintenance.org b/docs/maintenance.org new file mode 100644 index 0000000..42b5075 --- /dev/null +++ b/docs/maintenance.org @@ -0,0 +1,104 @@ +#+TITLE: Incremental maintenance + +* Purpose +An [[file:../lib/kernel/EphemeralRelation.ml][ephemeral relation]] is computed when it is read. That is right for a +relation read rarely, and wrong for one read on every commit or over a +large input, where each read repeats the whole computation. A +materialized ephemeral relation would store its tuples, so that reading +it costs what reading a substantial relation costs. Every commit that +changes its inputs then has to change it as well. + +Recomputing it from scratch on each commit costs as much as the +relation itself. Incremental maintenance computes only the change, from +the change to the inputs. The literature calls this [[https://en.wikipedia.org/wiki/Materialized_view][incremental view +maintenance]], and Gupta and Mumick survey it in "Maintenance of +Materialized Views: Problems, Techniques, and Applications" (1995). +RNT has none of it yet. This document is the design it should follow. + +* Deltas +A commit changes each relation it touches by a set of inserted tuples, +Δ⁺, and a set of deleted tuples, Δ⁻. For a relation =D= derived from +inputs =R₁ … Rₙ=, maintenance computes =ΔD⁺= and =ΔD⁻= from the =ΔRᵢ= and +the states before and after the commit, operator by operator. + +- =Base r= changes exactly as =r= does. +- =Project (p, A)= gains the projection of each tuple in =Δp⁺= that it + did not hold before. It loses the projection of a tuple in =Δp⁻= only + if no other tuple of =p= projects to the same tuple, which is the + problem [[*Counting][counting]] solves. +- A join, once [[file:../lib/evaluators/FOL.ml][FOL]] has one, gains =ΔR⁺ ⋈ S= and =R ⋈ ΔS⁺=, against the + right states. Computing =ΔR⁺ ⋈ S= means asking =S= for the tuples that + agree with each inserted tuple of =R= on the join attributes. + +That last question binds some attributes of =S= and leaves the rest +free. It is the partial binding that no operation in RNT can ask +today, the gap [[file:modes.org::*Reachable bindings][reachable bindings]] describes. Without it, the only way +to compute a delta through a join is to read =S= whole, which is +recomputation by another name. + +* Counting +Deletion through a projection needs to know how many tuples of the input +produce each tuple of the output. A materialized relation can store that +count beside each tuple. An inserted input tuple raises the count of +its projection, a deleted one lowers it, and the projected tuple leaves +the relation when its count reaches zero. This is the counting algorithm +of Gupta, Mumick and Subrahmanian ("Maintaining Views Incrementally", +1993). The same paper gives DRed for recursive relations, where counts +do not terminate, by deleting an overestimate and rederiving what +survives. + +* Denials are the simplest case +A [[file:denial.org][denial]] is an ephemeral relation that must stay empty, and checking it +incrementally is maintenance with most of the work removed. + +- Only insertions matter. The state before the commit was admitted, so + every denial was empty, and an empty relation has nothing to lose. + =ΔD⁻= is always empty. +- Only emptiness matters. One tuple of =ΔD⁺= is enough to refuse the + commit, so the check stops at the first. +- Nothing is stored. A denial is never materialized, and its delta is + thrown away once judged. +- Nothing is counted, because nothing is ever deleted from a denial. + +Incremental denial checking therefore reuses the insertion half of the +delta rules, stopped at the first tuple. Full maintenance adds +deletions, counts and storage on top of it. + +* What it needs +Some pieces are shared with incremental denial checking. + +1. A binding-aware read, which every relation implements and FOL passes + through its plans, to compute deltas through joins. +2. Indexes, so that such a read is a lookup on a substantial relation + rather than a filtered scan. +3. Read sets, so that RNT knows which relations a derived relation + reads and how their attributes line up with its own, and can tell + which relations a commit touches. +4. Tuple deltas. [[file:../lib/kernel/Path.mli][Path.diff]] names the relations that changed between + two states, and skips subtrees with equal addresses. The tuples that + changed inside a relation can be found the same way, by diffing its + two tuple sets, since a prolly tree shares every unchanged subtree. + RNT does not expose that diff yet. + +Others belong to maintenance alone. + +5. Materialization, so that a derived relation can be stored with its + tuples and counts, and read like a substantial relation. +6. Deletion rules and counts, as above. + +* When maintenance runs +A commit would apply its changes to the base relations, maintain every +materialized relation that reads them, then judge the denials against +the resulting state, and only then move the head. Maintenance has to +come before judgement, because a denial may read a materialized +relation. The maintained relations land in the same state as the change +that caused them, so no state ever holds a stale one. + +* Checking it +A tuple set is content addressed. If the shape of its tree depended only +on the tuples it holds, and not on the order they were inserted in, a +maintained relation and the same relation recomputed from scratch would +have equal addresses exactly when maintenance was correct, and +comparing the two addresses would test the delta rules completely. The +chunking in [[file:../lib/kernel/Merkle.ml][Merkle]] is still naive and does not promise that, so until +it does, the test has to compare the tuples themselves. diff --git a/docs/modes.org b/docs/modes.org new file mode 100644 index 0000000..2337b29 --- /dev/null +++ b/docs/modes.org @@ -0,0 +1,171 @@ +#+TITLE: Modes + +* Extension and intension +A relation can be known in two ways. Its [[https://en.wikipedia.org/wiki/Extensional_and_intensional_definitions][extension]] is the set of tuples it +holds, and a tuple belongs to it if it is among them. Its intension is +the predicate those tuples satisfy, and a tuple belongs to it if the +predicate says so. A finite relation can be answered from either. A +relation of [[https://en.wikipedia.org/wiki/Aleph_number][countably infinite]] cardinality can only be answered from +its intension, since enumerating it never ends. + +A reader that waits for the end of an endless relation hangs, so RNT +has to know before reading whether a read ends, and whether a relation +can decide membership at all. Modes are how a relation says so. A mode +states what a relation can answer under a given binding of its +attributes, and says nothing of whether the answer comes from the +extension or the intension. The idea comes from logic languages such +as Mercury, where a predicate declares its [[https://mercurylang.org/information/doc-latest/mercury_ref/Modes.html][modes]], which arguments must +be bound for a call, and its [[https://mercurylang.org/information/doc-latest/mercury_ref/Determinism.html][determinism]], how many solutions such a +call has. + +* A mode +[[file:../lib/concepts/Mode.mli][Mode]] describes one with two fields. + +#+begin_src ocaml +type mode = {bound: attributes; yields: Cardinality.t} +#+end_src + +Given values for the attributes in =bound=, the relation produces every +tuple that agrees with them, and there are at most =yields= of them. +[[file:../lib/concepts/Cardinality.mli][Cardinality]] has four classes, =Empty=, =Bounded n=, =Finite= and +=Countable=. Every class but =Countable= is exhaustible, meaning that +enumeration ends. + +A relation declares its modes through the [[file:../lib/protocols/Relation.mli][Relation]] protocol. + +#+begin_src ocaml +method modes : (Concepts.Mode.t, Concepts.Condition.condition) result +#+end_src + +* Generation under a binding +A mode declared for =B= also serves any binding that includes =B=. The +relation produces the tuples that agree with =B= and drops those that +disagree with the extra values, so it produces no more than before. + +=Mode.generation modes bound= is therefore the tightest =yields= among +the modes whose =bound= is a subset of the binding. It is =None= when +no mode applies, and then the relation cannot be asked under that +binding at all. This differs from =Countable=, where the relation can +be asked but its answer never ends. =Mode.exhaustible= tells whether +the generation ends. + +* Membership +Deciding whether a tuple belongs to a relation means asking the +relation with every attribute bound. A relation is a set, so at most +one tuple agrees with a full binding, and a mode over every attribute +yields =Bounded 1=. That mode is a direct test, an intension. A +relation without one can still decide by producing the tuples under a +smaller binding and comparing each, provided that production ends, +which is deciding by extension. In principle, then, a relation decides +membership exactly when it is exhaustible with every attribute bound, +and extension and intension are the same question asked under +different bindings. + +* Reachable bindings +The principle above is wider than what RNT can do today. The +[[file:../lib/protocols/Relation.mli][Relation]] and [[file:../lib/protocols/Enumerable.mli][Enumerable]] protocols reach exactly two bindings. + +- =enumerate= produces tuples with nothing bound, so it realizes the + modes whose =bound= is empty. +- =contains= answers with every attribute bound, so it realizes the + modes whose =bound= is every attribute. + +No operation produces the tuples that agree with a partial binding. A +relation may declare a mode such as ={title; Finite}=, and +=Mode.generation= takes it into account, but nothing in RNT can act on +it. In particular, a relation cannot decide membership through a mode +with a partial binding. It decides only by its own test, or by +enumerating with nothing bound. A partial mode becomes usable once +there is an operation that produces tuples under a binding, which is +also what [[*Indexes][indexes]] need. + +* How contains decides +A substantial relation looks the tuple up by its hash. + +An ephemeral relation takes an optional membership test from whoever +builds it, through =EphemeralRelation.instantiate ?decide=. + +- With a test, =contains= uses it. +- Without one, =contains= enumerates the relation and compares, but + only when =Mode.exhaustible modes ∅= holds, meaning its generation + with nothing bound ends. +- Otherwise it fails with =undecidable-membership= and does not + enumerate. This is the case when that generation is =Countable=, or + when no mode has an empty =bound=. + +A relation that declares ={all; Bounded 1}= promises a direct test, so +whoever builds it must give it one. Nothing checks that promise yet. + +The evaluator protocol has no membership method. An ephemeral relation +generated by a program answers =contains= the way it answers =modes=. +It invokes the program, asks the relation the program returns, and +releases it. That result is a relation the evaluator built, and the +evaluator gave it whatever test it could. + +* What relations declare +A substantial relation stores its tuples in a set keyed by the hash of +each whole tuple. It declares ={∅; Finite}= for enumerating that set, +and ={all; Bounded 1}= for the lookup by hash, which needs every +attribute to compute the hash. + +An ephemeral relation that =EphemeralRelation.literal= builds from =n= +tuples declares ={∅; Bounded n}=. + +An ephemeral relation generated by a [[file:../lib/kernel/Program.ml][program]] knows its modes only from +the relation the program returns, so asking for them invokes the +program and asks the result. Invoking is lazy. An [[file:evaluators.org][evaluator]] builds +the result without reading tuples, and FOL reads tuples only when the +result is enumerated. A program with no state to run within fails with +=unbound-program=, just as reading its relation would. + +A relation that declares no modes cannot be asked under any binding. + +* Modes of a FOL plan +[[file:../lib/evaluators/FOL.ml][FOL]] computes the modes of a plan alongside its heading, before it +executes anything, and records them on each relation it derives. + +- =Base r= has the modes of =r=. +- =Project (p, A)= keeps the modes of =p= whose =bound= lies within + =A=, with the same =yields=. + +A projection never yields more tuples than its input, so =yields= +carries over. A mode that needs an attribute outside =A= no longer +applies, because a tuple of the projection holds no value for it. + +Take =book(title, author)= as a substantial relation, projected on +=title=. Asking whether ={title: "Codd"}= belongs to the projection +asks whether some book has that title, by any author. The lookup by +hash needs the author to hash the whole tuple, so the projection keeps +only ={∅; Finite}=. + +FOL gives a membership test only where it has one. The relation it +derives for =Base r= takes the =contains= of =r= as its test, so FOL +over a substantial relation still looks tuples up by hash. The relation +it derives for a projection has no test, so its =contains= enumerates +the projection, which reads all of =book=, and compares. That ends +because =book= is finite. + +A projection of a =Countable= relation stays =Countable=. FOL still +streams it, since a projection reads one tuple at a time and never +needs the end. Asking such a projection whether it holds a tuple fails +with =undecidable-membership=. + +* Indexes +An index on an attribute =a= would be a tree keyed by the value of =a= +and the hash of the tuple, and would add the mode ={a; Finite}=. A +projection that keeps =a= keeps that mode, so with one index per +attribute every membership question could stay a lookup. That takes two +things RNT does not have, the index trees and an operation that +produces tuples under a partial binding, as [[*Reachable bindings][reachable bindings]] +explains. Without the operation, the mode an index adds would be +declared and never used. + +Modes carry no cost. A lookup and a full scan both appear as an +exhaustible generation, and choosing between them belongs to whatever +plans the query. + +* Where exhaustion matters +Only a reader that runs a relation to its end needs it exhaustible. +=Relation.read= drains a relation, and admission drains every [[file:denial.org][denial]] +that holds a tuple, so both hang on a =Countable= relation. Neither +checks modes yet. Denials will check them once they are reworked. diff --git a/docs/object-system.org b/docs/object-system.org index a2f7929..facdda0 100644 --- a/docs/object-system.org +++ b/docs/object-system.org @@ -134,7 +134,7 @@ RNT exposes its resources as a hierarchy of objects. The root of this tree is an #+end_src =register= and =unregister=, as implemented by the root of the hierarchy, allows components to register resources that can be retrieved by users of the system through the corresponding =Directory= interface. The handle passed as an argument to =register= must support being "copy"ed. -As a convenience, a =path= represents a pattern of traversal the object tree. The path ="branch" @/ "master" @/ "multigroup" @/ "universe" @/ this= represents the object that can be retrieved by, from a given reference point, "open"ing the child denoted by ="branch"= on the given reference point, then "open"ing the child denoted ="master"= on the retrieved object, and so on. Every traversal assumes that the object in question has a =Directory= protocol. The ability to construct and manipulate paths is implemented by the =Path= module: +As a convenience, a =path= represents a pattern of traversal the object tree. The path ="system" @/ "branch" @/ "master" @/ "multigroup" @/ "universe" @/ this= represents the object that can be retrieved by, from a given reference point, "open"ing the child denoted by ="system"= on the given reference point, then "open"ing the child denoted ="branch"= on the retrieved object, and so on. Every traversal assumes that the object in question has a =Directory= protocol. The ability to construct and manipulate paths is implemented by the =Path= module: #+begin_src ocaml module Path : sig type path diff --git a/docs/object-taxonomy.org b/docs/object-taxonomy.org index d948845..dda3de3 100644 --- a/docs/object-taxonomy.org +++ b/docs/object-taxonomy.org @@ -21,7 +21,9 @@ may remain invariant while the extension differs between the earlier and later states. A branch identifies one such coherent state and provides the basis -from which another may be produced. It therefore gives RNT a +from which another may be produced. Each state names the one it +succeeded, under =previous=, so the history of a branch is reached by +path. It therefore gives RNT a representation of change without requiring mutation to be part of the relational semantics. How successive states are physically represented, shared, or persisted is an implementation concern. @@ -253,6 +255,10 @@ state exposed through a branch. A branch may reference multiple multigroups and determine the particular state of each that is visible from that view of the world. +Within a multigroup, relations are grouped into schemas, which for now +are only namespaces: \multigroup\[m]\schema\[s]\relation\[r]. The +canonical name of an attribute is therefore =m:s:r:a=. + * Session A session contains state specific to an interaction between a client environment and the RNT kernel. It establishes the execution context diff --git a/docs/roadmap.org b/docs/roadmap.org new file mode 100644 index 0000000..c9d14cc --- /dev/null +++ b/docs/roadmap.org @@ -0,0 +1,137 @@ +#+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]] 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. + +* 1. Binding-aware read +Incremental checking and maintenance both ask a relation for the tuples +that agree with a partial binding, and no operation can ask that today. +A mode such as ={title; Finite}= can be declared, and nothing can act on +it. This is the [[file:modes.org::*Reachable bindings][reachable bindings]] gap, and every later step depends +on closing it. + +The step adds an operation that produces the tuples of a relation under +a binding of some of its attributes, implemented by every relation. + +- A substantial relation filters a scan until it has indexes. +- FOL passes a binding through a projection to its input when the + projection keeps the bound attributes. +- A relation that wraps a program passes the binding to the relation + the program returns. + +Membership becomes the case where every attribute is bound. + +It is done when a mode with a partial =bound= is usable, and the read +does what =Mode.generation= says it can. Two questions are open: how a +binding is represented, and what a relation does when no mode covers +the binding. Filtering a read under a smaller binding works when that +read ends, and failing as undecidable is the only other honest answer. + +* 2. Indexes +Without an index, a binding-aware read on a substantial relation still +reads the whole relation and filters it. It is correct and no faster, +and a projection still loses the lookup by hash. + +The step adds one index per attribute, a prolly tree keyed by the value +of the attribute and the hash of the tuple, written in the same +transaction as the tuple set. Each index adds the mode ={a; Finite}=, and +a projection that keeps =a= keeps it, so membership in a projection +becomes a lookup. + +It is done when a read bound on an indexed attribute reads only the +matching tuples. Two questions are open: whether indexes on combinations +of attributes are needed, and whether an index takes part in the +relation's address. It should not, since an index is derived from the +tuples. + +* 3. 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. + +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. + +* 4. 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. + +It is done when RNT gives the inserted and deleted tuples of each +relation a commit changed, at a cost proportional to the change. + +* 5. Incremental denial checking +Every commit judges every denial over the whole state. With the four +steps above, a commit can judge only what it can break. For each tuple +it inserted, it asks each denial that reads that tuple's relation for +its tuples under 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 full check stays for a commit that installs a denial, since a new +denial has no earlier emptiness to rely on, and for denials that +declare no usable mode for the binding. + +It is done when a commit that touches one relation reads only the bound +instances of the denials that read it, and its verdict equals the full +check's on the same states. + +* 6. 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. +- 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. + +* 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. +- 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. +- =Path.update= keeps the target it looks up and never releases it, so + each call leaks one reference to a counted namespace. This came with + the lifecycle rework and needs a decision. +- The signatures in [[file:object-system.org][the object system]] predate the code. |