mirror of
https://github.com/block/buzz.git
synced 2026-08-18 06:50:31 +02:00
docs(terminal): say why tail_full cannot fire, not just that nothing calls it
The previous wording said the signal has no consumer. That is the weaker half of the fact and the half that ages badly: a reader who deletes the pump loop learns the rest by wedging a terminal. Both measurements are now in the comment. With the loop, 1 MiB of pure RIS through 16 KiB reads leaves a tail high-water of exactly 0 -- the tail is empty between iterations, so the predicate is unreachable by construction. Without it, the same stream reaches TAIL_CAP at read 257. Reproduced here before quoting: 0 and 257 both hold on this tree. Wording is Sami's, who measured it first and made the argument that the signal and the loop are one fact from two sides. Delete the loop and this predicate stops being unreachable in the same instant it starts being needed. Co-authored-by: tlongwell-block <109685178+tlongwell-block@users.noreply.github.com> Signed-off-by: tlongwell-block <109685178+tlongwell-block@users.noreply.github.com>
This commit is contained in:
co-authored by
tlongwell-block
parent
9ca661ee8e
commit
232f56b672
@@ -112,14 +112,19 @@ impl Feeder {
|
||||
/// exactly how a paused reader strands a child mid-teardown; a reader that
|
||||
/// simply stops asking resumes by default.
|
||||
///
|
||||
/// **Not yet consumed in production.** The runtime reader pumps
|
||||
/// [`Feeder::drain`] to completion after every read, so the tail cannot
|
||||
/// currently grow to the cap and nothing needs to ask. This signal exists
|
||||
/// for the reader that stops pumping -- it is the queue bound, and the
|
||||
/// pump loop is the only reason the queue bound is not load-bearing
|
||||
/// today. Stated rather than left to be inferred from an empty
|
||||
/// call-graph: an unused signal that looks wired is worse than one that
|
||||
/// says it isn't.
|
||||
/// **No production consumer today, and not an oversight.** The runtime
|
||||
/// reader pumps [`Feeder::drain`] to completion after every read
|
||||
/// (`terminal_runtime.rs`), so the tail is empty between iterations and
|
||||
/// this can never go true -- measured 0 bytes high-water against 1 MiB of
|
||||
/// pure RIS, the densest atom there is. It exists for a future reader
|
||||
/// that defers pumping, and such a reader **must** consult it: without
|
||||
/// the pump loop the same stream reaches [`TAIL_CAP`] in 257 reads of
|
||||
/// 16 KiB.
|
||||
///
|
||||
/// The numbers are here rather than "nothing calls this" because the
|
||||
/// signal and the loop are one fact from two sides. Delete the loop and
|
||||
/// this predicate stops being unreachable in the same instant it starts
|
||||
/// being needed.
|
||||
pub fn tail_full(&self) -> bool {
|
||||
self.pending_bytes() >= TAIL_CAP
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user