A declaration that fails to build or deliver leaves the session as it found it
Session.eval committed the checked program the moment a form checked, and the two steps that can still refuse it — the build, and the agent taking the module — come after that, in the daemon. Either one left the editor holding an error and the session holding a declaration the process has no body for. The next module built for that session lists the name in its install prologue, which interns a cell for it and never stores anything into it, and a dev build's call through a cell has no null test in front of it: the game thread jumps to address 0 at the next C-x C-e, locals render or globals refresh. Session.held takes the four fields eval commits as one unit and Session.restore puts them back. Dev.eval and Dev.eval_expr take one before checking and restore it on every arm where nothing was accepted — a failed build, a refused delivery, an unreachable agent. eval_expr needed it for the generic instances it keeps, whose own comment already claimed the invariant: "the session must not come to believe it holds a body that no module was ever written for." A delivered module that then times out is not a refusal and does not roll back: the agent has it and will install it at a frame boundary.
This commit is contained in:
parent
ce3e879e83
commit
cf410c5da3
47
lib/dev.ml
47
lib/dev.ml
@ -545,6 +545,18 @@ let parked why = error (parked_msg why)
|
||||
let eval t ~code ~origin ~pause =
|
||||
let now = liveness t in
|
||||
let parked_now = now = Parked in
|
||||
(* What the session was before the form was checked, and every failure below
|
||||
puts it back. [Session.eval] commits as soon as the check succeeds, which
|
||||
is two fallible steps too early: the build can fail and the agent can
|
||||
refuse, and a session left holding a declaration no module was accepted
|
||||
for hands the *next* module a name to intern a cell for and nothing to put
|
||||
in it — a null cell the first call through jumps to. See [Session.held].
|
||||
|
||||
Only the failures restore. The [installs = false] arm is a real
|
||||
acceptance: there is nothing to build and nothing to deliver, so there is
|
||||
nothing that can go wrong after it. *)
|
||||
let before = Session.held t.session in
|
||||
let refused msg = Session.restore t.session before; error msg in
|
||||
if now = Gone then error gone
|
||||
else
|
||||
match Session.eval ~origin ?pause t.session code with
|
||||
@ -595,13 +607,20 @@ let eval t ~code ~origin ~pause =
|
||||
when it is run again rather than at its next frame \
|
||||
boundary" ]
|
||||
else []))
|
||||
| reply -> error ("the program refused the module: " ^ reply)
|
||||
| reply -> refused ("the program refused the module: " ^ reply)
|
||||
| exception Unix.Unix_error (e, _, _) ->
|
||||
error
|
||||
refused
|
||||
("cannot reach the program on " ^ t.agent ^ ": "
|
||||
^ Unix.error_message e))
|
||||
| exception Failure m -> error m)
|
||||
| exception Loc.Error { Loc.dloc = l; dmsg = msg; _ } -> error ~loc:(Loc.to_string l) msg
|
||||
| exception Failure m -> refused m)
|
||||
(* Nothing to put back: the check itself raised, so [Session.eval] never
|
||||
reached its assignments. The restore is written anyway rather than
|
||||
reasoned about at each arm — a refusal that costs one record copy is
|
||||
cheaper than a reader working out which of the four fields this one
|
||||
could have moved. *)
|
||||
| exception Loc.Error { Loc.dloc = l; dmsg = msg; _ } ->
|
||||
Session.restore t.session before;
|
||||
error ~loc:(Loc.to_string l) msg
|
||||
|
||||
(* Redefining a name installs a body; evaluating an expression has no name to
|
||||
install into, so the module carries a thunk the agent runs once. The value
|
||||
@ -620,6 +639,15 @@ let eval_expr t ~code ~origin ~pause =
|
||||
"an expression is evaluated at a frame boundary, and a parked program \
|
||||
reaches none"
|
||||
| Live ->
|
||||
(* The same rollback [eval] takes, for the same reason and a smaller
|
||||
cargo. A thunk is not a declaration and never joins the session, but the
|
||||
generic instances the expression forced *are* kept — [Session.eval_expr]
|
||||
says why — and they are kept before this module has been built or taken.
|
||||
An instance the session holds and no module ever defined is a null cell
|
||||
exactly as a stranded [defn] is, and the next expression that mentions
|
||||
the same instantiation would list it as already there. *)
|
||||
let held = Session.held t.session in
|
||||
let refused msg = Session.restore t.session held; error msg in
|
||||
match Session.eval_expr ~origin ~pause t.session code with
|
||||
| c ->
|
||||
let before = match result t with Some (g, _) -> g | None -> 0L in
|
||||
@ -682,10 +710,15 @@ let eval_expr t ~code ~origin ~pause =
|
||||
error
|
||||
"the program did not reach a frame boundary; is it calling \
|
||||
(agent/poll)?")
|
||||
| reply -> error ("the program refused the module: " ^ reply)
|
||||
(* A module that was taken is the program's from here on, whatever
|
||||
the wait then says: a timeout is a frame boundary not reached
|
||||
yet, not a module refused, so the instances in it stay in the
|
||||
session. Only the two arms below, where nothing was accepted,
|
||||
put the session back. *)
|
||||
| reply -> refused ("the program refused the module: " ^ reply)
|
||||
| exception Unix.Unix_error (e, _, _) ->
|
||||
error ("cannot reach the program: " ^ Unix.error_message e))
|
||||
| exception Failure m -> error m)
|
||||
refused ("cannot reach the program: " ^ Unix.error_message e))
|
||||
| exception Failure m -> refused m)
|
||||
| exception Loc.Error { Loc.dloc = l; dmsg = msg; _ } -> error ~loc:(Loc.to_string l) msg
|
||||
|
||||
(* What a macro call expands to — [C-c C-m], and the one verb here that never
|
||||
|
||||
@ -408,6 +408,67 @@ let redefinition (t : t) ?retains ?call ?(consts = []) program ~fns =
|
||||
in
|
||||
fail loc "the x86 dev backend cannot compile this: %s" m
|
||||
|
||||
(* ── Undoing an acceptance ─────────────────────────────────────────── *)
|
||||
|
||||
(* Checking is not the last thing that can fail, and until this existed the
|
||||
session behaved as though it were. [eval] assigns the four mutable fields
|
||||
the moment a form checks; the *build* and the *delivery* happen afterwards,
|
||||
in the daemon, and either can refuse — llc can fail, and the agent's reload
|
||||
ring can be full, which a parked program guarantees after enough queued
|
||||
installs, since nothing drains the ring while the main thread waits. The
|
||||
editor saw an error either way, so the evaluation looked refused; the
|
||||
session went on holding the declaration anyway.
|
||||
|
||||
That leftover is not untidiness, it is a segfault. A declaration the session
|
||||
holds and the host does not export is a name every later module lists in its
|
||||
install prologue, and the prologue interns a cell for it. A cell nothing
|
||||
ever stored a body into is NULL, and a dev build's call through a cell is a
|
||||
load and an indirect call with no test in front of it — so the next
|
||||
[C-x C-e], the next locals render, the next globals refresh jumps the game
|
||||
thread to address 0. One failed build, and the next thing anybody types
|
||||
kills the program.
|
||||
|
||||
So the four fields are one unit that can be put back. [held] is what the
|
||||
session was before the evaluation and [restore] is the session being that
|
||||
again — all four together, because they are four views of one answer: the
|
||||
declarations, the checked program, the checker's environment, and the macros
|
||||
a later form expands against. Putting back three of them would leave the
|
||||
checker willing to accept a call to a name the program does not have, which
|
||||
is the same crash by a longer road.
|
||||
|
||||
What a restored session can claim is the honest sentence rather than the one
|
||||
anyone would rather have: it holds no declaration that no module was
|
||||
*accepted* for. Accepted is not installed — the agent queues a module and
|
||||
the game thread installs it at a frame boundary — but a queued module is one
|
||||
the process has and will run, and that is as far as this side can see.
|
||||
|
||||
A [defmacro] evaluated in the same breath as a [defn] that fails to build
|
||||
goes back with it, and that is right: they arrived as one form and were
|
||||
accepted as one. A [defmacro] on its own never reaches a restore, because a
|
||||
change with no body to install and no storage to allocate is answered before
|
||||
anything is built.
|
||||
|
||||
[thunks] is not in here. It is a counter that keeps two evaluations from
|
||||
naming their thunks alike, not something the session believes about the
|
||||
program, and the agent refuses a full ring *before* it dlopens — so a
|
||||
rolled-back number would be reused for a module nothing ever mapped, and
|
||||
reusing it is the one way to make two live modules share a symbol. *)
|
||||
type held = {
|
||||
hdecls : Ast.decl list;
|
||||
hprogram : Tast.program;
|
||||
henv : Check.env;
|
||||
hmacros : Form.t list;
|
||||
}
|
||||
|
||||
let held t =
|
||||
{ hdecls = t.decls; hprogram = t.program; henv = t.env; hmacros = t.macros }
|
||||
|
||||
let restore t h =
|
||||
t.decls <- h.hdecls;
|
||||
t.program <- h.hprogram;
|
||||
t.env <- h.henv;
|
||||
t.macros <- h.hmacros
|
||||
|
||||
let eval ?(origin = "<eval>") ?pause t src : change =
|
||||
let forms = Reader.read_all ~file:origin src in
|
||||
Parse.with_imported t.macros @@ fun () ->
|
||||
@ -593,9 +654,15 @@ let eval ?(origin = "<eval>") ?pause t src : change =
|
||||
(fun (g : Tast.global) -> not (known t g.Tast.gname))
|
||||
program.Tast.globals
|
||||
in
|
||||
(* Every one of these together, and after the last thing that can raise:
|
||||
until this line the session is still the one the evaluation started
|
||||
against, which is what makes a refusal cost nothing. *)
|
||||
(* Every one of these together, and after the last thing *here* that can
|
||||
raise: until this line the session is still the one the evaluation started
|
||||
against, which is what makes a refusal cost nothing.
|
||||
|
||||
It is not the last thing that can fail, though, and this line used to be
|
||||
written as if it were. The build and the delivery come after it, in the
|
||||
daemon, and both can refuse — so the caller takes a [held] first and puts
|
||||
it back when they do. See [restore] above for what a session that kept the
|
||||
declaration anyway does to the program. *)
|
||||
t.macros <- !macros;
|
||||
t.decls <- decls;
|
||||
t.program <- program;
|
||||
@ -1297,7 +1364,13 @@ let eval_expr ?(origin = "<eval>") ?(pause = false) t src : change =
|
||||
|
||||
After [Emit], not before it: the session must not come to believe it holds
|
||||
a body that no module was ever written for. A daemon that answers and has
|
||||
lost track of what the program contains is worse than one that died. *)
|
||||
lost track of what the program contains is worse than one that died.
|
||||
|
||||
Written for is as far as this line can get, and it is not far enough on
|
||||
its own: the module still has to build and still has to be taken. The
|
||||
caller closes that half by taking a [held] before this and restoring it
|
||||
when either fails — a copy the session holds and no module defines is a
|
||||
null cell exactly as a stranded declaration is. *)
|
||||
t.program <- { t.program with Tast.fns = t.program.Tast.fns @ fresh };
|
||||
{ ir; x86 = t.x86; names = []; fns = []; installs = true }
|
||||
|
||||
|
||||
@ -189,6 +189,55 @@ let () =
|
||||
| exception Loc.Error { Loc.dmsg = m; _ } ->
|
||||
fail "the session was poisoned by a bad expression: %s" m);
|
||||
|
||||
(* The other half of "a refusal costs nothing", and the half that used to be
|
||||
missing: a form can check and *then* fail, in the build or at the agent,
|
||||
and the session that already accepted it has no way to hear about it
|
||||
unless the caller puts it back. [Session.held] and [Session.restore] are
|
||||
that way, and this is the crash they close.
|
||||
|
||||
Rehearsed rather than simulated: neither llc nor a full reload ring can be
|
||||
summoned from here, and what matters is not which of them failed but what
|
||||
the session does afterwards. So the declaration is accepted, shown to be
|
||||
callable — the module for an expression that calls it names it, which is
|
||||
the name a later install prologue would intern a cell for and never store
|
||||
a body into — and then the session is put back and asked again.
|
||||
|
||||
Both sides are asserted. Without the first, a test that only checked the
|
||||
refusal would pass on a session that had never accepted the [defn] at
|
||||
all. *)
|
||||
(let rt, _ = Session.create ~file:"programs/reload.flan" () in
|
||||
let h = Session.held rt in
|
||||
(match Session.eval rt "(defn stranded [] i64 7)" with
|
||||
| c ->
|
||||
if c.Session.fns <> [ "stranded" ] then
|
||||
fail "a new declaration did not offer its body to install"
|
||||
| exception Loc.Error { Loc.dmsg = m; _ } ->
|
||||
fail "a new declaration was refused: %s" m);
|
||||
(match Session.eval_expr rt "(println (stranded))" with
|
||||
| e ->
|
||||
if not (has e.Session.ir "stranded") then
|
||||
fail "an expression calling a fresh declaration did not name it"
|
||||
| exception Loc.Error { Loc.dmsg = m; _ } ->
|
||||
fail "a fresh declaration was not callable: %s" m);
|
||||
Session.restore rt h;
|
||||
(* The module that would have jumped to address 0. After the restore the
|
||||
name is simply not one this session has, which is the whole of the
|
||||
fix: a refusal in the editor instead of a segfault in the program. *)
|
||||
(match Session.eval_expr rt "(println (stranded))" with
|
||||
| _ ->
|
||||
fail "a restored session still let an undelivered declaration be called"
|
||||
| exception Loc.Error { Loc.dmsg = m; _ } ->
|
||||
if not (has m "stranded") then
|
||||
fail "the refusal after a restore was about something else: %S" m);
|
||||
(* And it is a restore, not a poisoning: the same form offered again is
|
||||
accepted again, which is what an editor does after reading the error. *)
|
||||
match Session.eval rt "(defn stranded [] i64 7)" with
|
||||
| c ->
|
||||
if c.Session.fns <> [ "stranded" ] then
|
||||
fail "a re-sent declaration did not offer its body to install"
|
||||
| exception Loc.Error { Loc.dmsg = m; _ } ->
|
||||
fail "the session was poisoned by a restore: %s" m);
|
||||
|
||||
(* A declaration the program already has, with no body and no new storage,
|
||||
is accepted and has nothing to send. Building a module for it would report
|
||||
success for a change that cannot have taken effect, and would cost the
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user