server: document proof of no deadlocks

src/bin/mgen-server.rs

@@ -122,6 +122,51 @@ async fn main() -> Result<(), Box<dyn Error>> {
     }
 }
 
+/*
+An informal proof that the main thread + handshake threads will not deadlock.
+(The rest of the code mainly uses channels so is a lot simpler.)
+
+locks:
+ - writer_db (WDB)
+ - snd_db (SDB)
+   - group_snds (GSS)
+
+== CFG ==
+WDB.R() |-> Some(socket_updater) -> SDB.R(); drop(WDB.R, SDB.R)
+        |-> None -> drop(WDB.R); SDB.R() |-> Some(group_snds) -> drop(SDB.R); GSS.W(); drop(GSS.W)
+                                         |-> None -> drop(SDB.R); SDB.W(); GSS.W(); drop(GSS.W, SDB.W)
+=========
+
+The program deadlocks iff lock A can't drop until it gets lock B, while lock B can't drop until it
+gets lock A, or a transitive equivalent.
+
+We have three potential locks that can deadlock: WDB, SDB, and GSS.
+
+Can WDB ever deadlock?
+It only ever locks in one place: at the start, when the thread holds no other locks.
+None case: Drops immediately, never takes any other locks, no opportunity to deadlock.
+Some case: Get SDB.R. Can locked SDB ever be waiting for WDB? No, SDB only
+locks either after it already has the WDB.R (in another copy of this branch), or the WDB isn't
+locked (in the other branch).
+This covers all branches, therefore, WDB can never deadlock.
+
+Can GSS ever deadlock?
+GSS locks in three places (one of which is not shown in the CFG, it's in get_messages() as
+global_db, and is extra irrelevant because it doesn't even read lock until all write lock threads
+have terminated). In all three places, it immediately drops the lock without doing any other locking
+operations.  Therefore, GSS can never deadlock.
+
+Can SDB ever deadlock?
+SDB locks in three places: a read lock in the top None (1), a write lock in the bottom None (2), and
+a read lock in the top Some (3).
+The read lock in (1) drops before doing any locking operations in either option of the next branch,
+and therefore has no chance to deadlock.
+The read lock in (3) also does no locking operations before dropping, so has no chance to deadlock.
+The write lock in (2) can't deadlock with the GSS write lock, since we already proved GSS never
+deadlocks. The only remaining operation is then dropping (2).
+Therefore, SDB can never deadlock.
+*/
+
 async fn handle_handshake<const REGISTRATION_PHASE: bool>(
     stream: TcpStream,
     acceptor: TlsAcceptor,