feat(ipc): saved replies: SaveReply/ReplySaved (8 per thread, released on thread death, unforgeable); terminal READ saved until Enter (line.rs editor, reader queue), now pinged
This commit is contained in:
24
docs/ipc.md
24
docs/ipc.md
@@ -141,9 +141,11 @@ init's calls each server with `server_framework::PING` every 2 s, which
|
||||
the framework's loop answers without the server's code. A ping
|
||||
unanswered for 5 s means the server is stuck in a handler; init kills it,
|
||||
and the death is handled as a crash, so the restarted server answers the
|
||||
still-queued ping. The terminal and the permission manager are not
|
||||
pinged: their handlers wait for the user (`READ`, a consent prompt),
|
||||
which a ping cannot tell from a hang.
|
||||
still-queued ping. The permission manager is not pinged: while it asks
|
||||
the user for consent it is itself waiting on the terminal inside a
|
||||
handler, which a ping cannot tell from a hang. (The terminal does not
|
||||
wait inside one: a `READ` before the line is typed is saved, `SaveReply`,
|
||||
and answered when Enter is.)
|
||||
|
||||
A program's `uses` endpoints arrive as badged copies with `Execute` and
|
||||
`Delegate`: the badge (unique per copy) tells the server which client is
|
||||
@@ -262,6 +264,13 @@ never reveals the sender's process or thread id.
|
||||
- `Reply(msg)`: deliver `msg` to the thread in the caller's reply slot and
|
||||
clear the slot. Error if the slot is empty. Never blocks.
|
||||
- `ReplyRecv(ep, msg)`: `Reply` if the slot is full, then `Receive(ep)`.
|
||||
- `SaveReply`: move the caller in the reply slot into the thread's table of
|
||||
saved replies (8 places) and return which place, a `SavedReply`; the
|
||||
slot is empty again, so the thread can receive others. `NoReply` if the
|
||||
slot is empty, `NoFreeSlot` if the table is full (the reply stays
|
||||
pending).
|
||||
- `ReplySaved(reply, msg)`: deliver `msg` to the caller saved there, as
|
||||
`Reply` would, and free the place. `NoReply` if nothing is saved there.
|
||||
- `Signal(ntfn)`: let `b` be the capability's badge, or `1` if unbadged. If
|
||||
a waiter is blocked, wake the first with `b`. Else if the bound thread is
|
||||
blocked in `Receive`, wake it with `b`. Else `bits |= b`.
|
||||
@@ -285,9 +294,12 @@ set it stays masked.
|
||||
`NoReply` instead of blocking forever.
|
||||
- A reply slot names the caller by thread id **and generation**, so a reply
|
||||
can never reach a different thread that reused the id.
|
||||
- If the server thread dies, its pending caller wakes with `NoReply`.
|
||||
- If the caller dies, the reply slot is simply stale and `Reply` is a
|
||||
successful no-op.
|
||||
- If the server thread dies, its pending caller and every caller it saved
|
||||
wake with `NoReply`.
|
||||
- If the caller dies, the reply slot (or saved place) is simply stale and
|
||||
`Reply` (`ReplySaved`) is a successful no-op.
|
||||
- A saved reply is named only within the thread that saved it: it cannot
|
||||
be passed on, and another thread's number means nothing.
|
||||
|
||||
## Budgets
|
||||
|
||||
|
||||
Reference in New Issue
Block a user