aboutsummaryrefslogtreecommitdiffstats
path: root/docs/design/029-past-one-node.md
Commit message (Collapse)AuthorAgeFilesLines
* 029, 030: 047 written into 029 (the leaf as the commit: appends pass, sparse ↵eunhhu22 hours1-1/+32
| | | | updates break, two units as said beforehand; packets as 32-row column chunks 1,318 to 44 a row); 030 the one execution path, settled but for one choice: border reading rows where the payload has them, the handler emitted with registers, typed event buffers, shared captures and whole numbers, stored lists read in their leaves (a keyed seek by the guides' keys: 813 a point end to end, cycles 348, nothing copied out), commits writing appends into the leaf's tail and sparse updates to the log, replication as 046; what goes (the executor as a path, the batch lanes, the AArch64 layer, pure_list_read each message, the 54-state walks, the generic list API on hot paths, the bytes piece tree for whole sets); the verifier's three facts (N1, N4 new; N2 widened); representation choices; the user's choice (system cc at install, or Pure's own emitter per instruction set); the order, representation first inside the executor, each step with its check
* 029: two framings in the 009 section made plain: there is no disk leaf for a ↵eunhhu22 hours1-2/+8
| | | | list today (090's tree is in memory, a list on disk is images and a log), so the zero copy measured is memory's; and the seek rung is another program, not an emission (it halves by the tree's order, charges the budget once a call): 578 holds only with a keyed list, its seek and the order, an emitter alone gets 1,576; cycles beside instructions (388 against 312, end to end 368 against 292)
* 029: feedback 009's rule (one byte shape for the same data) applied to both ↵eunhhu22 hours1-0/+44
| | | | principles' results: packet to execution with no decoding holds in the hand-written border (rows read where the payload has them; checks stay), not in the runtime (a tree each message); the leaf as the execution array with no copy costs nothing only when the search follows the tree's order (578 against the copy's 564; a positional halving descends each probe: 1,576 and 2,114), which needs ranges ordered by start (a keyed list would say it; the app's own halving rebuilds the index the tree is); commit extent = replication record = follower bytes holds as files (046), but an item has more than one shape there: packet = TREE leaf column = image body for one field, the log re-frames each change (64 B a message, 56 of them frame), several fields go by rows in packets and images and by columns in leaves, FLAT event lists narrow; the next question put, not built: the leaf as the commit
* 046, 029: the taken-over store sent a message too (opened() works on a copy: ↵eunhhu22 hours1-6/+9
| | | | show, add, show; 20 more kill -9s: all open and take it as owners; 667 prefixes again with it: all pass); the price measured again without the fold that inflated it (entries.aup's summed view folded every entry each message): 48.5 to 232 us a message on tmpfs, 146 us of the 183 waiting for acks; the shim never stopped across the runs
* 029: principle 2 passed its breaking experiment (046), written with what it ↵eunhhu22 hours1-1/+37
| | | | showed against its own words: identity (233 samples and the ends of 100,000 and 200,000 messages: 0 bytes differ), taking over (70 kill -9s, all open with every message done), torn tails (867 op boundaries opened, 568 within cuts); "every write a save makes is a self-delimiting, self-verifying extent" false as written (zeros ahead, installs by rename under process-numbered names, directory syncs, 8 MB segments taken): file operations shipped, still no replication layer (the store's own ops cut at its own syncs, heard the ack); the price on tmpfs (204 to 400 us, 903 B a message, 42% zeros the follower could make); what was not tried (a follower started again and heard from its files, pure-serve's checkpoint thread, a real medium and two machines, a segment let go, asynchronous, choosing the owner)
* 045, 029: a message end to end, the event's border written by hand too ↵eunhhu23 hours1-1/+25
| | | | (app.c's BORDER: rows whole and finite, the budget and memory begun again, the one state the handler changes written apart and made the state's at a faultless end into a buffer no reader holds, events and changes counted; every end answers all 18,672 lines, the broken-rule build refused at both hand ends): machine instructions a code point, the runtime 40,365, its empty handler 1,595, the hand border with shared 592 and with plain 379, Vega's C given the same payload 240: 68x, 2.5x C (cycles 3.2x), the border 1,595 to about 22; what went: the rows rebuilt into a tree each message (pure_list_read's make_tree), 54 states walked five times an event (40 of them t.X's registers), the last event's nested lists, a bytes state set whole through a text's piece tree; no new fact (N2, today's proof, the language, forms chosen)
* 029: the facts counted again: two new (N1 whole numbers, N4 unchanged after ↵eunhhu23 hours1-7/+11
| | | | LIST_VALUE) and one analysis widened (N2 the handler's changes), not three new as 7ffb114 says: the 9.43x of the event's lists as typed buffers needs no new fact (keyed and indexed are declared, an event's list is one by its place; a typed buffer does every operation an unkeyed, unindexed one gets), only the form chosen and the memory charge's contract; seven fns (range and six), not six
* 029: UAX #14's whole chain and the facts it needs: the handler 38,623 ↵eunhhu23 hours1-7/+45
| | | | machine instructions a point (event aside) to 564 emitted by hand, 2.5x Vega's C (225; cycles 3.6x), factors 1.46 (dispatch), 3.02 (memory slots and calls), 1.10 (whole numbers), 1.22 (ranges flat), 9.43 (the event's lists typed buffers), 1.23 (Text sharing), the contract left (bounds 1.12, budget and memory 1.39) and the algorithm (1.61); the facts: today's proof licenses exact (each fn's registers, lists and changes: none of the six has lists or changes), then three new (N1 whole numbers, N3 a let list's operations, N4 unchanged after LIST_VALUE) and one analysis widened (N2 the handler's changes); the event itself now the largest layer (1,566 a point: the points decoded into a list, lists cleared and freed, malloc, breaks through the store tree), outside this chain; a premise corrected (the event's lists are FLAT arrays since 021, not trees: the 9.43x is the generic list path); the let lists' factor, broken by a share before, measured as the chain's largest
* 029: range()'s chain written, and two of its own claims taken back: the ↵eunhhu24 hours1-14/+47
| | | | executor 14,488 machine instructions a point, stitched 8,144, emitted exact 2,474, with integers 1,587, a flat column 1,083, both 226, C 129 (dispatch 1.78x, memory slots and the call's machinery 3.29x, the numbers' and lists' form 10.9x, bounds and budget 1.75x C); the bar set before (3x C's round) missed by exact (217) and passed by both (19.8); the premises checked: an unchanged list proven (function_changes), a whole-number index not (number slots, INDEX_AT checks it: a fact for the proof to take on), a local's lifetime not tested here; "no layer holds most, each 1.4-1.5x" and the let lists' "broken by arithmetic" were shares inside the executor, not factors; "one machine instruction an instruction is 2.5x C" was wrong (both does 269.5 in 226); what is bundled (memory slots with the call), the flat column's cost moved to changes (unmeasured), and 36% of the app only
* 045: Pure's answers checked for real (cost.c and where.c compared only the ↵eunhhu24 hours1-1/+4
| | | | C's with the test before; now Pure's boundaries are read from its view, and a wrong variant is refused with 0 lines right); the executor and the stitched build, rebuilt at adccf58, both answer all 18,672 lines, and the stitched build's numbers stand (40,189 to 28,089 machine instructions a point, 1.43x; cycles 1.32x); 029 says so
* 029: principle 1's break by mechanism (045's samples): dispatch 30.6%, lists ↵eunhhu24 hours1-1/+27
| | | | built 17.3%, numbers 13.5%, lists read 13.0%, moves 9.0%, calls 7.1%, malloc 4.0%: no layer holds most of the cliff, three generic ones (interpretation, the lists' form, the numbers') 1.4-1.5x each, the cliff their product; range()'s binary search 36% of the machine instructions and 269.5 of 549.9 executed (an algorithm Vega's C does not use); a candidate broken by arithmetic before code (let lists held again as versioned states: 13,000 of 40,236 at most, 1.5x); the bar's arithmetic (one machine instruction an instruction is still 2.5x C: the instructions must fall too); "the general JIT 008 forbids" corrected (008's task A asks for one execution principle from the proof; it forbids the executors' split and scaled-down techniques)
* 029: principle 1 broken on UAX #14 (045), written as its own rule asks: (a) ↵eunhhu24 hours1-2/+31
| | | | 2.19x against 4x, its premise wrong (the source already keeps t.cls[i] in locals: the reads only the proof merges are 16.4 of 549.9), (b) 1.31x against 3x, and the path capped (interpretation is 22 of an instruction's 74 machine instructions: stitching bodies gives at most 1.42x); what was tested (step() on constant instructions, frame and checks as they are) and what was not (an emitter given the proof, the general JIT 008 forbids); where it goes (runtime machinery: a call 1,375, a stored read 331, the lists 22,651 a point) and the 7x the batch lanes give that a fn in a block loses; the 1,774 and 3.2-3.9 ns corrected (the budget's count: 549.9 run, 11.7 ns each) here and in 140; the op counts kept
* 029 second draft from a blank page (the first, five techniques listed, ↵eunhhu25 hours1-189/+95
| | | | rejected by outside feedback 008): two principles, each a layer deleted because another already holds what it holds, each with one experiment that can break it before code; 1 the proof is the compiler (the verifier proves stack places and types, loop bounds, each fn's change set, no aliasing between lists, and the three executors throw it away; a C compiler must guess what Pure has proven, so verified aup should be easier to compile to C's speed than C; delete the executor as a path, the batch lanes and the AArch64 backend, emit by stitching the executor's own op bodies; break it on UAX #14: the merging the proof licenses 4x fewer instructions, no dispatch 3x less a instruction), 2 the commit is the replica (a save's extents self-delimiting and self-verifying, the link's heard their durable ack: no replication layer, the follower's files the leader's byte for byte; break it with two hosts on one Pi, cmp at sampled saves, kill -9 and open as owner; checkpoints and compaction to ship or make deterministic; the owner-choosing rule deferred); schema evolution an open question (one shape in the tree, projected on read: unmeasured, and leaves are columns); effects and screens already one boundary, backends
* 029: spreading fns at load is a reason to try, not a result (an early return ↵eunhhu26 hours1-1/+3
| | | | in a loop's body becomes a branch out of it, unmeasured): ③'s first work settles it
* 029 (draft, not a 1.0 freeze): past one node, outside feedback 007's five ↵eunhhu26 hours1-0/+194
gaps as architecture and order, each hung on an invariant already there (deterministic events, the chained commit log, ordered once delivery, views as pure functions) with a first proof on the Pi, its pass number and a stop rule: 1 the computing cliff and views' fns (the slow specs all runner 2: fns send whole blocks to the executor; fns spread at load below the language, bytes as columns, fewer instructions, CALL in a view whose callees change nothing), 2 the living store's evolution (a migration a pure fn of the new module, rewritten in batches while the app answers; 030's items-wide at 1M under 5 ms unanswered, the store the same bytes), 3 distribution (committed bursts replayed by a follower, an epoch fenced owner chosen by two of three, topology as a directory app's views; two hosts on one Pi first), 4 Vega past the grid (a display list as a view type, layout in aup with text measured by the host, IME and clipboard as input events, native windows last), alongside 5 effects whose results come back as events, one entry, a C ABI v0; the app contract gathered as draft v0, the fixed limits deferred