diff --git a/lib/artdag/conformance.sh b/lib/artdag/conformance.sh index 84b96d13..6027026e 100755 --- a/lib/artdag/conformance.sh +++ b/lib/artdag/conformance.sh @@ -13,7 +13,7 @@ if [ ! -x "$SX_SERVER" ]; then exit 1 fi -SUITES=(dag analyze plan execute optimize fed cost serialize stats fault maude-optimize) +SUITES=(dag analyze plan execute optimize fed cost serialize stats fault maude-optimize schedule) OUT_JSON="lib/artdag/scoreboard.json" OUT_MD="lib/artdag/scoreboard.md" @@ -25,6 +25,27 @@ run_suite() { TMP=$(mktemp) local MAUDE_LOADS="" local BRIDGE_LOAD="" + local MK_LOADS="" + local SCHED_LOAD="" + if [ "$suite" = "schedule" ]; then + MK_LOADS='(load "lib/guest/match.sx") +(load "lib/minikanren/unify.sx") +(load "lib/minikanren/stream.sx") +(load "lib/minikanren/goals.sx") +(load "lib/minikanren/fresh.sx") +(load "lib/minikanren/conde.sx") +(load "lib/minikanren/run.sx") +(load "lib/minikanren/relations.sx") +(load "lib/minikanren/project.sx") +(load "lib/minikanren/diseq.sx") +(load "lib/minikanren/intarith.sx") +(load "lib/minikanren/matche.sx") +(load "lib/minikanren/defrel.sx") +(load "lib/minikanren/nafc.sx") +(load "lib/minikanren/fd.sx") +(load "lib/minikanren/clpfd.sx")' + SCHED_LOAD='(load "lib/artdag/schedule.sx")' + fi if [ "$suite" = "maude-optimize" ]; then MAUDE_LOADS='(load "lib/guest/lex.sx") (load "lib/guest/pratt.sx") @@ -64,6 +85,7 @@ run_suite() { (load "lib/persist/kv.sx") (load "lib/persist/api.sx") ${MAUDE_LOADS} +${MK_LOADS} (load "lib/artdag/dag.sx") (load "lib/artdag/analyze.sx") (load "lib/artdag/plan.sx") @@ -76,6 +98,7 @@ ${MAUDE_LOADS} (load "lib/artdag/fault.sx") (load "lib/artdag/api.sx") ${BRIDGE_LOAD} +${SCHED_LOAD} (epoch 2) (eval "(define artdag-test-pass 0)") (eval "(define artdag-test-fail 0)") diff --git a/lib/artdag/schedule.sx b/lib/artdag/schedule.sx new file mode 100644 index 00000000..b9af4613 --- /dev/null +++ b/lib/artdag/schedule.sx @@ -0,0 +1,139 @@ +; lib/artdag/schedule.sx — relational scheduling on lib/minikanren CLP(FD). +; Each node gets a slot var in [1..max-slots]; every edge (input->node) imposes +; `fd-lt slot(input) slot(node)`. `fd-label` searches the finite domains; a solution +; is a {node-id -> slot} assignment respecting all dependencies. Grouping by slot +; gives parallel batches (plan.sx's batch shape). Labeling picks smallest slots +; first, so the FIRST solution is the ASAP leveling — it agrees with plan.sx's greedy +; Kahn waves; the relational extra is enumerating EVERY valid schedule. The +; parallelism cap is a cardinality property, enforced by filtering labeled solutions +; (the FD core handles precedence only). lib/minikanren is a READ-ONLY consumed +; substrate: make-var, fd-in, fd-lt, fd-label, mk-conj, reify, stream-take, empty-s. + +(define + artdag/range1 + (fn (n) (map (fn (i) (+ i 1)) (range 0 n)))) + +(define + artdag/-zip-assoc + (fn + (ids vals) + (reduce + (fn (m p) (assoc m (first p) (nth p 1))) + {} + (zip ids vals)))) + +; build the constraint goal + the ordered slot vars for a dag over domain 1..maxslots. +(define + artdag/sched-goal-and-vars + (fn + (dag maxslots) + (let + ((ids (artdag/dag-order dag))) + (let + ((vars (map (fn (id) (make-var)) ids))) + (let + ((id->var (artdag/-zip-assoc ids vars)) + (dom (artdag/range1 maxslots))) + (let + ((in-goals (map (fn (v) (fd-in v dom)) vars)) + (lt-goals + (reduce + (fn + (acc id) + (concat + acc + (map + (fn + (inp) + (fd-lt (get id->var inp) (get id->var id))) + (artdag/node-inputs (artdag/dag-get dag id))))) + (list) + ids))) + {:goal (apply mk-conj (concat in-goals lt-goals (list (fd-label vars)))) :vars vars :ids ids})))))) + +(define + artdag/-sched-solutions + (fn + (g limit) + (map + (fn (sol) (artdag/-zip-assoc (get g :ids) sol)) + (map + (fn (s) (reify (get g :vars) s)) + (stream-take limit ((get g :goal) empty-s)))))) + +; all valid dependency-respecting slot assignments within 1..maxslots. +(define + artdag/schedules + (fn + (dag maxslots) + (artdag/-sched-solutions + (artdag/sched-goal-and-vars dag maxslots) + -1))) + +; one valid assignment (ASAP within the bound), or nil if maxslots is too small. +(define + artdag/schedule + (fn + (dag maxslots) + (let + ((ss (artdag/-sched-solutions (artdag/sched-goal-and-vars dag maxslots) 1))) + (if (empty? ss) nil (first ss))))) + +; ASAP schedule: node-count slots are always sufficient (a linear chain is the worst +; case), and smallest-first labeling yields the tightest leveling. +(define + artdag/schedule-asap + (fn (dag) (artdag/schedule dag (artdag/node-count dag)))) + +(define + artdag/schedule-makespan + (fn + (assignment) + (reduce + (fn (m id) (max m (get assignment id))) + 0 + (keys assignment)))) + +; group node-ids by slot (ascending), each batch id-sorted for determinism. +(define + artdag/schedule->batches + (fn + (dag assignment) + (let + ((mx (artdag/schedule-makespan assignment))) + (filter + (fn (b) (not (empty? b))) + (map + (fn + (slot) + (artdag/sort-strings + (filter + (fn (id) (= (get assignment id) slot)) + (keys assignment)))) + (artdag/range1 mx)))))) + +; independent check: every input is scheduled strictly before its consumer. +(define + artdag/schedule-valid? + (fn + (dag assignment) + (every? + (fn + (id) + (every? + (fn (inp) (< (get assignment inp) (get assignment id))) + (artdag/node-inputs (artdag/dag-get dag id)))) + (artdag/dag-order dag)))) + +; schedules whose every slot holds <= cap nodes (parallelism cap as a post-filter). +(define + artdag/schedules-capped + (fn + (dag maxslots cap) + (filter + (fn + (asn) + (every? + (fn (b) (<= (len b) cap)) + (artdag/schedule->batches dag asn))) + (artdag/schedules dag maxslots)))) diff --git a/lib/artdag/scoreboard.json b/lib/artdag/scoreboard.json index bbc68281..ccd74e30 100644 --- a/lib/artdag/scoreboard.json +++ b/lib/artdag/scoreboard.json @@ -10,9 +10,10 @@ "serialize": {"pass": 13, "fail": 0}, "stats": {"pass": 12, "fail": 0}, "fault": {"pass": 14, "fail": 0}, - "maude-optimize": {"pass": 40, "fail": 0} + "maude-optimize": {"pass": 40, "fail": 0}, + "schedule": {"pass": 15, "fail": 0} }, - "total_pass": 198, + "total_pass": 213, "total_fail": 0, - "total": 198 + "total": 213 } diff --git a/lib/artdag/scoreboard.md b/lib/artdag/scoreboard.md index 957c003c..785cb792 100644 --- a/lib/artdag/scoreboard.md +++ b/lib/artdag/scoreboard.md @@ -15,4 +15,5 @@ _Generated by `lib/artdag/conformance.sh`_ | stats | 12 | 0 | 12 | | fault | 14 | 0 | 14 | | maude-optimize | 40 | 0 | 40 | -| **Total** | **198** | **0** | **198** | +| schedule | 15 | 0 | 15 | +| **Total** | **213** | **0** | **213** | diff --git a/lib/artdag/tests/schedule.sx b/lib/artdag/tests/schedule.sx new file mode 100644 index 00000000..106e38ef --- /dev/null +++ b/lib/artdag/tests/schedule.sx @@ -0,0 +1,127 @@ +; Phase 3/7 (optional) — relational scheduling on lib/minikanren CLP(FD). +; Each node gets a slot var; edges impose fd-lt; fd-label searches. The ASAP solution +; agrees with plan.sx's greedy Kahn waves; enumerating all solutions is the extra. + +; ---- linear chain a -> b -> c: exactly one minimal schedule ---- + +(define + sc-chain + (artdag/build + (list + (list "a" "src" (list) {}) + (list "b" "blur" (list "a") {:radius 1}) + (list "c" "blur" (list "b") {:radius 2})))) +(define sc-chain-a (artdag/dag-id sc-chain "a")) +(define sc-chain-b (artdag/dag-id sc-chain "b")) +(define sc-chain-c (artdag/dag-id sc-chain "c")) +(define sc-chain-asap (artdag/schedule-asap sc-chain)) + +(artdag-test "chain: ASAP schedule exists" (nil? sc-chain-asap) false) + +(artdag-test + "chain: slots are strictly increasing along the chain" + (list + (get sc-chain-asap sc-chain-a) + (get sc-chain-asap sc-chain-b) + (get sc-chain-asap sc-chain-c)) + (list 1 2 3)) + +(artdag-test + "chain: makespan equals chain length" + (artdag/schedule-makespan sc-chain-asap) + 3) + +(artdag-test + "chain: exactly one schedule when slots = node count (no slack)" + (len (artdag/schedules sc-chain 3)) + 1) + +(artdag-test + "chain: ASAP batches are one node per slot" + (map len (artdag/schedule->batches sc-chain sc-chain-asap)) + (list 1 1 1)) + +(artdag-test + "chain: ASAP schedule is valid (deps respected)" + (artdag/schedule-valid? sc-chain sc-chain-asap) + true) + +; ---- diamond a -> b,c -> d: b and c are parallel ---- + +(define + sc-dia + (artdag/build + (list + (list "a" "src" (list) {}) + (list "b" "blur" (list "a") {:radius 1}) + (list "c" "bright" (list "a") {:radius 1}) + (list "d" "over" (list "b" "c") {} true)))) +(define sc-dia-asap (artdag/schedule-asap sc-dia)) + +(artdag-test + "diamond: ASAP makespan is 3 (a | b,c | d)" + (artdag/schedule-makespan sc-dia-asap) + 3) + +(artdag-test + "diamond: ASAP batch sizes are 1,2,1" + (map len (artdag/schedule->batches sc-dia sc-dia-asap)) + (list 1 2 1)) + +(artdag-test + "diamond: FD ASAP batches agree with plan.sx greedy waves" + (= + (artdag/schedule->batches sc-dia sc-dia-asap) + (map artdag/sort-strings (artdag/plan sc-dia 0))) + true) + +(artdag-test + "diamond: every enumerated schedule is valid" + (every? + (fn (asn) (artdag/schedule-valid? sc-dia asn)) + (artdag/schedules sc-dia 4)) + true) + +(artdag-test + "diamond: b and c share a slot in the ASAP schedule" + (= + (get sc-dia-asap (artdag/dag-id sc-dia "b")) + (get sc-dia-asap (artdag/dag-id sc-dia "c"))) + true) + +; ---- parallelism cap: filter schedules to <= cap nodes per slot ---- + +(artdag-test + "cap 1: the ASAP (b,c parallel) schedule is excluded, serial ones remain" + (every? + (fn + (asn) + (every? + (fn (b) (<= (len b) 1)) + (artdag/schedule->batches sc-dia asn))) + (artdag/schedules-capped sc-dia 4 1)) + true) + +(artdag-test + "cap 1: at least one serial schedule exists within 4 slots" + (> (len (artdag/schedules-capped sc-dia 4 1)) 0) + true) + +(artdag-test + "cap 2: admits the parallel ASAP schedule" + (if + (some + (fn (shape) (= shape (list 1 2 1))) + (map + (fn (asn) (map len (artdag/schedule->batches sc-dia asn))) + (artdag/schedules-capped sc-dia 4 2))) + true + false) + true) + +; ---- unsatisfiable: too few slots for the chain ---- + +(artdag-test + "chain: no schedule when slots < chain length" + (nil? (artdag/schedule sc-chain 2)) + true) diff --git a/plans/artdag-on-sx.md b/plans/artdag-on-sx.md index b6bf9573..fae5b899 100644 --- a/plans/artdag-on-sx.md +++ b/plans/artdag-on-sx.md @@ -31,14 +31,21 @@ edges. ## Status (rolling) -`bash lib/artdag/conformance.sh` → **198/198** (11 suites: dag, analyze, plan, execute, optimize, fed, cost, serialize, stats, fault, maude-optimize) +`bash lib/artdag/conformance.sh` → **213/213** (12 suites: dag, analyze, plan, execute, optimize, fed, cost, serialize, stats, fault, maude-optimize, schedule) Base roadmap (Phases 1–6) COMPLETE + Phase 7 (maude rule-based optimization) COMPLETE (only optional miniKanren scheduling remains). Now hardening only. ## Integration / merge status (2026-06-28) -**READY TO MERGE `loops/artdag` → `architecture`.** `origin/architecture`'s `lib/artdag/` +**MERGED to architecture (Phase 7) at `b0d845bb`** — local `architecture` now carries +`lib/maude` + artdag Phase 7, conformance green there (198/198 at merge time). The merge +was clean/additive; `architecture` itself was NOT pushed (pushing it triggers a large dev +reload — a deliberate separate call). **NOTE: re-merge needed** — `loops/artdag` has since +added `lib/artdag/schedule.sx` (miniKanren CLP(FD) scheduler, 213/213), not yet on +architecture. + +(Historical, for the Phase 7 merge above:) `origin/architecture`'s `lib/artdag/` is stale — it predates the maude-bridge, so it is missing ALL of Phase 7 (`maude-bridge.sx` + `optimize-rules.sx` both absent). `loops/artdag` is 9 commits ahead of `origin/architecture` (the Phase 7 chain `657d8061..4a02a9c4` + the architecture-merge @@ -122,7 +129,10 @@ lib/artdag/optimize.sx lib/artdag/federation.sx nodes have all deps satisfied → run in parallel); respect a max-parallelism limit - [x] plan over the *dirty* subset only (incremental plan) - [x] `lib/artdag/tests/plan.sx` — batch correctness, parallelism cap, dirty-only plan -- [ ] (optional/later) miniKanren constraint scheduling — flag, don't block on it +- [x] miniKanren constraint scheduling — `lib/artdag/schedule.sx` on lib/minikanren + CLP(FD): slot var per node, `fd-lt` per edge, `fd-label` search; ASAP solution agrees + with the greedy Kahn waves above, plus full schedule enumeration + parallelism-cap + filter (Phase 3 + Phase 7 optional box) ## Phase 4 — Execute (incremental + memoized) @@ -209,6 +219,23 @@ be an op token. ## Progress log +- **2026-06-28 Phase 3/7 — miniKanren CLP(FD) scheduler** (schedule suite 15/15, total + 213/213). `lib/artdag/schedule.sx` on `lib/minikanren` (read-only substrate): each node + gets a slot var in `[1..max-slots]`, every edge `(input->node)` imposes `fd-lt + slot(input) slot(node)`, `fd-label` searches the finite domains. A solution is a + `{node-id -> slot}` assignment respecting all dependencies; `schedule->batches` groups by + slot into parallel waves. Smallest-first labeling makes `schedule-asap` the tightest + leveling — and it **agrees exactly with `plan.sx`'s greedy Kahn waves** (cross-validated + in the suite: FD batches == `artdag/plan dag 0`). The relational extra over the greedy + planner: `schedules` enumerates EVERY valid schedule, and `schedules-capped` filters to + `<= cap` nodes per slot (cardinality is a post-filter; the FD core handles precedence). + `schedule-valid?` independently checks deps; unsatisfiable bounds return nil. Substrate + load deps: `lib/guest/match.sx` (the kit: `mk-var`) before the minikanren stack, then + `fd.sx`+`clpfd.sx`. Built functionally (`make-var`/`mk-conj`/`reify`/`stream-take`/ + `empty-s`) since the node count is runtime data, not macro-time. Gotcha: `artdag/member?` + uses `equal?` (representation-sensitive) — membership of `map`-built lists must compare + with `=`, not `member?`. + - **2026-06-19 Phase 7 — confluence gate is non-vacuous** (maude-optimize 40/40, total 198/198). Added a regression proving `mau/confluent?` actually discriminates: the Peano-arithmetic variant of the same laws (`0 + N = N`, `s M + N = s(M+N)` instead of