PORTING.md Tier 1 item 6, the last one on that list. Not a language feature and nothing was added to the language: restart-case, struct assignment and fixed-arrays-as-values were already built, and what was missing was the worked example. test/programs/frame-rollback.flan is it — snapshot at the top of the frame, restore in the `continue` clause, over one fixed array and one struct, which is engine.clj's grids plus engine.lisp's shallow copy of the state object. Two `set`s each way, because both are values; there is no IntGrid walk and no sb-mop:class-slots walk to write. The decision in it is the ordering against defers, and both orderings compile. An answered bounds failure runs the abandoned function's defers, innermost-first, before the restart clause body starts. Restore in the clause is therefore the last write on the abandoned path and needs no agreement with what any defer did on the way out. The rejected alternative — restore in a defer inside the frame function — also runs on the ordinary return path, so it rolls back the frames that succeeded, and nothing reports that as an error. Pinned with numbers rather than prose: a tick counter inside the snapshot, written by the frame's defer, reads its pre-frame value, while a counter outside the snapshot shows the defer ran. And there is a negative control, the same bad frame with a `continue` that only counts, because "state equals snapshot" passes trivially on a program that never wrote anything. Three acceptance rows beside bounds-condition.flan's, for the same reasons: -O0, and the dev build where every call goes through a cell.
208 lines
9.8 KiB
Plaintext
208 lines
9.8 KiB
Plaintext
;;;; Frame rollback: the half of the frame loop that `continue` does not do.
|
|
;;;;
|
|
;;;; PORTING.md Tier 1 item 6. Not a language feature — restart-case, struct
|
|
;;;; assignment and fixed-arrays-as-values are all built. This is the worked
|
|
;;;; example, the way sand.flan is the worked example for the loop itself.
|
|
;;;;
|
|
;;;; Both reference hosts survive a bad frame and keep the window open, and
|
|
;;;; both do it the same way underneath: engine.clj's `run-game!` snapshots
|
|
;;;; every IntGrid at the top of the frame, catches Throwable and restores;
|
|
;;;; engine.lisp's `run-frame` wraps update and draw in a restart-case whose
|
|
;;;; `retry-frame`, `skip-frame` and `reinit` each roll the grids *and* a MOP
|
|
;;;; shallow copy of the state object back. Flan already had the restart-case
|
|
;;;; and, since a bad index signals BoundsError rather than calling exit(134),
|
|
;;;; already lands in `continue` instead of ending the session. What it did
|
|
;;;; not have was the rollback — so an abandoned frame left the grid
|
|
;;;; half-written, which is bounds-condition.flan's last line (`10 99 12 13`)
|
|
;;;; read as a bug rather than as a result.
|
|
;;;;
|
|
;;;; **A restart is not a transaction** (spec-conditions.md §5). A transfer
|
|
;;;; runs defers and moves control; it does not undo. Nothing here is a
|
|
;;;; mechanism the compiler provides, and that is the point: rollback is a
|
|
;;;; discipline the author writes, and in Flan it is two lines, because a
|
|
;;;; fixed array and a struct are values. `(set backup grid)` is the whole of
|
|
;;;; snapshot! — no walk, no sb-mop:class-slots, no per-cell copy loop.
|
|
;;;;
|
|
;;;; ── The ordering decision, which is the reason to read this file ──
|
|
;;;;
|
|
;;;; An *answered* bounds failure runs the abandoned function's defers, because
|
|
;;;; it leaves through the same unwind path a `return` does, and those defers
|
|
;;;; run innermost-first **before** the restart clause body starts. So a
|
|
;;;; snapshot has to be ordered against them deliberately, and both orderings
|
|
;;;; compile:
|
|
;;;;
|
|
;;;; - **restore in the restart clause** — chosen. It is the last write on
|
|
;;;; the abandoned path, so it needs no agreement with what any defer did
|
|
;;;; on the way out. A defer that writes into the snapshotted state is
|
|
;;;; simply overwritten, which is what "the frame did not happen" means.
|
|
;;;; - restore in a `defer` inside the frame function — **rejected, and it is
|
|
;;;; the silent one.** A defer runs on the ordinary return path too, so
|
|
;;;; that version rolls back the frames that *succeeded*. Nothing errors;
|
|
;;;; the game just stops advancing.
|
|
;;;;
|
|
;;;; `tick` below is the discriminator. It is written by update-frame's defer,
|
|
;;;; it lives inside the snapshot, and after an abandoned frame it reads as its
|
|
;;;; pre-frame value while `tails` — which lives outside the snapshot — proves
|
|
;;;; the defer ran. Only the chosen ordering produces that pair.
|
|
;;;;
|
|
;;;; **The snapshot covers plain values only.** If a defer frees a resource and
|
|
;;;; the snapshot holds a pointer or a handle to it, restore resurrects a
|
|
;;;; dangling one. Value state in the snapshot, resources in the defers, and
|
|
;;;; no overlap between them.
|
|
;;;;
|
|
;;;; ── What is asserted ──
|
|
;;;;
|
|
;;;; Frame 2 is the negative control and it is what makes frame 3 mean
|
|
;;;; anything: the same bad frame, the same snapshot taken, and a `continue`
|
|
;;;; clause that only counts. It leaves drift 3. Frame 3 restores and leaves
|
|
;;;; drift 0. Without the control, "state equals snapshot" would pass on a
|
|
;;;; program that never wrote anything and never restored anything.
|
|
|
|
;;; The state the engine owns: one grid of cells, and one struct of scalars.
|
|
;;; Two shapes on purpose — engine.clj rolls back grids, engine.lisp rolls
|
|
;;; back grids *and* a copy of the state object, and in Flan each is one `set`.
|
|
(defstruct World [placed i32 brush i32])
|
|
|
|
(defvar grid [8 i32])
|
|
(defvar world World)
|
|
|
|
;;; The snapshot. Same types, same declarations; there is nothing else to it.
|
|
(defvar grid-backup [8 i32])
|
|
(defvar world-backup World)
|
|
|
|
;;; Evidence, and it has to live *outside* the snapshot or restore rolls back
|
|
;;; the proof along with the state. `writes` counts the mutations a frame made
|
|
;;; before it failed, `tails` counts the defers that ran on the way out.
|
|
(defvar frames i64)
|
|
(defvar skipped i64)
|
|
(defvar writes i64)
|
|
(defvar tails i64)
|
|
|
|
;;; Handlers cannot see the locals of the function that established them —
|
|
;;; check.ml refuses a capture by name and says to use a global — so the
|
|
;;; condition's numbers land up here too.
|
|
(defvar low i64)
|
|
(defvar length i64)
|
|
|
|
;;; ── snapshot and restore ──────────────────────────────────────────────
|
|
;;; The whole of it. A fixed array copies on assignment and so does a struct
|
|
;;; (values.flan), so these are two stores each and the cost is the size of
|
|
;;; the state, not the shape of it.
|
|
|
|
(defn snapshot [] ()
|
|
(set grid-backup grid)
|
|
(set world-backup world))
|
|
|
|
(defn restore [] ()
|
|
(set grid grid-backup)
|
|
(set world world-backup))
|
|
|
|
;;; How far the live state has drifted from the snapshot: the assertion this
|
|
;;; program exists to make. Counted rather than compared with `=`, because
|
|
;;; `=` is numeric and enum only — there is no structural equality in the
|
|
;;; surface language, and a hand-written walk is what a game would write too.
|
|
(defn drift [] i64
|
|
(let [d (i64 0)]
|
|
(dotimes [i 8]
|
|
(when (!= (at grid i) (at grid-backup i)) (set d (+ d 1))))
|
|
(when (!= (.placed world) (.placed world-backup)) (set d (+ d 1)))
|
|
(when (!= (.brush world) (.brush world-backup)) (set d (+ d 1)))
|
|
d))
|
|
|
|
(defn show [name string n i64] ()
|
|
(print name) (print " ") (print n) (println ""))
|
|
|
|
(defn dump [] ()
|
|
(print (at grid 0)) (print " ") (print (at grid 3)) (print " ")
|
|
(print (at grid 7)) (print " ") (print (.placed world)) (println ""))
|
|
|
|
;;; ── the frame ─────────────────────────────────────────────────────────
|
|
|
|
;;; The engine's tail write. It runs on every exit path — the good one and the
|
|
;;; abandoned one — and it writes into the snapshotted state deliberately, so
|
|
;;; that cell 7 discriminates the two orderings. `tails` does not, which is why
|
|
;;; it is a separate counter.
|
|
(defn tick [] ()
|
|
(set (at grid 7) (+ (at grid 7) 1))
|
|
(set tails (+ tails 1)))
|
|
|
|
;;; Mutate first, fail second: the half-written frame this whole file is about.
|
|
;;; `col` is a mouse column in the real thing — game.clj computes it straight
|
|
;;; from the pointer with no check anywhere, which is how an ordinary session
|
|
;;; walks into this by moving one pixel outside the window.
|
|
(defn update-frame [col i32] ()
|
|
(defer (tick))
|
|
(set (.placed world) (+ (.placed world) 1))
|
|
(set (at grid 0) (+ (at grid 0) 1))
|
|
(set writes (+ writes 1))
|
|
(set (at grid col) 5))
|
|
|
|
;;; The frame loop, without the rollback. sand.flan's shape exactly, and the
|
|
;;; negative control: the snapshot is taken and then ignored.
|
|
(defn frame-no-rollback [col i32] ()
|
|
(snapshot)
|
|
(restart-case
|
|
(do (update-frame col)
|
|
(set frames (+ frames 1)))
|
|
(continue [] (set skipped (+ skipped 1)))))
|
|
|
|
;;; And with it. One line more, in one place, and it is the *last* thing on the
|
|
;;; abandoned path rather than the first.
|
|
(defn frame [col i32] ()
|
|
(snapshot)
|
|
(restart-case
|
|
(do (update-frame col)
|
|
(set frames (+ frames 1)))
|
|
(continue [] (restore)
|
|
(set skipped (+ skipped 1)))))
|
|
|
|
(defn main [] i32
|
|
(set (.brush world) 1)
|
|
|
|
(handler-bind
|
|
[(BoundsError [c]
|
|
(set low (.low c))
|
|
(set length (.length c))
|
|
;; Abandon the frame. The transfer crosses update-frame, running its
|
|
;; defer, and lands in the clause of the restart-case one frame out.
|
|
(invoke-restart 'continue))]
|
|
|
|
;; Frame 1: in bounds. The handler never runs, the frame finishes, and the
|
|
;; defer runs on the ordinary return path — which is exactly why restore
|
|
;; must not live in a defer: this frame's work has to survive.
|
|
(frame 3)
|
|
(dump) ; 1 5 1 1
|
|
(show "drift" (drift)) ; 1 5 1 1 vs the zeroed snapshot: 4
|
|
|
|
;; Frame 2: out of bounds, and nothing rolls back. The frame is abandoned
|
|
;; and the session survives — that much `continue` already gave us — but
|
|
;; the state is the frame's leftovers: cell 0 bumped, placed bumped, the
|
|
;; defer's tick landed, and the write that failed never happened.
|
|
(frame-no-rollback 9)
|
|
(dump) ; 2 5 2 2
|
|
(show "drift" (drift)) ; 3 — and this is the bug
|
|
|
|
;; Frame 3: the same bad index, the same snapshot, restore in the clause.
|
|
(frame 9)
|
|
(dump) ; 2 5 2 2 — frame 2's state, intact
|
|
(show "drift" (drift)) ; 0
|
|
|
|
;; The ordering, in two numbers. `tails` is 3, so update-frame's defer ran
|
|
;; on the abandoned path as well as the good one; cell 7 is back at 2, so
|
|
;; the restore happened *after* it. Had restore run first — in a defer
|
|
;; registered *below* `(defer (tick))`, since defers run innermost-first
|
|
;; and the later registration is the inner one — cell 7 would read 3 and
|
|
;; drift above would have read 1, which is the quiet kind of wrong.
|
|
(show "tails" tails) ; 3
|
|
(show "tick" (i64 (at grid 7))) ; 2
|
|
|
|
;; Three frames, two of them bad; one finished, two were abandoned; three
|
|
;; mutations were made before the failures, of which only frame 1's
|
|
;; survives. And the condition carried the real numbers both times.
|
|
(show "frames" frames) ; 1
|
|
(show "skipped" skipped) ; 2
|
|
(show "writes" writes) ; 3
|
|
(show "low" low) ; 9
|
|
(show "length" length)) ; 8
|
|
0)
|