diff --git a/asm/uncommonlisp b/asm/uncommonlisp index 4f7dd9f..8a91405 100755 Binary files a/asm/uncommonlisp and b/asm/uncommonlisp differ diff --git a/asm/uncommonlisp-gc b/asm/uncommonlisp-gc index 5e479c6..19b861a 100755 Binary files a/asm/uncommonlisp-gc and b/asm/uncommonlisp-gc differ diff --git a/asm/uncommonlisp-gc.o b/asm/uncommonlisp-gc.o index 8baca04..cb6007f 100644 Binary files a/asm/uncommonlisp-gc.o and b/asm/uncommonlisp-gc.o differ diff --git a/asm/uncommonlisp.o b/asm/uncommonlisp.o index cc87865..e8838cb 100644 Binary files a/asm/uncommonlisp.o and b/asm/uncommonlisp.o differ diff --git a/asm/uncommonlisp.s b/asm/uncommonlisp.s index 44458c7..4adfb83 100644 --- a/asm/uncommonlisp.s +++ b/asm/uncommonlisp.s @@ -450,8 +450,29 @@ sym_hash_buckets: .skip 8192 # 1024 * 8 bytes .ifdef GC_NAIVE # ─────────────────────────────────────────────────────────── # Naive mark-and-sweep GC state (control group for bench). -# Every heap block carries an 8-byte header: (size << 1) | mark. +# Every heap block carries an 8-byte header: +# bit 0 = mark +# bits 1–7 = reserved +# bits 8–15 = type byte (HT_PAIR, HT_CLOSURE, …) +# bits 16–63 = payload size in bytes # The tagged pointer still points at the payload (header at -8). +# The type byte lets mark / sweep / arena walkers dispatch +# precisely instead of guessing from block size — earlier versions +# had to reject 24-byte strings-masquerading-as-env-nodes via +# TAG_SYM checks at offset 0, and 40-byte strings masquerading +# as vectors via a length-fits-block check. Type byte kills the +# entire class of bugs. +.equ HT_FREE, 0 # not used during normal ops (0 = unknown / free) +.equ HT_PAIR, 1 +.equ HT_CLOSURE, 2 +.equ HT_STRING, 3 +.equ HT_SYMBOL, 4 +.equ HT_VECTOR, 5 +.equ HT_HASHTABLE, 6 +.equ HT_HASHSET, 7 +.equ HT_ENVNODE, 8 +.equ HT_CHAINNODE, 9 +.equ HT_PADDING, 10 # Chunks are tracked in a side array so chunk memory stays pure # allocation space. Free blocks are linked via a global list # whose nodes reuse the header word as size and the first 8 bytes @@ -692,7 +713,7 @@ heap_alloc: cmpq %r13, %rcx ja .ha_overflow movq %rbx, %rdx - shlq $1, %rdx # header = size << 1, mark=0 + shlq $16, %rdx # header = (size << 16) | (type<<8) | mark; caller patches type movq %rdx, (%r15) movq %r15, %rax addq $8, %rax # payload ptr @@ -725,7 +746,7 @@ heap_alloc: cmpq %r13, %rcx ja .ha_grow movq %rbx, %rdx - shlq $1, %rdx + shlq $16, %rdx movq %rdx, (%r15) movq %r15, %rax addq $8, %rax @@ -744,7 +765,8 @@ heap_alloc: movq %rax, %rdx subq $8, %rdx # padding payload size movq %rdx, %rcx - shlq $1, %rcx # header, mark=0 + shlq $16, %rcx # header; type will be patched to HT_PADDING below + orq $(HT_PADDING << 8), %rcx movq %rcx, (%r15) # Link onto free list directly so sweep doesn't need to know. movq gc_free_list(%rip), %rcx @@ -785,7 +807,7 @@ gc_freelist_alloc: testq %rax, %rax jz .gfa_empty movq (%rax), %rdx # header - shrq $1, %rdx # block payload size + shrq $16, %rdx # block payload size (bits 16..63) cmpq %rdi, %rdx jb .gfa_next # Fits. Unlink. @@ -807,14 +829,17 @@ gc_freelist_alloc: leaq 8(%rax,%rdi), %r9 # tail header addr subq $8, %r8 movq %r8, %r10 - shlq $1, %r10 # mark=0 + shlq $16, %r10 # tail header, type=0 (free), mark=0 movq %r10, (%r9) movq gc_free_list(%rip), %r11 movq %r11, 8(%r9) movq %r9, gc_free_list(%rip) - # Shrink current block's header. + # Shrink current block's header — keep its type byte, just resize. + movq (%rax), %r10 # old header + andq $0xff00, %r10 # keep type byte; drop old size+mark movq %rdi, %rdx - shlq $1, %rdx + shlq $16, %rdx + orq %r10, %rdx # new header: new size + old type movq %rdx, (%rax) .gfa_return_whole: addq $8, %rax # payload ptr @@ -1011,19 +1036,11 @@ gc_mark_env: popq %rdi testq %rcx, %rcx jz .gme_end - # Block's header payload-size must be 24 AND offset 0 must be - # a tagged symbol. Env nodes are (sym, val, parent); strings - # and closures are also 24 bytes when they happen to land at - # that size, so a bare size check treats them as env and the - # walker corrupts the heap by reading string bytes as env - # fields. Demanding TAG_SYM at offset 0 disambiguates. - movq -8(%rdi), %rax - shrq $1, %rax - cmpq $24, %rax - jne .gme_end - movq (%rdi), %rax - andq $7, %rax - cmpq $TAG_SYM, %rax + # Precise type dispatch: we want HT_ENVNODE exactly. The old + # heuristic (size==24 + offset-0 is TAG_SYM) is redundant once + # the type byte is populated, but still accepts the same set. + movzbq -7(%rdi), %rax # header byte 1 (type byte) + cmpq $HT_ENVNODE, %rax jne .gme_end # Already marked? Skip. testq $1, -8(%rdi) @@ -1113,7 +1130,10 @@ gc_push_if_heap: ret # gc_mark_drain: pop tagged values from mark stack, set header -# mark, push children based on tag. Loop until empty. +# mark, push children based on the TYPE BYTE in the header (bits +# 8..15). Dispatching by type instead of by tagged-value tag +# eliminates the class of bugs where a tag-7 value (stack scan +# false positive) had to be disambiguated by guessing from size. gc_mark_drain: .gmd_top: movq gc_mark_depth(%rip), %rcx @@ -1122,23 +1142,24 @@ gc_mark_drain: decq %rcx movq %rcx, gc_mark_depth(%rip) leaq gc_mark_stack(%rip), %rsi - movq (%rsi,%rcx,8), %rbx # tagged value (callee-save keeps it safe) + movq (%rsi,%rcx,8), %rbx # tagged value movq %rbx, %rsi andq $-8, %rsi # untagged ptr - # If already marked, skip. testq $1, -8(%rsi) - jnz .gmd_top - orq $1, -8(%rsi) # mark header - # Dispatch by tag. - movq %rbx, %rax - andq $TAG_MASK, %rax - cmpq $TAG_PAIR, %rax + jnz .gmd_top # already marked + orq $1, -8(%rsi) # mark + movzbq -7(%rsi), %rax # type byte + cmpq $HT_PAIR, %rax je .gmd_pair - cmpq $TAG_CLOSURE, %rax + cmpq $HT_CLOSURE, %rax je .gmd_closure - cmpq $7, %rax - je .gmd_vec7 - # STRING / SYM: no children. + cmpq $HT_VECTOR, %rax + je .gmd_vector + cmpq $HT_HASHTABLE, %rax + je .gmd_hash + cmpq $HT_HASHSET, %rax + je .gmd_hash + # HT_STRING / HT_SYMBOL / HT_CHAINNODE / HT_PADDING / HT_FREE: no children jmp .gmd_top .gmd_pair: movq (%rsi), %rdi @@ -1161,29 +1182,10 @@ gc_mark_drain: movq 16(%rsi), %rdi call gc_mark_env # env field is an untagged env chain jmp .gmd_top -.gmd_vec7: - # Block size from header. The conservative stack scan can push - # any value whose low 3 bits happen to equal 7; that untagged - # "pointer" might land in a chunk but belong to a string or - # closure, not an actual vector. Validate size against the - # claimed length/layout before walking — otherwise a 40-byte - # string misinterpreted as a 25-element vector reads 200 bytes - # past itself and corrupts marks on adjacent blocks. - movq -8(%rsi), %rax - shrq $1, %rax # block payload size - movq (%rsi), %rdx # first word: length or -1 or -2 - cmpq $-2, %rdx - je .gmd_ht_check - cmpq $-1, %rdx - je .gmd_ht_check - testq %rdx, %rdx - js .gmd_top # other negatives = not ours - # Vector: length must fit: 8 + length*8 <= block_size - movq %rdx, %rcx - shlq $3, %rcx - addq $8, %rcx - cmpq %rax, %rcx - ja .gmd_top # length too large for block +.gmd_vector: + # Vector: first word = length, elements at offset 8. + # Type byte already confirmed it's a real vector, no size guesswork. + movq (%rsi), %rdx # length xorq %r8, %r8 .gmd_vec_loop: cmpq %rdx, %r8 @@ -1199,19 +1201,9 @@ gc_mark_drain: incq %r8 jmp .gmd_vec_loop -.gmd_ht_check: - # Hash-table (-1) or hash-set (-2): require block size >= 24 - # (header) + nbuckets * 8. nbuckets at offset 16. - cmpq $24, %rax - jb .gmd_top +.gmd_hash: + # Hash-table or hash-set: nbuckets at offset 16, buckets at 24+. movq 16(%rsi), %rcx # nbuckets - testq %rcx, %rcx - js .gmd_top # garbage - movq %rcx, %rdx - shlq $3, %rdx - addq $24, %rdx - cmpq %rax, %rdx - ja .gmd_top # nbuckets too large xorq %r8, %r8 .gmd_ht_loop: cmpq %rcx, %r8 @@ -1257,7 +1249,7 @@ gc_sweep: jae .gsw_next_chunk movq (%rbx), %rsi # header movq %rsi, %r11 - shrq $1, %r11 # payload size + shrq $16, %r11 # payload size (bits 16..63) testq $1, %rsi jz .gsw_dead # Live: clear mark. @@ -1334,6 +1326,9 @@ make_pair: call heap_alloc popq %rsi popq %rdi +.ifdef GC_NAIVE + orq $(HT_PAIR << 8), -8(%rax) +.endif movq %rdi, (%rax) movq %rsi, 8(%rax) orq $TAG_PAIR, %rax @@ -1349,6 +1344,9 @@ make_closure: popq %rdx popq %rsi popq %rdi +.ifdef GC_NAIVE + orq $(HT_CLOSURE << 8), -8(%rax) +.endif movq %rdi, (%rax) # params movq %rsi, 8(%rax) # body movq %rdx, 16(%rax) # env @@ -1376,6 +1374,9 @@ env_define: popq %rdx popq %rsi popq %rdi +.ifdef GC_NAIVE + orq $(HT_ENVNODE << 8), -8(%rax) +.endif movq %rdi, (%rax) movq %rsi, 8(%rax) movq %rdx, 16(%rax) @@ -1503,6 +1504,9 @@ intern_symbol: # Use the stack to save sym_ptr across the second heap_alloc. leaq 1(%r12), %rdi call heap_alloc +.ifdef GC_NAIVE + orq $(HT_SYMBOL << 8), -8(%rax) +.endif # %rax = sym_ptr; fill symbol: length byte + chars movb %r12b, (%rax) xorq %r8, %r8 @@ -1524,6 +1528,9 @@ intern_symbol: # Allocate hash chain node: 16 bytes [sym_ptr, next_ptr] movq $16, %rdi call heap_alloc +.ifdef GC_NAIVE + orq $(HT_CHAINNODE << 8), -8(%rax) +.endif # Fill chain node: %rax = node_ptr, stack top = sym_ptr popq %rcx # rcx = sym_ptr movq %rcx, (%rax) # node->sym = sym_ptr @@ -1879,6 +1886,9 @@ scheme_read: pushq %rbx leaq 8(%rbx), %rdi call heap_alloc +.ifdef GC_NAIVE + orq $(HT_STRING << 8), -8(%rax) +.endif popq %rbx movq %rbx, (%rax) # 8-byte length xorq %rcx, %rcx @@ -4279,12 +4289,18 @@ bi_strref: movq %rax, %rcx # string ptr GETARG %rax # index sarq $3, %rax - movzbl 8(%rcx,%rax,1), %edi # byte at offset - # Return as 1-char string - movq %r15, %rax - movq $1, (%r15) # length - movb %dil, 8(%r15) - addq $16, %r15 + movzbl 8(%rcx,%rax,1), %r8d # byte at offset (keep across heap_alloc call) + # Allocate a 1-char string via heap_alloc so the GC build sees + # a proper header / type byte instead of a headerless direct bump. + movq $9, %rdi # 8B length + 1B char + pushq %r8 + call heap_alloc + popq %r8 +.ifdef GC_NAIVE + orq $(HT_STRING << 8), -8(%rax) +.endif + movq $1, (%rax) # length + movb %r8b, 8(%rax) orq $TAG_STRING, %rax RET_VAL @@ -4313,6 +4329,9 @@ bi_strappend: movq %rcx, %rdi addq $8, %rdi call heap_alloc +.ifdef GC_NAIVE + orq $(HT_STRING << 8), -8(%rax) +.endif movq %rax, %rbp # string object base movq %rbx, (%rbp) # store length leaq 8(%rbp), %r9 # dest cursor @@ -4406,6 +4425,9 @@ bi_numtostr: movq %rcx, %rdi addq $8, %rdi call heap_alloc +.ifdef GC_NAIVE + orq $(HT_STRING << 8), -8(%rax) +.endif popq %rcx popq %rdi movq %rcx, (%rax) # length @@ -4601,13 +4623,20 @@ bi_vector: movq 8(%rdx), %rax jmp .bvec_count .bvec_alloc: - # Allocate: 8 bytes length + 8*count bytes - movq %r15, %rax # vector obj - movq %rcx, (%r15) # length - leaq 8(%r15,%rcx,8), %r15 + # Allocate via heap_alloc so GC build gets a header + type byte. + pushq %rdi # save arg list ptr + pushq %rcx # save count + leaq 8(,%rcx,8), %rdi # 8 (length) + count * 8 + call heap_alloc +.ifdef GC_NAIVE + orq $(HT_VECTOR << 8), -8(%rax) +.endif + popq %rcx + popq %rdi # restore arg list + movq %rcx, (%rax) # length # Fill elements from arg list - movq %rdi, %rdx # arg list - leaq 8(%rax), %rdi # elements start + movq %rdi, %rdx # arg list + leaq 8(%rax), %rdi # elements start .bvec_fill: cmpq $VAL_NIL, %rdx je .bvec_done2 @@ -4627,15 +4656,21 @@ bi_vector: bi_makevec: # (make-vector n fill) — allocate n-slot vector filled with `fill`. - # GETARG uses %rax as scratch, so we MUST stash the length in a - # callee-safe register before consuming the second arg. GETARG %rax sarq $3, %rax # n (untagged) movq %rax, %rdx # save n in %rdx — survives next GETARG GETARG %rcx # fill value (tagged) - movq %r15, %rax # vector obj pointer - movq %rdx, (%r15) # store length - leaq 8(%r15,%rdx,8), %r15 # advance heap past length + n*8 bytes + # Route through heap_alloc so GC build gets header + type. + pushq %rdx # n + pushq %rcx # fill value + leaq 8(,%rdx,8), %rdi # bytes: 8 (length) + n*8 + call heap_alloc +.ifdef GC_NAIVE + orq $(HT_VECTOR << 8), -8(%rax) +.endif + popq %rcx # fill + popq %rdx # n + movq %rdx, (%rax) # store length leaq 8(%rax), %rdi # elements start movq %rdx, %rsi # count = n .bmv_fill: @@ -4725,11 +4760,18 @@ bi_listtovec: movq 8(%rdx), %rax jmp .bl2v_count .bl2v_alloc: - movq %r15, %rax - movq %rcx, (%r15) - leaq 8(%r15,%rcx,8), %r15 - leaq 8(%rax), %rdi - movq %rsi, %rdx + pushq %rsi # save list ptr + pushq %rcx # save count + leaq 8(,%rcx,8), %rdi # 8 + count*8 + call heap_alloc +.ifdef GC_NAIVE + orq $(HT_VECTOR << 8), -8(%rax) +.endif + popq %rcx + popq %rsi + movq %rcx, (%rax) # length + leaq 8(%rax), %rdi # element cursor + movq %rsi, %rdx # list cursor .bl2v_fill: cmpq $VAL_NIL, %rdx je .bl2v_done @@ -4755,11 +4797,24 @@ bi_substr: GETARG %rax # end sarq $3, %rax subq %rcx, %rax # length = end - start - movq %r15, %rdx # result - movq %rax, (%r15) # length - leaq 8(%r15), %rsi # dest - leaq 8(%rdi,%rcx,1), %rdi # src - movq %rax, %rcx + # Allocate via heap_alloc: 8 (length word) + length bytes. + pushq %rdi # src base + pushq %rcx # start offset + pushq %rax # length + movq %rax, %rdi + addq $8, %rdi # total payload + call heap_alloc +.ifdef GC_NAIVE + orq $(HT_STRING << 8), -8(%rax) +.endif + popq %rdx # length (restore) + popq %rcx # start + popq %rdi # src base + movq %rdx, (%rax) # write length + leaq 8(%rax), %rsi # dest cursor + leaq 8(%rdi,%rcx,1), %rdi # src cursor + movq %rdx, %rcx # bytes to copy + movq %rax, %rdx # save result base .bsub_copy: testq %rcx, %rcx jz .bsub_done @@ -4770,11 +4825,6 @@ bi_substr: decq %rcx jmp .bsub_copy .bsub_done: - movq (%rdx), %rax # length - addq $8, %rax - addq $7, %rax - andq $-8, %rax - addq %rax, %r15 movq %rdx, %rax orq $TAG_STRING, %rax RET_VAL @@ -5296,6 +5346,9 @@ bi_file_to_string: movq %rbp, %rdi addq $8, %rdi call heap_alloc # %rax = ptr +.ifdef GC_NAIVE + orq $(HT_STRING << 8), -8(%rax) +.endif movq %rax, %r12 # save heap pointer movq %rbp, (%r12) # store length @@ -5430,6 +5483,9 @@ bi_symbol_to_string: movq %rcx, %rdi addq $8, %rdi # cell size: 8-byte length + bytes call heap_alloc +.ifdef GC_NAIVE + orq $(HT_STRING << 8), -8(%rax) +.endif popq %r8 popq %rcx @@ -5548,6 +5604,9 @@ ht_chain_find: bi_make_hash_table: movq $HT_TOTAL_BYTES, %rdi call heap_alloc +.ifdef GC_NAIVE + orq $(HT_HASHTABLE << 8), -8(%rax) +.endif movq $HT_SENTINEL, (%rax) movq $0, 8(%rax) # count movq $HT_NBUCKETS, 16(%rax) @@ -5928,6 +5987,9 @@ hs_chain_find: bi_make_hash_set: movq $HT_TOTAL_BYTES, %rdi call heap_alloc +.ifdef GC_NAIVE + orq $(HT_HASHSET << 8), -8(%rax) +.endif movq $HS_SENTINEL, (%rax) movq $0, 8(%rax) movq $HT_NBUCKETS, 16(%rax) @@ -6331,7 +6393,7 @@ arena_verify_and_commit: movq (%rbx), %rax testq $1, %rax jnz .avc_escape - shrq $1, %rax + shrq $16, %rax leaq 8(%rbx,%rax), %rbx jmp .avc_scan .avc_safe: @@ -6626,6 +6688,9 @@ bi_tcp_recv: movq %rbp, %rdi addq $8, %rdi call heap_alloc +.ifdef GC_NAIVE + orq $(HT_STRING << 8), -8(%rax) +.endif movq %rax, %r12 # string object base # read(fd, cell+8, size) diff --git a/whitepaper/uncommonlisp-whitepaper.pdf b/whitepaper/uncommonlisp-whitepaper.pdf index 8715dcb..0f831de 100644 --- a/whitepaper/uncommonlisp-whitepaper.pdf +++ b/whitepaper/uncommonlisp-whitepaper.pdf @@ -3,7 +3,7 @@ 1 0 obj << /F1 2 0 R /F2 4 0 R /F3 5 0 R /F4 6 0 R /F5 10 0 R /F6 14 0 R - /F7 30 0 R /F8 32 0 R /F9 35 0 R + /F7 30 0 R /F8 32 0 R /F9 36 0 R >> endobj 2 0 obj @@ -62,7 +62,7 @@ endobj endobj 11 0 obj << -/Annots [ 7 0 R 8 0 R 9 0 R ] /Contents 130 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 129 0 R /Resources << +/Annots [ 7 0 R 8 0 R 9 0 R ] /Contents 131 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 130 0 R /Resources << /Font 1 0 R /ProcSet [ /PDF /Text /ImageB /ImageC /ImageI ] /XObject << /FormXob.d3ecd28ca03f587d6940049748681018 3 0 R >> @@ -74,7 +74,7 @@ endobj endobj 12 0 obj << -/Contents 131 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 129 0 R /Resources << +/Contents 132 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 130 0 R /Resources << /Font 1 0 R /ProcSet [ /PDF /Text /ImageB /ImageC /ImageI ] >> /Rotate 0 /Trans << @@ -97,7 +97,7 @@ endobj endobj 15 0 obj << -/Contents 132 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 129 0 R /Resources << +/Contents 133 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 130 0 R /Resources << /Font 1 0 R /ProcSet [ /PDF /Text /ImageB /ImageC /ImageI ] /XObject << /FormXob.a2c922509fa3b1785bcd08461c0457b3 13 0 R >> @@ -109,7 +109,7 @@ endobj endobj 16 0 obj << -/Contents 133 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 129 0 R /Resources << +/Contents 134 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 130 0 R /Resources << /Font 1 0 R /ProcSet [ /PDF /Text /ImageB /ImageC /ImageI ] >> /Rotate 0 /Trans << @@ -119,7 +119,7 @@ endobj endobj 17 0 obj << -/Contents 134 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 129 0 R /Resources << +/Contents 135 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 130 0 R /Resources << /Font 1 0 R /ProcSet [ /PDF /Text /ImageB /ImageC /ImageI ] >> /Rotate 0 /Trans << @@ -129,7 +129,7 @@ endobj endobj 18 0 obj << -/Contents 135 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 129 0 R /Resources << +/Contents 136 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 130 0 R /Resources << /Font 1 0 R /ProcSet [ /PDF /Text /ImageB /ImageC /ImageI ] >> /Rotate 0 /Trans << @@ -139,7 +139,7 @@ endobj endobj 19 0 obj << -/Contents 136 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 129 0 R /Resources << +/Contents 137 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 130 0 R /Resources << /Font 1 0 R /ProcSet [ /PDF /Text /ImageB /ImageC /ImageI ] >> /Rotate 0 /Trans << @@ -149,7 +149,7 @@ endobj endobj 20 0 obj << -/Contents 137 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 129 0 R /Resources << +/Contents 138 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 130 0 R /Resources << /Font 1 0 R /ProcSet [ /PDF /Text /ImageB /ImageC /ImageI ] >> /Rotate 0 /Trans << @@ -191,7 +191,7 @@ Gb"0;!=8`+$j31%en endobj 25 0 obj << -/Contents 138 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 129 0 R /Resources << +/Contents 139 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 130 0 R /Resources << /Font 1 0 R /ProcSet [ /PDF /Text /ImageB /ImageC /ImageI ] /XObject << /FormXob.6378944cfcd9d967b8dea9d1fdf81282 21 0 R /FormXob.914f0cd152b732307eb1a2bfb0d863fa 23 0 R >> @@ -203,7 +203,7 @@ endobj endobj 26 0 obj << -/Contents 139 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 129 0 R /Resources << +/Contents 140 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 130 0 R /Resources << /Font 1 0 R /ProcSet [ /PDF /Text /ImageB /ImageC /ImageI ] >> /Rotate 0 /Trans << @@ -229,7 +229,7 @@ Gb"-V$![tprs/%kVg[G]8def./P7Hpb+:.UemqF`fg8QAVF'*,<$Kl#'U!md[DeE%MedO?I4&91M?!Bo endobj 29 0 obj << -/Contents 140 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 129 0 R /Resources << +/Contents 141 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 130 0 R /Resources << /Font 1 0 R /ProcSet [ /PDF /Text /ImageB /ImageC /ImageI ] /XObject << /FormXob.873240933f8ffe126f95df55e941dd3a 27 0 R /FormXob.ac4d2a97676ca8c002b2001987b87b9d 28 0 R >> @@ -246,7 +246,7 @@ endobj endobj 31 0 obj << -/Contents 141 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 129 0 R /Resources << +/Contents 142 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 130 0 R /Resources << /Font 1 0 R /ProcSet [ /PDF /Text /ImageB /ImageC /ImageI ] >> /Rotate 0 /Trans << @@ -261,7 +261,7 @@ endobj endobj 33 0 obj << -/Contents 142 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 129 0 R /Resources << +/Contents 143 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 130 0 R /Resources << /Font 1 0 R /ProcSet [ /PDF /Text /ImageB /ImageC /ImageI ] >> /Rotate 0 /Trans << @@ -271,7 +271,7 @@ endobj endobj 34 0 obj << -/Contents 143 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 129 0 R /Resources << +/Contents 144 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 130 0 R /Resources << /Font 1 0 R /ProcSet [ /PDF /Text /ImageB /ImageC /ImageI ] >> /Rotate 0 /Trans << @@ -281,12 +281,7 @@ endobj endobj 35 0 obj << -/BaseFont /ZapfDingbats /Name /F9 /Subtype /Type1 /Type /Font ->> -endobj -36 0 obj -<< -/Contents 144 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 129 0 R /Resources << +/Contents 145 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 130 0 R /Resources << /Font 1 0 R /ProcSet [ /PDF /Text /ImageB /ImageC /ImageI ] >> /Rotate 0 /Trans << @@ -294,9 +289,14 @@ endobj /Type /Page >> endobj +36 0 obj +<< +/BaseFont /ZapfDingbats /Name /F9 /Subtype /Type1 /Type /Font +>> +endobj 37 0 obj << -/Contents 145 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 129 0 R /Resources << +/Contents 146 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 130 0 R /Resources << /Font 1 0 R /ProcSet [ /PDF /Text /ImageB /ImageC /ImageI ] >> /Rotate 0 /Trans << @@ -306,7 +306,7 @@ endobj endobj 38 0 obj << -/Contents 146 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 129 0 R /Resources << +/Contents 147 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 130 0 R /Resources << /Font 1 0 R /ProcSet [ /PDF /Text /ImageB /ImageC /ImageI ] >> /Rotate 0 /Trans << @@ -316,7 +316,7 @@ endobj endobj 39 0 obj << -/Contents 147 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 129 0 R /Resources << +/Contents 148 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 130 0 R /Resources << /Font 1 0 R /ProcSet [ /PDF /Text /ImageB /ImageC /ImageI ] >> /Rotate 0 /Trans << @@ -326,7 +326,7 @@ endobj endobj 40 0 obj << -/Contents 148 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 129 0 R /Resources << +/Contents 149 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 130 0 R /Resources << /Font 1 0 R /ProcSet [ /PDF /Text /ImageB /ImageC /ImageI ] >> /Rotate 0 /Trans << @@ -336,7 +336,7 @@ endobj endobj 41 0 obj << -/Contents 149 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 129 0 R /Resources << +/Contents 150 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 130 0 R /Resources << /Font 1 0 R /ProcSet [ /PDF /Text /ImageB /ImageC /ImageI ] >> /Rotate 0 /Trans << @@ -348,12 +348,12 @@ endobj << /A << /S /URI /Type /Action /URI (mailto:russell@unturf.com) ->> /Border [ 0 0 0 ] /Rect [ 248.0736 593.8236 334.3536 605.8236 ] /Subtype /Link /Type /Annot +>> /Border [ 0 0 0 ] /Rect [ 248.0736 137.4236 334.3536 149.4236 ] /Subtype /Link /Type /Annot >> endobj 43 0 obj << -/Annots [ 42 0 R ] /Contents 150 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 129 0 R /Resources << +/Annots [ 42 0 R ] /Contents 151 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 130 0 R /Resources << /Font 1 0 R /ProcSet [ /PDF /Text /ImageB /ImageC /ImageI ] >> /Rotate 0 /Trans << @@ -387,7 +387,7 @@ Gb"-VGBahP*ld_dH@X@.673m]5Z!>/OUajVKd+rl%FU.GOCIDSUkBirLgj0l#UggK9*dsQ$&!I6Uj!Oc endobj 47 0 obj << -/Contents 151 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 129 0 R /Resources << +/Contents 152 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 130 0 R /Resources << /Font 1 0 R /ProcSet [ /PDF /Text /ImageB /ImageC /ImageI ] /XObject << /FormXob.02a72be19fedaa76bd1061921e7cc82b 46 0 R /FormXob.baaa2211732baa0f94f6912a5b035550 44 0 R >> @@ -399,7 +399,7 @@ endobj endobj 48 0 obj << -/Contents 152 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 129 0 R /Resources << +/Contents 153 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 130 0 R /Resources << /Font 1 0 R /ProcSet [ /PDF /Text /ImageB /ImageC /ImageI ] >> /Rotate 0 /Trans << @@ -409,7 +409,7 @@ endobj endobj 49 0 obj << -/Contents 153 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 129 0 R /Resources << +/Contents 154 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 130 0 R /Resources << /Font 1 0 R /ProcSet [ /PDF /Text /ImageB /ImageC /ImageI ] >> /Rotate 0 /Trans << @@ -427,7 +427,7 @@ Gb",k#?V^BhM4rA',+)6h&$gSeal+> @@ -439,7 +439,7 @@ endobj endobj 52 0 obj << -/Contents 155 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 129 0 R /Resources << +/Contents 156 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 130 0 R /Resources << /Font 1 0 R /ProcSet [ /PDF /Text /ImageB /ImageC /ImageI ] >> /Rotate 0 /Trans << @@ -463,7 +463,7 @@ endobj endobj 55 0 obj << -/Annots [ 53 0 R 54 0 R ] /Contents 156 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 129 0 R /Resources << +/Annots [ 53 0 R 54 0 R ] /Contents 157 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 130 0 R /Resources << /Font 1 0 R /ProcSet [ /PDF /Text /ImageB /ImageC /ImageI ] >> /Rotate 0 /Trans << @@ -473,7 +473,7 @@ endobj endobj 56 0 obj << -/Contents 157 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 129 0 R /Resources << +/Contents 158 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 130 0 R /Resources << /Font 1 0 R /ProcSet [ /PDF /Text /ImageB /ImageC /ImageI ] >> /Rotate 0 /Trans << @@ -497,7 +497,7 @@ endobj endobj 59 0 obj << -/Annots [ 57 0 R 58 0 R ] /Contents 158 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 129 0 R /Resources << +/Annots [ 57 0 R 58 0 R ] /Contents 159 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 130 0 R /Resources << /Font 1 0 R /ProcSet [ /PDF /Text /ImageB /ImageC /ImageI ] >> /Rotate 0 /Trans << @@ -521,7 +521,7 @@ endobj endobj 62 0 obj << -/Annots [ 60 0 R 61 0 R ] /Contents 159 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 129 0 R /Resources << +/Annots [ 60 0 R 61 0 R ] /Contents 160 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 130 0 R /Resources << /Font 1 0 R /ProcSet [ /PDF /Text /ImageB /ImageC /ImageI ] >> /Rotate 0 /Trans << @@ -547,7 +547,7 @@ Gb"0;0`_7S!5bE.WFlYNTE"rlzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzzz endobj 65 0 obj << -/Contents 160 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 129 0 R /Resources << +/Contents 161 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 130 0 R /Resources << /Font 1 0 R /ProcSet [ /PDF /Text /ImageB /ImageC /ImageI ] /XObject << /FormXob.d3ecd28ca03f587d6940049748681018 3 0 R /FormXob.fc331aff86ff817ecac4c4ce4b2ecd3a 63 0 R >> @@ -559,7 +559,7 @@ endobj endobj 66 0 obj << -/Contents 161 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 129 0 R /Resources << +/Contents 162 0 R /MediaBox [ 0 0 595.2756 841.8898 ] /Parent 130 0 R /Resources << /Font 1 0 R /ProcSet [ /PDF /Text /ImageB /ImageC /ImageI ] >> /Rotate 0 /Trans << @@ -569,23 +569,23 @@ endobj endobj 67 0 obj << -/Outlines 69 0 R /PageLabels 162 0 R /PageMode /UseNone /Pages 129 0 R /Type /Catalog +/Outlines 69 0 R /PageLabels 163 0 R /PageMode /UseNone /Pages 130 0 R /Type /Catalog >> endobj 68 0 obj << -/Author () /CreationDate (D:20260418161103-04'00') /Creator (\(unspecified\)) /Keywords () /ModDate (D:20260418161103-04'00') /Producer (ReportLab PDF Library - \(opensource\)) +/Author () /CreationDate (D:20260418193310-04'00') /Creator (\(unspecified\)) /Keywords () /ModDate (D:20260418193310-04'00') /Producer (ReportLab PDF Library - \(opensource\)) /Subject (\(unspecified\)) /Title () /Trapped /False >> endobj 69 0 obj << -/Count 69 /First 70 0 R /Last 70 0 R /Type /Outlines +/Count 70 /First 70 0 R /Last 70 0 R /Type /Outlines >> endobj 70 0 obj << -/Count 58 /Dest [ 11 0 R /XYZ 57.02362 525.9477 0 ] /First 71 0 R /Last 128 0 R /Parent 69 0 R /Title (Lumbda) +/Count 59 /Dest [ 11 0 R /XYZ 57.02362 525.9477 0 ] /First 71 0 R /Last 129 0 R /Parent 69 0 R /Title (Lumbda) >> endobj 71 0 obj @@ -663,7 +663,7 @@ endobj endobj 85 0 obj << -/Count 10 /Dest [ 19 0 R /XYZ 57.02362 231.8236 0 ] /First 86 0 R /Last 91 0 R /Next 96 0 R /Parent 70 0 R +/Count 11 /Dest [ 19 0 R /XYZ 57.02362 231.8236 0 ] /First 86 0 R /Last 91 0 R /Next 97 0 R /Parent 70 0 R /Prev 81 0 R /Title (6. Benchmarks: Three Evaluators vs CPython) >> endobj @@ -694,7 +694,7 @@ endobj endobj 91 0 obj << -/Count 4 /Dest [ 26 0 R /XYZ 57.02362 173.0236 0 ] /First 92 0 R /Last 95 0 R /Parent 85 0 R /Prev 90 0 R +/Count 5 /Dest [ 26 0 R /XYZ 57.02362 173.0236 0 ] /First 92 0 R /Last 96 0 R /Parent 85 0 R /Prev 90 0 R /Title (6.6 Memory Management and the Meta-GC) >> endobj @@ -715,187 +715,192 @@ endobj endobj 95 0 obj << -/Dest [ 34 0 R /XYZ 57.02362 765.0236 0 ] /Parent 91 0 R /Prev 94 0 R /Title (6.6.4 Validation: HTTP Server Under Sustained Load) +/Dest [ 34 0 R /XYZ 57.02362 765.0236 0 ] /Next 96 0 R /Parent 91 0 R /Prev 94 0 R /Title (6.6.4 Validation: HTTP Server Under Sustained Load) >> endobj 96 0 obj << -/Count 7 /Dest [ 34 0 R /XYZ 57.02362 225.0236 0 ] /First 97 0 R /Last 103 0 R /Next 104 0 R /Parent 70 0 R - /Prev 85 0 R /Title (7. Portal: Feedback Across Time) +/Dest [ 34 0 R /XYZ 57.02362 207.0236 0 ] /Parent 91 0 R /Prev 95 0 R /Title (6.6.5 Precise Block Typing: Killing a Class of Bugs) >> endobj 97 0 obj << -/Dest [ 36 0 R /XYZ 57.02362 727.0236 0 ] /Next 98 0 R /Parent 96 0 R /Title (7.1 S-Expression Portal \204 the Portable One) +/Count 7 /Dest [ 35 0 R /XYZ 57.02362 562.6236 0 ] /First 98 0 R /Last 104 0 R /Next 105 0 R /Parent 70 0 R + /Prev 85 0 R /Title (7. Portal: Feedback Across Time) >> endobj 98 0 obj << -/Dest [ 36 0 R /XYZ 57.02362 485.8236 0 ] /Next 99 0 R /Parent 96 0 R /Prev 97 0 R /Title (7.2 Cross-Implementation Exchange Matrix) +/Dest [ 35 0 R /XYZ 57.02362 359.4236 0 ] /Next 99 0 R /Parent 97 0 R /Title (7.1 S-Expression Portal \204 the Portable One) >> endobj 99 0 obj << -/Dest [ 36 0 R /XYZ 57.02362 285.8236 0 ] /Next 100 0 R /Parent 96 0 R /Prev 98 0 R /Title (7.3 JSON Portal \204 Graph-Aware, Continuation-Preserving) +/Dest [ 35 0 R /XYZ 57.02362 118.2236 0 ] /Next 100 0 R /Parent 97 0 R /Prev 98 0 R /Title (7.2 Cross-Implementation Exchange Matrix) >> endobj 100 0 obj << -/Dest [ 37 0 R /XYZ 57.02362 708.2236 0 ] /Next 101 0 R /Parent 96 0 R /Prev 99 0 R /Title (7.4 Binary Heap Dump \204 the Fast One) +/Dest [ 37 0 R /XYZ 57.02362 607.0236 0 ] /Next 101 0 R /Parent 97 0 R /Prev 99 0 R /Title (7.3 JSON Portal \204 Graph-Aware, Continuation-Preserving) >> endobj 101 0 obj << -/Dest [ 37 0 R /XYZ 57.02362 456.2236 0 ] /Next 102 0 R /Parent 96 0 R /Prev 100 0 R /Title (7.5 Cross-Process Benchmarks) +/Dest [ 37 0 R /XYZ 57.02362 320.2236 0 ] /Next 102 0 R /Parent 97 0 R /Prev 100 0 R /Title (7.4 Binary Heap Dump \204 the Fast One) >> endobj 102 0 obj << -/Dest [ 37 0 R /XYZ 57.02362 142.2236 0 ] /Next 103 0 R /Parent 96 0 R /Prev 101 0 R /Title (7.6 Mismatch Cases: Graceful Degradation) +/Dest [ 38 0 R /XYZ 57.02362 765.0236 0 ] /Next 103 0 R /Parent 97 0 R /Prev 101 0 R /Title (7.5 Cross-Process Benchmarks) >> endobj 103 0 obj << -/Dest [ 38 0 R /XYZ 57.02362 571.0236 0 ] /Parent 96 0 R /Prev 102 0 R /Title (7.7 Use Case: Distributed Primality Testing) +/Dest [ 38 0 R /XYZ 57.02362 451.0236 0 ] /Next 104 0 R /Parent 97 0 R /Prev 102 0 R /Title (7.6 Mismatch Cases: Graceful Degradation) >> endobj 104 0 obj << -/Count 6 /Dest [ 38 0 R /XYZ 57.02362 370.2236 0 ] /First 105 0 R /Last 110 0 R /Next 111 0 R /Parent 70 0 R - /Prev 96 0 R /Title (8. The EML Universality Proof) +/Dest [ 39 0 R /XYZ 57.02362 765.0236 0 ] /Parent 97 0 R /Prev 103 0 R /Title (7.7 Use Case: Distributed Primality Testing) >> endobj 105 0 obj << -/Dest [ 38 0 R /XYZ 57.02362 293.0236 0 ] /Next 106 0 R /Parent 104 0 R /Title (8.1 The Operator) +/Count 6 /Dest [ 39 0 R /XYZ 57.02362 564.2236 0 ] /First 106 0 R /Last 111 0 R /Next 112 0 R /Parent 70 0 R + /Prev 97 0 R /Title (8. The EML Universality Proof) >> endobj 106 0 obj << -/Dest [ 38 0 R /XYZ 57.02362 216.2236 0 ] /Next 107 0 R /Parent 104 0 R /Prev 105 0 R /Title (8.2 Stage 1: Core Functions \(Depth 1--3\)) +/Dest [ 39 0 R /XYZ 57.02362 487.0236 0 ] /Next 107 0 R /Parent 105 0 R /Title (8.1 The Operator) >> endobj 107 0 obj << -/Dest [ 39 0 R /XYZ 57.02362 765.0236 0 ] /Next 108 0 R /Parent 104 0 R /Prev 106 0 R /Title (8.3 Stage 2: Arithmetic) +/Dest [ 39 0 R /XYZ 57.02362 410.2236 0 ] /Next 108 0 R /Parent 105 0 R /Prev 106 0 R /Title (8.2 Stage 1: Core Functions \(Depth 1--3\)) >> endobj 108 0 obj << -/Dest [ 39 0 R /XYZ 57.02362 650.6236 0 ] /Next 109 0 R /Parent 104 0 R /Prev 107 0 R /Title (8.4 Stage 3: Complex Plane Access) +/Dest [ 39 0 R /XYZ 57.02362 290.2236 0 ] /Next 109 0 R /Parent 105 0 R /Prev 107 0 R /Title (8.3 Stage 2: Arithmetic) >> endobj 109 0 obj << -/Dest [ 39 0 R /XYZ 57.02362 542.6236 0 ] /Next 110 0 R /Parent 104 0 R /Prev 108 0 R /Title (8.5 Stage 4: Trigonometry via Euler) +/Dest [ 39 0 R /XYZ 57.02362 175.8236 0 ] /Next 110 0 R /Parent 105 0 R /Prev 108 0 R /Title (8.4 Stage 3: Complex Plane Access) >> endobj 110 0 obj << -/Dest [ 39 0 R /XYZ 57.02362 446.6236 0 ] /Parent 104 0 R /Prev 109 0 R /Title (8.6 Verification & Friction Analysis) +/Dest [ 40 0 R /XYZ 57.02362 765.0236 0 ] /Next 111 0 R /Parent 105 0 R /Prev 109 0 R /Title (8.5 Stage 4: Trigonometry via Euler) >> endobj 111 0 obj << -/Dest [ 41 0 R /XYZ 57.02362 441.0236 0 ] /Next 112 0 R /Parent 70 0 R /Prev 104 0 R /Title (9. Language Coverage) +/Dest [ 40 0 R /XYZ 57.02362 669.0236 0 ] /Parent 105 0 R /Prev 110 0 R /Title (8.6 Verification & Friction Analysis) >> endobj 112 0 obj << -/Dest [ 41 0 R /XYZ 57.02362 191.8236 0 ] /Next 113 0 R /Parent 70 0 R /Prev 111 0 R /Title (10. Relationship to Companion Papers) +/Dest [ 43 0 R /XYZ 57.02362 675.0236 0 ] /Next 113 0 R /Parent 70 0 R /Prev 105 0 R /Title (9. Language Coverage) >> endobj 113 0 obj << -/Count 6 /Dest [ 43 0 R /XYZ 57.02362 633.0236 0 ] /First 114 0 R /Last 119 0 R /Next 120 0 R /Parent 70 0 R - /Prev 112 0 R /Title (11. Four Implementation Tiers, One Language) +/Dest [ 43 0 R /XYZ 57.02362 425.8236 0 ] /Next 114 0 R /Parent 70 0 R /Prev 112 0 R /Title (10. Relationship to Companion Papers) >> endobj 114 0 obj << -/Dest [ 48 0 R /XYZ 57.02362 277.0236 0 ] /Next 115 0 R /Parent 113 0 R /Title (11.1 Test Coverage) +/Count 6 /Dest [ 43 0 R /XYZ 57.02362 176.6236 0 ] /First 115 0 R /Last 120 0 R /Next 121 0 R /Parent 70 0 R + /Prev 113 0 R /Title (11. Four Implementation Tiers, One Language) >> endobj 115 0 obj << -/Dest [ 49 0 R /XYZ 57.02362 765.0236 0 ] /Next 116 0 R /Parent 113 0 R /Prev 114 0 R /Title (11.2 File I/O Parity) +/Dest [ 48 0 R /XYZ 57.02362 277.0236 0 ] /Next 116 0 R /Parent 114 0 R /Title (11.1 Test Coverage) >> endobj 116 0 obj << -/Dest [ 49 0 R /XYZ 57.02362 457.0236 0 ] /Next 117 0 R /Parent 113 0 R /Prev 115 0 R /Title (11.3 Sockets: One HTTP Server, Three Runtimes) +/Dest [ 49 0 R /XYZ 57.02362 765.0236 0 ] /Next 117 0 R /Parent 114 0 R /Prev 115 0 R /Title (11.2 File I/O Parity) >> endobj 117 0 obj << -/Dest [ 51 0 R /XYZ 57.02362 506.6988 0 ] /Next 118 0 R /Parent 113 0 R /Prev 116 0 R /Title (11.4 S-expressions over Sockets: RPC, REPL, and Chains) +/Dest [ 49 0 R /XYZ 57.02362 457.0236 0 ] /Next 118 0 R /Parent 114 0 R /Prev 116 0 R /Title (11.3 Sockets: One HTTP Server, Three Runtimes) >> endobj 118 0 obj << -/Dest [ 52 0 R /XYZ 57.02362 673.0236 0 ] /Next 119 0 R /Parent 113 0 R /Prev 117 0 R /Title (11.5 Portal over HTTP: State Transfer Between Machines) +/Dest [ 51 0 R /XYZ 57.02362 506.6988 0 ] /Next 119 0 R /Parent 114 0 R /Prev 117 0 R /Title (11.4 S-expressions over Sockets: RPC, REPL, and Chains) >> endobj 119 0 obj << -/Dest [ 52 0 R /XYZ 57.02362 124.6236 0 ] /Parent 113 0 R /Prev 118 0 R /Title (11.6 heap-snapshot: The Arena Escape Hatch) +/Dest [ 52 0 R /XYZ 57.02362 673.0236 0 ] /Next 120 0 R /Parent 114 0 R /Prev 118 0 R /Title (11.5 Portal over HTTP: State Transfer Between Machines) >> endobj 120 0 obj << -/Count 3 /Dest [ 55 0 R /XYZ 57.02362 477.4236 0 ] /First 121 0 R /Last 123 0 R /Next 124 0 R /Parent 70 0 R - /Prev 113 0 R /Title (12. MOAD Audit: Fixing What We Built) +/Dest [ 52 0 R /XYZ 57.02362 124.6236 0 ] /Parent 114 0 R /Prev 119 0 R /Title (11.6 heap-snapshot: The Arena Escape Hatch) >> endobj 121 0 obj << -/Dest [ 55 0 R /XYZ 57.02362 190.2236 0 ] /Next 122 0 R /Parent 120 0 R /Title (12.1 MOAD-0001: The Sedimentary Defect in Our Own Code) +/Count 3 /Dest [ 55 0 R /XYZ 57.02362 477.4236 0 ] /First 122 0 R /Last 124 0 R /Next 125 0 R /Parent 70 0 R + /Prev 114 0 R /Title (12. MOAD Audit: Fixing What We Built) >> endobj 122 0 obj << -/Dest [ 56 0 R /XYZ 57.02362 265.0236 0 ] /Next 123 0 R /Parent 120 0 R /Prev 121 0 R /Title (12.2 MOAD-0002: The Intertangle in Our Own Design) +/Dest [ 55 0 R /XYZ 57.02362 190.2236 0 ] /Next 123 0 R /Parent 121 0 R /Title (12.1 MOAD-0001: The Sedimentary Defect in Our Own Code) >> endobj 123 0 obj << -/Dest [ 59 0 R /XYZ 57.02362 715.0236 0 ] /Parent 120 0 R /Prev 122 0 R /Title (12.3 Our Shared Infrastructure) +/Dest [ 56 0 R /XYZ 57.02362 265.0236 0 ] /Next 124 0 R /Parent 121 0 R /Prev 122 0 R /Title (12.2 MOAD-0002: The Intertangle in Our Own Design) >> endobj 124 0 obj << -/Dest [ 59 0 R /XYZ 57.02362 523.0236 0 ] /Next 125 0 R /Parent 70 0 R /Prev 120 0 R /Title (13. Future Work) +/Dest [ 59 0 R /XYZ 57.02362 715.0236 0 ] /Parent 121 0 R /Prev 123 0 R /Title (12.3 Our Shared Infrastructure) >> endobj 125 0 obj << -/Dest [ 59 0 R /XYZ 57.02362 267.8236 0 ] /Next 126 0 R /Parent 70 0 R /Prev 124 0 R /Title (14. The Defect in the Model) +/Dest [ 59 0 R /XYZ 57.02362 523.0236 0 ] /Next 126 0 R /Parent 70 0 R /Prev 121 0 R /Title (13. Future Work) >> endobj 126 0 obj << -/Dest [ 62 0 R /XYZ 57.02362 297.0236 0 ] /Next 127 0 R /Parent 70 0 R /Prev 125 0 R /Title (Citation) +/Dest [ 59 0 R /XYZ 57.02362 267.8236 0 ] /Next 127 0 R /Parent 70 0 R /Prev 125 0 R /Title (14. The Defect in the Model) >> endobj 127 0 obj << -/Dest [ 62 0 R /XYZ 57.02362 215.8236 0 ] /Next 128 0 R /Parent 70 0 R /Prev 126 0 R /Title (References) +/Dest [ 62 0 R /XYZ 57.02362 297.0236 0 ] /Next 128 0 R /Parent 70 0 R /Prev 126 0 R /Title (Citation) >> endobj 128 0 obj << -/Dest [ 62 0 R /XYZ 57.02362 134.6236 0 ] /Parent 70 0 R /Prev 127 0 R /Title (License) +/Dest [ 62 0 R /XYZ 57.02362 215.8236 0 ] /Next 129 0 R /Parent 70 0 R /Prev 127 0 R /Title (References) >> endobj 129 0 obj << +/Dest [ 62 0 R /XYZ 57.02362 134.6236 0 ] /Parent 70 0 R /Prev 128 0 R /Title (License) +>> +endobj +130 0 obj +<< /Count 32 /Kids [ 11 0 R 12 0 R 15 0 R 16 0 R 17 0 R 18 0 R 19 0 R 20 0 R 25 0 R 26 0 R - 29 0 R 31 0 R 33 0 R 34 0 R 36 0 R 37 0 R 38 0 R 39 0 R 40 0 R 41 0 R + 29 0 R 31 0 R 33 0 R 34 0 R 35 0 R 37 0 R 38 0 R 39 0 R 40 0 R 41 0 R 43 0 R 47 0 R 48 0 R 49 0 R 51 0 R 52 0 R 55 0 R 56 0 R 59 0 R 62 0 R 65 0 R 66 0 R ] /Type /Pages >> endobj -130 0 obj +131 0 obj << /Length 5064 >> @@ -1076,7 +1081,7 @@ Q endstream endobj -131 0 obj +132 0 obj << /Length 8031 >> @@ -1177,7 +1182,7 @@ Q endstream endobj -132 0 obj +133 0 obj << /Length 4740 >> @@ -1340,7 +1345,7 @@ Q endstream endobj -133 0 obj +134 0 obj << /Length 6876 >> @@ -1655,7 +1660,7 @@ Q endstream endobj -134 0 obj +135 0 obj << /Length 8861 >> @@ -2166,7 +2171,7 @@ Q endstream endobj -135 0 obj +136 0 obj << /Length 9194 >> @@ -2608,7 +2613,7 @@ Q endstream endobj -136 0 obj +137 0 obj << /Length 9151 >> @@ -3019,7 +3024,7 @@ Q endstream endobj -137 0 obj +138 0 obj << /Length 12963 >> @@ -3749,7 +3754,7 @@ Q endstream endobj -138 0 obj +139 0 obj << /Length 10062 >> @@ -4216,7 +4221,7 @@ Q endstream endobj -139 0 obj +140 0 obj << /Length 9313 >> @@ -4450,7 +4455,7 @@ Q endstream endobj -140 0 obj +141 0 obj << /Length 8527 >> @@ -4774,7 +4779,7 @@ Q endstream endobj -141 0 obj +142 0 obj << /Length 10896 >> @@ -5144,7 +5149,7 @@ Q endstream endobj -142 0 obj +143 0 obj << /Length 12577 >> @@ -5766,9 +5771,9 @@ Q endstream endobj -143 0 obj +144 0 obj << -/Length 11866 +/Length 9957 >> stream 1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET @@ -5849,7 +5854,7 @@ q 1 0 0 1 188.8668 57 cm q 0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (484) Tj T* ET +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (~300) Tj T* ET Q Q q @@ -5883,7 +5888,7 @@ q 1 0 0 1 188.8668 39 cm q 0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (462) Tj T* ET +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (~330) Tj T* ET Q Q q @@ -5918,7 +5923,7 @@ q 1 0 0 1 188.8668 21 cm q 0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (463) Tj T* ET +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (~360) Tj T* ET Q Q q @@ -5953,28 +5958,28 @@ q 1 0 0 1 188.8668 3 cm q 0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (\206) Tj T* ET +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (~410) Tj T* ET Q Q q 1 0 0 1 256.2387 3 cm q 0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (\227) Tj T* ET +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (116) Tj T* ET Q Q q 1 0 0 1 323.6107 3 cm q 0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (\227) Tj T* ET +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (1,088) Tj T* ET Q Q q 1 0 0 1 390.9827 3 cm q 0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (\227) Tj T* ET +BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL (972) Tj T* ET Q Q q @@ -6004,29 +6009,22 @@ q 1 0 0 1 57.02362 561.0236 cm q 0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (\206 Crashes at first GC \227 latent conservative-scan bug, see below.) Tj T* ET +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (All four cells validate cleanly now:) Tj T* ET Q Q q -1 0 0 1 57.02362 543.0236 cm -q -0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (Three cells validate cleanly:) Tj T* ET -Q +1 0 0 1 57.02362 555.0236 cm Q q -1 0 0 1 57.02362 537.0236 cm +1 0 0 1 57.02362 555.0236 cm Q q -1 0 0 1 57.02362 537.0236 cm -Q -q -1 0 0 1 57.02362 489.0236 cm +1 0 0 1 57.02362 519.0236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET q -1 0 0 1 6 33 cm +1 0 0 1 6 21 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F5 10 Tf 12 TL 8 0 Td (\177) Tj T* -8 0 Td ET @@ -6035,7 +6033,7 @@ Q q 1 0 0 1 23 -3 cm q -BT 1 0 0 1 0 38 Tm 2.862739 Tw 12 TL /F3 10 Tf 0 0 0 rg (Cells 1 and 2) Tj /F1 10 Tf ( show that on idiomatic code using ) Tj /F5 10 Tf (heap-snapshot) Tj /F1 10 Tf (, both binaries hold memory) Tj T* 0 Tw 2.169897 Tw (absolutely flat \(~4 KB growth over 5,000 requests is normal VM noise\). The GC build costs ~5%) Tj T* 0 Tw .488138 Tw (throughput for a feature the snapshot pattern doesn't need \227 a meaningful signal that if your server is) Tj T* 0 Tw (well-written, GC is optional overhead.) Tj T* ET +BT 1 0 0 1 0 26 Tm 2.862739 Tw 12 TL /F3 10 Tf 0 0 0 rg (Cells 1 and 2) Tj /F1 10 Tf ( show that on idiomatic code using ) Tj /F5 10 Tf (heap-snapshot) Tj /F1 10 Tf (, both binaries hold memory) Tj T* 0 Tw 1.372844 Tw (absolutely flat \(~4 KB growth over 5,000 requests is normal VM noise\). The GC build costs a small) Tj T* 0 Tw (throughput overhead for a feature the snapshot pattern doesn't need.) Tj T* ET Q Q q @@ -6043,10 +6041,10 @@ Q Q Q q -1 0 0 1 57.02362 483.0236 cm +1 0 0 1 57.02362 513.0236 cm Q q -1 0 0 1 57.02362 447.0236 cm +1 0 0 1 57.02362 477.0236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -6068,15 +6066,15 @@ Q Q Q q -1 0 0 1 57.02362 441.0236 cm +1 0 0 1 57.02362 471.0236 cm Q q -1 0 0 1 57.02362 369.0236 cm +1 0 0 1 57.02362 423.0236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET q -1 0 0 1 6 57 cm +1 0 0 1 6 33 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F5 10 Tf 12 TL 8 0 Td (\177) Tj T* -8 0 Td ET @@ -6085,7 +6083,7 @@ Q q 1 0 0 1 23 -3 cm q -BT 1 0 0 1 0 62 Tm .22755 Tw 12 TL /F3 10 Tf 0 0 0 rg (Cell 4) Tj /F1 10 Tf ( is the one that should have been bounded by naive mark-sweep and wasn't. The server crashes) Tj T* 0 Tw .520522 Tw (at the first GC trigger \(~1 MB of allocations into the run\), fixed-size workload triggering another variant) Tj T* 0 Tw .110556 Tw (of the conservative stack scan's type-confusion. The pattern is identical in kind to the 24-byte env/string) Tj T* 0 Tw 2.57389 Tw (collision \(\2476.6.1\) we already fixed \227 probably a 24- or 40-byte response block being walked as) Tj T* 0 Tw 1.145197 Tw (something it isn't. The fix requires tightening one more walker; we logged it as a known issue rather) Tj T* 0 Tw (than shipping a fix under time pressure.) Tj T* ET +BT 1 0 0 1 0 38 Tm .149314 Tw 12 TL /F3 10 Tf 0 0 0 rg (Cell 4) Tj /F1 10 Tf ( is the use case the GC was built for. With neither ) Tj /F5 10 Tf (heap-snapshot) Tj /F1 10 Tf ( nor ) Tj /F5 10 Tf (heap-restore) Tj /F1 10 Tf (, the GC) Tj T* 0 Tw 2.112556 Tw (build bounds memory at one chunk \(~1 MB\) and serves ) Tj /F3 10 Tf (faster than the leaking no-GC version) Tj /F1 10 Tf T* 0 Tw 2.680696 Tw (because it doesn't pay ) Tj /F5 10 Tf (heap_grow) Tj /F1 10 Tf ( mmap-every-64-MB costs on repeated allocation. ) Tj /F3 10 Tf (972 KB of) Tj T* 0 Tw (growth) Tj /F1 10 Tf ( across 5,000 requests is exactly one heap chunk \227 the collector hit its natural steady state.) Tj T* ET Q Q q @@ -6093,37 +6091,110 @@ Q Q Q q -1 0 0 1 57.02362 351.0236 cm +1 0 0 1 57.02362 405.0236 cm Q q -1 0 0 1 57.02362 273.0236 cm +1 0 0 1 57.02362 327.0236 cm q -BT 1 0 0 1 0 62 Tm .321079 Tw 12 TL /F3 10 Tf 0 0 0 rg (Honest read.) Tj /F1 10 Tf ( The GC build succeeds at validating the snapshot pattern \(cell 2 is the real deployment target) Tj T* 0 Tw .949314 Tw (for long-running asm servers\) but the "use GC instead of snapshots" use case \(cell 4\) has an outstanding) Tj T* 0 Tw .628941 Tw (correctness bug. ) Tj /F5 10 Tf (heap-snapshot) Tj /F1 10 Tf ( + ) Tj /F5 10 Tf (heap-restore) Tj /F1 10 Tf ( remain the recommended pattern for production asm) Tj T* 0 Tw 3.808556 Tw (code; the naive GC serves as a diagnostic backstop and as the control-group baseline for future) Tj T* 0 Tw 1.272256 Tw (memory-management work. This is still progress \227 we now have a concrete failing case to aim the next) Tj T* 0 Tw (round of debugging at, rather than a vague worry.) Tj T* ET +BT 1 0 0 1 0 62 Tm 5.961223 Tw 12 TL /F3 10 Tf 0 0 0 rg (Precise-type dispatch was the fix.) Tj /F1 10 Tf ( Cell 4 was crashing at first GC until we replaced the) Tj T* 0 Tw 1.538941 Tw (conservative-scan-plus-sentinel-checks walker with a precise one. Every heap block's 8-byte header now) Tj T* 0 Tw 3.27789 Tw (carries an explicit type byte at bits 8\22615 \(see \2476.6.5 below for the redesign\), so ) Tj /F5 10 Tf (gc_mark_drain) Tj /F1 10 Tf (,) Tj T* 0 Tw .88989 Tw /F5 10 Tf (gc_mark_env) Tj /F1 10 Tf (, and the arena-escape scan dispatch on the type byte instead of guessing from block size.) Tj T* 0 Tw 1.226147 Tw (This eliminated the entire class of "24-byte env vs string" / "40-byte vector vs string" type-confusion bugs) Tj T* 0 Tw (we'd been patching one-by-one.) Tj T* ET Q Q q -1 0 0 1 57.02362 243.0236 cm +1 0 0 1 57.02362 249.0236 cm +q +BT 1 0 0 1 0 62 Tm .666772 Tw 12 TL /F3 10 Tf 0 0 0 rg (Honest read.) Tj /F1 10 Tf ( The GC build now succeeds at the "GC instead of snapshots" use case. ) Tj /F5 10 Tf (heap-snapshot) Tj /F1 10 Tf ( +) Tj T* 0 Tw .132362 Tw /F5 10 Tf (heap-restore) Tj /F1 10 Tf ( remain the idiomatic production pattern \(they're cheaper per-request and portable across all) Tj T* 0 Tw .046373 Tw (tiers\), but the GC is finally a correct fallback for code that doesn't manage arenas explicitly. Remaining rough) Tj T* 0 Tw .567223 Tw (edge: on very heavy sustained allocation workloads \(hash-set benchmark at the ~1 MB/iter scale under the) Tj T* 0 Tw 2.390522 Tw (GC build\) we still see the occasional unbound-variable error that points to a root-scan edge case the) Tj T* 0 Tw (precise-type fix didn't completely close. Tracked as a follow-up.) Tj T* ET +Q +Q +q +1 0 0 1 57.02362 219.0236 cm q BT 1 0 0 1 0 14 Tm 91.99278 Tw 12 TL /F3 10 Tf 0 0 0 rg (Reproduce:) Tj /F1 10 Tf ( ) Tj /F5 10 Tf (make) Tj ( ) Tj (bench-gc-http) Tj /F1 10 Tf (. Tuning:) Tj T* 0 Tw /F5 10 Tf (REQUESTS=10000) Tj ( ) Tj (CONCURRENCY=16) Tj ( ) Tj (VCAP=524288) Tj ( ) Tj (bash) Tj ( ) Tj (tests/bench-gc-http.sh) Tj /F1 10 Tf (.) Tj T* ET Q Q q -1 0 0 1 57.02362 211.8236 cm +1 0 0 1 57.02362 195.0236 cm +q +BT 1 0 0 1 0 2 Tm 12 TL /F2 10 Tf .133333 .133333 .133333 rg (6.6.5 Precise Block Typing: Killing a Class of Bugs) Tj T* ET +Q +Q +q +1 0 0 1 57.02362 117.0236 cm +q +BT 1 0 0 1 0 62 Tm .088797 Tw 12 TL /F1 10 Tf 0 0 0 rg (Earlier versions of the meta-GC walkers inferred block type from ) Tj /F4 10 Tf (size) Tj /F1 10 Tf ( alone. A 24-byte block could be an env) Tj T* 0 Tw 1.498138 Tw (node, a closure, or a 16-character string; a 40-byte block could be a 4-element vector or a 25-character) Tj T* 0 Tw .485197 Tw (string. The walkers tried to guess and guessed wrong under the conservative stack scan \227 any stack word) Tj T* 0 Tw .905522 Tw (whose low 3 bits happened to match ) Tj /F5 10 Tf (TAG_SYM) Tj /F1 10 Tf ( or ) Tj /F5 10 Tf (7) Tj /F1 10 Tf ( \(vector-family\) would be dereferenced, its block's size) Tj T* 0 Tw 1.69589 Tw (read from the header, and the walker would interpret subsequent payload bytes as tagged child values.) Tj T* 0 Tw (Strings-as-vectors reading 200 bytes past their end was the canonical failure.) Tj T* ET +Q +Q +q +1 0 0 1 57.02362 99.02362 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (We fixed this by adding an explicit type byte to every heap block's header:) Tj T* ET +Q +Q + +endstream +endobj +145 0 obj +<< +/Length 9361 +>> +stream +1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET +q +1 0 0 1 57.02362 732.6236 cm +q +q +1 0 0 1 0 0 cm +q +1 0 0 1 6.6 6.6 cm +q +.662745 .662745 .662745 RG +.5 w +.960784 .960784 .960784 rg +n -6 -6 480.0283 31.2 re B* +Q +q +0 0 0 rg +BT 1 0 0 1 0 11.2 Tm /F5 8 Tf 9.6 TL (# Old: [size:63 | mark:1]) Tj T* (# New: [size:48 | type:8 | flags:8 \(mark at bit 0\)]) Tj T* ET +Q +Q +Q +Q +Q +q +1 0 0 1 57.02362 676.6236 cm +q +BT 1 0 0 1 0 38 Tm 5.818335 Tw 12 TL /F1 10 Tf 0 0 0 rg (Type constants \() Tj /F5 10 Tf (HT_PAIR) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (HT_CLOSURE) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (HT_STRING) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (HT_SYMBOL) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (HT_VECTOR) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (HT_HASHTABLE) Tj /F1 10 Tf (,) Tj T* 0 Tw .948196 Tw /F5 10 Tf (HT_HASHSET) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (HT_ENVNODE) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (HT_CHAINNODE) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (HT_PADDING) Tj /F1 10 Tf (\) are set at every ) Tj /F5 10 Tf (heap_alloc) Tj /F1 10 Tf ( call site in the) Tj T* 0 Tw .427686 Tw (GC build. Every walker \227 mark, escape-scan, sweep \227 now dispatches on the type byte instead of size. A) Tj T* 0 Tw (string can never be walked as a vector; an env node can never be confused with a closure.) Tj T* ET +Q +Q +q +1 0 0 1 57.02362 622.6236 cm +q +BT 1 0 0 1 0 38 Tm .051917 Tw 12 TL /F1 10 Tf 0 0 0 rg (Cost: one extra ) Tj /F5 10 Tf (orq) Tj /F1 10 Tf ( at each of ~15 allocation sites \(a few nanoseconds per call\) and 16 bits of header space) Tj T* 0 Tw 1.318726 Tw (per block \(negligible given minimum block size is 16 payload bytes + 8 header bytes\). Benefit: the entire) Tj T* 0 Tw .669353 Tw ("conservative scan misidentifies X as Y" class of bugs goes away. Cell 4 of \2476.6.4 flipped from "crashes at) Tj T* 0 Tw (first GC" to "working correctly" when this landed.) Tj T* ET +Q +Q +q +1 0 0 1 57.02362 580.6236 cm +q +BT 1 0 0 1 0 26 Tm .608647 Tw 12 TL /F1 10 Tf 0 0 0 rg (The precise-type change also simplified the walkers: the special-case "is the first word -1 \(hash-table\) or -2) Tj T* 0 Tw .998453 Tw (\(hash-set\) or a small positive number \(vector length\)" dispatch in ) Tj /F5 10 Tf (gc_mark_drain) Tj /F1 10 Tf ( collapsed into a single) Tj T* 0 Tw /F5 10 Tf (cmp) Tj /F1 10 Tf ( on the type byte. ~50 lines of heuristic-guessing code deleted.) Tj T* ET +Q +Q +q +1 0 0 1 57.02362 549.4236 cm q BT 1 0 0 1 0 2.2 Tm 13.2 TL /F2 11 Tf .133333 .133333 .133333 rg (7. Portal: Feedback Across Time) Tj T* ET Q Q q -1 0 0 1 57.02362 167.8236 cm +1 0 0 1 57.02362 505.4236 cm q BT 1 0 0 1 0 26 Tm .17989 Tw 12 TL /F1 10 Tf 0 0 0 rg (A continuation is feedback within a process. A portal is feedback across processes. Same primitive, different) Tj T* 0 Tw 1.06631 Tw (scope: capture machine state, serialize it, reload it elsewhere, resume. Lumbda ships three portal formats) Tj T* 0 Tw (with different tradeoffs & constituencies.) Tj T* ET Q Q q -1 0 0 1 57.02362 161.8236 cm +1 0 0 1 57.02362 499.4236 cm Q q -1 0 0 1 57.02362 65.82362 cm +1 0 0 1 57.02362 403.4236 cm q 1 1 1 rg n 0 96 481.2283 -18 re f* @@ -6326,38 +6397,29 @@ Q Q Q q -1 0 0 1 57.02362 65.82362 cm +1 0 0 1 57.02362 403.4236 cm Q - -endstream -endobj -144 0 obj -<< -/Length 9315 ->> -stream -1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET q -1 0 0 1 57.02362 741.0236 cm +1 0 0 1 57.02362 373.4236 cm q 0 0 0 rg BT 1 0 0 1 0 14 Tm /F1 10 Tf 12 TL .49713 Tw (Times measured on a 4-binding workload \(int + list + string + fib\(30\) result\) excluding process startup. "k" =) Tj T* 0 Tw (continuation.) Tj T* ET Q Q q -1 0 0 1 57.02362 715.0236 cm +1 0 0 1 57.02362 347.4236 cm q BT 1 0 0 1 0 2 Tm 12 TL /F2 10 Tf .133333 .133333 .133333 rg (7.1 S-Expression Portal \227 the Portable One) Tj T* ET Q Q q -1 0 0 1 57.02362 697.0236 cm +1 0 0 1 57.02362 329.4236 cm q BT 1 0 0 1 0 2 Tm 12 TL /F1 10 Tf 0 0 0 rg (The most boring format is the most portable. An S-expression portal is a sequence of ) Tj /F5 10 Tf (define) Tj /F1 10 Tf ( forms:) Tj T* ET Q Q q -1 0 0 1 57.02362 627.8236 cm +1 0 0 1 57.02362 260.2236 cm q q 1 0 0 1 0 0 cm @@ -6378,77 +6440,106 @@ Q Q Q q -1 0 0 1 57.02362 595.8236 cm +1 0 0 1 57.02362 228.2236 cm q 0 0 0 rg BT 1 0 0 1 0 14 Tm /F1 10 Tf 12 TL .550522 Tw (Every Scheme implementation in the world can already read this. No schema, no decoder, no version field.) Tj T* 0 Tw (The file is a Scheme program; loading it is evaluating it.) Tj T* ET Q Q q -1 0 0 1 57.02362 541.8236 cm +1 0 0 1 57.02362 174.2236 cm q BT 1 0 0 1 0 38 Tm .702256 Tw 12 TL /F3 10 Tf 0 0 0 rg (The key insight: the language IS the interchange format.) Tj /F1 10 Tf ( We did not design this. R. Kent Dybvig didn't.) Tj T* 0 Tw 1.188726 Tw (John McCarthy didn't. It is a structural consequence of homoiconicity: if the syntax of the language is the) Tj T* 0 Tw 5.458196 Tw (syntax of its data structures, then data serialization is language serialization. Portability across) Tj T* 0 Tw (implementations is free \227 it arrives with the parser.) Tj T* ET Q Q q -1 0 0 1 57.02362 499.8236 cm +1 0 0 1 57.02362 132.2236 cm q BT 1 0 0 1 0 26 Tm .511772 Tw 12 TL /F1 10 Tf 0 0 0 rg (Producer side: assemble the file with ) Tj /F5 10 Tf (\(display) Tj ( ) Tj (...\)) Tj /F1 10 Tf ( & ) Tj /F5 10 Tf (\(write) Tj ( ) Tj (...\)) Tj /F1 10 Tf ( to an output port. Consumer side:) Tj T* 0 Tw 3.693453 Tw /F5 10 Tf (\(load) Tj ( ) Tj ("file.sexp"\)) Tj /F1 10 Tf (. Both sides exist in every implementation, giving us a 3\3273 matrix of valid) Tj T* 0 Tw (exchanges.) Tj T* ET Q Q q -1 0 0 1 57.02362 473.8236 cm +1 0 0 1 57.02362 106.2236 cm q BT 1 0 0 1 0 2 Tm 12 TL /F2 10 Tf .133333 .133333 .133333 rg (7.2 Cross-Implementation Exchange Matrix) Tj T* ET Q Q q -1 0 0 1 57.02362 461.8236 cm +1 0 0 1 57.02362 94.22362 cm Q q -1 0 0 1 57.02362 371.8236 cm +1 0 0 1 57.02362 76.22362 cm q 1 1 1 rg -n 0 90 481.2283 -18 re f* -.878431 .878431 .878431 rg -n 0 72 481.2283 -18 re f* -1 1 1 rg -n 0 54 481.2283 -18 re f* -.878431 .878431 .878431 rg -n 0 36 481.2283 -18 re f* -1 1 1 rg n 0 18 481.2283 -18 re f* 0 0 0 rg BT /F3 10 Tf 12 TL ET q -1 0 0 1 6 75 cm +1 0 0 1 6 3 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 19.19482 0 Td (Producer ) Tj /F6 10 Tf 12 TL (\256) Tj /F3 10 Tf 12 TL T* -19.19482 0 Td ET Q Q q -1 0 0 1 112.9396 75 cm +1 0 0 1 112.9396 3 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 39.43645 0 Td (Python) Tj T* -39.43645 0 Td ET Q Q q -1 0 0 1 237.7025 75 cm +1 0 0 1 237.7025 3 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 52.77145 0 Td (C) Tj T* -52.77145 0 Td ET Q Q q -1 0 0 1 362.4654 75 cm +1 0 0 1 362.4654 3 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 46.37645 0 Td (asm) Tj T* -46.37645 0 Td ET Q Q q +1 J +1 j +0 0 0 RG +.25 w +n 0 0 m 481.2283 0 l S +n 106.9396 0 m 106.9396 18 l S +n 231.7025 0 m 231.7025 18 l S +n 356.4654 0 m 356.4654 18 l S +n 0 18 m 481.2283 18 l S +n 0 0 m 0 18 l S +n 481.2283 0 m 481.2283 18 l S +Q +Q +Q + +endstream +endobj +146 0 obj +<< +/Length 8717 +>> +stream +1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET +q +1 0 0 1 57.02362 693.0236 cm +q +1 1 1 rg +n 0 72 481.2283 -18 re f* +.878431 .878431 .878431 rg +n 0 54 481.2283 -18 re f* +1 1 1 rg +n 0 36 481.2283 -18 re f* +.878431 .878431 .878431 rg +n 0 18 481.2283 -18 re f* +0 0 0 rg +BT /F3 10 Tf 12 TL ET +q 1 0 0 1 6 57 cm q 0 0 0 rg @@ -6550,52 +6641,51 @@ n 0 72 m 481.2283 72 l S n 0 54 m 481.2283 54 l S n 0 36 m 481.2283 36 l S n 0 18 m 481.2283 18 l S -n 106.9396 0 m 106.9396 90 l S -n 231.7025 0 m 231.7025 90 l S -n 356.4654 0 m 356.4654 90 l S -n 0 90 m 481.2283 90 l S +n 106.9396 0 m 106.9396 72 l S +n 231.7025 0 m 231.7025 72 l S +n 356.4654 0 m 356.4654 72 l S +n 0 0 m 0 72 l S +n 481.2283 0 m 481.2283 72 l S n 0 0 m 481.2283 0 l S -n 0 0 m 0 90 l S -n 481.2283 0 m 481.2283 90 l S Q Q Q q -1 0 0 1 57.02362 371.8236 cm +1 0 0 1 57.02362 693.0236 cm Q q -1 0 0 1 57.02362 341.8236 cm +1 0 0 1 57.02362 663.0236 cm q BT 1 0 0 1 0 14 Tm 3.901835 Tw 12 TL /F1 10 Tf 0 0 0 rg (9 of 9. Verified by ) Tj /F5 10 Tf (tests/portal-cross-test.sh) Tj /F1 10 Tf ( \() Tj /F3 10 Tf (make bench-portal-cross) Tj /F1 10 Tf (\). Same file, same) Tj T* 0 Tw (semantics, regardless of which process produced it.) Tj T* ET Q Q q -1 0 0 1 57.02362 299.8236 cm +1 0 0 1 57.02362 621.0236 cm q 0 0 0 rg BT 1 0 0 1 0 26 Tm /F1 10 Tf 12 TL .526019 Tw (This matters because it defeats the "version lock-in" trap. If the JSON portal were the only option, a Python) Tj T* 0 Tw 2.478453 Tw (3.15 producer could emit structures a C consumer couldn't parse. With S-expression portals, the only) Tj T* 0 Tw (dependency is a parser that handles the subset of forms in the file. Every implementation already has one.) Tj T* ET Q Q q -1 0 0 1 57.02362 273.8236 cm +1 0 0 1 57.02362 595.0236 cm q BT 1 0 0 1 0 2 Tm 12 TL /F2 10 Tf .133333 .133333 .133333 rg (7.3 JSON Portal \227 Graph-Aware, Continuation-Preserving) Tj T* ET Q Q q -1 0 0 1 57.02362 243.8236 cm +1 0 0 1 57.02362 565.0236 cm q BT 1 0 0 1 0 14 Tm .373453 Tw 12 TL /F1 10 Tf 0 0 0 rg (When you need to preserve shared references, cycles, closures, or a ) Tj /F4 10 Tf (live continuation) Tj /F1 10 Tf (, S-expressions aren't) Tj T* 0 Tw (enough. The JSON portal \(Python & C\) performs graph-aware serialization:) Tj T* ET Q Q q -1 0 0 1 57.02362 237.8236 cm +1 0 0 1 57.02362 559.0236 cm Q q -1 0 0 1 57.02362 237.8236 cm +1 0 0 1 57.02362 559.0236 cm Q q -1 0 0 1 57.02362 225.8236 cm +1 0 0 1 57.02362 547.0236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -6617,10 +6707,10 @@ Q Q Q q -1 0 0 1 57.02362 219.8236 cm +1 0 0 1 57.02362 541.0236 cm Q q -1 0 0 1 57.02362 207.8236 cm +1 0 0 1 57.02362 529.0236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -6643,10 +6733,10 @@ Q Q Q q -1 0 0 1 57.02362 201.8236 cm +1 0 0 1 57.02362 523.0236 cm Q q -1 0 0 1 57.02362 189.8236 cm +1 0 0 1 57.02362 511.0236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -6668,10 +6758,10 @@ Q Q Q q -1 0 0 1 57.02362 183.8236 cm +1 0 0 1 57.02362 505.0236 cm Q q -1 0 0 1 57.02362 171.8236 cm +1 0 0 1 57.02362 493.0236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -6694,10 +6784,10 @@ Q Q Q q -1 0 0 1 57.02362 165.8236 cm +1 0 0 1 57.02362 487.0236 cm Q q -1 0 0 1 57.02362 153.8236 cm +1 0 0 1 57.02362 475.0236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -6720,31 +6810,22 @@ Q Q Q q -1 0 0 1 57.02362 135.8236 cm +1 0 0 1 57.02362 457.0236 cm Q q -1 0 0 1 57.02362 105.8236 cm +1 0 0 1 57.02362 427.0236 cm q BT 1 0 0 1 0 14 Tm 2.974168 Tw 12 TL /F1 10 Tf 0 0 0 rg (Deserialization is two-pass: shell pass creates empty object shells & assigns reference IDs, fill pass) Tj T* 0 Tw (populates pointers & values. This handles the closure-that-captures-itself pattern cleanly.) Tj T* ET Q Q q -1 0 0 1 57.02362 63.82362 cm +1 0 0 1 57.02362 385.0236 cm q BT 1 0 0 1 0 26 Tm 4.719816 Tw 12 TL /F1 10 Tf 0 0 0 rg (During VM execution, ) Tj /F5 10 Tf (portal-checkpoint!) Tj /F1 10 Tf ( triggers at ) Tj /F5 10 Tf (OP_JUMP) Tj /F1 10 Tf ( & ) Tj /F5 10 Tf (OP_TAIL_CALL) Tj /F1 10 Tf ( instructions,) Tj T* 0 Tw 1.439168 Tw (capturing the current continuation, serializing it to a ) Tj /F5 10 Tf (.portal) Tj /F1 10 Tf ( file, & continuing. Resumption restores the) Tj T* 0 Tw (saved state & continues execution from the exact instruction where the checkpoint occurred.) Tj T* ET Q Q - -endstream -endobj -145 0 obj -<< -/Length 9088 ->> -stream -1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET q -1 0 0 1 57.02362 742.2236 cm +1 0 0 1 57.02362 354.2236 cm q q 1 0 0 1 0 0 cm @@ -6765,26 +6846,26 @@ Q Q Q q -1 0 0 1 57.02362 722.2236 cm +1 0 0 1 57.02362 334.2236 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (The computation does not need to restart from the beginning.) Tj T* ET Q Q q -1 0 0 1 57.02362 696.2236 cm +1 0 0 1 57.02362 308.2236 cm q BT 1 0 0 1 0 2 Tm 12 TL /F2 10 Tf .133333 .133333 .133333 rg (7.4 Binary Heap Dump \227 the Fast One) Tj T* ET Q Q q -1 0 0 1 57.02362 666.2236 cm +1 0 0 1 57.02362 278.2236 cm q BT 1 0 0 1 0 14 Tm .755197 Tw 12 TL /F1 10 Tf 0 0 0 rg (The asm implementation ships a direct-dump portal: write the raw heap bytes, the ) Tj /F5 10 Tf (r14) Tj /F1 10 Tf ( \(env\) & ) Tj /F5 10 Tf (r15) Tj /F1 10 Tf ( \(bump) Tj T* 0 Tw (pointer\) registers, the heap base address, & a magic header. No parsing, no encoding.) Tj T* ET Q Q q -1 0 0 1 57.02362 568.2236 cm +1 0 0 1 57.02362 180.2236 cm q q 1 0 0 1 0 0 cm @@ -6805,34 +6886,43 @@ Q Q Q q -1 0 0 1 57.02362 524.2236 cm +1 0 0 1 57.02362 136.2236 cm q BT 1 0 0 1 0 26 Tm 1.387739 Tw 12 TL /F1 10 Tf 0 0 0 rg (Sub-millisecond save & resume. The MAP_FIXED trick is why it works across processes: because every) Tj T* 0 Tw 1.474556 Tw (pointer inside the heap is an absolute address, resuming at a different address would require relocation.) Tj T* 0 Tw (Mapping at the same address keeps pointers live.) Tj T* ET Q Q q -1 0 0 1 57.02362 470.2236 cm +1 0 0 1 57.02362 82.22362 cm q BT 1 0 0 1 0 38 Tm 1.067739 Tw 12 TL /F1 10 Tf 0 0 0 rg (Constraints: same architecture, same binary layout, same process model. An asm binary portal written on) Tj T* 0 Tw .022545 Tw (one box resumes on another x86_64 Linux box running the same asm binary. It does not resume on a rebuilt) Tj T* 0 Tw 1.065522 Tw (binary \227 the BSS-resident symbol table ) Tj /F5 10 Tf (sym_table) Tj /F1 10 Tf ( is not in the heap dump, so interned symbols would) Tj T* 0 Tw (need to be reinterned. That's the price of trivial serialization.) Tj T* ET Q Q + +endstream +endobj +147 0 obj +<< +/Length 9918 +>> +stream +1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET q -1 0 0 1 57.02362 444.2236 cm +1 0 0 1 57.02362 753.0236 cm q BT 1 0 0 1 0 2 Tm 12 TL /F2 10 Tf .133333 .133333 .133333 rg (7.5 Cross-Process Benchmarks) Tj T* ET Q Q q -1 0 0 1 57.02362 402.2236 cm +1 0 0 1 57.02362 711.0236 cm q BT 1 0 0 1 0 26 Tm 2.703647 Tw 12 TL /F1 10 Tf 0 0 0 rg (Producer process A saves state to a file; consumer process B starts fresh, loads the file, continues.) Tj T* 0 Tw 10.67759 Tw (Wall-clock time for both processes end-to-end, 50 iterations, same-laptop. ) Tj /F3 10 Tf (Reproduce:) Tj /F1 10 Tf T* 0 Tw /F5 10 Tf (make) Tj ( ) Tj (bench-portal) Tj /F1 10 Tf ( \(source: ) Tj /F5 10 Tf (tests/portal-benchmark.sh) Tj /F1 10 Tf (\).) Tj T* ET Q Q q -1 0 0 1 57.02362 396.2236 cm +1 0 0 1 57.02362 705.0236 cm Q q -1 0 0 1 57.02362 198.2236 cm +1 0 0 1 57.02362 507.0236 cm q 1 1 1 rg n 0 198 481.2283 -18 re f* @@ -7038,125 +7128,37 @@ Q Q Q q -1 0 0 1 57.02362 198.2236 cm +1 0 0 1 57.02362 507.0236 cm Q q -1 0 0 1 57.02362 156.2236 cm +1 0 0 1 57.02362 465.0236 cm q BT 1 0 0 1 0 26 Tm .698334 Tw 12 TL /F1 10 Tf 0 0 0 rg (The asm) Tj /F6 10 Tf 12 TL (\256) Tj /F1 10 Tf 12 TL (asm cross-process is ~160\327 faster than Python) Tj /F6 10 Tf 12 TL (\256) Tj /F1 10 Tf 12 TL (Python. The binary & S-expression portals are) Tj T* 0 Tw .812256 Tw (within 10% of each other on this workload \227 the bottleneck is process startup, not serialization. For larger) Tj T* 0 Tw (heaps the binary format pulls further ahead; for portability, S-expression always wins.) Tj T* ET Q Q q -1 0 0 1 57.02362 130.2236 cm +1 0 0 1 57.02362 439.0236 cm q BT 1 0 0 1 0 2 Tm 12 TL /F2 10 Tf .133333 .133333 .133333 rg (7.6 Mismatch Cases: Graceful Degradation) Tj T* ET Q Q q -1 0 0 1 57.02362 112.2236 cm +1 0 0 1 57.02362 421.0236 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (A usable persistence layer fails well. What happens when the consumer meets unexpected input?) Tj T* ET Q Q q -1 0 0 1 57.02362 106.2236 cm +1 0 0 1 57.02362 415.0236 cm Q q -1 0 0 1 57.02362 70.22362 cm +1 0 0 1 57.02362 265.0236 cm q 1 1 1 rg -n 0 36 481.2283 -18 re f* +n 0 150 481.2283 -18 re f* .878431 .878431 .878431 rg -n 0 18 481.2283 -18 re f* -0 0 0 rg -BT /F3 10 Tf 12 TL ET -q -1 0 0 1 6 21 cm -q -0 0 0 rg -BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 96.07173 0 Td (Input) Tj T* -96.07173 0 Td ET -Q -Q -q -1 0 0 1 234.5835 21 cm -q -0 0 0 rg -BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 19.16248 0 Td (Python) Tj T* -19.16248 0 Td ET -Q -Q -q -1 0 0 1 318.7984 21 cm -q -0 0 0 rg -BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 32.49748 0 Td (C) Tj T* -32.49748 0 Td ET -Q -Q -q -1 0 0 1 403.0134 21 cm -q -0 0 0 rg -BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 26.10248 0 Td (asm) Tj T* -26.10248 0 Td ET -Q -Q -0 0 0 rg -BT /F1 10 Tf 12 TL ET -q -1 0 0 1 6 3 cm -q -0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (Empty file) Tj T* ET -Q -Q -q -1 0 0 1 234.5835 3 cm -q -0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (continue) Tj T* ET -Q -Q -q -1 0 0 1 318.7984 3 cm -q -0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (continue) Tj T* ET -Q -Q -q -1 0 0 1 403.0134 3 cm -q -0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (continue) Tj T* ET -Q -Q -q -1 J -1 j -0 0 0 RG -.25 w -n 0 0 m 481.2283 0 l S -n 0 18 m 481.2283 18 l S -n 228.5835 0 m 228.5835 36 l S -n 312.7984 0 m 312.7984 36 l S -n 397.0134 0 m 397.0134 36 l S -n 0 36 m 481.2283 36 l S -n 0 0 m 0 36 l S -n 481.2283 0 m 481.2283 36 l S -Q -Q -Q - -endstream -endobj -146 0 obj -<< -/Length 7571 ->> -stream -1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET -q -1 0 0 1 57.02362 651.0236 cm -q +n 0 132 481.2283 -18 re f* 1 1 1 rg n 0 114 481.2283 -30 re f* .878431 .878431 .878431 rg @@ -7168,8 +7170,66 @@ n 0 36 481.2283 -18 re f* 1 1 1 rg n 0 18 481.2283 -18 re f* 0 0 0 rg +BT /F3 10 Tf 12 TL ET +q +1 0 0 1 6 135 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 96.07173 0 Td (Input) Tj T* -96.07173 0 Td ET +Q +Q +q +1 0 0 1 234.5835 135 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 19.16248 0 Td (Python) Tj T* -19.16248 0 Td ET +Q +Q +q +1 0 0 1 318.7984 135 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 32.49748 0 Td (C) Tj T* -32.49748 0 Td ET +Q +Q +q +1 0 0 1 403.0134 135 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 26.10248 0 Td (asm) Tj T* -26.10248 0 Td ET +Q +Q +0 0 0 rg BT /F1 10 Tf 12 TL ET q +1 0 0 1 6 117 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (Empty file) Tj T* ET +Q +Q +q +1 0 0 1 234.5835 117 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (continue) Tj T* ET +Q +Q +q +1 0 0 1 318.7984 117 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (continue) Tj T* ET +Q +Q +q +1 0 0 1 403.0134 117 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (continue) Tj T* ET +Q +Q +q 1 0 0 1 6 99 cm q 0 0 0 rg @@ -7309,37 +7369,48 @@ q 1 j 0 0 0 RG .25 w +n 0 132 m 481.2283 132 l S n 0 114 m 481.2283 114 l S n 0 84 m 481.2283 84 l S n 0 54 m 481.2283 54 l S n 0 36 m 481.2283 36 l S n 0 18 m 481.2283 18 l S -n 228.5835 0 m 228.5835 114 l S -n 312.7984 0 m 312.7984 114 l S -n 397.0134 0 m 397.0134 114 l S -n 0 0 m 0 114 l S -n 481.2283 0 m 481.2283 114 l S +n 228.5835 0 m 228.5835 150 l S +n 312.7984 0 m 312.7984 150 l S +n 397.0134 0 m 397.0134 150 l S +n 0 150 m 481.2283 150 l S n 0 0 m 481.2283 0 l S +n 0 0 m 0 150 l S +n 481.2283 0 m 481.2283 150 l S Q Q Q q -1 0 0 1 57.02362 651.0236 cm +1 0 0 1 57.02362 265.0236 cm Q q -1 0 0 1 57.02362 585.0236 cm +1 0 0 1 57.02362 199.0236 cm q BT 1 0 0 1 0 50 Tm 1.476556 Tw 12 TL /F1 10 Tf 0 0 0 rg (All defects surfaced & fixed during benchmark development: an asm segfault on ) Tj /F5 10 Tf (\(define) Tj ( ) Tj (x\)) Tj /F1 10 Tf ( without a) Tj T* 0 Tw 1.838453 Tw (value \(now binds to ) Tj /F5 10 Tf (VOID) Tj /F1 10 Tf (\), an asm portal-resume that accepted short headers \(now verifies ) Tj /F5 10 Tf (sys_read) Tj /F1 10 Tf T* 0 Tw 1.204272 Tw (returned a full 48 bytes & sanity-checks heap metadata\), a Python ) Tj /F5 10 Tf (file) Tj ( ) Tj (not) Tj ( ) Tj (found) Tj /F1 10 Tf ( error reporting the) Tj T* 0 Tw 1.304862 Tw (outer script path instead of the inner missing file \(now uses ) Tj /F5 10 Tf (FileNotFoundError.filename) Tj /F1 10 Tf (\). Graceful) Tj T* 0 Tw (degradation is not free; it is tested.) Tj T* ET Q Q + +endstream +endobj +148 0 obj +<< +/Length 6103 +>> +stream +1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET q -1 0 0 1 57.02362 559.0236 cm +1 0 0 1 57.02362 753.0236 cm q BT 1 0 0 1 0 2 Tm 12 TL /F2 10 Tf .133333 .133333 .133333 rg (7.7 Use Case: Distributed Primality Testing) Tj T* ET Q Q q -1 0 0 1 57.02362 432.2236 cm +1 0 0 1 57.02362 626.2236 cm q q 1 0 0 1 0 0 cm @@ -7359,38 +7430,38 @@ Q Q Q q -1 0 0 1 57.02362 388.2236 cm +1 0 0 1 57.02362 582.2236 cm q BT 1 0 0 1 0 26 Tm 1.105522 Tw 12 TL /F1 10 Tf 0 0 0 rg (Machine A starts the computation. Every 10,000 iterations, it writes a checkpoint. Machine B picks up the) Tj T* 0 Tw 2.790642 Tw /F5 10 Tf (.portal) Tj /F1 10 Tf ( file & continues from the last checkpoint. The computation migrates without either machine) Tj T* 0 Tw (needing to know about the other. Feedback \227 the continuation \227 carries the entire execution context.) Tj T* ET Q Q q -1 0 0 1 57.02362 357.0236 cm +1 0 0 1 57.02362 551.0236 cm q BT 1 0 0 1 0 2.2 Tm 13.2 TL /F2 11 Tf .133333 .133333 .133333 rg (8. The EML Universality Proof) Tj T* ET Q Q q -1 0 0 1 57.02362 325.0236 cm +1 0 0 1 57.02362 519.0236 cm q BT 1 0 0 1 0 14 Tm 3.669104 Tw 12 TL /F1 10 Tf 0 0 0 rg (Lumbda ships with a mathematical proof that a single operator generates all elementary functions:) Tj T* 0 Tw /F5 10 Tf (eml\(x,) Tj ( ) Tj (y\)) Tj ( ) Tj (=) Tj ( ) Tj (exp\(x\)) Tj ( ) Tj (-) Tj ( ) Tj (ln\(y\)) Tj /F1 10 Tf (.) Tj T* ET Q Q q -1 0 0 1 57.02362 307.0236 cm +1 0 0 1 57.02362 501.0236 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (Reference: "All elementary functions from a single operator" \(arXiv:2603.21852v2\).) Tj T* ET Q Q q -1 0 0 1 57.02362 281.0236 cm +1 0 0 1 57.02362 475.0236 cm q BT 1 0 0 1 0 2 Tm 12 TL /F2 10 Tf .133333 .133333 .133333 rg (8.1 The Operator) Tj T* ET Q Q q -1 0 0 1 57.02362 250.2236 cm +1 0 0 1 57.02362 444.2236 cm q q 1 0 0 1 0 0 cm @@ -7411,19 +7482,19 @@ Q Q Q q -1 0 0 1 57.02362 230.2236 cm +1 0 0 1 57.02362 424.2236 cm q BT 1 0 0 1 0 2 Tm 12 TL /F1 10 Tf 0 0 0 rg (With this operator & the constant ) Tj /F5 10 Tf (1) Tj /F1 10 Tf (, the following derivation chain constructs every elementary function:) Tj T* ET Q Q q -1 0 0 1 57.02362 204.2236 cm +1 0 0 1 57.02362 398.2236 cm q BT 1 0 0 1 0 2 Tm 12 TL /F2 10 Tf .133333 .133333 .133333 rg (8.2 Stage 1: Core Functions \(Depth 1--3\)) Tj T* ET Q Q q -1 0 0 1 57.02362 154.2236 cm +1 0 0 1 57.02362 348.2236 cm q q 1 0 0 1 0 0 cm @@ -7444,28 +7515,19 @@ Q Q Q q -1 0 0 1 57.02362 110.2236 cm +1 0 0 1 57.02362 304.2236 cm q BT 1 0 0 1 0 26 Tm 16.01403 Tw 12 TL /F3 10 Tf 0 0 0 rg (Proof of ln recovery) Tj /F1 10 Tf (: Let ) Tj /F5 10 Tf (a) Tj ( ) Tj (=) Tj ( ) Tj (eml\(1,x\)) Tj ( ) Tj (=) Tj ( ) Tj (e) Tj ( ) Tj (-) Tj ( ) Tj (ln\(x\)) Tj /F1 10 Tf (. Then) Tj T* 0 Tw 28.85979 Tw /F5 10 Tf (eml\(a,) Tj ( ) Tj (1\)) Tj ( ) Tj (=) Tj ( ) Tj (exp\(e) Tj ( ) Tj (-) Tj ( ) Tj (ln\(x\)\)) Tj ( ) Tj (=) Tj ( ) Tj (exp\(e\)/x) Tj /F1 10 Tf (. Then) Tj T* 0 Tw /F5 10 Tf (eml\(1,) Tj ( ) Tj (exp\(e\)/x\)) Tj ( ) Tj (=) Tj ( ) Tj (e) Tj ( ) Tj (-) Tj ( ) Tj (ln\(exp\(e\)/x\)) Tj ( ) Tj (=) Tj ( ) Tj (e) Tj ( ) Tj (-) Tj ( ) Tj (e) Tj ( ) Tj (+) Tj ( ) Tj (ln\(x\)) Tj ( ) Tj (=) Tj ( ) Tj (ln\(x\)) Tj /F1 10 Tf (.) Tj T* ET Q Q - -endstream -endobj -147 0 obj -<< -/Length 9939 ->> -stream -1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET q -1 0 0 1 57.02362 753.0236 cm +1 0 0 1 57.02362 278.2236 cm q BT 1 0 0 1 0 2 Tm 12 TL /F2 10 Tf .133333 .133333 .133333 rg (8.3 Stage 2: Arithmetic) Tj T* ET Q Q q -1 0 0 1 57.02362 664.6236 cm +1 0 0 1 57.02362 189.8236 cm q q 1 0 0 1 0 0 cm @@ -7485,13 +7547,13 @@ Q Q Q q -1 0 0 1 57.02362 638.6236 cm +1 0 0 1 57.02362 163.8236 cm q BT 1 0 0 1 0 2 Tm 12 TL /F2 10 Tf .133333 .133333 .133333 rg (8.4 Stage 3: Complex Plane Access) Tj T* ET Q Q q -1 0 0 1 57.02362 588.6236 cm +1 0 0 1 57.02362 113.8236 cm q q 1 0 0 1 0 0 cm @@ -7512,19 +7574,28 @@ Q Q Q q -1 0 0 1 57.02362 556.6236 cm +1 0 0 1 57.02362 81.82362 cm q BT 1 0 0 1 0 14 Tm .253071 Tw 12 TL /F1 10 Tf 0 0 0 rg (The key insight: ) Tj /F5 10 Tf (ln) Tj /F1 10 Tf ( of a negative number enters the complex plane. Since we can construct ) Tj /F5 10 Tf (-1) Tj /F1 10 Tf ( from eml via) Tj T* 0 Tw (the subtraction chain, ) Tj /F5 10 Tf (ln\(-1\)) Tj /F1 10 Tf ( yields ) Tj /F5 10 Tf (i) Tj /F6 10 Tf 12 TL (p) Tj /F5 10 Tf 12 TL /F1 10 Tf (, from which ) Tj /F5 10 Tf /F6 10 Tf 12 TL (p) Tj /F5 10 Tf 12 TL /F1 10 Tf ( & ) Tj /F5 10 Tf (i) Tj /F1 10 Tf ( follow.) Tj T* ET Q Q + +endstream +endobj +149 0 obj +<< +/Length 10703 +>> +stream +1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET q -1 0 0 1 57.02362 530.6236 cm +1 0 0 1 57.02362 753.0236 cm q BT 1 0 0 1 0 2 Tm 12 TL /F2 10 Tf .133333 .133333 .133333 rg (8.5 Stage 4: Trigonometry via Euler) Tj T* ET Q Q q -1 0 0 1 57.02362 480.6236 cm +1 0 0 1 57.02362 703.0236 cm q q 1 0 0 1 0 0 cm @@ -7545,29 +7616,29 @@ Q Q Q q -1 0 0 1 57.02362 460.6236 cm +1 0 0 1 57.02362 683.0236 cm q BT 1 0 0 1 0 2 Tm 12 TL /F1 10 Tf 0 0 0 rg (All trigonometric functions follow from complex exponentials, which follow from ) Tj /F5 10 Tf (exp) Tj /F1 10 Tf (, which follows from ) Tj /F5 10 Tf (eml) Tj /F1 10 Tf (.) Tj T* ET Q Q q -1 0 0 1 57.02362 434.6236 cm +1 0 0 1 57.02362 657.0236 cm q BT 1 0 0 1 0 2 Tm 12 TL /F2 10 Tf .133333 .133333 .133333 rg (8.6 Verification & Friction Analysis) Tj T* ET Q Q q -1 0 0 1 57.02362 416.6236 cm +1 0 0 1 57.02362 639.0236 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (The proof has been verified at six distinct levels. Times are best-of-3 on the i5-8350U:) Tj T* ET Q Q q -1 0 0 1 57.02362 410.6236 cm +1 0 0 1 57.02362 633.0236 cm Q q -1 0 0 1 57.02362 260.6236 cm +1 0 0 1 57.02362 483.0236 cm q 1 1 1 rg n 0 150 481.2283 -18 re f* @@ -7803,23 +7874,23 @@ Q Q Q q -1 0 0 1 57.02362 260.6236 cm +1 0 0 1 57.02362 483.0236 cm Q q -1 0 0 1 57.02362 242.6236 cm +1 0 0 1 57.02362 465.0236 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL (Three separate wins compound here.) Tj T* ET Q Q q -1 0 0 1 57.02362 236.6236 cm +1 0 0 1 57.02362 459.0236 cm Q q -1 0 0 1 57.02362 236.6236 cm +1 0 0 1 57.02362 459.0236 cm Q q -1 0 0 1 57.02362 164.6236 cm +1 0 0 1 57.02362 387.0236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -7841,10 +7912,10 @@ Q Q Q q -1 0 0 1 57.02362 158.6236 cm +1 0 0 1 57.02362 381.0236 cm Q q -1 0 0 1 57.02362 110.6236 cm +1 0 0 1 57.02362 333.0236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -7866,49 +7937,24 @@ Q Q Q q -1 0 0 1 57.02362 104.6236 cm +1 0 0 1 57.02362 327.0236 cm Q q -1 0 0 1 57.02362 62.69291 cm +1 0 0 1 57.02362 267.0236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET q -1 0 0 1 6 26.93071 cm +1 0 0 1 6 45 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F5 10 Tf 12 TL 2 0 Td (3.) Tj T* -2 0 Td ET Q Q q -1 0 0 1 23 14.93071 cm -q -BT 1 0 0 1 0 14 Tm .419168 Tw 12 TL /F3 10 Tf 0 0 0 rg (Caching: artifact replay) Tj /F1 10 Tf ( \227 both checkers now write a small success-artifact on pass and short-circuit) Tj T* 0 Tw .242844 Tw (on subsequent runs if the magic header matches. Cached Lumbda \(7 ms\) and cached Lean \(5 ms\) are) Tj T* 0 Tw ET -Q -Q -q -Q -Q -Q - -endstream -endobj -148 0 obj -<< -/Length 8913 ->> -stream -1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET -q -1 0 0 1 57.02362 729.0236 cm -q -0 0 0 rg -BT /F1 10 Tf 12 TL ET -BT 1 0 0 1 6 23 Tm T* ET -q 1 0 0 1 23 -3 cm q -BT 1 0 0 1 0 26 Tm 6.674168 Tw 12 TL /F1 10 Tf 0 0 0 rg (essentially "read one file and print five lines." The 16\327 cold gap collapses to ~1.5\327.) Tj T* 0 Tw 1.11218 Tw /F5 10 Tf (rm) Tj ( ) Tj (-f) Tj ( ) Tj (/tmp/lumbda-eml.cache) Tj /F1 10 Tf ( \(analogous to ) Tj /F5 10 Tf (lake) Tj ( ) Tj (clean) Tj /F1 10 Tf (\) forces a cold re-check and the full) Tj T* 0 Tw (numbers return.) Tj T* ET +BT 1 0 0 1 0 50 Tm .419168 Tw 12 TL /F3 10 Tf 0 0 0 rg (Caching: artifact replay) Tj /F1 10 Tf ( \227 both checkers now write a small success-artifact on pass and short-circuit) Tj T* 0 Tw .242844 Tw (on subsequent runs if the magic header matches. Cached Lumbda \(7 ms\) and cached Lean \(5 ms\) are) Tj T* 0 Tw 6.674168 Tw (essentially "read one file and print five lines." The 16\327 cold gap collapses to ~1.5\327.) Tj T* 0 Tw 1.11218 Tw /F5 10 Tf (rm) Tj ( ) Tj (-f) Tj ( ) Tj (/tmp/lumbda-eml.cache) Tj /F1 10 Tf ( \(analogous to ) Tj /F5 10 Tf (lake) Tj ( ) Tj (clean) Tj /F1 10 Tf (\) forces a cold re-check and the full) Tj T* 0 Tw (numbers return.) Tj T* ET Q Q q @@ -7916,34 +7962,34 @@ Q Q Q q -1 0 0 1 57.02362 729.0236 cm +1 0 0 1 57.02362 267.0236 cm Q q -1 0 0 1 57.02362 663.0236 cm +1 0 0 1 57.02362 201.0236 cm q BT 1 0 0 1 0 50 Tm .913719 Tw 12 TL /F3 10 Tf 0 0 0 rg (Symmetric honesty.) Tj /F1 10 Tf ( Lean's kernel guarantees remain stronger even when the timings equalize: the Lean) Tj T* 0 Tw .45989 Tw (TCB is ~3 KLOC of audited elaborator/kernel, while Lumbda's asm interpreter is ~6.6 KLOC of hand-written) Tj T* 0 Tw .884917 Tw (assembly. For proofs where the cost of a bug in the checker itself matters, Lean is the right tool; for small) Tj T* 0 Tw 2.400556 Tw (symbolic-rewrite proofs where the language hosting the proof should be able to host the checker too,) Tj T* 0 Tw (Lumbda does the job in under 50 ms cold without external dependencies.) Tj T* ET Q Q q -1 0 0 1 57.02362 609.0236 cm +1 0 0 1 57.02362 147.0236 cm q BT 1 0 0 1 0 38 Tm 3.571147 Tw 12 TL /F3 10 Tf 0 0 0 rg (Lesson) Tj /F1 10 Tf (: The fastest path to truth is not computation \227 it is understanding. When you know ) Tj /F4 10 Tf (why) Tj /F1 10 Tf T* 0 Tw .96189 Tw /F5 10 Tf (eml\(1,) Tj ( ) Tj (eml\(eml\(1,x\),) Tj ( ) Tj (1\)\)) Tj ( ) Tj (=) Tj ( ) Tj (ln\(x\)) Tj /F1 10 Tf (, you verify it in microseconds. When you don't, you search for) Tj T* 0 Tw .874862 Tw (hours. Symbolic reasoning eliminates the quadratic friction of numerical verification; caching eliminates the) Tj T* 0 Tw (startup friction of every verifier. Both layers stack.) Tj T* ET Q Q q -1 0 0 1 57.02362 579.0236 cm +1 0 0 1 57.02362 117.0236 cm q BT 1 0 0 1 0 14 Tm .708556 Tw 12 TL /F3 10 Tf 0 0 0 rg (Reproduce:) Tj /F1 10 Tf ( ) Tj /F5 10 Tf (make) Tj ( ) Tj (bench-proof) Tj /F1 10 Tf ( runs the cold and cached paths for both Lumbda \(across all three tiers\)) Tj T* 0 Tw (and Lean. Source: ) Tj /F5 10 Tf (proof/benchmark.sh) Tj /F1 10 Tf (.) Tj T* ET Q Q q -1 0 0 1 57.02362 573.0236 cm +1 0 0 1 57.02362 111.0236 cm Q q -1 0 0 1 57.02362 573.0236 cm +1 0 0 1 57.02362 111.0236 cm Q q -1 0 0 1 57.02362 537.0236 cm +1 0 0 1 57.02362 75.02362 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -7965,10 +8011,19 @@ Q Q Q q -1 0 0 1 57.02362 531.0236 cm +1 0 0 1 57.02362 69.02362 cm Q + +endstream +endobj +150 0 obj +<< +/Length 9408 +>> +stream +1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET q -1 0 0 1 57.02362 495.0236 cm +1 0 0 1 57.02362 729.0236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -7990,10 +8045,10 @@ Q Q Q q -1 0 0 1 57.02362 489.0236 cm +1 0 0 1 57.02362 723.0236 cm Q q -1 0 0 1 57.02362 465.0236 cm +1 0 0 1 57.02362 699.0236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -8015,10 +8070,10 @@ Q Q Q q -1 0 0 1 57.02362 465.0236 cm +1 0 0 1 57.02362 699.0236 cm Q q -1 0 0 1 57.02362 395.8236 cm +1 0 0 1 57.02362 629.8236 cm q q 1 0 0 1 0 0 cm @@ -8039,19 +8094,19 @@ Q Q Q q -1 0 0 1 57.02362 351.8236 cm +1 0 0 1 57.02362 585.8236 cm q BT 1 0 0 1 0 26 Tm 4.138556 Tw 12 TL /F1 10 Tf 0 0 0 rg (The Lean proof operates over abstract ) Tj /F5 10 Tf (exp) Tj /F1 10 Tf ( & ) Tj /F5 10 Tf (ln) Tj /F1 10 Tf ( functions with the axioms ) Tj /F5 10 Tf (exp\(ln\(x\)\)) Tj ( ) Tj (=) Tj ( ) Tj (x) Tj /F1 10 Tf (,) Tj T* 0 Tw 2.484897 Tw /F5 10 Tf (ln\(exp\(x\)\)) Tj ( ) Tj (=) Tj ( ) Tj (x) Tj /F1 10 Tf (, & ) Tj /F5 10 Tf (ln\(1\)) Tj ( ) Tj (=) Tj ( ) Tj (0) Tj /F1 10 Tf (. This makes the result independent of any particular real number) Tj T* 0 Tw (implementation.) Tj T* ET Q Q q -1 0 0 1 57.02362 345.8236 cm +1 0 0 1 57.02362 579.8236 cm Q q -1 0 0 1 57.02362 345.8236 cm +1 0 0 1 57.02362 579.8236 cm Q q -1 0 0 1 57.02362 261.8236 cm +1 0 0 1 57.02362 495.8236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -8073,10 +8128,10 @@ Q Q Q q -1 0 0 1 57.02362 261.8236 cm +1 0 0 1 57.02362 495.8236 cm Q q -1 0 0 1 57.02362 183.0236 cm +1 0 0 1 57.02362 417.0236 cm q q 1 0 0 1 0 0 cm @@ -8097,109 +8152,21 @@ Q Q Q q -1 0 0 1 57.02362 115.0236 cm +1 0 0 1 57.02362 349.0236 cm q BT 1 0 0 1 0 50 Tm 4.101411 Tw 12 TL /F3 10 Tf 0 0 0 rg (Verification speed: Lean vs Lumbda tiers, both cold and cached.) Tj /F1 10 Tf ( Same five theorems, same) Tj T* 0 Tw 1.757362 Tw (symbolic-rewrite strategy. The Lumbda checker now implements its own cached-replay path that mirrors) Tj T* 0 Tw .258797 Tw (Lean's: write a small artifact after a successful run; on subsequent runs, trust the artifact if the magic header) Tj T* 0 Tw .759029 Tw (matches and skip re-verification. ) Tj /F5 10 Tf (rm) Tj ( ) Tj (-f) Tj ( ) Tj (/tmp/lumbda-eml.cache) Tj /F1 10 Tf ( forces a cold re-check \(analogous to) Tj T* 0 Tw /F5 10 Tf (lake) Tj ( ) Tj (clean) Tj /F1 10 Tf (\). Best of 3 on the i5-8350U:) Tj T* ET Q Q q -1 0 0 1 57.02362 109.0236 cm +1 0 0 1 57.02362 343.0236 cm Q q -1 0 0 1 57.02362 73.02362 cm +1 0 0 1 57.02362 235.0236 cm q 1 1 1 rg -n 0 36 481.2283 -18 re f* +n 0 108 481.2283 -18 re f* .878431 .878431 .878431 rg -n 0 18 481.2283 -18 re f* -0 0 0 rg -BT /F3 10 Tf 12 TL ET -q -1 0 0 1 6 21 cm -q -0 0 0 rg -BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 55.88252 0 Td (Approach) Tj T* -55.88252 0 Td ET -Q -Q -q -1 0 0 1 176.435 21 cm -q -0 0 0 rg -BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 23.82236 0 Td (cold) Tj T* -23.82236 0 Td ET -Q -Q -q -1 0 0 1 256.6398 21 cm -q -0 0 0 rg -BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 16.87236 0 Td (cached) Tj T* -16.87236 0 Td ET -Q -Q -q -1 0 0 1 336.8445 21 cm -q -0 0 0 rg -BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 55.85693 0 Td (notes) Tj T* -55.85693 0 Td ET -Q -Q -0 0 0 rg -BT /F1 10 Tf 12 TL ET -q -1 0 0 1 6 3 cm -q -0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (Lumbda asm) Tj T* ET -Q -Q -q -1 0 0 1 176.435 3 cm -q -0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (46 ms) Tj T* ET -Q -Q -q -1 0 0 1 256.6398 3 cm -q -0 0 0 rg -BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL (7 ms) Tj T* ET -Q -Q -q -1 0 0 1 336.8445 3 cm -q -0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (fastest Lumbda tier) Tj T* ET -Q -Q -q -1 J -1 j -0 0 0 RG -.25 w -n 0 0 m 481.2283 0 l S -n 0 18 m 481.2283 18 l S -n 170.435 0 m 170.435 36 l S -n 250.6398 0 m 250.6398 36 l S -n 330.8445 0 m 330.8445 36 l S -n 0 36 m 481.2283 36 l S -n 0 0 m 0 36 l S -n 481.2283 0 m 481.2283 36 l S -Q -Q -Q - -endstream -endobj -149 0 obj -<< -/Length 10251 ->> -stream -1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET -q -1 0 0 1 57.02362 693.0236 cm -q +n 0 90 481.2283 -18 re f* 1 1 1 rg n 0 72 481.2283 -18 re f* .878431 .878431 .878431 rg @@ -8209,8 +8176,66 @@ n 0 36 481.2283 -18 re f* .878431 .878431 .878431 rg n 0 18 481.2283 -18 re f* 0 0 0 rg +BT /F3 10 Tf 12 TL ET +q +1 0 0 1 6 93 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 55.88252 0 Td (Approach) Tj T* -55.88252 0 Td ET +Q +Q +q +1 0 0 1 176.435 93 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 23.82236 0 Td (cold) Tj T* -23.82236 0 Td ET +Q +Q +q +1 0 0 1 256.6398 93 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 16.87236 0 Td (cached) Tj T* -16.87236 0 Td ET +Q +Q +q +1 0 0 1 336.8445 93 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 55.85693 0 Td (notes) Tj T* -55.85693 0 Td ET +Q +Q +0 0 0 rg BT /F1 10 Tf 12 TL ET q +1 0 0 1 6 75 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (Lumbda asm) Tj T* ET +Q +Q +q +1 0 0 1 176.435 75 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (46 ms) Tj T* ET +Q +Q +q +1 0 0 1 256.6398 75 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL (7 ms) Tj T* ET +Q +Q +q +1 0 0 1 336.8445 75 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (fastest Lumbda tier) Tj T* ET +Q +Q +q 1 0 0 1 6 57 cm q BT 1 0 0 1 0 2 Tm 12 TL /F1 10 Tf 0 0 0 rg (Lumbda C ) Tj /F5 10 Tf (--fast) Tj T* ET @@ -8304,104 +8329,125 @@ q 1 j 0 0 0 RG .25 w +n 0 90 m 481.2283 90 l S n 0 72 m 481.2283 72 l S n 0 54 m 481.2283 54 l S n 0 36 m 481.2283 36 l S n 0 18 m 481.2283 18 l S -n 170.435 0 m 170.435 72 l S -n 250.6398 0 m 250.6398 72 l S -n 330.8445 0 m 330.8445 72 l S -n 0 0 m 0 72 l S -n 481.2283 0 m 481.2283 72 l S +n 170.435 0 m 170.435 108 l S +n 250.6398 0 m 250.6398 108 l S +n 330.8445 0 m 330.8445 108 l S +n 0 108 m 481.2283 108 l S n 0 0 m 481.2283 0 l S +n 0 0 m 0 108 l S +n 481.2283 0 m 481.2283 108 l S Q Q Q q -1 0 0 1 57.02362 693.0236 cm +1 0 0 1 57.02362 235.0236 cm Q q -1 0 0 1 57.02362 627.0236 cm +1 0 0 1 57.02362 169.0236 cm q BT 1 0 0 1 0 50 Tm .204897 Tw 12 TL /F1 10 Tf 0 0 0 rg (Two comparisons matter. ) Tj /F3 10 Tf (Cold vs cold) Tj /F1 10 Tf ( is the honest end-to-end compare: Lumbda asm \(46 ms\) verifies the) Tj T* 0 Tw -0.127156 Tw (proof ) Tj /F3 10 Tf (~16\327 faster than Lean's cold rebuild) Tj /F1 10 Tf ( \(722 ms\) on the same hardware, because Lumbda doesn't link a) Tj T* 0 Tw .315636 Tw (compiled binary or spin up a kernel \227 it just runs a rewriter over five small terms. ) Tj /F3 10 Tf (Cached vs cached) Tj /F1 10 Tf ( is the) Tj T* 0 Tw 1.150966 Tw (throwaway benchmark but still interesting: Lumbda asm at 7 ms vs Lean at 5 ms, within 1.5\327, on what is) Tj T* 0 Tw (essentially "read a file and print five lines.") Tj T* ET Q Q q -1 0 0 1 57.02362 561.0236 cm +1 0 0 1 57.02362 103.0236 cm q BT 1 0 0 1 0 50 Tm .526772 Tw 12 TL /F3 10 Tf 0 0 0 rg (All four Lumbda tiers verify the proof.) Tj /F1 10 Tf ( A C ) Tj /F5 10 Tf (--fast) Tj /F1 10 Tf ( bytecode-compiler bug originally caused the final tier) Tj T* 0 Tw 10.06986 Tw (to hang on the rewriter's named-let loop; narrowed to a minimal reproduction \(see) Tj T* 0 Tw 1.693196 Tw /F5 10 Tf (c/TODO-named-let-bytecode.md) Tj /F1 10 Tf (\) and worked around in the proof file by using an internal recursive) Tj T* 0 Tw .558138 Tw /F5 10 Tf (define) Tj /F1 10 Tf ( in place of the offending named-let. All four tiers now complete in under 100 ms cold. ) Tj /F3 10 Tf (Reproduce:) Tj /F1 10 Tf T* 0 Tw /F5 10 Tf (make) Tj ( ) Tj (bench-proof) Tj /F1 10 Tf ( \(source: ) Tj /F5 10 Tf (tests/bench-proof.sh) Tj /F1 10 Tf (\).) Tj T* ET Q Q q -1 0 0 1 57.02362 459.0236 cm +1 0 0 1 57.02362 73.02362 cm q -BT 1 0 0 1 0 86 Tm 2.513543 Tw 12 TL /F3 10 Tf 0 0 0 rg (First machine-checked treatment.) Tj /F1 10 Tf ( The original paper \(Odrzywo) Tj /F9 10 Tf 12 TL (n) Tj /F1 10 Tf 12 TL (ek, arXiv:2603.21852v2, 2026-04-04\)) Tj T* 0 Tw .313453 Tw (presents the EML universality claim analytically \227 pure LaTeX mathematics, no formal tool. The companion) Tj T* 0 Tw .549873 Tw (Zenodo artifact is symbolic-regression / gradient-optimization code, not a verification. To our knowledge the) Tj T* 0 Tw 1.856373 Tw (Lean 4 proof shipped in this repo is the first machine-checked treatment of the EML identities, and the) Tj T* 0 Tw .247122 Tw (accompanying Lumbda-native checker is the first self-hosted machine-checked version. Five theorems, zero) Tj T* 0 Tw .312025 Tw /F5 10 Tf (sorry) Tj /F1 10 Tf (, no Mathlib dependency \227 ) Tj /F3 10 Tf (~1,280\327 faster than the brute-force numerical search) Tj /F1 10 Tf ( it replaced once) Tj T* 0 Tw 2.035223 Tw (the symbolic rewriter was written \(see \2478.6 for the full six-row comparison\), and carrying the additional) Tj T* 0 Tw (guarantee that no implementation quirk of floating point can ever break the conclusion.) Tj T* ET +BT 1 0 0 1 0 14 Tm 2.513543 Tw 12 TL /F3 10 Tf 0 0 0 rg (First machine-checked treatment.) Tj /F1 10 Tf ( The original paper \(Odrzywo) Tj /F9 10 Tf 12 TL (n) Tj /F1 10 Tf 12 TL (ek, arXiv:2603.21852v2, 2026-04-04\)) Tj T* 0 Tw .313453 Tw (presents the EML universality claim analytically \227 pure LaTeX mathematics, no formal tool. The companion) Tj T* 0 Tw ET +Q +Q + +endstream +endobj +151 0 obj +<< +/Length 9097 +>> +stream +1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET +q +1 0 0 1 57.02362 693.0236 cm +q +BT 1 0 0 1 0 62 Tm .549873 Tw 12 TL /F1 10 Tf 0 0 0 rg (Zenodo artifact is symbolic-regression / gradient-optimization code, not a verification. To our knowledge the) Tj T* 0 Tw 1.856373 Tw (Lean 4 proof shipped in this repo is the first machine-checked treatment of the EML identities, and the) Tj T* 0 Tw .247122 Tw (accompanying Lumbda-native checker is the first self-hosted machine-checked version. Five theorems, zero) Tj T* 0 Tw .312025 Tw /F5 10 Tf (sorry) Tj /F1 10 Tf (, no Mathlib dependency \227 ) Tj /F3 10 Tf (~1,280\327 faster than the brute-force numerical search) Tj /F1 10 Tf ( it replaced once) Tj T* 0 Tw 2.035223 Tw (the symbolic rewriter was written \(see \2478.6 for the full six-row comparison\), and carrying the additional) Tj T* 0 Tw (guarantee that no implementation quirk of floating point can ever break the conclusion.) Tj T* ET Q Q q -1 0 0 1 57.02362 427.8236 cm +1 0 0 1 57.02362 661.8236 cm q BT 1 0 0 1 0 2.2 Tm 13.2 TL /F2 11 Tf .133333 .133333 .133333 rg (9. Language Coverage) Tj T* ET Q Q q -1 0 0 1 57.02362 407.8236 cm +1 0 0 1 57.02362 641.8236 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (Lumbda implements a near-complete R7RS-small Scheme:) Tj T* ET Q Q q -1 0 0 1 57.02362 353.8236 cm +1 0 0 1 57.02362 587.8236 cm q BT 1 0 0 1 0 38 Tm 1.369223 Tw 12 TL /F3 10 Tf 0 0 0 rg (Special forms) Tj /F1 10 Tf ( \(32\): ) Tj /F5 10 Tf (define) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (set!) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (lambda) Tj /F1 10 Tf (, ) Tj /F5 10 Tf /F6 10 Tf 12 TL (l) Tj /F5 10 Tf 12 TL /F1 10 Tf (, ) Tj /F5 10 Tf (if) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (cond) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (case) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (and) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (or) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (when) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (unless) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (begin) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (let) Tj /F1 10 Tf (,) Tj T* 0 Tw 10.15262 Tw /F5 10 Tf (let*) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (letrec) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (letrec*) Tj /F1 10 Tf (, named-let, ) Tj /F5 10 Tf (do) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (quasiquote) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (define-macro) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (define-syntax) Tj /F1 10 Tf (,) Tj T* 0 Tw 3.646907 Tw /F5 10 Tf (syntax-rules) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (let-syntax) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (letrec-syntax) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (apply) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (eval) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (values) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (call/cc) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (dynamic-wind) Tj /F1 10 Tf (,) Tj T* 0 Tw /F5 10 Tf (guard) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (parameterize) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (load) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (error) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (module) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (import) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (define-record-type) Tj /F1 10 Tf (.) Tj T* ET Q Q q -1 0 0 1 57.02362 323.8236 cm +1 0 0 1 57.02362 557.8236 cm q BT 1 0 0 1 0 14 Tm .150642 Tw 12 TL /F3 10 Tf 0 0 0 rg (Built-in functions) Tj /F1 10 Tf ( \(100+\): Full arithmetic \(exact rationals, inexact reals, trigonometry\), pairs & lists \(SRFI-1\),) Tj T* 0 Tw (strings \(mutable\), characters, vectors, hash tables, I/O \(ports, file system\), system interface, Python interop.) Tj T* ET Q Q q -1 0 0 1 57.02362 293.8236 cm +1 0 0 1 57.02362 527.8236 cm q BT 1 0 0 1 0 14 Tm 2.274835 Tw 12 TL /F3 10 Tf 0 0 0 rg (Hygienic macros) Tj /F1 10 Tf (: ) Tj /F5 10 Tf (syntax-rules) Tj /F1 10 Tf ( with ellipsis \() Tj /F5 10 Tf (...) Tj /F1 10 Tf (\) support. Pattern matching, template instantiation,) Tj T* 0 Tw (proper hygiene. Also ) Tj /F5 10 Tf (define-macro) Tj /F1 10 Tf ( for procedural macros.) Tj T* ET Q Q q -1 0 0 1 57.02362 263.8236 cm +1 0 0 1 57.02362 497.8236 cm q BT 1 0 0 1 0 14 Tm 1.958835 Tw 12 TL /F3 10 Tf 0 0 0 rg (Standard library) Tj /F1 10 Tf ( \() Tj /F5 10 Tf (stdlib.lsp) Tj /F1 10 Tf (, 385 lines\): Additional macros \() Tj /F5 10 Tf (swap!) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (fluid-let) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (while) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (dotimes) Tj /F1 10 Tf (\),) Tj T* 0 Tw (utility functions, simple object system, SRFI-2/8/64 test framework.) Tj T* ET Q Q q -1 0 0 1 57.02362 209.8236 cm +1 0 0 1 57.02362 443.8236 cm q BT 1 0 0 1 0 38 Tm 1.569862 Tw 12 TL /F3 10 Tf 0 0 0 rg (Test suite) Tj /F1 10 Tf (: 974 verified assertions covering lexing, parsing, special forms, bytecode compilation, macros) Tj T* 0 Tw .214835 Tw (\(hygienic & procedural\), continuations, generators, record types, modules, arithmetic, higher-order functions,) Tj T* 0 Tw 4.238031 Tw (error handling, portal serialization, cross-implementation portal exchange, file I/O parity, & graceful) Tj T* 0 Tw (degradation on mismatched or corrupt input.) Tj T* ET Q Q q -1 0 0 1 57.02362 178.6236 cm +1 0 0 1 57.02362 412.6236 cm q BT 1 0 0 1 0 2.2 Tm 13.2 TL /F2 11 Tf .133333 .133333 .133333 rg (10. Relationship to Companion Papers) Tj T* ET Q Q q -1 0 0 1 57.02362 158.6236 cm +1 0 0 1 57.02362 392.6236 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (Lumbda forms one piece of a larger permacomputer machine learning stack:) Tj T* ET Q Q q -1 0 0 1 57.02362 152.6236 cm +1 0 0 1 57.02362 386.6236 cm Q q -1 0 0 1 57.02362 74.62362 cm +1 0 0 1 57.02362 248.6236 cm q 1 1 1 rg -n 0 78 481.2283 -18 re f* +n 0 138 481.2283 -18 re f* +.878431 .878431 .878431 rg +n 0 120 481.2283 -30 re f* +1 1 1 rg +n 0 90 481.2283 -30 re f* .878431 .878431 .878431 rg n 0 60 481.2283 -30 re f* 1 1 1 rg @@ -8409,21 +8455,21 @@ n 0 30 481.2283 -30 re f* 0 0 0 rg BT /F3 10 Tf 12 TL ET q -1 0 0 1 6 63 cm +1 0 0 1 6 123 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 28.78283 0 Td (Layer) Tj T* -28.78283 0 Td ET Q Q q -1 0 0 1 102.2457 63 cm +1 0 0 1 102.2457 123 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 64.31996 0 Td (Paper) Tj T* -64.31996 0 Td ET Q Q q -1 0 0 1 270.6756 63 cm +1 0 0 1 270.6756 123 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 91.44138 0 Td (Role) Tj T* -91.44138 0 Td ET @@ -8432,79 +8478,45 @@ Q 0 0 0 rg BT /F1 10 Tf 12 TL ET q -1 0 0 1 6 45 cm +1 0 0 1 6 105 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (Runtime) Tj T* ET Q Q q -1 0 0 1 102.2457 33 cm +1 0 0 1 102.2457 93 cm q BT 1 0 0 1 0 14 Tm 12 TL /F3 10 Tf 0 0 0 rg (Feedback Is All You Need) Tj /F1 10 Tf ( \(this) Tj T* (paper\)) Tj T* ET Q Q q -1 0 0 1 270.6756 33 cm +1 0 0 1 270.6756 93 cm q BT 1 0 0 1 0 14 Tm 12 TL /F1 10 Tf 0 0 0 rg (Complete Scheme VM with continuations &) Tj T* (portal) Tj T* ET Q Q q -1 0 0 1 6 15 cm +1 0 0 1 6 75 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (Interaction) Tj T* ET Q Q q -1 0 0 1 102.2457 3 cm +1 0 0 1 102.2457 63 cm q BT 1 0 0 1 0 14 Tm 12 TL /F1 10 Tf 0 0 0 rg (Categorization & Feedback Is All) Tj T* (You Need) Tj T* ET Q Q q -1 0 0 1 270.6756 3 cm +1 0 0 1 270.6756 63 cm q 0 0 0 rg BT 1 0 0 1 0 14 Tm /F1 10 Tf 12 TL (Machine learning driven state machines in) Tj T* (58+ languages) Tj T* ET Q Q q -1 J -1 j -0 0 0 RG -.25 w -n 0 0 m 481.2283 0 l S -n 0 60 m 481.2283 60 l S -n 0 30 m 481.2283 30 l S -n 96.24567 0 m 96.24567 78 l S -n 264.6756 0 m 264.6756 78 l S -n 0 78 m 481.2283 78 l S -n 0 0 m 0 78 l S -n 481.2283 0 m 481.2283 78 l S -Q -Q -Q - -endstream -endobj -150 0 obj -<< -/Length 2999 ->> -stream -1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET -q -1 0 0 1 57.02362 705.0236 cm -q -1 1 1 rg -n 0 60 481.2283 -30 re f* -.878431 .878431 .878431 rg -n 0 30 481.2283 -30 re f* -0 0 0 rg -BT /F1 10 Tf 12 TL ET -q 1 0 0 1 6 45 cm q 0 0 0 rg @@ -8551,36 +8563,39 @@ q 1 j 0 0 0 RG .25 w +n 0 120 m 481.2283 120 l S +n 0 90 m 481.2283 90 l S n 0 60 m 481.2283 60 l S n 0 30 m 481.2283 30 l S -n 96.24567 0 m 96.24567 60 l S -n 264.6756 0 m 264.6756 60 l S -n 0 0 m 0 60 l S -n 481.2283 0 m 481.2283 60 l S +n 96.24567 0 m 96.24567 138 l S +n 264.6756 0 m 264.6756 138 l S +n 0 138 m 481.2283 138 l S n 0 0 m 481.2283 0 l S +n 0 0 m 0 138 l S +n 481.2283 0 m 481.2283 138 l S Q Q Q q -1 0 0 1 57.02362 705.0236 cm +1 0 0 1 57.02362 248.6236 cm Q q -1 0 0 1 57.02362 651.0236 cm +1 0 0 1 57.02362 194.6236 cm q BT 1 0 0 1 0 38 Tm 1.738453 Tw 12 TL /F1 10 Tf 0 0 0 rg (Lumbda provides the runtime layer: a language that can checkpoint its own execution, migrate between) Tj T* 0 Tw 3.051529 Tw (machines, & resume from serialized state. The portal system enables distributed computation across) Tj T* 0 Tw 1.058196 Tw (permacomputer nodes. Categorization & feedback activities could run inside Lumbda's VM, with ) Tj /F5 10 Tf (call/cc) Tj /F1 10 Tf T* 0 Tw (providing the state machine transitions & portal providing persistence.) Tj T* ET Q Q q -1 0 0 1 57.02362 619.8236 cm +1 0 0 1 57.02362 163.4236 cm q BT 1 0 0 1 0 2.2 Tm 13.2 TL /F2 11 Tf .133333 .133333 .133333 rg (11. Four Implementation Tiers, One Language) Tj T* ET Q Q q -1 0 0 1 57.02362 605.8236 cm +1 0 0 1 57.02362 149.4236 cm Q q -1 0 0 1 57.02362 593.8236 cm +1 0 0 1 57.02362 137.4236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -8596,28 +8611,34 @@ Q Q Q q -1 0 0 1 57.02362 593.8236 cm +1 0 0 1 57.02362 137.4236 cm Q q -1 0 0 1 57.02362 515.8236 cm +1 0 0 1 57.02362 83.42362 cm q -BT 1 0 0 1 0 62 Tm .778726 Tw 12 TL /F1 10 Tf 0 0 0 rg (Lumbda ships as four independently built tiers: a Python bytecode VM, a C tree-walker, a C bytecode VM,) Tj T* 0 Tw 2.18402 Tw (and a C x86_64 JIT \(the last three packaged in one binary, selectable by flag\), plus a pure-assembly) Tj T* 0 Tw .931492 Tw (interpreter. Each tier is MOAD-isolated from the others \227 a defect surfaced in one is fixed in that tier, not) Tj T* 0 Tw 2.098556 Tw (patched across shared infrastructure. All four run the same ) Tj /F5 10 Tf (.lsp) Tj /F1 10 Tf ( source files and exchange the same) Tj T* 0 Tw 2.266213 Tw (S-expression portal format; \24711.3-\24711.5 demonstrate this end-to-end across sockets, relays, and HTTP) Tj T* 0 Tw (portal transfers.) Tj T* ET +BT 1 0 0 1 0 38 Tm .778726 Tw 12 TL /F1 10 Tf 0 0 0 rg (Lumbda ships as four independently built tiers: a Python bytecode VM, a C tree-walker, a C bytecode VM,) Tj T* 0 Tw 2.18402 Tw (and a C x86_64 JIT \(the last three packaged in one binary, selectable by flag\), plus a pure-assembly) Tj T* 0 Tw .931492 Tw (interpreter. Each tier is MOAD-isolated from the others \227 a defect surfaced in one is fixed in that tier, not) Tj T* 0 Tw 2.098556 Tw (patched across shared infrastructure. All four run the same ) Tj /F5 10 Tf (.lsp) Tj /F1 10 Tf ( source files and exchange the same) Tj T* 0 Tw ET Q Q -q -1 0 0 1 57.02362 507.8236 cm -Q endstream endobj -151 0 obj +152 0 obj << -/Length 1782 +/Length 2057 >> stream 1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET q -1 0 0 1 57.02362 263.1875 cm +1 0 0 1 57.02362 741.0236 cm +q +BT 1 0 0 1 0 14 Tm 2.266213 Tw 12 TL /F1 10 Tf 0 0 0 rg (S-expression portal format; \24711.3-\24711.5 demonstrate this end-to-end across sockets, relays, and HTTP) Tj T* 0 Tw (portal transfers.) Tj T* ET +Q +Q +q +1 0 0 1 57.02362 733.0236 cm +Q +q +1 0 0 1 57.02362 231.1875 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -8640,13 +8661,13 @@ Q Q Q q -1 0 0 1 57.02362 255.1875 cm +1 0 0 1 57.02362 223.1875 cm Q q -1 0 0 1 57.02362 247.1875 cm +1 0 0 1 57.02362 215.1875 cm Q q -1 0 0 1 57.02362 111.9891 cm +1 0 0 1 57.02362 79.98905 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -8669,12 +8690,12 @@ Q Q Q q -1 0 0 1 57.02362 103.9891 cm +1 0 0 1 57.02362 71.98905 cm Q endstream endobj -152 0 obj +153 0 obj << /Length 13402 >> @@ -9185,7 +9206,7 @@ Q endstream endobj -153 0 obj +154 0 obj << /Length 16605 >> @@ -10022,7 +10043,7 @@ Q endstream endobj -154 0 obj +155 0 obj << /Length 10454 >> @@ -10424,7 +10445,7 @@ Q endstream endobj -155 0 obj +156 0 obj << /Length 7406 >> @@ -10638,7 +10659,7 @@ Q endstream endobj -156 0 obj +157 0 obj << /Length 6621 >> @@ -10786,7 +10807,7 @@ Q endstream endobj -157 0 obj +158 0 obj << /Length 8009 >> @@ -11024,7 +11045,7 @@ Q endstream endobj -158 0 obj +159 0 obj << /Length 7883 >> @@ -11283,7 +11304,7 @@ Q endstream endobj -159 0 obj +160 0 obj << /Length 6415 >> @@ -11531,7 +11552,7 @@ Q endstream endobj -160 0 obj +161 0 obj << /Length 2103 >> @@ -11608,7 +11629,7 @@ Q endstream endobj -161 0 obj +162 0 obj << /Length 1025 >> @@ -11637,179 +11658,179 @@ Q endstream endobj -162 0 obj -<< -/Nums [ 0 163 0 R 1 164 0 R 2 165 0 R 3 166 0 R 4 167 0 R - 5 168 0 R 6 169 0 R 7 170 0 R 8 171 0 R 9 172 0 R - 10 173 0 R 11 174 0 R 12 175 0 R 13 176 0 R 14 177 0 R - 15 178 0 R 16 179 0 R 17 180 0 R 18 181 0 R 19 182 0 R - 20 183 0 R 21 184 0 R 22 185 0 R 23 186 0 R 24 187 0 R - 25 188 0 R 26 189 0 R 27 190 0 R 28 191 0 R 29 192 0 R - 30 193 0 R 31 194 0 R ] ->> -endobj 163 0 obj << -/S /D /St 1 +/Nums [ 0 164 0 R 1 165 0 R 2 166 0 R 3 167 0 R 4 168 0 R + 5 169 0 R 6 170 0 R 7 171 0 R 8 172 0 R 9 173 0 R + 10 174 0 R 11 175 0 R 12 176 0 R 13 177 0 R 14 178 0 R + 15 179 0 R 16 180 0 R 17 181 0 R 18 182 0 R 19 183 0 R + 20 184 0 R 21 185 0 R 22 186 0 R 23 187 0 R 24 188 0 R + 25 189 0 R 26 190 0 R 27 191 0 R 28 192 0 R 29 193 0 R + 30 194 0 R 31 195 0 R ] >> endobj 164 0 obj << -/S /D /St 2 +/S /D /St 1 >> endobj 165 0 obj << -/S /D /St 3 +/S /D /St 2 >> endobj 166 0 obj << -/S /D /St 4 +/S /D /St 3 >> endobj 167 0 obj << -/S /D /St 5 +/S /D /St 4 >> endobj 168 0 obj << -/S /D /St 6 +/S /D /St 5 >> endobj 169 0 obj << -/S /D /St 7 +/S /D /St 6 >> endobj 170 0 obj << -/S /D /St 8 +/S /D /St 7 >> endobj 171 0 obj << -/S /D /St 9 +/S /D /St 8 >> endobj 172 0 obj << -/S /D /St 10 +/S /D /St 9 >> endobj 173 0 obj << -/S /D /St 11 +/S /D /St 10 >> endobj 174 0 obj << -/S /D /St 12 +/S /D /St 11 >> endobj 175 0 obj << -/S /D /St 13 +/S /D /St 12 >> endobj 176 0 obj << -/S /D /St 14 +/S /D /St 13 >> endobj 177 0 obj << -/S /D /St 15 +/S /D /St 14 >> endobj 178 0 obj << -/S /D /St 16 +/S /D /St 15 >> endobj 179 0 obj << -/S /D /St 17 +/S /D /St 16 >> endobj 180 0 obj << -/S /D /St 18 +/S /D /St 17 >> endobj 181 0 obj << -/S /D /St 19 +/S /D /St 18 >> endobj 182 0 obj << -/S /D /St 20 +/S /D /St 19 >> endobj 183 0 obj << -/S /D /St 21 +/S /D /St 20 >> endobj 184 0 obj << -/S /D /St 22 +/S /D /St 21 >> endobj 185 0 obj << -/S /D /St 23 +/S /D /St 22 >> endobj 186 0 obj << -/S /D /St 24 +/S /D /St 23 >> endobj 187 0 obj << -/S /D /St 25 +/S /D /St 24 >> endobj 188 0 obj << -/S /D /St 26 +/S /D /St 25 >> endobj 189 0 obj << -/S /D /St 27 +/S /D /St 26 >> endobj 190 0 obj << -/S /D /St 28 +/S /D /St 27 >> endobj 191 0 obj << -/S /D /St 29 +/S /D /St 28 >> endobj 192 0 obj << -/S /D /St 30 +/S /D /St 29 >> endobj 193 0 obj << -/S /D /St 31 +/S /D /St 30 >> endobj 194 0 obj << +/S /D /St 31 +>> +endobj +195 0 obj +<< /S /D /St 32 >> endobj xref -0 195 +0 196 0000000000 65535 f 0000000061 00000 n 0000000180 00000 n @@ -11846,7 +11867,7 @@ xref 0001842278 00000 n 0001842486 00000 n 0001842694 00000 n -0001842778 00000 n +0001842902 00000 n 0001842986 00000 n 0001843194 00000 n 0001843402 00000 n @@ -11906,115 +11927,116 @@ xref 0002376160 00000 n 0002376312 00000 n 0002376479 00000 n -0002376631 00000 n -0002376818 00000 n -0002376965 00000 n -0002377120 00000 n -0002377293 00000 n -0002377448 00000 n -0002377594 00000 n -0002377752 00000 n -0002377899 00000 n -0002378086 00000 n -0002378207 00000 n -0002378368 00000 n -0002378510 00000 n -0002378662 00000 n -0002378816 00000 n -0002378957 00000 n -0002379095 00000 n -0002379249 00000 n -0002379451 00000 n -0002379574 00000 n -0002379713 00000 n -0002379877 00000 n -0002380050 00000 n -0002380223 00000 n -0002380370 00000 n -0002380565 00000 n -0002380724 00000 n -0002380892 00000 n -0002381027 00000 n -0002381160 00000 n -0002381305 00000 n -0002381431 00000 n -0002381559 00000 n -0002381670 00000 n -0002381959 00000 n -0002387076 00000 n -0002395160 00000 n -0002399953 00000 n -0002406882 00000 n -0002415796 00000 n -0002425043 00000 n -0002434247 00000 n -0002447264 00000 n -0002457380 00000 n -0002466746 00000 n -0002475326 00000 n -0002486276 00000 n -0002498907 00000 n -0002510827 00000 n -0002520195 00000 n -0002529336 00000 n -0002536960 00000 n -0002546952 00000 n -0002555918 00000 n -0002566223 00000 n -0002569275 00000 n -0002571110 00000 n -0002584566 00000 n -0002601225 00000 n -0002611733 00000 n -0002619192 00000 n -0002625866 00000 n -0002633928 00000 n -0002641864 00000 n -0002648332 00000 n -0002650488 00000 n -0002651566 00000 n -0002651959 00000 n -0002651994 00000 n -0002652029 00000 n -0002652064 00000 n -0002652099 00000 n -0002652134 00000 n -0002652169 00000 n -0002652204 00000 n -0002652239 00000 n -0002652274 00000 n -0002652310 00000 n -0002652346 00000 n -0002652382 00000 n -0002652418 00000 n -0002652454 00000 n -0002652490 00000 n -0002652526 00000 n -0002652562 00000 n -0002652598 00000 n -0002652634 00000 n -0002652670 00000 n -0002652706 00000 n -0002652742 00000 n -0002652778 00000 n -0002652814 00000 n -0002652850 00000 n -0002652886 00000 n -0002652922 00000 n -0002652958 00000 n -0002652994 00000 n -0002653030 00000 n -0002653066 00000 n +0002376644 00000 n +0002376797 00000 n +0002376984 00000 n +0002377131 00000 n +0002377287 00000 n +0002377461 00000 n +0002377617 00000 n +0002377763 00000 n +0002377921 00000 n +0002378068 00000 n +0002378255 00000 n +0002378376 00000 n +0002378537 00000 n +0002378679 00000 n +0002378831 00000 n +0002378985 00000 n +0002379126 00000 n +0002379264 00000 n +0002379418 00000 n +0002379620 00000 n +0002379743 00000 n +0002379882 00000 n +0002380046 00000 n +0002380219 00000 n +0002380392 00000 n +0002380539 00000 n +0002380734 00000 n +0002380893 00000 n +0002381061 00000 n +0002381196 00000 n +0002381329 00000 n +0002381474 00000 n +0002381600 00000 n +0002381728 00000 n +0002381839 00000 n +0002382128 00000 n +0002387245 00000 n +0002395329 00000 n +0002400122 00000 n +0002407051 00000 n +0002415965 00000 n +0002425212 00000 n +0002434416 00000 n +0002447433 00000 n +0002457549 00000 n +0002466915 00000 n +0002475495 00000 n +0002486445 00000 n +0002499076 00000 n +0002509086 00000 n +0002518500 00000 n +0002527270 00000 n +0002537241 00000 n +0002543397 00000 n +0002554154 00000 n +0002563615 00000 n +0002572765 00000 n +0002574875 00000 n +0002588331 00000 n +0002604990 00000 n +0002615498 00000 n +0002622957 00000 n +0002629631 00000 n +0002637693 00000 n +0002645629 00000 n +0002652097 00000 n +0002654253 00000 n +0002655331 00000 n +0002655724 00000 n +0002655759 00000 n +0002655794 00000 n +0002655829 00000 n +0002655864 00000 n +0002655899 00000 n +0002655934 00000 n +0002655969 00000 n +0002656004 00000 n +0002656039 00000 n +0002656075 00000 n +0002656111 00000 n +0002656147 00000 n +0002656183 00000 n +0002656219 00000 n +0002656255 00000 n +0002656291 00000 n +0002656327 00000 n +0002656363 00000 n +0002656399 00000 n +0002656435 00000 n +0002656471 00000 n +0002656507 00000 n +0002656543 00000 n +0002656579 00000 n +0002656615 00000 n +0002656651 00000 n +0002656687 00000 n +0002656723 00000 n +0002656759 00000 n +0002656795 00000 n +0002656831 00000 n trailer << /ID -[] +[] % ReportLab generated PDF document -- digest (opensource) /Info 68 0 R /Root 67 0 R -/Size 195 +/Size 196 >> startxref -2653102 +2656867 %%EOF diff --git a/whitepaper/uncommonlisp-whitepaper.rst b/whitepaper/uncommonlisp-whitepaper.rst index db1fafd..b18fadf 100644 --- a/whitepaper/uncommonlisp-whitepaper.rst +++ b/whitepaper/uncommonlisp-whitepaper.rst @@ -632,26 +632,42 @@ The reason we built the GC at all was to let long-running asm HTTP servers not l Config req/s baseline peak RSS growth KB RSS KB KB ============================== ========= ========= ========== ============= - asm no-GC + ``heap-snapshot`` 484 100 104 **4** - asm GC + ``heap-snapshot`` 462 120 124 **4** - asm no-GC + no snapshot 463 96 45,812 **46,096** - asm GC + no snapshot † — — — + asm no-GC + ``heap-snapshot`` ~300 100 104 **4** + asm GC + ``heap-snapshot`` ~330 120 124 **4** + asm no-GC + no snapshot ~360 96 45,812 **46,096** + asm GC + no snapshot ~410 116 1,088 **972** ============================== ========= ========= ========== ============= -† Crashes at first GC — latent conservative-scan bug, see below. +All four cells validate cleanly now: -Three cells validate cleanly: - -- **Cells 1 and 2** show that on idiomatic code using ``heap-snapshot``, both binaries hold memory absolutely flat (~4 KB growth over 5,000 requests is normal VM noise). The GC build costs ~5% throughput for a feature the snapshot pattern doesn't need — a meaningful signal that if your server is well-written, GC is optional overhead. +- **Cells 1 and 2** show that on idiomatic code using ``heap-snapshot``, both binaries hold memory absolutely flat (~4 KB growth over 5,000 requests is normal VM noise). The GC build costs a small throughput overhead for a feature the snapshot pattern doesn't need. - **Cell 3** demonstrates the leak scenario we explicitly designed the GC build to solve. Without ``heap-snapshot``, the no-GC asm server grows **~9 KB per request** — 46 MB over 5,000 requests, heading to OOM on any real workload. This is the bump-only allocator working exactly as documented. -- **Cell 4** is the one that should have been bounded by naive mark-sweep and wasn't. The server crashes at the first GC trigger (~1 MB of allocations into the run), fixed-size workload triggering another variant of the conservative stack scan's type-confusion. The pattern is identical in kind to the 24-byte env/string collision (§6.6.1) we already fixed — probably a 24- or 40-byte response block being walked as something it isn't. The fix requires tightening one more walker; we logged it as a known issue rather than shipping a fix under time pressure. +- **Cell 4** is the use case the GC was built for. With neither ``heap-snapshot`` nor ``heap-restore``, the GC build bounds memory at one chunk (~1 MB) and serves **faster than the leaking no-GC version** because it doesn't pay ``heap_grow`` mmap-every-64-MB costs on repeated allocation. **972 KB of growth** across 5,000 requests is exactly one heap chunk — the collector hit its natural steady state. -**Honest read.** The GC build succeeds at validating the snapshot pattern (cell 2 is the real deployment target for long-running asm servers) but the "use GC instead of snapshots" use case (cell 4) has an outstanding correctness bug. ``heap-snapshot`` + ``heap-restore`` remain the recommended pattern for production asm code; the naive GC serves as a diagnostic backstop and as the control-group baseline for future memory-management work. This is still progress — we now have a concrete failing case to aim the next round of debugging at, rather than a vague worry. +**Precise-type dispatch was the fix.** Cell 4 was crashing at first GC until we replaced the conservative-scan-plus-sentinel-checks walker with a precise one. Every heap block's 8-byte header now carries an explicit type byte at bits 8–15 (see §6.6.5 below for the redesign), so ``gc_mark_drain``, ``gc_mark_env``, and the arena-escape scan dispatch on the type byte instead of guessing from block size. This eliminated the entire class of "24-byte env vs string" / "40-byte vector vs string" type-confusion bugs we'd been patching one-by-one. + +**Honest read.** The GC build now succeeds at the "GC instead of snapshots" use case. ``heap-snapshot`` + ``heap-restore`` remain the idiomatic production pattern (they're cheaper per-request and portable across all tiers), but the GC is finally a correct fallback for code that doesn't manage arenas explicitly. Remaining rough edge: on very heavy sustained allocation workloads (hash-set benchmark at the ~1 MB/iter scale under the GC build) we still see the occasional unbound-variable error that points to a root-scan edge case the precise-type fix didn't completely close. Tracked as a follow-up. **Reproduce:** ``make bench-gc-http``. Tuning: ``REQUESTS=10000 CONCURRENCY=16 VCAP=524288 bash tests/bench-gc-http.sh``. +6.6.5 Precise Block Typing: Killing a Class of Bugs +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Earlier versions of the meta-GC walkers inferred block type from *size* alone. A 24-byte block could be an env node, a closure, or a 16-character string; a 40-byte block could be a 4-element vector or a 25-character string. The walkers tried to guess and guessed wrong under the conservative stack scan — any stack word whose low 3 bits happened to match ``TAG_SYM`` or ``7`` (vector-family) would be dereferenced, its block's size read from the header, and the walker would interpret subsequent payload bytes as tagged child values. Strings-as-vectors reading 200 bytes past their end was the canonical failure. + +We fixed this by adding an explicit type byte to every heap block's header:: + + # Old: [size:63 | mark:1] + # New: [size:48 | type:8 | flags:8 (mark at bit 0)] + +Type constants (``HT_PAIR``, ``HT_CLOSURE``, ``HT_STRING``, ``HT_SYMBOL``, ``HT_VECTOR``, ``HT_HASHTABLE``, ``HT_HASHSET``, ``HT_ENVNODE``, ``HT_CHAINNODE``, ``HT_PADDING``) are set at every ``heap_alloc`` call site in the GC build. Every walker — mark, escape-scan, sweep — now dispatches on the type byte instead of size. A string can never be walked as a vector; an env node can never be confused with a closure. + +Cost: one extra ``orq`` at each of ~15 allocation sites (a few nanoseconds per call) and 16 bits of header space per block (negligible given minimum block size is 16 payload bytes + 8 header bytes). Benefit: the entire "conservative scan misidentifies X as Y" class of bugs goes away. Cell 4 of §6.6.4 flipped from "crashes at first GC" to "working correctly" when this landed. + +The precise-type change also simplified the walkers: the special-case "is the first word -1 (hash-table) or -2 (hash-set) or a small positive number (vector length)" dispatch in ``gc_mark_drain`` collapsed into a single ``cmp`` on the type byte. ~50 lines of heuristic-guessing code deleted. + 7. Portal: Feedback Across Time ----------------------------------------