The park left for a re-run without draining its ring
[flan_merged_park] drained the agent's ring on one of the two flags that wake it. [program_poll] — which an expression sets, by way of [Program.wake] — polled and went back to sleep; [program_asked] broke out of the loop and re-entered [flan_program_main] with the queue untouched. A plain redefinition sets neither, so a body delivered to a parked program was still in the ring when the run it was delivered for started, and installed at that run's first frame boundary instead: everything main did before its first (agent/poll) ran the body the person had already replaced, and the change showed up one run late. A redefined main is the whole of a run, so it would have had to be asked for twice. Both flags drain now, and the exit drains before it leaves. The re-run is still tested first and cannot be starved: the flag is latched at the top of the round and nothing in the round can clear it. The transcript row in test_dev.ml asserted the old ordering by name — two lines out of the second run, the first of them the stale body — so it is a line shorter now, and the absence of that line is the claim. The park-note fixture grew a print of the redefinable body before its first poll, which is what makes the new row able to see which body the re-run started with. This is what the note the delivery is answered with has been promising: a module queued against a park installs no later than the program's next run. It now installs before that run's first frame rather than during it.
This commit is contained in:
parent
89481cf8ec
commit
097161fd41
49
lib/dev.ml
49
lib/dev.ml
@ -749,10 +749,11 @@ let refusal ~parked reply =
|
|||||||
Three of them, in the order of how far the module is from being live:
|
Three of them, in the order of how far the module is from being live:
|
||||||
|
|
||||||
A PARKED program has finished [main] and is asleep in [flan_merged_park].
|
A PARKED program has finished [main] and is asleep in [flan_merged_park].
|
||||||
Its ring is drained by the park's own poll when it is woken and by the next
|
Its ring is drained whenever that sleep ends — for an expression to run, or
|
||||||
run's frame boundaries, so the module lands no later than that run — and an
|
to start the next run — so the module lands no later than that run, and
|
||||||
expression evaluated in the meantime takes it first, because the poll that
|
before its first frame rather than at one. An expression evaluated in the
|
||||||
runs a thunk installs whatever is queued ahead of it. That is the whole
|
meantime takes it first, because the poll that runs a thunk installs
|
||||||
|
whatever is queued ahead of it. That is the whole
|
||||||
sentence, and it is worth reading once. It is not worth reading on every
|
sentence, and it is worth reading once. It is not worth reading on every
|
||||||
C-c C-c, and a finished program is parked, so every redefinition while a
|
C-c C-c, and a finished program is parked, so every redefinition while a
|
||||||
run's output is still on the screen used to repeat it. [park_noted] is what
|
run's output is still on the screen used to repeat it. [park_noted] is what
|
||||||
@ -2714,8 +2715,8 @@ let rerun t =
|
|||||||
the break loop, so main starts once that is resumed or aborted"
|
the break loop, so main starts once that is resumed or aborted"
|
||||||
else
|
else
|
||||||
"running main again; the globals are as the last run left them, and \
|
"running main again; the globals are as the last run left them, and \
|
||||||
anything delivered while it was parked installs at the first frame \
|
anything delivered while it was parked is installed before this \
|
||||||
boundary"
|
run starts"
|
||||||
in
|
in
|
||||||
ok [ ":note " ^ Wire.quote note ]
|
ok [ ":note " ^ Wire.quote note ]
|
||||||
| Error m -> error m)
|
| Error m -> error m)
|
||||||
@ -4025,11 +4026,12 @@ static void flan_merged_exit(int32_t status) {
|
|||||||
* from the same poll.
|
* from the same poll.
|
||||||
*
|
*
|
||||||
* So the wait has two flags and not one, and the difference between them is
|
* So the wait has two flags and not one, and the difference between them is
|
||||||
* what the thread does next. [program_asked] leaves the park; [program_poll]
|
* what the thread does next: [program_asked] leaves the park and
|
||||||
* drains the ring and waits again. The program stays PROGRAM_PARKED across the
|
* [program_poll] waits again. What they no longer differ about is the ring,
|
||||||
* whole of the second — a thunk is not a run, and an editor that saw [:parked
|
* which is drained on the way round either way — see the loop. The program
|
||||||
* nil] for the duration of a C-x C-e would show the program as live for a
|
* stays PROGRAM_PARKED across the whole of a poll — a thunk is not a run, and
|
||||||
* moment that has no frames in it.
|
* an editor that saw [:parked nil] for the duration of a C-x C-e would show
|
||||||
|
* the program as live for a moment that has no frames in it.
|
||||||
*
|
*
|
||||||
* A re-run is tested first, so a stream of evaluations cannot starve one. The
|
* A re-run is tested first, so a stream of evaluations cannot starve one. The
|
||||||
* poll flag is cleared BEFORE the lock is dropped, which is what makes a
|
* poll flag is cleared BEFORE the lock is dropped, which is what makes a
|
||||||
@ -4059,7 +4061,29 @@ static void flan_merged_park(void) {
|
|||||||
for (;;) {
|
for (;;) {
|
||||||
while (!program_asked && !program_poll)
|
while (!program_asked && !program_poll)
|
||||||
pthread_cond_wait(&program_wake, &program_lock);
|
pthread_cond_wait(&program_wake, &program_lock);
|
||||||
if (program_asked) break;
|
/* Which flag woke this, latched before the lock is dropped — and the ring
|
||||||
|
* is drained on BOTH paths, which is the whole of the fix below.
|
||||||
|
*
|
||||||
|
* A re-run used to [break] here, leaving the ring untouched. A plain
|
||||||
|
* redefinition does not set [program_poll] (only an expression does, by
|
||||||
|
* way of [Program.wake]), so a body redefined against the park was still
|
||||||
|
* sitting in the queue when this thread re-entered
|
||||||
|
* [flan_program_main] — and it installed at the coming run's first frame
|
||||||
|
* boundary, which is *after* main has been entered and after everything
|
||||||
|
* main calls before its first [(agent/poll)]. The run that was asked for
|
||||||
|
* in order to see the change ran the old body, and the change appeared in
|
||||||
|
* the run after it. A redefined [main] is the sharpest case, because
|
||||||
|
* nothing about that run is in front of it.
|
||||||
|
*
|
||||||
|
* So the drain goes in front of the exit as well: a delivery made while
|
||||||
|
* the program was parked is installed before the re-run starts, which is
|
||||||
|
* what "installs no later than its next run" means in the reply that
|
||||||
|
* accepted it.
|
||||||
|
*
|
||||||
|
* The re-run is still tested first and cannot be starved by a stream of
|
||||||
|
* evaluations: [leaving] is read at the top of the round and nothing in
|
||||||
|
* the round can clear it. */
|
||||||
|
int leaving = program_asked;
|
||||||
program_poll = 0;
|
program_poll = 0;
|
||||||
pthread_mutex_unlock(&program_lock);
|
pthread_mutex_unlock(&program_lock);
|
||||||
if (flan_agent_poll) flan_agent_poll();
|
if (flan_agent_poll) flan_agent_poll();
|
||||||
@ -4069,6 +4093,7 @@ static void flan_merged_park(void) {
|
|||||||
* a thunk that printed after both. */
|
* a thunk that printed after both. */
|
||||||
fflush(NULL);
|
fflush(NULL);
|
||||||
pthread_mutex_lock(&program_lock);
|
pthread_mutex_lock(&program_lock);
|
||||||
|
if (leaving) break;
|
||||||
}
|
}
|
||||||
program_asked = 0;
|
program_asked = 0;
|
||||||
program_state = PROGRAM_RUNNING;
|
program_state = PROGRAM_RUNNING;
|
||||||
|
|||||||
@ -14,8 +14,12 @@
|
|||||||
|
|
||||||
(defn step [] i64 7)
|
(defn step [] i64 7)
|
||||||
|
|
||||||
|
;;; Called by main before the run reaches any (agent/poll), which is what
|
||||||
|
;;; makes it the probe for *when* a parked delivery installs: a body queued
|
||||||
|
;;; while the program was parked either got into the ring before main was
|
||||||
|
;;; re-entered or it did not, and this is the print that says which.
|
||||||
(defn main [] i32
|
(defn main [] i32
|
||||||
(agent/start "/tmp/flan-dev-parknote-fallback.sock")
|
(agent/start "/tmp/flan-dev-parknote-fallback.sock")
|
||||||
(set runs (+ runs 1))
|
(set runs (+ runs 1))
|
||||||
(print runs) (println "")
|
(print (step)) (println "")
|
||||||
0)
|
0)
|
||||||
|
|||||||
@ -663,9 +663,9 @@ let () =
|
|||||||
fail "the program did not stay parked across an evaluation";
|
fail "the program did not stay parked across an evaluation";
|
||||||
|
|
||||||
(* [eval] is the one op a parked program took before this, because it
|
(* [eval] is the one op a parked program took before this, because it
|
||||||
queues and waits for nothing: the module sits in the ring until the game
|
queues and waits for nothing: the module sits in the ring until the
|
||||||
thread next reaches a frame boundary, and the next frame boundary a
|
parked thread next looks at it, which is when it is woken — to run an
|
||||||
parked program reaches is in its next run. Having to run the program
|
expression, or to start the run below. Having to run the program
|
||||||
before being allowed to fix the thing you closed it over is the loop
|
before being allowed to fix the thing you closed it over is the loop
|
||||||
this feature exists to remove. *)
|
this feature exists to remove. *)
|
||||||
let r =
|
let r =
|
||||||
@ -690,19 +690,27 @@ let () =
|
|||||||
if status r <> "ok" then
|
if status r <> "ok" then
|
||||||
fail "rerun: %s" (Option.value ~default:"" (Wire.string_field r "message"));
|
fail "rerun: %s" (Option.value ~default:"" (Wire.string_field r "message"));
|
||||||
|
|
||||||
(* Two lines, and between them the whole claim. The first is [step] as
|
(* One line, and the whole claim is in which body printed it. It is the
|
||||||
the third reload left it, printed before the new run has reached a
|
body delivered while the program was parked — installed before the
|
||||||
frame boundary; the second is the body delivered while it was parked,
|
re-run re-entered [main] rather than at the first [agent/wait] after
|
||||||
installed at the first [agent/wait] of the new run — and its value is
|
it — and its value is 106 rather than 1, because [extra] is a global
|
||||||
106 rather than 1, because [extra] is a global of a process that never
|
of a process that never died and the second run reads what the first
|
||||||
died and the second run reads what the first left in it. Nothing is
|
left in it. Nothing is zeroed between runs, deliberately: a clean
|
||||||
zeroed between runs, deliberately: a clean slate is one evaluation
|
slate is one evaluation away, and cannot be had back once a re-run
|
||||||
away, and cannot be had back once a re-run has wiped something.
|
has wiped something.
|
||||||
|
|
||||||
Seven and not six, because [settle] counts every line the daemon has
|
This used to be two lines, and the first of them was the defect:
|
||||||
|
[flan_merged_park] left on the re-run flag without draining its ring,
|
||||||
|
so the new run printed the *old* [step] and the queued body did not
|
||||||
|
land until the [agent/wait] after it. Everything a run does before
|
||||||
|
its first poll ran a body the person had already replaced, and a
|
||||||
|
redefined [main] — which is all of that run — would have had to be
|
||||||
|
asked for twice.
|
||||||
|
|
||||||
|
Six and not five, because [settle] counts every line the daemon has
|
||||||
handed over and the printing expression above contributed one that no
|
handed over and the printing expression above contributed one that no
|
||||||
run printed. Six would be satisfied by the first of these two. *)
|
run printed. *)
|
||||||
if not (settle 7) then fail "the program did not run again";
|
if not (settle 6) then fail "the program did not run again";
|
||||||
|
|
||||||
(* And a re-run while it is running is refused rather than queued: two
|
(* And a re-run while it is running is refused rather than queued: two
|
||||||
mains in one process would be writing the same globals at once. *)
|
mains in one process would be writing the same globals at once. *)
|
||||||
@ -727,11 +735,13 @@ let () =
|
|||||||
and 777 from a restart clause in a third — reached by a transfer that
|
and 777 from a restart clause in a third — reached by a transfer that
|
||||||
started in a handler and crossed a function the host was built with.
|
started in a handler and crossed a function the host was built with.
|
||||||
|
|
||||||
Then the same [main], run a second time in the same process: 777
|
Then the same [main], run a second time in the same process: 106,
|
||||||
again, from the body the first run ended with, and 106 from the one
|
from the body delivered while it was parked. There is no second 777
|
||||||
delivered while it was parked. 106 and not 1 is the line that says
|
in front of it any more, and that absence is the claim — the park
|
||||||
the globals are the finished run's — the process never died, so
|
drains its ring on the way out, so the re-run starts with the body
|
||||||
[extra] is where the first run left it.
|
the person last sent rather than with the one they replaced. 106 and
|
||||||
|
not 1 is the other half: the globals are the finished run's, the
|
||||||
|
process never died, so [extra] is where the first run left it.
|
||||||
|
|
||||||
And [pk] between the two, which is a line no run printed: it is the
|
And [pk] between the two, which is a line no run printed: it is the
|
||||||
thunk evaluated against the park, on the parked thread, flushed there
|
thunk evaluated against the park, on the parked thread, flushed there
|
||||||
@ -740,7 +750,7 @@ let () =
|
|||||||
before anything the second did. *)
|
before anything the second did. *)
|
||||||
ignore (Unix.waitpid [] pid);
|
ignore (Unix.waitpid [] pid);
|
||||||
let text = Buffer.contents output in
|
let text = Buffer.contents output in
|
||||||
let wanted = "1\n5\n105\n777\npk\n777\n106\n" in
|
let wanted = "1\n5\n105\n777\npk\n106\n" in
|
||||||
if text <> wanted then
|
if text <> wanted then
|
||||||
fail "program transcript\n got: %S\n wanted: %S" text wanted
|
fail "program transcript\n got: %S\n wanted: %S" text wanted
|
||||||
end;
|
end;
|
||||||
@ -5163,8 +5173,8 @@ let () =
|
|||||||
if not (await parked) then
|
if not (await parked) then
|
||||||
fail "the park-note program never parked"
|
fail "the park-note program never parked"
|
||||||
else begin
|
else begin
|
||||||
let first = redefine 1 in
|
let first = redefine 4241 in
|
||||||
let second = redefine 2 in
|
let second = redefine 4242 in
|
||||||
(* The long one by what it explains and not by its length: the
|
(* The long one by what it explains and not by its length: the
|
||||||
sentence about an expression taking the module first is the part
|
sentence about an expression taking the module first is the part
|
||||||
that is worth reading once. *)
|
that is worth reading once. *)
|
||||||
@ -5180,15 +5190,40 @@ let () =
|
|||||||
dropping it: what the reader is told is smaller, not different. *)
|
dropping it: what the reader is told is smaller, not different. *)
|
||||||
if not (contains_sub second "next run") then
|
if not (contains_sub second "next run") then
|
||||||
fail "the short park note stopped saying when it installs: %S" second;
|
fail "the short park note stopped saying when it installs: %S" second;
|
||||||
(* A new park is a new reader. [rerun] sends the program round [main]
|
(* ── And the note has to be true, which is a claim about the run ──
|
||||||
again and it parks straight away, with nothing evaluated in
|
|
||||||
between — which is the case [eval]'s own clearing cannot reach. *)
|
What the note promises is that a body delivered to a park installs
|
||||||
|
no later than the next run. It did not: [flan_merged_park] drained
|
||||||
|
the agent's ring only on the flag an *expression* sets, and left on
|
||||||
|
the re-run flag without draining at all — so a redefinition sent
|
||||||
|
while parked was still in the queue when the thread re-entered
|
||||||
|
[flan_program_main], and installed at the coming run's first frame
|
||||||
|
boundary instead. Everything main did before its first
|
||||||
|
[(agent/poll)] ran the old body, and the change turned up one run
|
||||||
|
late.
|
||||||
|
|
||||||
|
[programs/dev-parknote.flan]'s main prints [(step)] before it polls
|
||||||
|
at all, so the first run after a parked redefinition either shows
|
||||||
|
the new body or shows the lag. The output arrives on a reply rather
|
||||||
|
than in a file — [request] collects [:output] into [output] — so
|
||||||
|
the window is measured round the ops that follow the re-run.
|
||||||
|
|
||||||
|
A new park is a new reader, so the note's own reset is checked on
|
||||||
|
the far side of the same op: main runs and parks straight away with
|
||||||
|
nothing evaluated in between, which is the case [eval]'s clearing
|
||||||
|
cannot reach and [rerun]'s can. *)
|
||||||
|
let before = Buffer.length output in
|
||||||
let r = request pc "(:op \"rerun\")" in
|
let r = request pc "(:op \"rerun\")" in
|
||||||
if status r <> "ok" then fail "the park-note rerun: %s" (said r)
|
if status r <> "ok" then fail "the park-note rerun: %s" (said r)
|
||||||
else if not (await parked) then
|
else if not (await parked) then
|
||||||
fail "the park-note program never parked a second time"
|
fail "the park-note program never parked a second time"
|
||||||
else begin
|
else begin
|
||||||
let again = redefine 3 in
|
let printed = Buffer.sub output before (Buffer.length output - before) in
|
||||||
|
if not (contains_sub printed "4242") then
|
||||||
|
fail
|
||||||
|
"the run after a parked redefinition printed %S, so the module \
|
||||||
|
was still in the ring when main was re-entered" printed;
|
||||||
|
let again = redefine 4243 in
|
||||||
if not (contains_sub again "an expression evaluated in the meantime")
|
if not (contains_sub again "an expression evaluated in the meantime")
|
||||||
then
|
then
|
||||||
fail "a second park did not get the explanation back: %S" again
|
fail "a second park did not get the explanation back: %S" again
|
||||||
|
|||||||
Loading…
x
Reference in New Issue
Block a user