ilyakooo0/urbit
1
0
Fork 0
mirror of https://github.com/ilyakooo0/urbit.git synced 2024-11-24 10:33:22 +03:00
Code Issues Packages Projects Releases Wiki Activity

Validate jet cores. Other cosmetic changes.

Browse Source
This commit is contained in:
C. Guy Yarvin 2014-11-24 14:41:47 -08:00
parent f6f4ce4624
commit d43bc56bb1
6 changed files with 213 additions and 80 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

185
Spec/u3.md
View File

@ -781,32 +781,26 @@ roads, we also nest jet state. The jet state in the road is:
In case you understand Hoon, `das` (cold state) is a `++dash`,
and `har_p` (warm state) is a map from battery to `++calx`:
++ bane ,@tas :: battery name
++ bash ,@uvH :: ctx identity hash
++ bosh ,@uvH :: local battery hash
++ batt ,* :: battery
++ calx :: cached by battery
$: jax=,@ud :: jet index
pax=,@ud :: parent axis or 0
hap=(map ,@ud ,@ud) :: axis/jet
huc=(map term nock) :: name/tool
== ::
++ chum $? lef=term :: jet name
[std=term kel=@] :: kelvin version
[ven=term pro=term kel=@] :: vendor and product
[ven=term pro=term ver=@ kel=@] :: all of the above
== ::
++ clue (trel chum nock (list (pair term nock))):: battery definition
++ clog (pair cope (map batt (map term nock))) :: identity record
++ cope (trel bane axis (each bash noun)) :: core pattern
++ dash :: jet system
$: sys=(map batt bash) :: battery/identity
haw=(map bash clog) :: identity/core
== ::
++ bane ,@tas :: battery name
++ bash ,@uvH :: ctx identity hash
++ bosh ,@uvH :: local battery hash
++ batt ,* :: battery
++ calf ::
$: jax=,@ud :: hot core index
hap=(map ,@ud ,@ud) :: axis/hot arm index
jit=* :: arbitrary data
== ::
++ calx (trel calf (pair bash cope) club) :: cached by battery
++ clog (pair cope (map batt club)) :: identity record
++ club (pair corp (map term nock)) :: battery pattern
++ cope (trel bane axis (each bash noun)) :: core pattern
++ core ,* :: core
++ corp (each core batt) :: parent or static
++ dash (map bash clog) :: jet system
The jet index in a `++calx` is an index into `ray_u` in the
dashboard - ie, a pointer into hot state. This is why the
warm state has to be reset when we reload the pier.
The jet index `jax` in a `++calx` is an index into `ray_u` in the
dashboard - ie, a pointer into hot state. This is why the warm
state has to be reset when we reload the pier in a new process.
Why is jet state nested? Nock of course is a functional system,
so as we compute we don't explicitly create state. Jet state is
@ -880,10 +874,10 @@ instance, if the core is a Hoon gate - a function - we will call
### u3j: the cold jet dashboard
For even more fun, the jet tree is not actually a tree of
batteries. Rather, *multiple batteries* may share any node in
the jet tree. For instance, it's normal to have two equivalent
Nock batteries at the same time in one pier: one battery compiled
with debugging hints, one not.
batteries. Rather, *multiple batteries* may share any location
in the jet tree. For instance, it's normal to have two
equivalent Nock batteries at the same time in one pier: one
battery compiled with debugging hints, one not.
Rather, the jet tree is a semantic hierarchy. The root of the
hierarchy is a constant, by convention the Hoon kernel version
@ -908,41 +902,67 @@ again, it's important to remember that we track jet bindings not
by the core, which may not be static, but by the battery, which
is always static.
(And if you're wondering how we can use a phat noun like a Nock
(And if you're wondering how we can use a deep noun like a Nock
formula or battery as a key in a key-value table, remember
`mug_w`, the lazily computed short hash, in all boxed nouns.)
In any case, `das`, the dashboard, contains `sys`, a map from
battery to battery identity hash (`++bash`), and `haw`, a map
from `bash` to battery record (`++clog`).
In any case, `das`, the dashboard, is a map from `bash` to jet
location record (`++clog`). A `clog` in turn contains two kinds
of information: the `++cope`, or per-location noun; and a map of
batteries to a per-battery `++club`.
A `clog` is a cell whose tail is a hook map, straight from the
user's clue. The head is a `++cope`, which is a triple of
`++bane` (battery name, right now just a `term`); `++axis`,
the axis, within *this* core, of the parent; and `(each bash
noun)`, which is either `[0 bash]` if the parent is another
core, or `[1 noun]`, for the constant noun (like `164`) if
there is no parent core.
The `cope` is a triple of `++bane` (battery name, right now just
a `term`); `++axis`, the axis, within *this* core, of the parent;
and `(each bash noun)`, which is either `[0 bash]` if the parent
is another core, or `[1 noun]`, for the constant noun (like
`164`) if there is no parent core.
A `bash` is just the noun hash (`++sham`) of a `cope`, which
uniquely expresses the battery's self-declared hierarchical
identity without depending on the actual battery code.
uniquely expresses the battery's hierarchical location without
depending on the actual formulas.
The `club` contains a `++corp`, which we use to actually validate
the core. Obviously jet execution has to be perfectly compatible
with Nock. We search on the battery, but getting the battery
right is not enough - a typical battery is dependent on its
context. For example, your jet-propelled library function is
very likely to call `++dec` or other advanced kernel technology.
If you've replaced the kernel in your context with something
else, we need to detect this and not run the jet.
There are two cases for a jet-propelled core - either the entire
core is a static constant, or it isn't. Hence the definition
of `corp`:
++ corp (each core batt) :: parent or static
Ie, a `corp` is `[0 core]` or `[1 batt]`. If it's static -
meaning that the jet only works with one specific core, ie, the
parent axis of each location in the hierarchy is `3` - we can
validate with a single comparison. Otherwise, we have to recurse
upward by checking the parent.
Note that there is at present no way to force a jet to depend on
static *data*.
### u3j: the warm jet dashboard
We don't use the cold state to match jets as we call them; we use
the cold state to register jets as we find them, and also to
We don't use the cold state to match jets as we call them. We
use the cold state to register jets as we find them, and also to
rebuild the warm state after the hot state is reset.
What we actually use at runtime is the warm state, `jed->har_p`,
which is a `u3h` (built-in hashtable), allocated on the loom,
from battery to `++calx`.
A `calx` is a quadruple of `jax`, the jet index, an index into
`ray_u` in `u3j_dash`; `pax`, the parent axis (as in
`cope` above); `hap`, a table from arm axis (ie, the axis of each
formula within the battery) to jet arm index (into `arm_u` in
`u3j_core`); and `huc`, the hook table (as in `clog`).
A `calx` is a triple of a `++calf`, a `[bash cope]` cell, and a
`club`. The latter two are all straight from cold state.
The `calf` contains data dependent on hot state. It's a triple
of `jax`, the hot jet index (in `ray_u` in `u3j_dash`); `hap`, a
table from arm axis (ie, the axis of each formula within the
battery) to jet arm index (into `arm_u` in `u3j_core`); and
`jit`, any other dynamic data that may speed up execution.
We construct `hap`, when we create the calx, by iterating through
the arms registered in the `u3j_core`. Note the way a `u3j_harm`
@ -955,6 +975,10 @@ and it would be sad to have to manage their axes by hand. To use
an `fcs_c` with a named arm, it's sufficient to make sure the
name is bound to a formula `[0 axis]` in the hook table.
`jit`, as its name suggests, is a stub where any sort of
optimization data computed on jet registration might go.
To use it, fill in the `_cj_jit()` function.
### u3j: the hot dashboard
Now it should be easy to see how we actually invoke jets. Every
@ -1031,7 +1055,8 @@ shared.
`u3w` interfaces use the same protocol as `fun_f` above: the
caller passes the entire core, which is retained if the function
returns `u3_none`, transferred otherwise.
returns `u3_none`, transferred otherwise. Why? Again, use
counts of 1 are special and precious for performance hackers.
`u3q` interfaces break the core into C arguments, *retain* noun
arguments, and *transfer* noun returns. `u3k` interfaces are the
@ -1067,7 +1092,63 @@ the macros `u3k()` and `u3z()` respectively.
Normally we create nouns through `u3i` functions, and don't call
the `u3a` allocators directly. But if you do:
One, there are *two* sets of allocators: the word-aligned alloca
One, there are *two* sets of allocators: the word-aligned
allocators and the fully-aligned (ie, malloc compatible)
allocators. For instance, on a typical OS X setup, malloc
produces 16-byte aligned results - needed for some SSE
instructions.
These allocators are *not compatible*. For 32-bit alignment
as used in nouns, call
/* u3a_walloc(): allocate storage measured in words.
*/
void*
u3a_walloc(c3_w len_w);
/* u3a_wfree(): free storage.
*/
void
u3a_wfree(void* lag_v);
/* u3a_wealloc(): word realloc.
*/
void*
u3a_wealloc(void* lag_v, c3_w len_w);
For full alignment, call:
/* u3a_malloc(): aligned storage measured in bytes.
*/
void*
u3a_malloc(size_t len_i);
/* u3a_realloc(): aligned realloc in bytes.
*/
void*
u3a_realloc(void* lag_v, size_t len_i);
/* u3a_realloc2(): gmp-shaped realloc.
*/
void*
u3a_realloc2(void* lag_v, size_t old_i, size_t new_i);
/* u3a_free(): free for aligned malloc.
*/
void
u3a_free(void* tox_v);
/* u3a_free2(): gmp-shaped free.
*/
void
u3a_free2(void* tox_v, size_t siz_i);
There are also a set of special-purpose allocators for building
atoms. When building atoms, please remember that it's incorrect
to have a high 0 word - the word length in the atom structure
must be strictly correct.
Most of its functions are
###

4
i/n/a.h
View File

@ -282,10 +282,10 @@
void*
u3a_walloc(c3_w len_w);
/* u3a_wdrop(): free storage.
/* u3a_wfree(): free storage.
*/
void
u3a_wdrop(void* lag_v);
u3a_wfree(void* lag_v);
/* u3a_wealloc(): word realloc.
*/

1
i/n/j.h
View File

@ -18,6 +18,7 @@
++ clog (pair cope (map batt club)) :: identity record
++ club (pair corp (map term nock)) :: battery pattern
++ cope (trel bane axis (each bash noun)) :: core pattern
++ core ,*
++ corp (each core batt) :: parent or static
++ dash (map bash clog) :: jet system
#endif

25
n/a.c
View File

@ -4,7 +4,6 @@
*/
#include "all.h"
/* _box_slot(): select the right free list to search for a block.
*/
c3_w
@ -397,16 +396,16 @@ u3a_wealloc(void* lag_v, c3_w len_w)
for ( i_w = 0; i_w < tiz_w; i_w++ ) {
new_w[i_w] = old_w[i_w];
}
u3a_wdrop(lag_v);
u3a_wfree(lag_v);
return new_w;
}
}
}
/* u3a_wdrop(): free storage.
/* u3a_wfree(): free storage.
*/
void
u3a_wdrop(void* tox_v)
u3a_wfree(void* tox_v)
{
u3a_box* box_u = u3a_botox(tox_v);
c3_w* box_w = (c3_w *)(void *)box_u;
@ -559,7 +558,7 @@ u3a_realloc(void* lag_v, size_t len_i)
for ( i_w = 0; i_w < tiz_w; i_w++ ) {
new_w[i_w] = old_w[i_w];
}
u3a_wdrop(org_w);
u3a_wfree(org_w);
return new_w;
}
}
@ -586,7 +585,7 @@ u3a_free(void* tox_v)
c3_w* org_w = tox_w - (pad_w + 1);
// printf("free %p %p\r\n", org_w, tox_w);
u3a_wdrop(org_w);
u3a_wfree(org_w);
}
/* u3a_free2(): gmp-shaped free.
@ -1095,14 +1094,14 @@ top:
if ( !_(u3a_is_cat(h_dog)) ) {
_me_lose_north(h_dog);
}
u3a_wdrop(dog_w);
u3a_wfree(dog_w);
if ( !_(u3a_is_cat(t_dog)) ) {
dog = t_dog;
goto top;
}
}
else {
u3a_wdrop(dog_w);
u3a_wfree(dog_w);
}
}
}
@ -1135,14 +1134,14 @@ top:
if ( !_(u3a_is_cat(h_dog)) ) {
_me_lose_south(h_dog);
}
u3a_wdrop(dog_w);
u3a_wfree(dog_w);
if ( !_(u3a_is_cat(t_dog)) ) {
dog = t_dog;
goto top;
}
}
else {
u3a_wdrop(dog_w);
u3a_wfree(dog_w);
}
}
}
@ -1504,7 +1503,7 @@ u3a_moot(c3_w* sal_w)
if ( 1 == len_w ) {
if ( _(u3a_is_cat(las_w)) ) {
u3a_wdrop(nov_w);
u3a_wfree(nov_w);
return las_w;
}
@ -1569,7 +1568,7 @@ u3a_mint(c3_w* sal_w, c3_w len_w)
/* See if we can free the slab entirely.
*/
if ( len_w == 0 ) {
u3a_wdrop(nov_w);
u3a_wfree(nov_w);
return 0;
}
@ -1577,7 +1576,7 @@ u3a_mint(c3_w* sal_w, c3_w len_w)
c3_w low_w = nov_u->buf_w[0];
if ( _(u3a_is_cat(low_w)) ) {
u3a_wdrop(nov_w);
u3a_wfree(nov_w);
return low_w;
}

10
n/h.c
View File

@ -72,7 +72,7 @@ _ch_buck_add(u3h_buck* hab_u, u3_noun kev)
bah_u->kev[i_w + 1] = hab_u->kev[i_w];
}
u3a_wdrop(hab_u);
u3a_wfree(hab_u);
return bah_u;
}
}
@ -150,7 +150,7 @@ _ch_node_add(u3h_node* han_u, c3_w lef_w, c3_w rem_w, u3_noun kev)
for ( i_w = inx_w; i_w < len_w; i_w++ ) {
nah_u->sot_w[i_w + 1] = han_u->sot_w[i_w];
}
u3a_wdrop(han_u);
u3a_wfree(han_u);
return nah_u;
}
}
@ -489,7 +489,7 @@ _ch_free_buck(u3h_buck* hab_u)
for ( i_w = 0; i_w < hab_u->len_w; i_w++ ) {
u3a_lose(hab_u->kev[i_w]);
}
u3a_wdrop(hab_u);
u3a_wfree(hab_u);
}
/* _ch_free_node(): free node.
@ -520,7 +520,7 @@ _ch_free_node(u3h_node* han_u, c3_w lef_w)
}
}
}
u3a_wdrop(han_u);
u3a_wfree(han_u);
}
/* u3h_free(): free hashtable.
@ -545,7 +545,7 @@ u3h_free(u3p(u3h_root) har_p)
_ch_free_node(han_u, 25);
}
}
u3a_wdrop(har_u);
u3a_wfree(har_u);
}
/* _ch_walk_buck(): walk bucket for gc.

68
n/j.c
View File

@ -265,12 +265,12 @@ _cj_warm_hump(c3_l jax_l, u3_noun huc)
return hap;
}
/* _cj_boil_mean(): in parent, declare a core. RETAINS.
/* _cj_hot_mean(): in parent, declare a core. RETAINS.
**
** XX bat is used only for printing, remove.
*/
static c3_l
_cj_boil_mean(c3_l par_l, u3_noun mop, u3_noun bat)
_cj_hot_mean(c3_l par_l, u3_noun mop, u3_noun bat)
{
u3j_core* par_u;
u3j_core* dev_u;
@ -291,7 +291,7 @@ _cj_boil_mean(c3_l par_l, u3_noun mop, u3_noun bat)
while ( (cop_u = &dev_u[i_l])->cos_c ) {
if ( _(u3r_sing_c(cop_u->cos_c, u3h(mop))) ) {
#if 0
fprintf(stderr, "boil: bound jet %d/%s/%s/%x\r\n",
fprintf(stderr, "hot: bound jet %d/%s/%s/%x\r\n",
cop_u->jax_l,
cop_u->cos_c,
par_u ? par_u->cos_c : "~",
@ -305,10 +305,10 @@ _cj_boil_mean(c3_l par_l, u3_noun mop, u3_noun bat)
return 0;
}
/* _cj_boil_mine(): in boiling state, declare a core. RETAINS.
/* _cj_hot_mine(): in hoting state, declare a core. RETAINS.
*/
static c3_l
_cj_boil_mine(u3_noun mop, u3_noun cor)
_cj_hot_mine(u3_noun mop, u3_noun cor)
{
u3_noun p_mop, q_mop, r_mop, hr_mop, tr_mop;
@ -327,7 +327,7 @@ _cj_boil_mine(u3_noun mop, u3_noun cor)
}
else par_l = 0;
return _cj_boil_mean(par_l, mop, u3h(cor));
return _cj_hot_mean(par_l, mop, u3h(cor));
}
}
@ -409,7 +409,7 @@ _cj_warm_ream_at(u3_noun soh, u3_noun cag)
}
else par_l = 0;
jax_l = _cj_boil_mean(par_l, mop, 0);
jax_l = _cj_hot_mean(par_l, mop, 0);
_cj_warm_ream_is(jax_l, soh, mop, sab);
return jax_l;
@ -678,6 +678,50 @@ u3j_hook(u3_noun cor,
return pro;
}
/* _cj_fine(): validate core. RETAIN.
*/
static c3_o
_cj_fine(u3_noun cup, u3_noun mop, u3_noun cor)
{
if ( c3y == u3h(cup) ) {
return u3r_sing(cor, u3t(cup));
}
else {
u3_noun par = u3t(u3t(mop));
u3_noun pax = u3h(u3t(mop));
if ( c3n == u3h(par) ) {
c3_assert(3 == pax);
return u3r_sing(u3t(par), u3t(cor));
}
else {
u3_weak pac = u3r_at(pax, cor);
if ( u3_none == pac || !_(u3du(pac)) ) {
return c3n;
}
else {
u3_weak cax = _cj_warm_fend(u3h(pac));
if ( u3_none == cax ) {
return c3n;
}
else {
c3_o pro_o;
cup = u3h(u3t(u3t(cax)));
mop = u3t(u3h(u3t(cax)));
cor = pac;
pro_o = _cj_fine(cup, mop, cor);
u3z(cax);
return pro_o;
}
}
}
}
}
/* u3j_kick(): new kick.
**
** `axe` is RETAINED by the caller; `cor` is RETAINED iff there
@ -693,12 +737,20 @@ u3j_kick(u3_noun cor, u3_noun axe)
if ( u3_none == cax ) { return u3_none; }
{
u3_noun mop = u3t(u3h(u3t(cax)));
u3_noun hap = u3h(u3t(u3h(cax)));
u3_noun cup = u3h(u3t(u3t(cax)));
u3_noun inx = u3kdb_get(u3k(hap), u3k(axe));
if ( u3_none == inx ) {
u3z(cax); return u3_none;
}
#if 1
else if ( !_(_cj_fine(cup, mop, cor)) ) {
fprintf(stderr, "improper core %x\r\n", u3r_mug(cor));
return u3_none;
}
#endif
else {
c3_l jax_l = u3h(u3h(cax));
u3j_core* cop_u = &u3D.ray_u[jax_l];
@ -815,7 +867,7 @@ _cj_mine(u3_noun cey, u3_noun cor)
// Save warm state.
//
{
c3_l jax_l = _cj_boil_mine(mop, cor);
c3_l jax_l = _cj_hot_mine(mop, cor);
u3h_put(u3R->jed.har_p,
bat,