Skip to content

refcount linter - #1059

Draft
dozreg-toplud wants to merge 61 commits into
developfrom
dozreg/refcount-check
Draft

refcount linter#1059
dozreg-toplud wants to merge 61 commits into
developfrom
dozreg/refcount-check

Conversation

@dozreg-toplud

@dozreg-toplud dozreg-toplud commented Jul 9, 2026

Copy link
Copy Markdown
Contributor

This PR contains the refcount linter, comment annotations for the linter as well as some jet fixes that are also PR'd separately in #1058.

The linter itself is fully vibecoded for now and I can't guarantee that it doesn't produce false negatives (it already did on previous iterations). At some point I'll rewrite the abstract interpreter.

What I would like to understand is whether the annotation grammar is uncontroversial. The annotations are placed either on functions, blocks of code (e.g. if we transfer a noun to some persistent structure) or the entire files (e.g. to supress checks for nock.c)

TODO:

  • Reread/rewrite the abstract interpreter
  • Add checking borrowed reference correctness considering unifying equality

Depends on #1057, #1079, #1080

Prompted by ~dozreg-toplud's refcount linter, which flagged leaks in
_check, plus a hand audit of the surrounding code.  The fixes fall
into four groups.

_check helper:
* take [meta data] as two borrowed nouns instead of consing a cell at
  every call site (the cell leaked, and it silently assumed ownership
  of the borrowed sample legs); drop the leaked u3qa_dec result
* stop punning raw c3_d/c3_w values as nouns: the shape product was
  truncated through a u3_atom and compared against a noun, so any ray
  with 2^31 or more elements failed _check spuriously (and a crafted
  overflowing shape could pass it)
* compute the product with 64-bit overflow detection; an overflowed
  product cannot match the block count of a real atom, mirroring the
  Hoon exactly
* validate the bloq before calling u3r_met, which is UB at or above
  block size 37 (release builds compile the guard out); at such sizes
  any nonzero atom is one block
* bail %exit only where +check itself crashes (cell dims, improper
  shape list, zero data underflowing +dec)

wrapper/Hoon divergences (jet computed where the Nock crashes, or
vice versa, or produced a different noun):
* transpose/diag passed the whole core to _check, reading the gate's
  battery as ray metadata -- those jets unconditionally bailed %exit
  whenever they fired
* the elementwise (+add/+sub/+mul/+div/+mod), comparison
  (+gth/+gte/+lth/+lte), scalar (+add-scalar &c), +abs, and +trace
  wrappers never called _check at all, though the Hoon asserts it
* +ravel has no +check and never reads the kind, so its wrapper now
  punts (not bails) on an inconsistent ray
* +dot only asserts equal shapes outside the %i754 path; the full
  meta equality and consistency checks moved inside the %i754 case
* +mmul never compared the two rays' bloq/kind, and its gemm switch
  silently returned a zero matrix for an out-of-range bloq; it now
  punts on both
* reduction results (+cumsum/+min/+max/+dot) hard-coded shapes ~[1]
  or ~[1 1] or ~[n 1]; +scalar-to-ray gives an all-ones shape of the
  input's rank
* _set_rounding returns c3n on an unrecognized mode and callers punt,
  instead of bailing %fail

kernel bugs (wrong results, previously unobservable because the
wrapper bailed or untested):
* trace computed (dot d d) -- the sum of SQUARES of the diagonal --
  instead of (cumsum (diag a)); identity-matrix tests masked it
* transpose read and wrote with rows/columns swapped, correct only
  for square inputs, and the wrapper did not swap the result shape
* argmin/argmax returned (len - i - 1) instead of the ravel index i
* diag and abs return elements in natural order, in lockstep with
  urbit/urbit#7388, which removes the erroneous flops in +diag and
  +el-wise-op (the old +abs jet already returned natural order, so
  jetted and unjetted ships disagreed about +abs; the diag jet never
  returned at all)
* trace honors the door rounding mode; linspace fences an indirect
  count atom before using it as a raw integer
* mod (ray and scalar) rounded the quotient with a hardcoded
  round-toward-zero; +toi rounds in the door mode (7 mod 2 is -1
  under %n, not 1).  It also returned values where the Hoon crashes:
  a non-finite quotient (zero or NaN divisor) is (need ~).  And
  mod-scalar/div-scalar multiplied by a rounded 1/n instead of
  dividing -- wrong even for exact quotients (21 mod 7 gave 7,
  21/7 gave 2.9999998).  All four now divide directly, round in
  softfloat_roundingMode, and bail %exit on a non-finite quotient
* gth/gte used SoftBLAS's f_gt/f_ge macros, which are (!le)/(!lt)
  and thus TRUE whenever either operand is NaN; IEEE gt/ge are
  false.  Same disease via f_min/f_max in min/max/argmax.  All now
  use lt/le with swapped operands, which also reproduces the Hoon
  reel-fold exactly (NaN in the head is sticky, interior NaN is
  skipped, first-of-ties wins)
* range counted elements with one-shot ceil((b-a)/d), but the Hoon
  iterates x+d in the door mode, testing each sum against b -- for
  d=.0.1 the shapes disagreed outright (10 vs 11).  The kernel now
  replicates the iteration (values are the accumulated sums) and
  the wrapper takes the count from the result's block count; it
  punts on non-finite bounds/step, a zero step, or a stalled
  accumulator, where the Nock loops forever

leaks:
* the _check cell at every call site; u3qa_dec inside _check;
  _get_dims arrays in the diag/dot wrappers and trace kernel (plus
  raw c3_d dimensions used directly as nouns there); argmin/argmax
  scan buffers; linspace/range result-shape overkeeps

Verified on a fresh fake ship against the base lagoon (with the
urbit/urbit#7388 fixes applied), differentially against a de-jetted
copy of the same library: 36/36 probes agree, including transpose of
non-square, trace, diag, reduction shapes at rank 1, argmin/argmax
with NaN at and after the head, mod under %n/%u, mod-scalar and
div-scalar on exact quotients, gth/gte/lth against NaN, range with
d=.0.1 and a negative step, and add/cumsum/mod-scalar/range under
non-default rounding modes; zero-divisor mod crashes on both doors.
A 40x40 %i754 mmul runs ~3s jetted vs ~25s interpreted, confirming
the jets fire.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@dozreg-toplud

Copy link
Copy Markdown
Contributor Author

Notes from core blitz:

  • Need more clear annotation for "custom" case:
    • functions in a "custom" file are all custom unless they have some @Refcount annotations
    • a "custom" function may only be called by custom functions and functions with asserted (i.e. not checked) refcount protocol

I'll describe refcount annotation syntax here:

  • A refcount annotation starts with @Refcount:, followed by a space and a refcount directive.

  • A refcount annotation of a function may appear in the header comment of a function definition, the header comment of a function declaration, or the same line as the function declaration if it spans for just one line:

/*  @Refcount: retain
 *  (header comment)
*/
u3_noun
foo(u3_noun a)
{ ... }

u3_noun bar(u3_noun u3_noun); // @Refcount: transfer (same line for declarations is OK)
  • A refcount annotation of a code block may appear on the same line as the opening brace:
if ( condition ) {  //  @Refcount: assert transfer (this assignement consumes)
  *ptr_u = u3k(u3h(list));
}
  • A refcount annotation of a file may appear in the first 4KB of a file:
//  @Refcount: assert custom file
  • Unless there is ambiguity, @Refcount: X, Y, Z is same as:
//  @Refcount: X
//  @Refcount: Y
//  @Refcount: Z
  • The function refcount directives are applied in order top to bottom, with each directive changing the refcount protocol of the function. If there are conflicting directives then the last one wins, but a warning about conflicting directives is raised.

  • A function must have the same directives across all its declarations and its definition.

  • If a function has no directive, and the file is not custom, then its refcount protocol is governed by the rules layed out in u3.md:

    • By default it transfers its arguments and its product;
    • u3r_*, u3x_*: retain arguments and the product;
    • u3q*, u3w*, u3z_*: retain arguments, transfer the product;
    • static functions or _-named functions in jets/[a-f]/: retain args, transfer product
  • If a function has no directive, and the file is custom, the function follows "custom" transfer protocol. It can be only called by other custom functions and functions with asserted refcount protocol.

  • List of refcount directives for a function:

    • assert: the body of the function is not checked
    • assert custom: marks the function as "custom". No other directives may be present
    • transfers product: the product of the function is owned by the caller
    • transfers `x`, `y`, `z`: the function takes ownership of the listed arguments
    • transfers arguments: the function takes ownership of all arguments
    • transfers: the function takes ownership of all arguments and the product of the function is owned by the caller
    • retains ...: as transfers, mutatis mutandis: the product is an uncounted reference, arguments are borrowed
    • passthrough `x`: identity: the product IS argument x, with unchanged ownership, counts are untouched
    • direct `x`, `y`, `z`: if the function returned, these arguments were direct
    • direct product: the product is a direct atom
    • direct arguments: if the function returned, all arguments were direct
  • List of refcount directives for a code block:

    • assert transfer `x`, `y`, `z`: if these variables were assigned, that assignement consumed them. Useful for assignements to persistent data structures or in defcons patterns;
    • assert retain `x`, `y`, `z`: the block has no effect on these variables
  • List of refcount directives for a file:

    • assert custom file: marks the file as custom. Can be used in low-level parts of Vere like nock.c to supress checks, especially for tricky protocols like semitransfer.

@dozreg-toplud
dozreg-toplud force-pushed the dozreg/refcount-check branch from e44669e to 8abe4f3 Compare July 21, 2026 10:19
@dozreg-toplud
dozreg-toplud force-pushed the dozreg/refcount-check branch from 43d0e40 to ff5b07d Compare August 6, 2026 14:14
@dozreg-toplud

dozreg-toplud commented Aug 8, 2026

Copy link
Copy Markdown
Contributor Author

extended the checks to pkg/vere, added more kinds of annotations.

moar fixes (these are the important ones, others less so):

  • _unix_sync_change and _mars_do_boot overfree (the last one was legit due to structural sharing recovery hacks, we entered a subroad so the refcounting ops noop)
  • _term_it_put_value direct atom assertion
  • _lord_writ_make missing break
  • u3_unix_ef_look / _unix_update_mount - refined the type of all to be c3_o to make sure that we don't leak
  • _term_io_kick remove leak
  • u3_ames_decode_lane + u3_mesa_decode_lane removed leaks
  • _fine_hunk_scry_cb leak
  • mesa callbacks now transfer
  • _http_scry_respond fix leak

and some other leak fixes

pkova added a commit that referenced this pull request Aug 10, 2026
Contains refcount fixes found in #1059 separately, so that #1059 only
contains only refcount annotations.

Depends on #1079

---

List of fixes:
- `by_all`/`by_any` jets slammed the gate while keeping uncounted
references to `l_a` and `r_a`
- `skid`/`skim`/`skip` held uncounted reference to `i` during slam.
- `ames.c` missing `u3z` in some branches
- `http.c` missing `u3z` in some branches, callbacks retained instead of
transferring, which seems to be the protocol for callbacks
- `term.c`: leak fixes (`_reck_orchid` retains), direct atom assertion
- `unix.c` direct atom assertions
- `dawn.c` u3r_string retains, u3nc transfers (although not a big deal
right now as dawn_fail is noreturn)
- `king.c` helpers transfer
- `lord.c` missing break in switch!
- `mars.c` `jar` leak
- `pier.c` `tag` is transferred (probably left from u3r_string
transferring long time ago)
dozreg-toplud added a commit that referenced this pull request Aug 17, 2026
Cherrypicked from #1059.

I added u3_none treatment in the linter per @joemfb's request, found
some omitted checks.

Also extended the linter to check functions that neither take nor return
nouns (common for callbacks for external code), found some leaks as
well. Refcount action in eval in main.c was very confusing, I refactored
it.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants