From 11f67e8324c5a5a0f892cb25d372b32eb321e329 Mon Sep 17 00:00:00 2001 From: Nils Lehnen <30603423+iderex@users.noreply.github.com> Date: Thu, 13 Aug 2026 14:25:09 +0200 Subject: [PATCH] Record sign-out, forgetting a server, and holding several sessions A decision record under docs/decisions/, and its line in the index. Sign-out and forgetting a server are separated into two acts. The first ends one session: the token leaves memory, the secret is forgotten through the interface in 0033, the session's outstanding work ends in named kinds from 0004, every other session keeps running, and all of that completes with no network. Telling the server is the only half that may fail, and a sign-out that could not tell it says so rather than refusing to complete. The second act does everything the first does and then removes every cache entry and every queued action under the key space 0041 fixes for that server and account. The queue survives a sign-out, which is what 0005 already requires when it says the answer must be the same whether the sign-out was asked for or forced by a refused renewal. The failures this prevents are the four a sign-out written to make a cache test pass would have. A sign-out that waits on the server before dropping the token leaves a token in memory exactly when the network is bad, which is when somebody is most likely to hand the device to somebody else. One that discards the queue loses actions a person took, silently, in the one act where throwing things away looks like the point. One that cancels a lane rather than a session stops the other account's screen on a television with two people signed in. And one that removes the cache reverses the argument in 0006 and 0068 for keeping entries across a sign-in, by fixture rather than by argument. That last one is where this record departs from the list in the issue, which puts cache removal inside sign-out. 0006 and 0068 landed the other answer with their reasons, so the record follows them and the removal is the second act. Refs #114. Three of its conditions are tests against running code and none of them is reachable in this tree. Signed-off-by: Nils Lehnen <30603423+iderex@users.noreply.github.com> --- ...114-signing-out-and-forgetting-a-server.md | 332 ++++++++++++++++++ docs/decisions/README.md | 1 + 2 files changed, 333 insertions(+) create mode 100644 docs/decisions/0114-signing-out-and-forgetting-a-server.md diff --git a/docs/decisions/0114-signing-out-and-forgetting-a-server.md b/docs/decisions/0114-signing-out-and-forgetting-a-server.md new file mode 100644 index 0000000..73a4a34 --- /dev/null +++ b/docs/decisions/0114-signing-out-and-forgetting-a-server.md @@ -0,0 +1,332 @@ +# 0114. Signing out, forgetting a server, and holding several sessions + +Date: 2026-08-13 + +Status: accepted. Supersedes nothing. Superseded by nothing. + +Issue: #114 + +## The decision + +Signing out and forgetting a server are two acts rather than one: a sign-out ends +one session, drops its token from memory, forgets its secret through 0033, +resolves that session's outstanding work into named kinds from 0004, leaves every +other session running and completes on a device with no network; forgetting a +server is a second act a client asks for, which does everything a sign-out does +and then removes every cache entry and every queued action under the key space +0041 fixes for that server and that account; and the queue survives a sign-out, +because an undelivered action is the one thing a person did that has no copy +anywhere else. + +## Two acts, and why they are not one + +Every client that was not told they differ collapses them into one button, and +which of the two that button does is then decided by whoever wrote it. + +The two answer different questions. Somebody signing out is saying that the next +person to pick this device up must not be them. Somebody forgetting a server is +saying that this device should stop holding anything about that server at all. +The first is ordinary and happens on a television in a house every evening. The +second is what a person does before they sell the device, or when they have +finished with a server they were only visiting. + +If sign-out did both, then signing back in on a device somebody already used +refetches the whole library over whatever connection they have, and 0006's +argument for keeping entries across a sign-in is lost. If forgetting a server did +only what a sign-out does, then there is no act at all that removes what the core +asked to be kept, and 0068's promise to an operator that they can have it removed +has nothing behind it. + +So both exist, they are named separately in the interface, and the second is +strictly the first plus removal. + +## What a sign-out does + +It takes a session, which 0005 fixes as one server, one account and one device +identity together, and it does five things. + +The token leaves memory. Nothing further is sent under it by this core. + +The secret is forgotten through the interface in 0033, under the name that +record derives from 0041's construction. Forgetting one that is not there +succeeds, so a sign-out on a session whose secret was never written is not a +failure. + +The session's outstanding work is resolved, in the terms of the next section. + +The session moves to signed out and stays addressable. A signed-out session is +still a server, an account and a device identity the client can name, which is +what a later sign-in and a later forget both need, and 0033 already requires the +client rather than the core to be holding that triple. + +The server is told, as one ordinary request under the bounds 0007 and 0038 +already fix, and it is the only half that may fail. A token this core stopped +using is still a token the server accepts until the server decides otherwise, so +telling it is worth attempting and worth reporting. Where the attempt did not +succeed the client is told through 0100, with the fact that the token may still +be live at the server, because that is a thing an operator can act on from the +server's own side and cannot act on if nobody said it. + +The first four happen whatever the network is doing. A sign-out on a train is a +sign-out, and it reports that the server was not told rather than refusing to +complete. Reversing that order, so that the local half waits on the server half, +produces the failure this whole act exists against: a person hands the device to +somebody else believing they signed out, and the token is still in memory because +a request timed out. + +A sign-out of a session that is already signed out succeeds and changes nothing. +A sign-out forced by a refused renewal in 0034 reaches exactly this state, with +the server half skipped because the server has already refused that token, which +is what 0005 requires when it says the answer must be the same whether the +sign-out was asked for or forced. + +## What a sign-out does not do + +It does not touch any other session. Not another account on the same server, not +the same account on another server, and not the same account on the same server +from a second device, which 0005 already fixes as a second session because the +server issued a second token and may end either one alone. + +It does not remove cache entries. 0006 and 0068 both landed this direction with +their reasons, and this record follows them rather than reopening them: the +entries are keyed per server, per account and per device, so leaving them costs +nobody else's privacy, and signing back in on a device somebody already used is +the case the cache exists for. This issue's own list of the parts of a sign-out +puts cache removal inside it, and the two landed records are the later answer; +what removes those entries is the second act below. + +The consequence of that is stated here rather than left to be found. A cache read +needs no token, which is what 0046's cold start depends on, so a signed-out +account's library is still servable to whoever names that session on that device. +0046 already says as much, in the sentence that naming a session is the act that +exposes its cache and that 0041 keeps two accounts apart while doing nothing to +keep one account's entries from whoever picked the device up. This record does +not weaken that and does not improve it: it is the reason the second act exists, +and a client whose sign-out button has to mean the stronger thing calls the +second one. + +It does not stop playback. 0005 guarantees that a token dying mid-playback does +not interrupt what somebody is watching, and an asked-for sign-out is not a +reason to break that guarantee either. The stream is being read by the platform's +own player against the address handed over in #111, and this core does not have a +way to stop it. What may happen is that the address stops working, because the +server was told the token is finished; that is the server's answer to the player +rather than something the core did, and the record says so here rather than +leaving a client to discover it as a defect. + +It does not end sessions elsewhere. What a sign-out reaches is this device. + +## Work in flight + +Four kinds of work can be running when a sign-out arrives, and each ends in a +named state rather than in silence. 0009 already refuses reporting a cancelled or +undelivered thing as something it is not, and this is that rule applied to one +moment. + +A request already sent on that session is cancelled and ends as `cancelled` from +0004. An answer that arrives afterwards is discarded rather than delivered, and +it is not written to the cache, because it was fetched under a session that has +ended. + +A decode running for that session ends the same way, at the step boundary 0009 +and 0115 already fix, since a decoder is not interruptible at an arbitrary +instruction. Bytes already handed to a caller are the caller's and are not +reached, which is the same boundary 0042 draws for eviction. + +A read or a write already begun through the byte store completes. That is 0115's +rule and its reason is that the store is the client's own code, and it holds here +without exception: a sign-out does not abandon a call inside somebody else's +implementation. + +A queued action stays queued, which is the section below. + +Cancelling by session is what makes this possible, and it is the part that will +be got wrong. 0009 gives the core two lanes shared by every session, so the unit +of work on a lane carries the session it belongs to and the sign-out cancels that +set and no other. A sign-out that cancelled a lane's work would stop the other +account's tile wall on a television with two people signed in, and the person who +lost their screen did nothing. + +## The queue survives, and what that costs + +0047 holds one durable queue per session, and its contents are the actions +somebody took that the server has not been told about yet. 0068 names it as the +one piece of this data with no copy on the server. + +So a sign-out keeps it. A later sign-in to the same server, account and device +finds the queue where it was, in its own order, and drains it before anything +else is sent, which is exactly what 0005 already promises for the sign-out that a +refused renewal forces. Keeping the two answers identical is what stops the +queue's guarantee from depending on which of the two ended the session. + +Before the server is told, and only while there is a session to send under, the +sign-out attempts a drain. It is an ordinary attempt under 0007 and 0038 and it +adds no number of its own: what drains, drains, and what does not stays queued. +A sign-out is not allowed to become slow because somebody has a fortnight of +positions waiting, and it is not allowed to discard them either. + +What that costs is a queue nobody comes back for. A person who signs out of a +server and never signs in again leaves entries under 0047's bound that will not +be delivered and will not expire, because 0047 refuses to expire an entry by age +and gives the reason. That cost is real, it is bounded by the count 0047 fixes, +and the act that removes it is the next section. Naming it here is the point: the +alternative is discovering it as a store that holds something forever for a +session that is finished. + +## Forgetting a server + +Everything a sign-out does, and then removal. + +Every cache entry under the key space for that server and that account, in both +tiers of 0054, which 0041 makes a well defined set: every entry whose first three +parts are that server, that account and that device identity, and no other. + +The queue for that session in 0047, including its standing count of what it +dropped. + +Whatever the core keeps to find those entries, which is the index 0042 holds for +eviction. 0040 gives the store no listing and 0041's keys are digests, so that +index is the only route to the set, and a removal that left it holding rows for +entries it has removed would leave the bound counting bytes that are gone. + +Removal goes through the same store interface as everything else. The core +removes what it wrote, through 0040's remove operation, one entry at a time. It +does not reach past the interface, it does not ask the client to delete a +directory, and it makes no claim about what an uninstall leaves behind, which +0068 already refuses to promise and this record does not promise either. + +The act is per server and account rather than per server, because two people on +one television are two key spaces and one of them forgetting a server is not the +other one asking for anything. + +## When a removal cannot be completed + +The index is the single point of failure and the record says so rather than +assuming it is there. + +Where the index is absent or was refused by 0105, the set is not reachable, and +the core reports that it removed what it could and names how many entries it +could not reach. It does not report a removal it did not make. This is 0068's +promise meeting its limit in the open, and the honest report is worth more than a +success value, because an operator who asked for their data to be removed and was +told it was gone has no reason ever to ask again. + +Where a removal fails part way, because the store answered `storage-unavailable` +from 0004, what has been removed stays removed and the act reports how far it +reached. Repeating it is safe, since removing an entry that is not there succeeds +under 0040's rule and the index says what is left. + +The local half of the sign-out inside a forget still completes in both cases. A +device that cannot reach its own store is not a device where somebody should +remain signed in. + +## Holding several at once + +0005 already fixes that the core holds any number, that every call names its +session, and that there is no ambient current session a second call can change +underneath the first. This record adds what holding several requires of the acts +above, and one thing about the set itself. + +The durable list of sessions is the client's, not the core's. 0033's store cannot +be asked what it holds and 0040's cannot either, so nothing in the core can +enumerate what was signed in on a previous run, and 0115 already makes restoring +a session a call the client makes naming the triple it wants. The core knows the +sessions it was told about during this run and no others. + +The consequence is that a client which loses its own list leaves both a secret +and a key space that nothing will ever name again. 0033 already states that cost +for the secret. It is the same cost for the cache, it is the reason forgetting a +server is a call rather than something the core does on its own, and a client +that lost the list clears the platform's own stores itself. + +## Why this is written down before the code + +Sign-out is written by whoever needs it first, and that is #41's own test, which +signs in, signs out and signs in as somebody else. A sign-out written to make +that test pass removes the cache, because the test is about the cache, and the +result is 0006's argument reversed by a fixture rather than by an argument. + +Each of the other three parts has a cheap default that is wrong in a way nothing +notices for a long time. A sign-out that waits on the server before dropping the +token in memory leaves a token in memory whenever a network is bad, which is the +one condition under which somebody is most likely to hand the device to somebody +else. A sign-out that discards the queue loses actions a person took, silently, +which is the failure 0047 exists against, arriving through the one act where +throwing things away looks like the point. A sign-out that cancels a lane rather +than a session stops the other person's screen, and on a developer's machine with +one account it is invisible. + +Two of the four cannot be corrected afterwards. An action discarded at sign-out +is gone from the only device that held it. A token left live at a server because +nobody reported that it was not ended stays live until the server decides, and no +later change to the core reaches it. + +None of this has happened here, because there is no session, no queue and no +store in this tree. The records quoted above are not all of the ones that named +this issue as the one that would answer them, and the set moves, so it is derived +rather than counted here: + + $ git grep -l '#114' -- docs/decisions + +## Alternatives, and what each cost + +One act, where signing out removes everything. It is the answer this issue's own +list assumes, it needs no second name in the interface, and it is what a person +who has just read a privacy page expects. It costs 0006's whole argument for +keeping entries across a sign-in, so every sign-in on a shared television refetches +a library over the connection the cache exists to avoid, and it makes the cheap +act destructive in a way that cannot be undone by signing back in. + +One act, where signing out removes nothing but the token, with no second act at +all. The smallest surface, and it is what the core can do without an index. It +costs 0068's promise to an operator outright, since nothing then removes what the +core asked to be kept, and the first client to want it builds its own removal +against a key space it cannot compute. + +Removing the cache lazily, by marking the key space dead and letting 0042's bound +evict it in time. No index walk, no partial removal to report, and the entries do +go eventually. It costs the promise its meaning: data removed when the cache +happens to fill is data still on the device for as long as somebody does not use +the application, which is exactly the period after they stopped using it. + +Discarding the queue at sign-out, on the argument that a session that ended has no +business holding work. Simpler, and it removes the queue-nobody-comes-back-for +cost named above. 0005 already refuses it by naming it as its own reversal +condition, and what it costs is a person's actions, silently, in the case where +they signed out on a train and back in the next morning. + +Waiting for the server to confirm before completing the local half. It makes the +report simple, since either the token is ended everywhere or the sign-out did not +happen. It costs the case the act is for, because a device with no network then +cannot sign out at all. + +Letting the core keep its own list of sessions so that it can offer one and clean +up after a client that lost theirs. It removes the orphan cost above. It costs a +durable list of servers and accounts written by the core somewhere it chose, +which 0101 refuses, and it needs an enumeration over stores that 0033 and 0040 +both deliberately do not have. + +## What would reverse this + +A client is measured, on the harness in #65, to spend longer walking the index at +a forget than an operator will wait on the smallest supported device. Removal by +key space then needs something the store can answer, the store grows an +operation, and that is 0040's reversal and this record's together. + +A supported server line offers no way to end a token from the device. The server +half above is then not merely best effort, it is absent, and what replaces this +record says what an operator is told instead, since the current text promises a +report about an attempt that would never be made. + +A second act turns out not to be enough, named with the case that cannot be +expressed. The candidate is a person wanting their playback positions removed +from the device while staying signed in, which is neither of the two acts here. +Then the removal is expressed per kind rather than per session and this record is +superseded rather than extended, because the argument for two acts is the +argument against a third. + +#105 refuses an index in ordinary use rather than after a version change, so the +report about a removal that could not be completed becomes the common answer +instead of the edge. That is evidence the index is the wrong place to hold the +only route to a key space, and what replaces this record says what holds it +instead. diff --git a/docs/decisions/README.md b/docs/decisions/README.md index 9ed01e2..73d777c 100644 --- a/docs/decisions/README.md +++ b/docs/decisions/README.md @@ -40,4 +40,5 @@ allocated, and why a record is superseded rather than edited are in - [0102. The clocks every deadline is measured against](0102-the-clocks-every-deadline-is-measured-against.md) - [0105. An entry this version did not write, and one that was not finished](0105-an-entry-this-version-did-not-write.md) - [0112. Where the platform decoder begins](0112-where-the-platform-decoder-begins.md) +- [0114. Signing out, forgetting a server, and holding several sessions](0114-signing-out-and-forgetting-a-server.md) - [0115. Creating the core, stopping it, and a host that suspends it](0115-creating-and-stopping-the-core.md)