You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Today we discussed ~dozreg-toplud's jetting strategy for his urWASM project, a WebAssembly interpreter written in Hoon. Before the meeting, ~dozreg had posted a writeup in Part I and Part II to explain his reasoning. While there are a few jetting options, there are two main ones that were discussed, and all core devs present (~master-morzod, ~fodwyt-ragful, ~ritpub-sipsyl, and myself) agreed that ~dozreg's "LIA" approach is the best option at this stage of the project.
"LIA" stands for Language for Interpreting Assembly, and it's a higher-level language, designed as an AST primarily, that represents multiple invocations of WASM from Hoon. The plan is to write and jet a Hoon function that executes a LIA expression. Since there's a top-level jet, the interpreter knows it can maintain intermediate state outside of Nock for the purposes of executing the expression faster than if it were required to stop after each step and marshal the outputs into Nock nouns -- we expect this to be especially true of any WASM interpreter state that needs to be threaded through as the WASM is invoked multiple times.
~dozreg's plan also includes adding a specialized cache to the runtime to allow WASM interpreter state to be persisted across Arvo events without the Hoon implementation of the WASM interpreter knowing any of the details of how that state is represented. The state never needs to be deoptimized into a noun. By construction, this sidesteps the problem of "shimmering" that plague systems such as Tcl where some values can have a formal data structure but also an informal optimized data structure.
It can be difficult to reason about when a value will need to be deoptimized to honor some standard interface -- the data can "shimmer" back and forth between the optimized and deoptimized representations. For large or complex values, the cost of this deoptimization can be quite severe. In Tcl, needing to convert arbitrary data structures to strings can take a lot of CPU time.
In Urbit, there have been a number of proposals over the years for "data jets". Usually an Urbit "jet" is a piece of code in the runtime that recognizes a Nock expression can be run in some way that would be faster than naively stepping through the Nock specification. So a jet is an optimized replacement for a function. By analogy, a data jet is an optimized replacement for a piece of data. If Urbit has function jets, why not also data jets?
One reason we haven't built data jets into Urbit is the shimmering issue. In Urbit, that would mean taking some optimized data structure -- say, a B-tree, or a hashtable; it's most appealing for containers that aren't easy to represent efficiently in Nock -- and defining conversions between the optimized data structure and the noun. Deoptimization corresponds to going from the optimized representation back to a noun. Unfortunately, nouns are often used as keys in maps and sets (implemented as "treap" binary search trees), in which case the "mug" short hash must be computed for that key in order to determine where the new item should be inserted into the sequence of sorted keys in the search tree. To compute the hash of a noun, you need to construct the whole noun, so for a large hashtable or other data structure, you would need to traverse the entire data structure, construct a new deoptimized version of it, and then hash that recursively -- not cheap.
~dozreg's plan avoids this by writing the Hoon in such a way that no top-level entry point into the LIA evaluator (which in turns runs a WASM interpreter, possibly more than once) ever returns an interpreter state other than a "formal state". This "formal state" is just the sequence of inputs to the LIA evaluator, as a noun -- something like a list of data structures representing LIA invocations, i.e. a list of inputs.
This can be thought of as an event log. Whenever the LIA interpreter runs an expression, the result will be added to a bespoke runtime cache. A key in this cache is one of these formal states, and the value is some jet-specific informal state that the Hoon code doesn't know about. Each time the jet for the LIA interpreter executes a new piece of WASM (well, really, any time it runs a new LIA expression, I think), it looks up the previous state of the interpreter from the runtime cache, picks up from where it left off, computes the new result, and sticks the new state in the cache.
This cache is "referentially transparent", in the sense that the value for any key can always be recomputed from the key deterministically. This is crucial for making sure the runtime's cache never requires invalidation -- only eviction, a much easier problem.
Last time I tried to use fancy math terms I got it wrong, but I believe this system is a "natural transformation" in category theory:
In this diagram, replayLIA is a function that takes in a "formal state" s_formal, a.k.a. an "event log", i.e. a list of inputs to the LIA evaluator, and runs them in order to obtain an optimized "informal state" s_informal. I expect there are also other relationships here that could be formalized mathematically, but what I like about this one is that it shows that the mapping from formal state to informal state is irreversible -- there is no inverse operation, which would correspond to deoptimization. This lack of inverse is what sidesteps the shimmering problem. I've tried to name this concept a "one-way data jet", to emphasize the irreversibility. We'll see if it sticks.
Different WASM interpreter jets could easily share the same Hoon code, which is a nice property to have and is in spirit the idea of Nock as an executable specification or policy, with jets as mechanism. It should be not only mathematically possible but also practically feasible to use a different mechanism to implement a policy. If the Hoon code included a specification of intermediate states of an optimized WASM interpreter, that would couple the policy to whatever mechanism that particular jet used.
One-way data jets could also be used for jetting other languages inside Urbit, or for other applications where optimized data formats would be useful. For WASM, in the long run, we might also want a different approach, where the Nock code represents more detail of the interpreter state formally. The biggest blocker that would make that slow now is that the memory arena for the WASM state is likely a large byte buffer intended to have lots of in-place mutations, but our current Nock interpreters would need to reallocate the entire state on every change, since they only know how to create new big atoms wholesale. An interpreter would need to break atoms into pages that could be independently mutated, in order to support efficient piecemeal mutation of big atoms. ~ritpub-sipsyl has a couple good ideas of how this could be done in Ares, and something similar but a bit less clever could also be done in Vere. Those deserve their own writeup.
The text was updated successfully, but these errors were encountered:
Today we discussed
~dozreg-toplud
's jetting strategy for his urWASM project, a WebAssembly interpreter written in Hoon. Before the meeting,~dozreg
had posted a writeup in Part I and Part II to explain his reasoning. While there are a few jetting options, there are two main ones that were discussed, and all core devs present (~master-morzod
,~fodwyt-ragful
,~ritpub-sipsyl
, and myself) agreed that~dozreg
's "LIA" approach is the best option at this stage of the project."LIA" stands for Language for Interpreting Assembly, and it's a higher-level language, designed as an AST primarily, that represents multiple invocations of WASM from Hoon. The plan is to write and jet a Hoon function that executes a LIA expression. Since there's a top-level jet, the interpreter knows it can maintain intermediate state outside of Nock for the purposes of executing the expression faster than if it were required to stop after each step and marshal the outputs into Nock nouns -- we expect this to be especially true of any WASM interpreter state that needs to be threaded through as the WASM is invoked multiple times.
~dozreg
's plan also includes adding a specialized cache to the runtime to allow WASM interpreter state to be persisted across Arvo events without the Hoon implementation of the WASM interpreter knowing any of the details of how that state is represented. The state never needs to be deoptimized into a noun. By construction, this sidesteps the problem of "shimmering" that plague systems such as Tcl where some values can have a formal data structure but also an informal optimized data structure.It can be difficult to reason about when a value will need to be deoptimized to honor some standard interface -- the data can "shimmer" back and forth between the optimized and deoptimized representations. For large or complex values, the cost of this deoptimization can be quite severe. In Tcl, needing to convert arbitrary data structures to strings can take a lot of CPU time.
In Urbit, there have been a number of proposals over the years for "data jets". Usually an Urbit "jet" is a piece of code in the runtime that recognizes a Nock expression can be run in some way that would be faster than naively stepping through the Nock specification. So a jet is an optimized replacement for a function. By analogy, a data jet is an optimized replacement for a piece of data. If Urbit has function jets, why not also data jets?
One reason we haven't built data jets into Urbit is the shimmering issue. In Urbit, that would mean taking some optimized data structure -- say, a B-tree, or a hashtable; it's most appealing for containers that aren't easy to represent efficiently in Nock -- and defining conversions between the optimized data structure and the noun. Deoptimization corresponds to going from the optimized representation back to a noun. Unfortunately, nouns are often used as keys in maps and sets (implemented as "treap" binary search trees), in which case the "mug" short hash must be computed for that key in order to determine where the new item should be inserted into the sequence of sorted keys in the search tree. To compute the hash of a noun, you need to construct the whole noun, so for a large hashtable or other data structure, you would need to traverse the entire data structure, construct a new deoptimized version of it, and then hash that recursively -- not cheap.
~dozreg
's plan avoids this by writing the Hoon in such a way that no top-level entry point into the LIA evaluator (which in turns runs a WASM interpreter, possibly more than once) ever returns an interpreter state other than a "formal state". This "formal state" is just the sequence of inputs to the LIA evaluator, as a noun -- something like a list of data structures representing LIA invocations, i.e. a list of inputs.This can be thought of as an event log. Whenever the LIA interpreter runs an expression, the result will be added to a bespoke runtime cache. A key in this cache is one of these formal states, and the value is some jet-specific informal state that the Hoon code doesn't know about. Each time the jet for the LIA interpreter executes a new piece of WASM (well, really, any time it runs a new LIA expression, I think), it looks up the previous state of the interpreter from the runtime cache, picks up from where it left off, computes the new result, and sticks the new state in the cache.
This cache is "referentially transparent", in the sense that the value for any key can always be recomputed from the key deterministically. This is crucial for making sure the runtime's cache never requires invalidation -- only eviction, a much easier problem.
Last time I tried to use fancy math terms I got it wrong, but I believe this system is a "natural transformation" in category theory:
In this diagram,
replayLIA
is a function that takes in a "formal state"s_formal
, a.k.a. an "event log", i.e. a list of inputs to the LIA evaluator, and runs them in order to obtain an optimized "informal state"s_informal
. I expect there are also other relationships here that could be formalized mathematically, but what I like about this one is that it shows that the mapping from formal state to informal state is irreversible -- there is no inverse operation, which would correspond to deoptimization. This lack of inverse is what sidesteps the shimmering problem. I've tried to name this concept a "one-way data jet", to emphasize the irreversibility. We'll see if it sticks.Different WASM interpreter jets could easily share the same Hoon code, which is a nice property to have and is in spirit the idea of Nock as an executable specification or policy, with jets as mechanism. It should be not only mathematically possible but also practically feasible to use a different mechanism to implement a policy. If the Hoon code included a specification of intermediate states of an optimized WASM interpreter, that would couple the policy to whatever mechanism that particular jet used.
One-way data jets could also be used for jetting other languages inside Urbit, or for other applications where optimized data formats would be useful. For WASM, in the long run, we might also want a different approach, where the Nock code represents more detail of the interpreter state formally. The biggest blocker that would make that slow now is that the memory arena for the WASM state is likely a large byte buffer intended to have lots of in-place mutations, but our current Nock interpreters would need to reallocate the entire state on every change, since they only know how to create new big atoms wholesale. An interpreter would need to break atoms into pages that could be independently mutated, in order to support efficient piecemeal mutation of big atoms.
~ritpub-sipsyl
has a couple good ideas of how this could be done in Ares, and something similar but a bit less clever could also be done in Vere. Those deserve their own writeup.The text was updated successfully, but these errors were encountered: