Skip to content

Instantly share code, notes, and snippets.

@Quodss
Last active June 14, 2024 14:59
Show Gist options
  • Save Quodss/2608695c50ed2d25b9107fa45f316828 to your computer and use it in GitHub Desktop.
Save Quodss/2608695c50ed2d25b9107fa45f316828 to your computer and use it in GitHub Desktop.

UIP draft: Nock 13

Abstract

This UIP draft describes a proposal to add a new virtual Nock operator to provide manual memory management without changing the base-level Nock. I believe this would allow to greatly increase the performance for certain tasks without requiring more difficult and less fine-grained optimization techniques like atom paging.

Motivation

It would be beneficial for Nock performance to have an ability to allocate a byte buffer in order to manually manage memory in it. Other languages have similar features, where in addition to garbage-collected objects a programmer can choose to allocate some memory in order to run some algorithms faster. A recent example is ++cue implementation in JS, where the solution was (AFAIK, to check) to allocate a ByteBuffer with the jammed noun for a faster traversal. Nock 13 would give the same affordance to virtual Nock without breaking the original Nock specification. Some gates (bitwise logic, maybe arithmetics) could be rewritten with Nock 13 in order to have a reasonable performance without jets: an interpreter could fall back to "jetting Nock with Nock 13" if a jet is not available.

Specification

++bink is a virtual Nock interpreter with a ++bahn gate that allows the virtual Nock to perform reads and writes to the outer level of virtualization. ++bahn gate takes a noun and returns a pair of a noun and a new version of itself. It acts similar to ++scry gate, except that the data can flow in both directions. Some opcodes and trace handling are skipped for brevity.

Note that this gate is not designed to be a jet target for reasons described below in "Discussion" section. It is instead a building blocks for jetted gates, see ++bink-mem below.

++  bink
  |=  $:  [subject=* formula=*]
          bahn=*  ::  _|~(* [** .])
      ==
  ^-  tone
  =<  -
  |^  ^-  [tone _bahn]
  ?+    formula  [[%2 ~] bahn]
      [^ *]
    =^  head  bahn  $(formula -.formula)
    ?.  ?=(%0 -.head)  [head bahn]
    =^  tail  bahn  $(formula +.formula)
    ?.  ?=(%0 -.tail)  [tail bahn]
    [[%0 product.head product.tail] bahn]
  ::
      [%0 axis=@]
    =/  part  (frag axis.formula subject)
    ?~  part  [[%2 ~] bahn]
    [[%0 u.part] bahn]
  ::
      [%1 constant=*]
    [[%0 constant.formula] bahn]
  ::
      [%2 subject=* formula=*]
    =^  subject  bahn  $(formula subject.formula)
    ?.  ?=(%0 -.subject)  [subject bahn]
    =^  formula  bahn  $(formula formula.formula)
    ?.  ?=(%0 -.formula)  [formula bahn]
    %=  $
      subject  product.subject
      formula  product.formula
    ==
  ::
      [%3 argument=*]
    =^  argument  bahn  $(formula argument.formula)
    ?.  ?=(%0 -.argument)  [argument bahn]
    [[%0 .?(product.argument)] bahn]
  ::  (...)
  ::
      [%13 sam=*]
    =^  sam  bahn  $(formula sam.formula)
    ?.  ?=(%0 -.sam)  [sam bahn]
    =^  result  bahn  (slum bahn product.sam)
    [[%0 result] bahn]
  ==
  ::
  ++  frag
    |=  [axis=@ noun=*]
    ^-  (unit)
    ?:  =(0 axis)  ~
    |-  ^-  (unit)
    ?:  =(1 axis)  `noun
    ?@  noun  ~
    =/  pick  (cap axis)
    %=  $
      axis  (mas axis)
      noun  ?-(pick %2 -.noun, %3 +.noun)
    ==
  ::
  ++  edit
    |=  [axis=@ target=* value=*]
    ^-  (unit)
    ?:  =(1 axis)  `value
    ?@  target  ~
    =/  pick  (cap axis)
    =/  mutant
      %=  $
        axis    (mas axis)
        target  ?-(pick %2 -.target, %3 +.target)
      ==
    ?~  mutant  ~
    ?-  pick
      %2  `[u.mutant +.target]
      %3  `[-.target u.mutant]
    ==
  --

++bink-mem is a gate that specifies a ++bahn gate that models an allocated heap. ++bink-mem serves as a jet target.

++  bink-mem
  ~%  %bink-mem
  |=  [arg=[sub=* fol=*] lim=@]
  =/  mem-read   ,%1
  =/  mem-write  ,%2
  %+  bink  arg
  =+  buff=0
  |=  op=*
  =*  this-bahn  .
  ^-  [* _this-bahn]
  ?+    op  !!
      [mem-read ptr=@ len=@]
    ?>  (lth (add ptr.op len.op) lim)
    :_  this-bahn
    (cut 3 [ptr.op len.op] buff)
  ::
      [mem-write ptr=@ len=@ dat=@]
    ?>  (lth (add ptr.op len.op) lim)
    :-  ~
    this-bahn(buff (sew 3 [ptr.op len.op dat.op] buff))
  ==

Discussion

Virtual Nock jetting and memory layout

Original virtual Nock interpreter ++mink can be easily jetted by the Nock interpreter itself due to strict discipline of data: nouns in the virtual context can point outwards to the older memory, but the converse is not the case. ++scry gate read-only nature upholds this discipline.

If we want to create a two-way path for data with a ++bahn read-write gate, then the same discipline can no longer be upheld. Either ++bahn gate, which is a noun in the outer context, has to be modified there, or it needs to be copied into the inner context to be slammed and be replaced with newer versions of itself. Since ++bahn gate copy in the virtual context is initially not referenced by either the nouns in the virtual context or the nouns in the outer context, it makes it garbage by definition. Memory handling becomes error-prone.

If, however, ++bahn gate is bound within a jetted gate, then we can make assumptions about the memory layout. Consider the inner gate within ++bink-mem:

|=  op=*
=*  this-bahn  .
^-  [* _this-bahn]
?+    op  !!
    [mem-read ptr=@ len=@]
  ?>  (lth (add ptr.op len.op) lim)
  :_  this-bahn
  (cut 3 [ptr.op len.op] buff)
::
    [mem-write ptr=@ len=@ dat=@]
  ?>  (lth (add ptr.op len.op) lim)
  :-  ~
  this-bahn(buff (sew 3 [ptr.op len.op dat.op] buff))
==

It models a byte array with length len defined in the outer gate sample, and supports two operations, read and write of an atom within the allocated space.

A ++bink-mem jet could then allocate len bytes of memory before e.g. the bottom of noun heap to be used by the virtual Nock. Nock bytecode generator could inspect the formula to check if the ++bahn arguments are Nock 1 literals to directly replace Nock execution with read/write opcodes. Different versions of ++bink-mem-style gates could be made supporting different alignments and allocation styles (maybe memory-adjacent array of jammed nouns?)

0    hip rut   hat                                    ffff
|    |    |     |                                       |
|~~~~@@@@@-------##########################+++++++$~~~~~|
|                                          |      |     |
0                                         cap    mat  ffff

abs(hip - rut) == len

Pitfalls

Auto-cons parallel execution

Nock specification does not prescribe the order in which formulas b, c in *(a [b c]) are evaluated. While current interpreters do not run these formulas in parallel, in the future they could, which would create a race condition in ++bink execution. A ++bink-mem jet would have to take precautions against that:

  • order 0: always run serially
  • order 1: check Nock 13 instances. If all of them are literals and the memory locations in two subformulas form a disjoint set, run in parallel, otherwise run serially
  • order 2: accept an additional argument/hint that specifies self-prescribed segments of memory that the subformulas want to access. Run in series if the segments overlap; run in parallel otherwise, crash the entire event if a subformula reaches outside of declared segment. Print out "SEGMENTATION FAULT" to trigger PTSD of C developers.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment