diff --git a/whitepaper/uncommonlisp-whitepaper.pdf b/whitepaper/uncommonlisp-whitepaper.pdf index ac6bf92..56aea33 100644 --- a/whitepaper/uncommonlisp-whitepaper.pdf +++ b/whitepaper/uncommonlisp-whitepaper.pdf @@ -358,7 +358,7 @@ 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 476.6236 334.3536 488.6236 ] /Subtype /Link /Type /Annot >> endobj 44 0 obj @@ -584,7 +584,7 @@ endobj endobj 69 0 obj << -/Author () /CreationDate (D:20260418194134-04'00') /Creator (\(unspecified\)) /Keywords () /ModDate (D:20260418194134-04'00') /Producer (ReportLab PDF Library - \(opensource\)) +/Author () /CreationDate (D:20260418195221-04'00') /Creator (\(unspecified\)) /Keywords () /ModDate (D:20260418195221-04'00') /Producer (ReportLab PDF Library - \(opensource\)) /Subject (\(unspecified\)) /Title () /Trapped /False >> endobj @@ -730,105 +730,105 @@ endobj endobj 97 0 obj << -/Dest [ 34 0 R /XYZ 57.02362 207.0236 0 ] /Parent 92 0 R /Prev 96 0 R /Title (6.6.5 Precise Block Typing: Killing a Class of Bugs) +/Dest [ 35 0 R /XYZ 57.02362 765.0236 0 ] /Parent 92 0 R /Prev 96 0 R /Title (6.6.5 Precise Block Typing: Killing a Class of Bugs) >> endobj 98 0 obj << -/Count 8 /Dest [ 35 0 R /XYZ 57.02362 562.6236 0 ] /First 99 0 R /Last 106 0 R /Next 107 0 R /Parent 71 0 R +/Count 8 /Dest [ 35 0 R /XYZ 57.02362 446.6236 0 ] /First 99 0 R /Last 106 0 R /Next 107 0 R /Parent 71 0 R /Prev 86 0 R /Title (7. Portal: Feedback Across Time) >> endobj 99 0 obj << -/Dest [ 35 0 R /XYZ 57.02362 359.4236 0 ] /Next 100 0 R /Parent 98 0 R /Title (7.1 S-Expression Portal \204 the Portable One) +/Dest [ 35 0 R /XYZ 57.02362 243.4236 0 ] /Next 100 0 R /Parent 98 0 R /Title (7.1 S-Expression Portal \204 the Portable One) >> endobj 100 0 obj << -/Dest [ 35 0 R /XYZ 57.02362 118.2236 0 ] /Next 101 0 R /Parent 98 0 R /Prev 99 0 R /Title (7.2 Cross-Implementation Exchange Matrix) +/Dest [ 37 0 R /XYZ 57.02362 685.0236 0 ] /Next 101 0 R /Parent 98 0 R /Prev 99 0 R /Title (7.2 Cross-Implementation Exchange Matrix) >> endobj 101 0 obj << -/Dest [ 37 0 R /XYZ 57.02362 577.0236 0 ] /Next 102 0 R /Parent 98 0 R /Prev 100 0 R /Title (7.3 JSON Portal \204 Graph-Aware, Continuation-Preserving) +/Dest [ 37 0 R /XYZ 57.02362 455.0236 0 ] /Next 102 0 R /Parent 98 0 R /Prev 100 0 R /Title (7.3 JSON Portal \204 Graph-Aware, Continuation-Preserving) >> endobj 102 0 obj << -/Count 1 /Dest [ 37 0 R /XYZ 57.02362 290.2236 0 ] /First 103 0 R /Last 103 0 R /Next 104 0 R /Parent 98 0 R +/Count 1 /Dest [ 37 0 R /XYZ 57.02362 168.2236 0 ] /First 103 0 R /Last 103 0 R /Next 104 0 R /Parent 98 0 R /Prev 101 0 R /Title (7.4 Binary Heap Dump \204 the Fast One) >> endobj 103 0 obj << -/Dest [ 38 0 R /XYZ 57.02362 729.0236 0 ] /Parent 102 0 R /Title (7.4.1 The GC Build Uses S-Expressions) +/Dest [ 38 0 R /XYZ 57.02362 603.4236 0 ] /Parent 102 0 R /Title (7.4.1 The GC Build Uses S-Expressions) >> endobj 104 0 obj << -/Dest [ 38 0 R /XYZ 57.02362 467.4236 0 ] /Next 105 0 R /Parent 98 0 R /Prev 102 0 R /Title (7.5 Cross-Process Benchmarks) +/Dest [ 38 0 R /XYZ 57.02362 341.8236 0 ] /Next 105 0 R /Parent 98 0 R /Prev 102 0 R /Title (7.5 Cross-Process Benchmarks) >> endobj 105 0 obj << -/Dest [ 38 0 R /XYZ 57.02362 153.4236 0 ] /Next 106 0 R /Parent 98 0 R /Prev 104 0 R /Title (7.6 Mismatch Cases: Graceful Degradation) +/Dest [ 39 0 R /XYZ 57.02362 715.0236 0 ] /Next 106 0 R /Parent 98 0 R /Prev 104 0 R /Title (7.6 Mismatch Cases: Graceful Degradation) >> endobj 106 0 obj << -/Dest [ 39 0 R /XYZ 57.02362 571.0236 0 ] /Parent 98 0 R /Prev 105 0 R /Title (7.7 Use Case: Distributed Primality Testing) +/Dest [ 39 0 R /XYZ 57.02362 449.0236 0 ] /Parent 98 0 R /Prev 105 0 R /Title (7.7 Use Case: Distributed Primality Testing) >> endobj 107 0 obj << -/Count 6 /Dest [ 39 0 R /XYZ 57.02362 370.2236 0 ] /First 108 0 R /Last 113 0 R /Next 114 0 R /Parent 71 0 R +/Count 6 /Dest [ 39 0 R /XYZ 57.02362 248.2236 0 ] /First 108 0 R /Last 113 0 R /Next 114 0 R /Parent 71 0 R /Prev 98 0 R /Title (8. The EML Universality Proof) >> endobj 108 0 obj << -/Dest [ 39 0 R /XYZ 57.02362 293.0236 0 ] /Next 109 0 R /Parent 107 0 R /Title (8.1 The Operator) +/Dest [ 39 0 R /XYZ 57.02362 171.0236 0 ] /Next 109 0 R /Parent 107 0 R /Title (8.1 The Operator) >> endobj 109 0 obj << -/Dest [ 39 0 R /XYZ 57.02362 216.2236 0 ] /Next 110 0 R /Parent 107 0 R /Prev 108 0 R /Title (8.2 Stage 1: Core Functions \(Depth 1--3\)) +/Dest [ 40 0 R /XYZ 57.02362 765.0236 0 ] /Next 110 0 R /Parent 107 0 R /Prev 108 0 R /Title (8.2 Stage 1: Core Functions \(Depth 1--3\)) >> endobj 110 0 obj << -/Dest [ 40 0 R /XYZ 57.02362 765.0236 0 ] /Next 111 0 R /Parent 107 0 R /Prev 109 0 R /Title (8.3 Stage 2: Arithmetic) +/Dest [ 40 0 R /XYZ 57.02362 645.0236 0 ] /Next 111 0 R /Parent 107 0 R /Prev 109 0 R /Title (8.3 Stage 2: Arithmetic) >> endobj 111 0 obj << -/Dest [ 40 0 R /XYZ 57.02362 650.6236 0 ] /Next 112 0 R /Parent 107 0 R /Prev 110 0 R /Title (8.4 Stage 3: Complex Plane Access) +/Dest [ 40 0 R /XYZ 57.02362 530.6236 0 ] /Next 112 0 R /Parent 107 0 R /Prev 110 0 R /Title (8.4 Stage 3: Complex Plane Access) >> endobj 112 0 obj << -/Dest [ 40 0 R /XYZ 57.02362 542.6236 0 ] /Next 113 0 R /Parent 107 0 R /Prev 111 0 R /Title (8.5 Stage 4: Trigonometry via Euler) +/Dest [ 40 0 R /XYZ 57.02362 422.6236 0 ] /Next 113 0 R /Parent 107 0 R /Prev 111 0 R /Title (8.5 Stage 4: Trigonometry via Euler) >> endobj 113 0 obj << -/Dest [ 40 0 R /XYZ 57.02362 446.6236 0 ] /Parent 107 0 R /Prev 112 0 R /Title (8.6 Verification & Friction Analysis) +/Dest [ 40 0 R /XYZ 57.02362 326.6236 0 ] /Parent 107 0 R /Prev 112 0 R /Title (8.6 Verification & Friction Analysis) >> endobj 114 0 obj << -/Dest [ 42 0 R /XYZ 57.02362 441.0236 0 ] /Next 115 0 R /Parent 71 0 R /Prev 107 0 R /Title (9. Language Coverage) +/Dest [ 42 0 R /XYZ 57.02362 339.0236 0 ] /Next 115 0 R /Parent 71 0 R /Prev 107 0 R /Title (9. Language Coverage) >> endobj 115 0 obj << -/Dest [ 42 0 R /XYZ 57.02362 191.8236 0 ] /Next 116 0 R /Parent 71 0 R /Prev 114 0 R /Title (10. Relationship to Companion Papers) +/Dest [ 44 0 R /XYZ 57.02362 765.0236 0 ] /Next 116 0 R /Parent 71 0 R /Prev 114 0 R /Title (10. Relationship to Companion Papers) >> endobj 116 0 obj << -/Count 6 /Dest [ 44 0 R /XYZ 57.02362 633.0236 0 ] /First 117 0 R /Last 122 0 R /Next 123 0 R /Parent 71 0 R +/Count 6 /Dest [ 44 0 R /XYZ 57.02362 515.8236 0 ] /First 117 0 R /Last 122 0 R /Next 123 0 R /Parent 71 0 R /Prev 115 0 R /Title (11. Four Implementation Tiers, One Language) >> endobj @@ -5789,7 +5789,7 @@ endstream endobj 146 0 obj << -/Length 9957 +/Length 9939 >> stream 1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET @@ -5855,7 +5855,7 @@ q 1 0 0 1 390.9827 75 cm q 0 0 0 rg -BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 16.84783 0 Td (growth KB) Tj T* -16.84783 0 Td ET +BT 1 0 0 1 0 14 Tm /F3 10 Tf 12 TL 8.232835 0 Td (growth KB \(20) Tj T* 14.715 0 Td (000 req\)) Tj T* -22.94783 0 Td ET Q Q 0 0 0 rg @@ -5870,28 +5870,28 @@ 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 (~300) Tj T* ET +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (~240) Tj T* ET Q Q q 1 0 0 1 256.2387 57 cm q 0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (100) Tj T* ET +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (96) Tj T* ET Q Q q 1 0 0 1 323.6107 57 cm q 0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (104) Tj T* ET +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (96) Tj T* ET Q Q q 1 0 0 1 390.9827 57 cm q 0 0 0 rg -BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL (4) Tj T* ET +BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL (0) Tj T* ET Q Q q @@ -5904,7 +5904,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 (~330) Tj T* ET +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (~235) Tj T* ET Q Q q @@ -5918,14 +5918,14 @@ q 1 0 0 1 323.6107 39 cm q 0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (124) Tj T* ET +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (120) Tj T* ET Q Q q 1 0 0 1 390.9827 39 cm q 0 0 0 rg -BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL (4) Tj T* ET +BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL (0) Tj T* ET Q Q q @@ -5939,28 +5939,28 @@ 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 (~360) Tj T* ET +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (~470) Tj T* ET Q Q q 1 0 0 1 256.2387 21 cm q 0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (96) Tj T* ET +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (264) Tj T* ET Q Q q 1 0 0 1 323.6107 21 cm q 0 0 0 rg -BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (45,812) Tj T* ET +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (185,000) Tj T* ET Q Q q 1 0 0 1 390.9827 21 cm q 0 0 0 rg -BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL (46,096) Tj T* ET +BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL (185,000) Tj T* ET Q Q q @@ -5974,21 +5974,21 @@ 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 (~410) Tj T* ET +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (~450) 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 (116) Tj T* ET +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (112) 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 (1,088) Tj T* ET +BT 1 0 0 1 0 2 Tm /F1 10 Tf 12 TL (1,084) Tj T* ET Q Q q @@ -6024,8 +6024,7 @@ Q 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 (All four cells validate cleanly now:) Tj T* ET +BT 1 0 0 1 0 2 Tm 12 TL /F1 10 Tf 0 0 0 rg (All four cells validate cleanly now at ) Tj /F3 10 Tf (20,000 requests per cell) Tj /F1 10 Tf ( \(up from the original 5,000\):) Tj T* ET Q Q q @@ -6116,47 +6115,59 @@ BT 1 0 0 1 0 62 Tm 5.961223 Tw 12 TL /F3 10 Tf 0 0 0 rg (Precise-type dispatch w Q Q q -1 0 0 1 57.02362 249.0236 cm +1 0 0 1 57.02362 285.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 +BT 1 0 0 1 0 26 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 (tiers\), but the GC is finally a correct fallback for code that doesn't manage arenas explicitly.) Tj T* ET Q Q q 1 0 0 1 57.02362 219.0236 cm q +BT 1 0 0 1 0 50 Tm .974609 Tw 12 TL /F3 10 Tf 0 0 0 rg (Soak result.) Tj /F1 10 Tf ( At 20,000 HTTP requests \327 16 concurrent clients, the GC build serves ~450 req/s with peak) Tj T* 0 Tw .635702 Tw (RSS of 1,084 KB \227 one heap chunk, steady state. 972 KB of growth represents the heap filling up exactly) Tj T* 0 Tw .734556 Tw (once after which the collector keeps reusing reclaimed space. This is the production validation we needed:) Tj T* 0 Tw .602844 Tw (naive mark-sweep is a correct, if not optimal, allocator for long-running asm servers that don't want to think) Tj T* 0 Tw (about arena discipline.) Tj T* ET +Q +Q +q +1 0 0 1 57.02362 141.0236 cm +q +BT 1 0 0 1 0 62 Tm .006147 Tw 12 TL /F1 10 Tf 0 0 0 rg (Remaining rough edges: at larger scales \(50k+ requests with 512 MB ) Tj /F5 10 Tf (ulimit) Tj ( ) Tj (-v) Tj /F1 10 Tf ( and the bump-only no-GC) Tj T* 0 Tw .22135 Tw (case saturating the cap right before cell 4 starts\) we've seen cell 4 die at server startup; this appears to be a) Tj T* 0 Tw .776147 Tw (process-environment issue rather than a GC bug, but we don't have a clean explanation yet. The hash-set) Tj T* 0 Tw 4.063453 Tw (benchmark on the GC build under the ~1 MB-per-iteration scale also still surfaces an occasional) Tj T* 0 Tw 1.755223 Tw (unbound-variable error pointing to a root-scan edge case the precise-type fix didn't fully close. Both are) Tj T* 0 Tw (tracked as follow-ups.) Tj T* ET +Q +Q +q +1 0 0 1 57.02362 111.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 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 147 0 obj << -/Length 9512 +/Length 8922 >> 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 +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 (6.6.5 Precise Block Typing: Killing a Class of Bugs) Tj T* ET +Q +Q +q +1 0 0 1 57.02362 675.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 657.0236 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 +q +1 0 0 1 57.02362 616.6236 cm q q 1 0 0 1 0 0 cm @@ -6177,40 +6188,40 @@ Q Q Q q -1 0 0 1 57.02362 676.6236 cm +1 0 0 1 57.02362 560.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 +1 0 0 1 57.02362 506.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 +1 0 0 1 57.02362 464.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 +1 0 0 1 57.02362 433.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 505.4236 cm +1 0 0 1 57.02362 389.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 499.4236 cm +1 0 0 1 57.02362 383.4236 cm Q q -1 0 0 1 57.02362 403.4236 cm +1 0 0 1 57.02362 287.4236 cm q 1 1 1 rg n 0 96 481.2283 -18 re f* @@ -6413,29 +6424,29 @@ Q Q Q q -1 0 0 1 57.02362 403.4236 cm +1 0 0 1 57.02362 287.4236 cm Q q -1 0 0 1 57.02362 373.4236 cm +1 0 0 1 57.02362 257.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 347.4236 cm +1 0 0 1 57.02362 231.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 329.4236 cm +1 0 0 1 57.02362 213.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 260.2236 cm +1 0 0 1 57.02362 144.2236 cm q q 1 0 0 1 0 0 cm @@ -6456,89 +6467,16 @@ Q Q Q q -1 0 0 1 57.02362 228.2236 cm +1 0 0 1 57.02362 112.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 174.2236 cm +1 0 0 1 57.02362 82.22362 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 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 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 94.22362 cm -Q -q -1 0 0 1 57.02362 76.22362 cm -q -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 3 cm -q -0 0 0 rg -BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 12.29549 0 Td (Producer ) Tj /F6 10 Tf 12 TL (\256) Tj /F3 10 Tf 12 TL T* -12.29549 0 Td ET -Q -Q -q -1 0 0 1 99.14097 3 cm -q -0 0 0 rg -BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 23.62549 0 Td (Python) Tj T* -23.62549 0 Td ET -Q -Q -q -1 0 0 1 192.2819 3 cm -q -0 0 0 rg -BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 36.96049 0 Td (C) Tj T* -36.96049 0 Td ET -Q -Q -q -1 0 0 1 285.4229 3 cm -q -0 0 0 rg -BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 30.56549 0 Td (asm) Tj T* -30.56549 0 Td ET -Q -Q -q -1 0 0 1 378.5639 3 cm -q -0 0 0 rg -BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 30.82723 0 Td (asm-gc) Tj T* -30.82723 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 93.14097 0 m 93.14097 18 l S -n 186.2819 0 m 186.2819 18 l S -n 279.4229 0 m 279.4229 18 l S -n 372.5639 0 m 372.5639 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 +BT 1 0 0 1 0 14 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 ET Q Q @@ -6546,26 +6484,84 @@ endstream endobj 148 0 obj << -/Length 9728 +/Length 10433 >> stream 1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET q -1 0 0 1 57.02362 675.0236 cm +1 0 0 1 57.02362 741.0236 cm +q +BT 1 0 0 1 0 14 Tm 5.458196 Tw 12 TL /F1 10 Tf 0 0 0 rg (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 699.0236 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 673.0236 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 661.0236 cm +Q +q +1 0 0 1 57.02362 553.0236 cm q 1 1 1 rg +n 0 108 481.2283 -18 re f* +.878431 .878431 .878431 rg n 0 90 481.2283 -18 re f* -.878431 .878431 .878431 rg +1 1 1 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* +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 93 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 12.29549 0 Td (Producer ) Tj /F6 10 Tf 12 TL (\256) Tj /F3 10 Tf 12 TL T* -12.29549 0 Td ET +Q +Q +q +1 0 0 1 99.14097 93 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 23.62549 0 Td (Python) Tj T* -23.62549 0 Td ET +Q +Q +q +1 0 0 1 192.2819 93 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 36.96049 0 Td (C) Tj T* -36.96049 0 Td ET +Q +Q +q +1 0 0 1 285.4229 93 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 30.56549 0 Td (asm) Tj T* -30.56549 0 Td ET +Q +Q +q +1 0 0 1 378.5639 93 cm +q +0 0 0 rg +BT 1 0 0 1 0 2 Tm /F3 10 Tf 12 TL 30.82723 0 Td (asm-gc) Tj T* -30.82723 0 Td ET +Q +Q +q 1 0 0 1 6 75 cm q 0 0 0 rg @@ -6724,52 +6720,53 @@ 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 93.14097 0 m 93.14097 90 l S -n 186.2819 0 m 186.2819 90 l S -n 279.4229 0 m 279.4229 90 l S -n 372.5639 0 m 372.5639 90 l S -n 0 0 m 0 90 l S -n 481.2283 0 m 481.2283 90 l S +n 93.14097 0 m 93.14097 108 l S +n 186.2819 0 m 186.2819 108 l S +n 279.4229 0 m 279.4229 108 l S +n 372.5639 0 m 372.5639 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 675.0236 cm +1 0 0 1 57.02362 553.0236 cm Q q -1 0 0 1 57.02362 633.0236 cm +1 0 0 1 57.02362 511.0236 cm q BT 1 0 0 1 0 26 Tm .856835 Tw 12 TL /F1 10 Tf 0 0 0 rg (16 of 16. 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 (\). The ) Tj /F5 10 Tf (asm-gc) Tj /F1 10 Tf ( column) Tj T* 0 Tw .316962 Tw (expands the matrix from 9 to 16 cells \227 the GC build's ) Tj /F5 10 Tf (portal-save) Tj /F1 10 Tf ( emits the same S-expression format,) Tj T* 0 Tw (so it exchanges with every other tier \(\2477.4.1 below\).) Tj T* ET Q Q q -1 0 0 1 57.02362 591.0236 cm +1 0 0 1 57.02362 469.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 565.0236 cm +1 0 0 1 57.02362 443.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 535.0236 cm +1 0 0 1 57.02362 413.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 529.0236 cm +1 0 0 1 57.02362 407.0236 cm Q q -1 0 0 1 57.02362 529.0236 cm +1 0 0 1 57.02362 407.0236 cm Q q -1 0 0 1 57.02362 517.0236 cm +1 0 0 1 57.02362 395.0236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -6791,10 +6788,10 @@ Q Q Q q -1 0 0 1 57.02362 511.0236 cm +1 0 0 1 57.02362 389.0236 cm Q q -1 0 0 1 57.02362 499.0236 cm +1 0 0 1 57.02362 377.0236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -6817,10 +6814,10 @@ Q Q Q q -1 0 0 1 57.02362 493.0236 cm +1 0 0 1 57.02362 371.0236 cm Q q -1 0 0 1 57.02362 481.0236 cm +1 0 0 1 57.02362 359.0236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -6842,10 +6839,10 @@ Q Q Q q -1 0 0 1 57.02362 475.0236 cm +1 0 0 1 57.02362 353.0236 cm Q q -1 0 0 1 57.02362 463.0236 cm +1 0 0 1 57.02362 341.0236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -6868,10 +6865,10 @@ Q Q Q q -1 0 0 1 57.02362 457.0236 cm +1 0 0 1 57.02362 335.0236 cm Q q -1 0 0 1 57.02362 445.0236 cm +1 0 0 1 57.02362 323.0236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -6894,22 +6891,22 @@ Q Q Q q -1 0 0 1 57.02362 427.0236 cm +1 0 0 1 57.02362 305.0236 cm Q q -1 0 0 1 57.02362 397.0236 cm +1 0 0 1 57.02362 275.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 355.0236 cm +1 0 0 1 57.02362 233.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 q -1 0 0 1 57.02362 324.2236 cm +1 0 0 1 57.02362 202.2236 cm q q 1 0 0 1 0 0 cm @@ -6930,26 +6927,26 @@ Q Q Q q -1 0 0 1 57.02362 304.2236 cm +1 0 0 1 57.02362 182.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 278.2236 cm +1 0 0 1 57.02362 156.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 248.2236 cm +1 0 0 1 57.02362 126.2236 cm q BT 1 0 0 1 0 14 Tm .625197 Tw 12 TL /F1 10 Tf 0 0 0 rg (The ) Tj /F3 10 Tf (no-GC) Tj /F1 10 Tf ( 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 T* 0 Tw (\(bump 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 150.2236 cm +1 0 0 1 57.02362 66.62362 cm q q 1 0 0 1 0 0 cm @@ -6959,57 +6956,72 @@ q .662745 .662745 .662745 RG .5 w .960784 .960784 .960784 rg -n -6 -6 480.0283 88.8 re B* +n -6 -6 480.0283 50.4 re B* Q q 0 0 0 rg -BT 1 0 0 1 0 68.8 Tm /F5 8 Tf 9.6 TL (bi_portal_save:) Tj T* ( # Magic | heap_size | heap_base | r14 | r15 | reserved | heap_bytes) Tj T* T* (bi_portal_resume:) Tj T* ( # Read 48-byte header, verify magic + sanity,) Tj T* ( # mmap MAP_FIXED at saved heap_base so pointers stay valid,) Tj T* ( # read heap bytes into fixed-address region,) Tj T* ( # restore r14/r15.) Tj T* ET +BT 1 0 0 1 0 30.4 Tm /F5 8 Tf 9.6 TL (bi_portal_save:) Tj T* ( # Magic | heap_size | heap_base | r14 | r15 | reserved | heap_bytes) Tj T* T* (bi_portal_resume:) Tj T* ET Q Q Q Q Q -q -1 0 0 1 57.02362 106.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 76.22362 cm -q -BT 1 0 0 1 0 14 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 ET -Q -Q endstream endobj 149 0 obj << -/Length 9597 +/Length 8524 >> 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 713.4236 cm q -BT 1 0 0 1 0 14 Tm 1.065522 Tw 12 TL /F1 10 Tf 0 0 0 rg (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 +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 50.4 re B* +Q +q +0 0 0 rg +BT 1 0 0 1 0 30.4 Tm /F5 8 Tf 9.6 TL ( # Read 48-byte header, verify magic + sanity,) Tj T* ( # mmap MAP_FIXED at saved heap_base so pointers stay valid,) Tj T* ( # read heap bytes into fixed-address region,) Tj T* ( # restore r14/r15.) Tj T* ET +Q +Q +Q Q Q q -1 0 0 1 57.02362 717.0236 cm +1 0 0 1 57.02362 669.4236 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 615.4236 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 +q +1 0 0 1 57.02362 591.4236 cm q BT 1 0 0 1 0 2 Tm 12 TL /F2 10 Tf .133333 .133333 .133333 rg (7.4.1 The GC Build Uses S-Expressions) Tj T* ET Q Q q -1 0 0 1 57.02362 651.0236 cm +1 0 0 1 57.02362 525.4236 cm q BT 1 0 0 1 0 50 Tm 1.037917 Tw 12 TL /F1 10 Tf 0 0 0 rg (The ) Tj /F3 10 Tf (GC) Tj /F1 10 Tf ( asm build can't use the binary heap dump because the heap is a linked list of chunks with typed) Tj T* 0 Tw .619897 Tw (block headers and a free list \227 raw-byte serialization would lose the structure. Rather than inventing portal) Tj T* 0 Tw 1.255596 Tw (v2 with chunk tables and pointer-relocation metadata, the GC build's ) Tj /F5 10 Tf (portal-save) Tj /F1 10 Tf ( walks the global env) Tj T* 0 Tw .200596 Tw (chain from ) Tj /F5 10 Tf (%r14) Tj /F1 10 Tf ( and emits one ) Tj /F5 10 Tf (\(define) Tj ( ) Tj (<) Tj (sym) Tj (>) Tj ( ) Tj (\(quote) Tj ( ) Tj (<) Tj (val) Tj (>) Tj (\)\)) Tj /F1 10 Tf ( form per binding. ) Tj /F5 10 Tf (portal-resume) Tj /F1 10 Tf ( is) Tj T* 0 Tw (equivalent to ) Tj /F5 10 Tf (\(load) Tj ( ) Tj (") Tj (<) Tj (filename) Tj (>) Tj ("\)) Tj /F1 10 Tf ( \227 read every form and eval it.) Tj T* ET Q Q q -1 0 0 1 57.02362 591.4236 cm +1 0 0 1 57.02362 465.8236 cm q q 1 0 0 1 0 0 cm @@ -7030,35 +7042,35 @@ Q Q Q q -1 0 0 1 57.02362 547.4236 cm +1 0 0 1 57.02362 421.8236 cm q 0 0 0 rg BT 1 0 0 1 0 26 Tm /F1 10 Tf 12 TL 1.557565 Tw (Every non-builtin, non-closure binding round-trips. Closures and builtins are skipped \227 closures can't be) Tj T* 0 Tw .869223 Tw (faithfully re-read from their printed form, builtins get re-created from the target interpreter's prelude. This is) Tj T* 0 Tw (the same treatment the JSON portal already gives to builtins \(\2477.3\).) Tj T* ET Q Q q -1 0 0 1 57.02362 481.4236 cm +1 0 0 1 57.02362 355.8236 cm q BT 1 0 0 1 0 50 Tm .145197 Tw 12 TL /F3 10 Tf 0 0 0 rg (Trade-off.) Tj /F1 10 Tf ( The GC build's portal is slower than the binary dump \(walks each binding through the printer\) and) Tj T* 0 Tw 1.91989 Tw (stricter about what it can preserve \(data only, no closures or continuations\). In exchange: ) Tj /F3 10 Tf (every portal) Tj T* 0 Tw 2.369223 Tw (produced by the GC build resumes on every other tier) Tj /F1 10 Tf (, with no MAP_FIXED trick, no architecture) Tj T* 0 Tw -0.128333 Tw (constraint, no "same binary" requirement. A GC-asm producer can hand a portal to a Python consumer \227 we) Tj T* 0 Tw (added the asm-gc column to the \2477.2 matrix and all 16 cells are green.) Tj T* ET Q Q q -1 0 0 1 57.02362 455.4236 cm +1 0 0 1 57.02362 329.8236 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 413.4236 cm +1 0 0 1 57.02362 287.8236 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 407.4236 cm +1 0 0 1 57.02362 281.8236 cm Q q -1 0 0 1 57.02362 209.4236 cm +1 0 0 1 57.02362 83.82362 cm q 1 1 1 rg n 0 198 481.2283 -18 re f* @@ -7264,125 +7276,46 @@ Q Q Q q -1 0 0 1 57.02362 209.4236 cm -Q -q -1 0 0 1 57.02362 167.4236 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 141.4236 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 123.4236 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 117.4236 cm -Q -q -1 0 0 1 57.02362 81.42362 cm -q -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 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 +1 0 0 1 57.02362 83.82362 cm Q endstream endobj 150 0 obj << -/Length 7571 +/Length 8126 >> 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 +1 0 0 1 57.02362 729.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 703.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 685.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 679.0236 cm +Q +q +1 0 0 1 57.02362 529.0236 cm +q +1 1 1 rg +n 0 150 481.2283 -18 re f* +.878431 .878431 .878431 rg +n 0 132 481.2283 -18 re f* 1 1 1 rg n 0 114 481.2283 -30 re f* .878431 .878431 .878431 rg @@ -7394,8 +7327,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 @@ -7535,37 +7526,39 @@ 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 529.0236 cm Q q -1 0 0 1 57.02362 585.0236 cm +1 0 0 1 57.02362 463.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 q -1 0 0 1 57.02362 559.0236 cm +1 0 0 1 57.02362 437.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 310.2236 cm q q 1 0 0 1 0 0 cm @@ -7585,38 +7578,38 @@ Q Q Q q -1 0 0 1 57.02362 388.2236 cm +1 0 0 1 57.02362 266.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 235.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 203.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 185.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 159.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 128.2236 cm q q 1 0 0 1 0 0 cm @@ -7637,19 +7630,28 @@ Q Q Q q -1 0 0 1 57.02362 230.2236 cm +1 0 0 1 57.02362 108.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 + +endstream +endobj +151 0 obj +<< +/Length 9423 +>> +stream +1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET q -1 0 0 1 57.02362 204.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 (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 703.0236 cm q q 1 0 0 1 0 0 cm @@ -7670,28 +7672,19 @@ Q Q Q q -1 0 0 1 57.02362 110.2236 cm +1 0 0 1 57.02362 659.0236 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 -151 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 633.0236 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 544.6236 cm q q 1 0 0 1 0 0 cm @@ -7711,13 +7704,13 @@ Q Q Q q -1 0 0 1 57.02362 638.6236 cm +1 0 0 1 57.02362 518.6236 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 468.6236 cm q q 1 0 0 1 0 0 cm @@ -7738,19 +7731,19 @@ Q Q Q q -1 0 0 1 57.02362 556.6236 cm +1 0 0 1 57.02362 436.6236 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 q -1 0 0 1 57.02362 530.6236 cm +1 0 0 1 57.02362 410.6236 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 360.6236 cm q q 1 0 0 1 0 0 cm @@ -7771,29 +7764,29 @@ Q Q Q q -1 0 0 1 57.02362 460.6236 cm +1 0 0 1 57.02362 340.6236 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 314.6236 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 296.6236 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 290.6236 cm Q q -1 0 0 1 57.02362 260.6236 cm +1 0 0 1 57.02362 140.6236 cm q 1 1 1 rg n 0 150 481.2283 -18 re f* @@ -8029,37 +8022,62 @@ Q Q Q q -1 0 0 1 57.02362 260.6236 cm +1 0 0 1 57.02362 140.6236 cm Q q -1 0 0 1 57.02362 242.6236 cm +1 0 0 1 57.02362 122.6236 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 116.6236 cm Q q -1 0 0 1 57.02362 236.6236 cm +1 0 0 1 57.02362 116.6236 cm Q q -1 0 0 1 57.02362 164.6236 cm +1 0 0 1 57.02362 62.69291 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 38.93071 cm q 0 0 0 rg BT 1 0 0 1 0 2 Tm /F5 10 Tf 12 TL 2 0 Td (1.) Tj T* -2 0 Td ET Q Q q +1 0 0 1 23 14.93071 cm +q +BT 1 0 0 1 0 26 Tm 1.90218 Tw 12 TL /F3 10 Tf 0 0 0 rg (Algorithmic: symbolic vs numerical) Tj /F1 10 Tf ( \227 the Lumbda symbolic rewriter is ) Tj /F3 10 Tf (~1,280\327 faster) Tj /F1 10 Tf ( than the) Tj T* 0 Tw .906556 Tw (Lumbda brute-force search \(46 ms vs 59 s\). This is the MOAD-0001 defect at the proof-methodology) Tj T* 0 Tw .474835 Tw (layer: O\(N\262\) enumerate-and-compare where O\(1\) algebraic reasoning suffices. The brute-force version) Tj T* 0 Tw ET +Q +Q +q +Q +Q +Q + +endstream +endobj +152 0 obj +<< +/Length 8752 +>> +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 62 Tm 1.90218 Tw 12 TL /F3 10 Tf 0 0 0 rg (Algorithmic: symbolic vs numerical) Tj /F1 10 Tf ( \227 the Lumbda symbolic rewriter is ) Tj /F3 10 Tf (~1,280\327 faster) Tj /F1 10 Tf ( than the) Tj T* 0 Tw .906556 Tw (Lumbda brute-force search \(46 ms vs 59 s\). This is the MOAD-0001 defect at the proof-methodology) Tj T* 0 Tw .474835 Tw (layer: O\(N\262\) enumerate-and-compare where O\(1\) algebraic reasoning suffices. The brute-force version) Tj T* 0 Tw .206529 Tw (enumerates every pairwise EML composition at each depth, comparing results against target functions;) Tj T* 0 Tw 2.312025 Tw (the symbolic checker applies 5 rewrites using 3 axioms \() Tj /F5 10 Tf (exp\(ln\(x\)\)) Tj ( ) Tj (=) Tj ( ) Tj (x) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (ln\(exp\(x\)\)) Tj ( ) Tj (=) Tj ( ) Tj (x) Tj /F1 10 Tf (,) Tj T* 0 Tw /F5 10 Tf (ln\(1\)) Tj ( ) Tj (=) Tj ( ) Tj (0) Tj /F1 10 Tf (\) and terminates. Understanding beats search by three orders of magnitude.) Tj T* ET +BT 1 0 0 1 0 26 Tm .206529 Tw 12 TL /F1 10 Tf 0 0 0 rg (enumerates every pairwise EML composition at each depth, comparing results against target functions;) Tj T* 0 Tw 2.312025 Tw (the symbolic checker applies 5 rewrites using 3 axioms \() Tj /F5 10 Tf (exp\(ln\(x\)\)) Tj ( ) Tj (=) Tj ( ) Tj (x) Tj /F1 10 Tf (, ) Tj /F5 10 Tf (ln\(exp\(x\)\)) Tj ( ) Tj (=) Tj ( ) Tj (x) Tj /F1 10 Tf (,) Tj T* 0 Tw /F5 10 Tf (ln\(1\)) Tj ( ) Tj (=) Tj ( ) Tj (0) Tj /F1 10 Tf (\) and terminates. Understanding beats search by three orders of magnitude.) Tj T* ET Q Q q @@ -8067,10 +8085,10 @@ Q Q Q q -1 0 0 1 57.02362 158.6236 cm +1 0 0 1 57.02362 723.0236 cm Q q -1 0 0 1 57.02362 110.6236 cm +1 0 0 1 57.02362 675.0236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -8092,49 +8110,24 @@ Q Q Q q -1 0 0 1 57.02362 104.6236 cm +1 0 0 1 57.02362 669.0236 cm Q q -1 0 0 1 57.02362 62.69291 cm +1 0 0 1 57.02362 609.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 -152 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 @@ -8142,34 +8135,34 @@ Q Q Q q -1 0 0 1 57.02362 729.0236 cm +1 0 0 1 57.02362 609.0236 cm Q q -1 0 0 1 57.02362 663.0236 cm +1 0 0 1 57.02362 543.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 489.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 459.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 453.0236 cm Q q -1 0 0 1 57.02362 573.0236 cm +1 0 0 1 57.02362 453.0236 cm Q q -1 0 0 1 57.02362 537.0236 cm +1 0 0 1 57.02362 417.0236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -8191,10 +8184,10 @@ Q Q Q q -1 0 0 1 57.02362 531.0236 cm +1 0 0 1 57.02362 411.0236 cm Q q -1 0 0 1 57.02362 495.0236 cm +1 0 0 1 57.02362 375.0236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -8216,10 +8209,10 @@ Q Q Q q -1 0 0 1 57.02362 489.0236 cm +1 0 0 1 57.02362 369.0236 cm Q q -1 0 0 1 57.02362 465.0236 cm +1 0 0 1 57.02362 345.0236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -8241,10 +8234,10 @@ Q Q Q q -1 0 0 1 57.02362 465.0236 cm +1 0 0 1 57.02362 345.0236 cm Q q -1 0 0 1 57.02362 395.8236 cm +1 0 0 1 57.02362 275.8236 cm q q 1 0 0 1 0 0 cm @@ -8265,19 +8258,19 @@ Q Q Q q -1 0 0 1 57.02362 351.8236 cm +1 0 0 1 57.02362 231.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 225.8236 cm Q q -1 0 0 1 57.02362 345.8236 cm +1 0 0 1 57.02362 225.8236 cm Q q -1 0 0 1 57.02362 261.8236 cm +1 0 0 1 57.02362 141.8236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -8299,10 +8292,10 @@ Q Q Q q -1 0 0 1 57.02362 261.8236 cm +1 0 0 1 57.02362 141.8236 cm Q q -1 0 0 1 57.02362 183.0236 cm +1 0 0 1 57.02362 63.02362 cm q q 1 0 0 1 0 0 cm @@ -8322,110 +8315,31 @@ Q Q Q Q -q -1 0 0 1 57.02362 115.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 -Q -q -1 0 0 1 57.02362 73.02362 cm -q -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 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 153 0 obj << -/Length 10251 +/Length 10148 >> 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 +1 0 0 1 57.02362 705.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 699.0236 cm +Q +q +1 0 0 1 57.02362 591.0236 cm +q +1 1 1 rg +n 0 108 481.2283 -18 re f* +.878431 .878431 .878431 rg +n 0 90 481.2283 -18 re f* 1 1 1 rg n 0 72 481.2283 -18 re f* .878431 .878431 .878431 rg @@ -8435,8 +8349,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 @@ -8530,104 +8502,119 @@ 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 591.0236 cm Q q -1 0 0 1 57.02362 627.0236 cm +1 0 0 1 57.02362 525.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 459.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 357.0236 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 Q Q q -1 0 0 1 57.02362 427.8236 cm +1 0 0 1 57.02362 325.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 305.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 251.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 221.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 191.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 161.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 107.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 + +endstream +endobj +154 0 obj +<< +/Length 4694 +>> +stream +1 0 0 1 0 0 cm BT /F1 12 Tf 14.4 TL ET q -1 0 0 1 57.02362 178.6236 cm +1 0 0 1 57.02362 751.8236 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 731.8236 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 725.8236 cm Q q -1 0 0 1 57.02362 74.62362 cm +1 0 0 1 57.02362 587.8236 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 @@ -8635,21 +8622,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 @@ -8658,79 +8645,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 -154 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 @@ -8777,36 +8730,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 587.8236 cm Q q -1 0 0 1 57.02362 651.0236 cm +1 0 0 1 57.02362 533.8236 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 502.6236 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 488.6236 cm Q q -1 0 0 1 57.02362 593.8236 cm +1 0 0 1 57.02362 476.6236 cm q 0 0 0 rg BT /F1 10 Tf 12 TL ET @@ -8822,16 +8778,16 @@ Q Q Q q -1 0 0 1 57.02362 593.8236 cm +1 0 0 1 57.02362 476.6236 cm Q q -1 0 0 1 57.02362 515.8236 cm +1 0 0 1 57.02362 398.6236 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 Q Q q -1 0 0 1 57.02362 507.8236 cm +1 0 0 1 57.02362 390.6236 cm Q endstream @@ -12188,63 +12144,63 @@ xref 0002475882 00000 n 0002486832 00000 n 0002499463 00000 n -0002509473 00000 n -0002519038 00000 n -0002528819 00000 n -0002538469 00000 n -0002546093 00000 n -0002556085 00000 n -0002565051 00000 n -0002575356 00000 n -0002578408 00000 n -0002580243 00000 n -0002593699 00000 n -0002610358 00000 n -0002620866 00000 n -0002628325 00000 n -0002634999 00000 n -0002643061 00000 n -0002650997 00000 n -0002657465 00000 n -0002659621 00000 n -0002660699 00000 n -0002661103 00000 n -0002661138 00000 n -0002661173 00000 n -0002661208 00000 n -0002661243 00000 n -0002661278 00000 n -0002661313 00000 n -0002661348 00000 n -0002661383 00000 n -0002661418 00000 n -0002661454 00000 n -0002661490 00000 n -0002661526 00000 n -0002661562 00000 n +0002509455 00000 n +0002518430 00000 n +0002528917 00000 n +0002537494 00000 n +0002545673 00000 n +0002555149 00000 n +0002563954 00000 n +0002574156 00000 n +0002578903 00000 n +0002580738 00000 n +0002594194 00000 n +0002610853 00000 n +0002621361 00000 n +0002628820 00000 n +0002635494 00000 n +0002643556 00000 n +0002651492 00000 n +0002657960 00000 n +0002660116 00000 n +0002661194 00000 n 0002661598 00000 n -0002661634 00000 n -0002661670 00000 n -0002661706 00000 n -0002661742 00000 n -0002661778 00000 n -0002661814 00000 n -0002661850 00000 n -0002661886 00000 n -0002661922 00000 n -0002661958 00000 n -0002661994 00000 n -0002662030 00000 n -0002662066 00000 n -0002662102 00000 n -0002662138 00000 n -0002662174 00000 n -0002662210 00000 n -0002662246 00000 n +0002661633 00000 n +0002661668 00000 n +0002661703 00000 n +0002661738 00000 n +0002661773 00000 n +0002661808 00000 n +0002661843 00000 n +0002661878 00000 n +0002661913 00000 n +0002661949 00000 n +0002661985 00000 n +0002662021 00000 n +0002662057 00000 n +0002662093 00000 n +0002662129 00000 n +0002662165 00000 n +0002662201 00000 n +0002662237 00000 n +0002662273 00000 n +0002662309 00000 n +0002662345 00000 n +0002662381 00000 n +0002662417 00000 n +0002662453 00000 n +0002662489 00000 n +0002662525 00000 n +0002662561 00000 n +0002662597 00000 n +0002662633 00000 n +0002662669 00000 n +0002662705 00000 n +0002662741 00000 n trailer << /ID -[<9ffe069fae61541297f64733839a76d9><9ffe069fae61541297f64733839a76d9>] +[] % ReportLab generated PDF document -- digest (opensource) /Info 69 0 R @@ -12252,5 +12208,5 @@ trailer /Size 200 >> startxref -2662282 +2662777 %%EOF diff --git a/whitepaper/uncommonlisp-whitepaper.rst b/whitepaper/uncommonlisp-whitepaper.rst index 74bfa54..1debe6d 100644 --- a/whitepaper/uncommonlisp-whitepaper.rst +++ b/whitepaper/uncommonlisp-whitepaper.rst @@ -628,17 +628,17 @@ The reason we built the GC at all was to let long-running asm HTTP servers not l .. table:: :widths: 38 14 14 14 20 - ============================== ========= ========= ========== ============= - Config req/s baseline peak RSS growth KB - RSS KB KB - ============================== ========= ========= ========== ============= - 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** - ============================== ========= ========= ========== ============= + ============================== ========= ========= =========== ============= + Config req/s baseline peak RSS growth KB + RSS KB KB (20 000 req) + ============================== ========= ========= =========== ============= + asm no-GC + ``heap-snapshot`` ~240 96 96 **0** + asm GC + ``heap-snapshot`` ~235 120 120 **0** + asm no-GC + no snapshot ~470 264 185,000 **185,000** + asm GC + no snapshot ~450 112 1,084 **972** + ============================== ========= ========= =========== ============= -All four cells validate cleanly now: +All four cells validate cleanly now at **20,000 requests per cell** (up from the original 5,000): - **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. @@ -648,7 +648,11 @@ All four cells validate cleanly now: **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. +**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. + +**Soak result.** At 20,000 HTTP requests × 16 concurrent clients, the GC build serves ~450 req/s with peak RSS of 1,084 KB — one heap chunk, steady state. 972 KB of growth represents the heap filling up exactly once after which the collector keeps reusing reclaimed space. This is the production validation we needed: naive mark-sweep is a correct, if not optimal, allocator for long-running asm servers that don't want to think about arena discipline. + +Remaining rough edges: at larger scales (50k+ requests with 512 MB ``ulimit -v`` and the bump-only no-GC case saturating the cap right before cell 4 starts) we've seen cell 4 die at server startup; this appears to be a process-environment issue rather than a GC bug, but we don't have a clean explanation yet. The hash-set benchmark on the GC build under the ~1 MB-per-iteration scale also still surfaces an occasional unbound-variable error pointing to a root-scan edge case the precise-type fix didn't fully close. Both are tracked as follow-ups. **Reproduce:** ``make bench-gc-http``. Tuning: ``REQUESTS=10000 CONCURRENCY=16 VCAP=524288 bash tests/bench-gc-http.sh``.