Three sentences that were true only while the state lagged
Follow-ups to the re-run flip, and all of one kind: each said something correct about a committed re-run that still read as parked, and the flip made it false. flan_merged_park's note that the program stays PROGRAM_PARKED across a poll is now true of every round but the one it leaves on — which is the round that drains the ring with a run already taken, and the round the fix's own argument leans on as the long one. Program.rerun's refusal told the reader to close a window or let the program finish. With a thunk stopped in the break loop a re-run is accepted, the state goes running, and a second is refused by that sentence — advice about a game loop for somebody whose thread is in a break. The C cannot see a break; this end can, so Dev.rerun passes what it already asked the agent and the refusal says resume or abort instead. The five-second timeout in eval_expr and run_render_thunk reached its break-loop sentence through the Parked arm, so a program stopped between runs was asked whether it calls (agent/poll). Both gain the arm that names the break. run_render_thunk's two sentences become a function first: the new one asks the agent, and that was the body of a five-millisecond tick. docs/BUILT.md gains the case an editor author meets — :parked nil :stopped t with no frames running — and FIX.org records that test_dev.ml:763's refusal assertion was racy before this and is narrowed by it.
This commit is contained in:
parent
1440ae4119
commit
ae46c5a878
21
FIX.org
21
FIX.org
@ -5710,6 +5710,27 @@ faces among them. Under two busy-loop burners, this machine's load average
|
|||||||
running 8 to 16: 9 failures in 25 runs. After the fix, same harness and the
|
running 8 to 16: 9 failures in 25 runs. After the fix, same harness and the
|
||||||
same two burners at the same load: 0 in 50.
|
same two burners at the same load: 0 in 50.
|
||||||
|
|
||||||
|
One test is strengthened rather than served by this. test_dev.ml:763 asserts
|
||||||
|
that a re-run asked for while the program is running is refused as "already
|
||||||
|
running" — and that assertion was itself racy: it fires after the run it
|
||||||
|
re-ran has been waited for, so the run could have finished and parked, and the
|
||||||
|
refusal it demands would not have come. With the flip at the acceptance the
|
||||||
|
RUNNING state starts earlier and covers more of that gap. It is a narrower
|
||||||
|
window, not a closed one; if that row ever flakes, the answer is to make the
|
||||||
|
test ask while a run is demonstrably in progress, not to widen the state
|
||||||
|
further.
|
||||||
|
|
||||||
|
Three sentences went stale the moment the state moved, and were rewritten with
|
||||||
|
it — the same class of defect as the one being fixed, since each was correct
|
||||||
|
only while a committed re-run still read as parked. [flan_merged_park]'s note
|
||||||
|
that the program stays PARKED across a poll, now true of every round but the
|
||||||
|
one it leaves on. [Program.rerun]'s refusal, which told a reader to close a
|
||||||
|
window or let the program finish when what holds it is a break loop: it takes
|
||||||
|
what the caller already knows and says resume or abort instead. And the
|
||||||
|
five-second timeout in [eval_expr] and [run_render_thunk], which reached its
|
||||||
|
break-loop sentence through the [Parked] arm and would otherwise have asked
|
||||||
|
whether a game loop calls [(agent/poll)] about a program stopped between runs.
|
||||||
|
|
||||||
Related but separate, and not this: test_reload's "the registry read under a
|
Related but separate, and not this: test_reload's "the registry read under a
|
||||||
writer" is a reader racing a writer over the allocation registry, about one run
|
writer" is a reader racing a writer over the allocation registry, about one run
|
||||||
in five in isolation, and shares nothing with this but the word intermittent.
|
in five in isolation, and shares nothing with this but the word intermittent.
|
||||||
|
|||||||
@ -1439,6 +1439,14 @@ between them, or arrived a moment later and were told the program was already ru
|
|||||||
symptoms. The park's own store of `PROGRAM_RUNNING` on the way back into `main` is now a no-op that documents where the
|
symptoms. The park's own store of `PROGRAM_RUNNING` on the way back into `main` is now a no-op that documents where the
|
||||||
thread has got to.
|
thread has got to.
|
||||||
|
|
||||||
|
The case an editor author has to know about is `:parked nil :stopped t` with no frames running. An expression evaluated
|
||||||
|
against a park can stop on a condition, which leaves the program's one thread inside the break loop; a re-run asked for
|
||||||
|
then is accepted — it is the next thing that thread will do — so the state says running while nothing is executing.
|
||||||
|
That is not a lie about a park: `:parked` reports a park, `:stopped` reports a break loop, and this is a break loop
|
||||||
|
with a run waiting behind it. `rerun`'s reply says so in its `:note`, a second `rerun` is refused with the resume-or-abort
|
||||||
|
sentence rather than the close-the-window one, and an evaluation that times out there names the break too. The run
|
||||||
|
starts when the break is resumed or aborted.
|
||||||
|
|
||||||
`close`ing stdout went with this change, and it had to. That was how the compiler learned the program was done — the
|
`close`ing stdout went with this change, and it had to. That was how the compiler learned the program was done — the
|
||||||
pipe read EOF, exactly as the two-process daemon learns it from a dead child — but a pipe delivers EOF *once*, so the
|
pipe read EOF, exactly as the two-process daemon learns it from a dead child — but a pipe delivers EOF *once*, so the
|
||||||
signal and the program's output were the same resource: spending it left the second run with nowhere to print. The
|
signal and the program's output were the same resource: spending it left the second run with nowhere to print. The
|
||||||
|
|||||||
70
lib/dev.ml
70
lib/dev.ml
@ -1263,6 +1263,23 @@ let eval_expr t ~code ~origin ~pause =
|
|||||||
program is parked, so nothing is competing with it: the \
|
program is parked, so nothing is competing with it: the \
|
||||||
thunk is most likely stopped on a condition inside the \
|
thunk is most likely stopped on a condition inside the \
|
||||||
break loop, which restart or abort answers"
|
break loop, which restart or abort answers"
|
||||||
|
(* The same cause without the park to name it. An earlier
|
||||||
|
evaluation can stop on something and still be sitting in the
|
||||||
|
break loop when this one arrives — [`Broke] above sees only
|
||||||
|
stops entered after the request — and the thread is then in
|
||||||
|
no state to run anything. That used to be reached through
|
||||||
|
the [Parked] arm, which is where such a thread was; it is
|
||||||
|
not any more once a re-run has been accepted, because taking
|
||||||
|
one ends the park while the break goes on holding the
|
||||||
|
thread. Sending that reader to look for [(agent/poll)] in a
|
||||||
|
game loop would be sending them away from the break buffer
|
||||||
|
their editor has open. *)
|
||||||
|
else if parked_break t then
|
||||||
|
error
|
||||||
|
"the expression produced no value in five seconds, because \
|
||||||
|
the program is stopped at an earlier break and runs \
|
||||||
|
nothing until that ends. Take a restart or abort in the \
|
||||||
|
break buffer, and evaluate this again"
|
||||||
(* And a third cause, which is the one a session now reaches
|
(* And a third cause, which is the one a session now reaches
|
||||||
early enough to hit: the program has not bound its agent
|
early enough to hit: the program has not bound its agent
|
||||||
socket, so it is still ahead of its own [(agent/start ...)]
|
socket, so it is still ahead of its own [(agent/start ...)]
|
||||||
@ -1825,7 +1842,10 @@ let run_render_thunk ?(stopped_only = false) ?at_stop t ~tag
|
|||||||
thing not to say here. A parked thread has nothing competing
|
thing not to say here. A parked thread has nothing competing
|
||||||
with it, so what it is doing is holding a break — the thunk
|
with it, so what it is doing is holding a break — the thunk
|
||||||
asked for a stopped stack and the stop has been let go of. *)
|
asked for a stopped stack and the stop has been let go of. *)
|
||||||
let gave_up =
|
(* A function and not a value, because the middle arm asks the
|
||||||
|
agent and this is the body of a five-millisecond tick. Only
|
||||||
|
the tick that gives up needs the answer. *)
|
||||||
|
let gave_up () =
|
||||||
if liveness t = Parked then
|
if liveness t = Parked then
|
||||||
Error
|
Error
|
||||||
"the inspection produced nothing in five seconds. The \
|
"the inspection produced nothing in five seconds. The \
|
||||||
@ -1833,12 +1853,27 @@ let run_render_thunk ?(stopped_only = false) ?at_stop t ~tag
|
|||||||
the break it was built against has most likely been \
|
the break it was built against has most likely been \
|
||||||
resumed since, and a stopped-only job is dropped rather \
|
resumed since, and a stopped-only job is dropped rather \
|
||||||
than run against a resumed program"
|
than run against a resumed program"
|
||||||
|
(* Still at a break, and not parked — a program stopped during
|
||||||
|
a run, or one whose park has ended because a re-run was
|
||||||
|
accepted while the break went on holding the thread. The
|
||||||
|
break loop is the poll loop, so the job had somewhere to
|
||||||
|
run; what it did not have is the stop it was built against,
|
||||||
|
which is the same story the parked sentence tells. Naming
|
||||||
|
the game loop here would send the reader past the break
|
||||||
|
buffer that is holding their program. *)
|
||||||
|
else if parked_break t then
|
||||||
|
Error
|
||||||
|
"the inspection produced nothing in five seconds. The \
|
||||||
|
program is stopped at a break, and a stopped-only job is \
|
||||||
|
dropped rather than run once the stop it was built against \
|
||||||
|
has been left behind. Ask again from the break buffer as \
|
||||||
|
it stands now"
|
||||||
else
|
else
|
||||||
Error
|
Error
|
||||||
"the program did not reach a frame boundary; is it calling \
|
"the program did not reach a frame boundary; is it calling \
|
||||||
(agent/poll)?"
|
(agent/poll)?"
|
||||||
in
|
in
|
||||||
if ms <= 0 then gave_up
|
if ms <= 0 then gave_up ()
|
||||||
else begin
|
else begin
|
||||||
ignore (Unix.select [] [] [] 0.005);
|
ignore (Unix.select [] [] [] 0.005);
|
||||||
(* Not [Gone], for the reason [eval_expr]'s own wait now gives:
|
(* Not [Gone], for the reason [eval_expr]'s own wait now gives:
|
||||||
@ -1846,7 +1881,7 @@ let run_render_thunk ?(stopped_only = false) ?at_stop t ~tag
|
|||||||
frame boundary, and a render job asked for at a break the
|
frame boundary, and a render job asked for at a break the
|
||||||
park is holding is running in that break's own poll. Gone is
|
park is holding is running in that break's own poll. Gone is
|
||||||
the only state no amount of waiting recovers from. *)
|
the only state no amount of waiting recovers from. *)
|
||||||
if liveness t <> Gone then wait (ms - 5) else gave_up
|
if liveness t <> Gone then wait (ms - 5) else gave_up ()
|
||||||
end
|
end
|
||||||
in
|
in
|
||||||
wait 5000
|
wait 5000
|
||||||
@ -3093,9 +3128,16 @@ let rerun t =
|
|||||||
the park — the C stores the new state as it accepts — so by the time
|
the park — the C stores the new state as it accepts — so by the time
|
||||||
there is an [Ok] to describe, this session's program reads as running
|
there is an [Ok] to describe, this session's program reads as running
|
||||||
whatever it was doing a moment ago, and the note below would have lost
|
whatever it was doing a moment ago, and the note below would have lost
|
||||||
the one case it exists for. *)
|
the one case it exists for.
|
||||||
let stopped_in_park = liveness t = Parked && parked_break t in
|
|
||||||
(match Program.rerun () with
|
[at_break] is asked of the agent whichever state the program is in,
|
||||||
|
because both answers need it and neither can be inferred from the other.
|
||||||
|
Accepted and stopped is the note below; refused and stopped is a refusal
|
||||||
|
whose advice would otherwise be about a window to close — see
|
||||||
|
[Program.rerun]. *)
|
||||||
|
let at_break = parked_break t in
|
||||||
|
let stopped_in_park = liveness t = Parked && at_break in
|
||||||
|
(match Program.rerun ~stopped:at_break () with
|
||||||
| Ok () ->
|
| Ok () ->
|
||||||
(* The park this session was explaining is over, so the park after it
|
(* The park this session was explaining is over, so the park after it
|
||||||
gets the explanation again — see [install_note]. Cleared here as
|
gets the explanation again — see [install_note]. Cleared here as
|
||||||
@ -4454,10 +4496,18 @@ static void flan_merged_exit(int32_t status) {
|
|||||||
* 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 and
|
* what the thread does next: [program_asked] leaves the park and
|
||||||
* [program_poll] waits again. What they no longer differ about is the ring,
|
* [program_poll] waits again. What they no longer differ about is the ring,
|
||||||
* which is drained on the way round either way — see the loop. The program
|
* which is drained on the way round either way — see the loop. A poll the
|
||||||
* stays PROGRAM_PARKED across the whole of a poll — a thunk is not a run, and
|
* program is only visiting leaves it PROGRAM_PARKED throughout — a thunk is
|
||||||
* an editor that saw [:parked nil] for the duration of a C-x C-e would show
|
* not a run, and an editor that saw [:parked nil] for the duration of a C-x
|
||||||
* the program as live for a moment that has no frames in it.
|
* C-e would show the program as live for a moment that has no frames in it.
|
||||||
|
*
|
||||||
|
* The round it leaves on is the exception, and it is one by the same rule
|
||||||
|
* rather than against it. That round begins with a re-run already taken, and a
|
||||||
|
* taken re-run is a run: [flan_merged_rerun] has stored PROGRAM_RUNNING
|
||||||
|
* before this thread is even awake. So the drain in front of the exit happens
|
||||||
|
* with the program reading as running, which is what it is — on its way into
|
||||||
|
* main, installing what was queued for that run. The state follows the
|
||||||
|
* decision either way; only the decision differs.
|
||||||
*
|
*
|
||||||
* 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
|
||||||
|
|||||||
@ -71,10 +71,26 @@ let wake () = ignore (raw_wake ())
|
|||||||
The refusal is the program's to make, not this end's. Checking the state
|
The refusal is the program's to make, not this end's. Checking the state
|
||||||
here and signalling after would leave a gap for the program to finish or
|
here and signalling after would leave a gap for the program to finish or
|
||||||
start in; the C does both under one lock, so a request is either taken or
|
start in; the C does both under one lock, so a request is either taken or
|
||||||
told the program is running, and never both. *)
|
told the program is running, and never both.
|
||||||
let rerun () =
|
|
||||||
|
[stopped] is the one thing the refusal cannot see for itself, and without it
|
||||||
|
the advice is wrong in the case that needs it most. The C knows the program
|
||||||
|
is not available; it does not know that the thread is sitting in a break
|
||||||
|
loop, which is a thing the agent reports and this end reads. "Close its
|
||||||
|
window, or let it finish" is what to do about a program that is running; it
|
||||||
|
is no use at all to somebody whose evaluation stopped on a breakpoint, or
|
||||||
|
who has already asked for a re-run that is waiting on that same break. Both
|
||||||
|
of those are ended by resuming or aborting, so that is what those are told.
|
||||||
|
The caller passes what it already knows — see [Dev.rerun]. *)
|
||||||
|
let rerun ?(stopped = false) () =
|
||||||
match raw_rerun () with
|
match raw_rerun () with
|
||||||
| 0 -> Ok ()
|
| 0 -> Ok ()
|
||||||
|
| 1 when stopped ->
|
||||||
|
Error
|
||||||
|
"the program is stopped at a break, so main cannot be started or \
|
||||||
|
restarted until that ends: resume it or abort it, and the program goes \
|
||||||
|
on from there. If a re-run was already accepted, it is waiting on the \
|
||||||
|
same thing and needs no second request"
|
||||||
| 1 ->
|
| 1 ->
|
||||||
Error
|
Error
|
||||||
"the program is already running; a re-run starts main again, and two \
|
"the program is already running; a re-run starts main again, and two \
|
||||||
|
|||||||
Loading…
x
Reference in New Issue
Block a user