| uip | title | description | author | status | type | category | created |
|---|---|---|---|---|---|---|---|
0115 |
Breadth-First Arvo |
Breadth-First Move Processing in the Arvo Kernel |
~wicdev-wisryt, ~rovnys-ricfer |
Draft |
Standards Track |
Kernel |
2023-08-19 |
This proposal modifies the Arvo kernel's move processing to process moves in a breadth-first order rather than the historical depth-first order. This ensures chronological move processing order, allows for a new concept of simultaneity among vane activations, and should be easier to reason about than depth-first move processing.
Large portions of this proposal are adapted or copied verbatim from ~wicdev-wisryt's original pull request from ~2022.10.7.
Breadth-first ordering guarantees that moves will be processed in the order they are emitted. Depth-first ordering constantly violates this, and in the presence of reentrancy this can cause extremely unexpected results.
The usual argument for depth-first ordering is that it feels like it should allow greater composability. In both cases, if A sends moves to B and C, then A knows that the move to B will happen before the move to C. However, in depth-first ordering, we further know that anything that B causes to happen will also happen before the move to C. This means the move to B will "fully complete", even if it delegates some of the work to another entity. Of course, this doesn't apply if B needs to send something over the wire to fully complete.
Another guarantee that depth-first ordering gives you is that the first move you send will be processed immediately, with no intervening moves. Breadth-first ordering often will process other moves that were already in the queue.
Overall, the guarantees that depth-first ordering gives are rarely useful because they can be violated in practice, while the guarantees that breadth-first ordering gives are consistent and more useful. Moves being processed out of chronological order in depth-first processing is particularly difficult to reason about and work with.
One place this comes up in the kernel is in breach handling: when Jael hears that another ship breached, ideally Ames, Clay, and Gall would all hear about the breach "simultaneoulsy", meaning none of those vanes would be able to emit moves to any of the other ones before they had all heard about the breach. Otherwise Gall might, for example, try to resynchronize with the breached ship and emit a move to Ames, but if Ames hasn't heard about the breach yet, Ames will emit moves to the stale, pre-breach version of the ship that breached, and the new moves will be lost.
Consider an example Arvo event. A keypress to Dill triggers a poke to the %hood agent, which pokes the %dojo agent. %dojo emits four %fact moves to %hood. Two of these %fact from %dojo cause %hood to give a %fact to Dill. The first %fact to Dill triggers it to give three %blit moves to Vere, and the second %fact triggers one more %blit move.
The current depth-first |verb command-line trace for this event looks like this:
["" %unix %belt /d/term/1 ~2022.10.27..06.32.09..30db]
["|" %pass [%dill %g] [[%deal [~zod ~zod] %hood %poke] /] ~[//term/1]]
["||" %give %gall [%unto %poke-ack] i=/dill t=~[//term/1]]
["||" %pass [%gall %g] [[%deal [~zod ~zod] %dojo %poke] /use/hood/0w2.efXKi/out/~zod/dojo/drum/phat/~zod/dojo] ~[/dill //term/1]]
["|||" %give %gall [%unto %poke-ack] i=/gall/use/hood/0w2.efXKi/out/~zod/dojo/drum/phat/~zod/dojo t=~[/dill //term/1]]
["|||" %give %gall [%unto %fact] i=/gall/use/hood/0w2.efXKi/out/~zod/dojo/1/drum/phat/~zod/dojo t=~[/dill //term/1]]
["||||" %give %gall [%unto %fact] i=/dill t=~[//term/1]]
["|||||" %give %dill %blit i=/gall/use/herm/0w2.efXKi/~zod/view/ t=~[/dill //term/1]]
["|||||" %give %dill %blit i=/gall/use/herm/0w2.efXKi/~zod/view/ t=~[/dill //term/1]]
["|||||" %give %dill %blit i=/gall/use/herm/0w2.efXKi/~zod/view/ t=~[/dill //term/1]]
["|||" %give %gall [%unto %fact] i=/gall/use/hood/0w2.efXKi/out/~zod/dojo/1/drum/phat/~zod/dojo t=~[/dill //term/1]]
["||||" %give %gall [%unto %fact] i=/dill t=~[//term/1]]
["|||||" %give %dill %blit i=/gall/use/herm/0w2.efXKi/~zod/view/ t=~[/dill //term/1]]
["|||" %give %gall [%unto %fact] i=/gall/use/hood/0w2.efXKi/out/~zod/dojo/1/drum/phat/~zod/dojo t=~[/dill //term/1]]
["|||" %give %gall [%unto %fact] i=/gall/use/hood/0w2.efXKi/out/~zod/dojo/1/drum/phat/~zod/dojo t=~[/dill //term/1]]
We can split this up into a few pieces to see it more clearly, adding a blank line before each time Gall processes a %fact from Dojo.
["" %unix %belt /d/term/1 ~2022.10.27..06.32.09..30db]
["|" %pass [%dill %g] [[%deal [~zod ~zod] %hood %poke] /] ~[//term/1]]
["||" %give %gall [%unto %poke-ack] i=/dill t=~[//term/1]]
["||" %pass [%gall %g] [[%deal [~zod ~zod] %dojo %poke] /use/hood/0w2.efXKi/out/~zod/dojo/drum/phat/~zod/dojo] ~[/dill //term/1]]
["|||" %give %gall [%unto %poke-ack] i=/gall/use/hood/0w2.efXKi/out/~zod/dojo/drum/phat/~zod/dojo t=~[/dill //term/1]]
["|||" %give %gall [%unto %fact] i=/gall/use/hood/0w2.efXKi/out/~zod/dojo/1/drum/phat/~zod/dojo t=~[/dill //term/1]]
["||||" %give %gall [%unto %fact] i=/dill t=~[//term/1]]
["|||||" %give %dill %blit i=/gall/use/herm/0w2.efXKi/~zod/view/ t=~[/dill //term/1]]
["|||||" %give %dill %blit i=/gall/use/herm/0w2.efXKi/~zod/view/ t=~[/dill //term/1]]
["|||||" %give %dill %blit i=/gall/use/herm/0w2.efXKi/~zod/view/ t=~[/dill //term/1]]
["|||" %give %gall [%unto %fact] i=/gall/use/hood/0w2.efXKi/out/~zod/dojo/1/drum/phat/~zod/dojo t=~[/dill //term/1]]
["||||" %give %gall [%unto %fact] i=/dill t=~[//term/1]]
["|||||" %give %dill %blit i=/gall/use/herm/0w2.efXKi/~zod/view/ t=~[/dill //term/1]]
["|||" %give %gall [%unto %fact] i=/gall/use/hood/0w2.efXKi/out/~zod/dojo/1/drum/phat/~zod/dojo t=~[/dill //term/1]]
["|||" %give %gall [%unto %fact] i=/gall/use/hood/0w2.efXKi/out/~zod/dojo/1/drum/phat/~zod/dojo t=~[/dill //term/1]]
We can see that Arvo processes everything downstream of the first %fact before processing the next %fact. Contrast this with a trace from a breadth-first version of Arvo:
["" %unix %belt /d/term/1 ~2022.10.27..06.32.57..1d2c]
["|" %pass [%dill %g] [[%deal [~zod ~zod] %hood %poke] /] ~[//term/1]]
["||" %give %gall [%unto %poke-ack] i=/dill t=~[//term/1]]
["||" %pass [%gall %g] [[%deal [~zod ~zod] %dojo %poke] /use/hood/0w3.qnAr5/out/~zod/dojo/drum/phat/~zod/dojo] ~[/dill //term/1]]
["|||" %give %gall [%unto %poke-ack] i=/gall/use/hood/0w3.qnAr5/out/~zod/dojo/drum/phat/~zod/dojo t=~[/dill //term/1]]
["|||" %give %gall [%unto %fact] i=/gall/use/hood/0w3.qnAr5/out/~zod/dojo/1/drum/phat/~zod/dojo t=~[/dill //term/1]]
["|||" %give %gall [%unto %fact] i=/gall/use/hood/0w3.qnAr5/out/~zod/dojo/1/drum/phat/~zod/dojo t=~[/dill //term/1]]
["|||" %give %gall [%unto %fact] i=/gall/use/hood/0w3.qnAr5/out/~zod/dojo/1/drum/phat/~zod/dojo t=~[/dill //term/1]]
["|||" %give %gall [%unto %fact] i=/gall/use/hood/0w3.qnAr5/out/~zod/dojo/1/drum/phat/~zod/dojo t=~[/dill //term/1]]
["||||" %give %gall [%unto %fact] i=/dill t=~[//term/1]]
["||||" %give %gall [%unto %fact] i=/dill t=~[//term/1]]
["|||||" %give %dill %blit i=/gall/use/herm/0w3.qnAr5/~zod/view/ t=~[/dill //term/1]]
["|||||" %give %dill %blit i=/gall/use/herm/0w3.qnAr5/~zod/view/ t=~[/dill //term/1]]
["|||||" %give %dill %blit i=/gall/use/herm/0w3.qnAr5/~zod/view/ t=~[/dill //term/1]]
["|||||" %give %dill %blit i=/gall/use/herm/0w3.qnAr5/~zod/view/ t=~[/dill //term/1]]
These are the same 15 lines, and they're each at the same depth, but they're in a different order. Most code we write is agnostic to this order, because there are many circumstances where this order gets inverted compared to our expectations.
The most obvious difference is that the four %facts from dojo to hood happen one right after the other instead of being mingled with other moves. If some of those intermingled moves invoked dojo (which would be a form of reentrancy) and caused dojo to emit more facts, those facts would be given to hood before the %facts which were already on the stack to be sent to hood. If this is textual output, then it will be in reverse order. The breadth-first move order fixes this problem completely by running all the facts that were issued at the same time before processing the moves that those themselves produced.
Here we can see the main advantage of depth-first ordering at work: moves are processed in the order they are emitted.
Whenever Arvo runs a vane, the vane emits a list of moves, some to the runtime and some to other vanes. A breadth-first Arvo enqueues the moves to other vanes to be run after any moves that are already enqueued; in contrast, depth-first Arvo kernels enqueue the moves from the latest vane to be run before other enqueued moves.
This is a small change to the Arvo code itself. A naive version can be done by changing only the implementation of Arvo's +emit arm to append a new list of moves to the queue rather than prepending it.
For efficiency, a simple double-ended queue data structure is used for the queue of moves, instead of a list. The data structure consists of two lists of move-lists (where each move-list, called a $plan, is the result of a vane activation): a hed list and a reversed tal list. New lists of moves are logically appended to this queue by prepending them one by one to the tal list. Moves are processed in order by reading from the hed list and popping off the first item in that list when done; if the hed list is empty, we rebalance the queue by setting hed to the reversed tal list and set tal to null.
There is also an added field to the $plan data structure, to improve the legibility of |verb debug printing.
Once Arvo uses breadth-first move processing, we could add a "tick" to Arvo that increments each time it runs a vane. This tick will be used as the case in scry requests to request data at the current tick, replacing date-based requests at now, which violate referential transparency when run multiple times within an event. Pinning the scry handler to the tick is considered out of scope for this proposal, however.
It is likely that some vanes, agents, and threads expect depth-first move processing and will behave incorrectly when run breadth-first. These cases mostly need to be found empirically, so it is crucial to exercise the system to shake out any potential bugs.
As for the migration from old to new Arvo, the normal Arvo upgrade semantics ensure that old moves will be handled in the order in which they expected to be handled. Old moves will be handled by the new Arvo with new vanes, so any downstream moves will be processed in the new breadth-first order. This is a principled way of handling the transition, and we don't expect issues to arise from the switch.
TODO: you can help improve this list by expanding it.
- Boot a fresh ship with a breadth-first kernel.
- Migrate a ship from an old depth-first kernel to a new breadth-first kernel.
- Check that a breadth-first Arvo can upgrade itself to a dummy future version.
- Ensure PKI updates can be received properly, including breach notices.
-
|installan app desk and open it in the web UI. -
|uninstallthe app,|reviveit, and check it works properly. - Exercise Gall's
%watch,%leave,%fact, and%kicklogic.
This does not meaningfully change the security model. If it does prove easier to reason about, however, then it reduces the effective security attack surface, by reducing likelihood of bugs and unexpected behaviors.
Copyright and related rights waived via CC0.