inductive System.TimeManager.HandleState : Type

State of a timeout handle.

• active : Nat → HandleState
• paused : HandleState
• canceled : HandleState

def System.TimeManager.instBEqHandleState.beq : HandleState → HandleState → Bool

Equations

• System.TimeManager.instBEqHandleState.beq (System.TimeManager.HandleState.active a) (System.TimeManager.HandleState.active b) = (a == b)
• System.TimeManager.instBEqHandleState.beq System.TimeManager.HandleState.paused System.TimeManager.HandleState.paused = true
• System.TimeManager.instBEqHandleState.beq System.TimeManager.HandleState.canceled System.TimeManager.HandleState.canceled = true
• System.TimeManager.instBEqHandleState.beq x✝¹ x✝ = false

@[implicit_reducible]

instance System.TimeManager.instBEqHandleState : BEq HandleState

Equations

• System.TimeManager.instBEqHandleState = { beq := System.TimeManager.instBEqHandleState.beq }

def System.TimeManager.instReprHandleState.repr : HandleState → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance System.TimeManager.instReprHandleState : Repr HandleState

Equations

• System.TimeManager.instReprHandleState = { reprPrec := System.TimeManager.instReprHandleState.repr }

structure System.TimeManager.Handle : Type

A timeout handle for a single connection. $$\text{Handle} = \text{IO.Ref}(\text{HandleState})$$

• state : IO.Ref HandleState
• onTimeout : IO Unit

structure System.TimeManager.Manager : Type

The timeout manager. Periodically checks all registered handles. $$\text{Manager} = \{ \text{timeout} : \mathbb{N},\; \text{handles} : \text{IO.Ref}(\text{Array}(\text{Handle})) \}$$

• timeoutUs : Nat

  Timeout duration in microseconds.

• handles : IO.Ref (Array Handle)

  All registered handles.

• token : Std.CancellationToken

  Cancellation token for stopping the background sweep.

def System.TimeManager.Manager.new (timeoutUs : Nat := 30000000) : IO Manager

Initialize a new timeout manager with the given timeout (microseconds). Starts a background sweep task on a dedicated OS thread. $$\text{initialize} : \mathbb{N} \to \text{IO}(\text{Manager})$$

Equations

• One or more equations did not get rendered due to their size.

def System.TimeManager.Manager.register (mgr : Manager) (onTimeout : IO Unit) : IO Handle

Register a new connection with the manager. Returns a handle for managing its timeout. $$\text{register} : \text{Manager} \to \text{IO}(\text{Unit}) \to \text{IO}(\text{Handle})$$

Equations

• One or more equations did not get rendered due to their size.

def System.TimeManager.Manager.stop (mgr : Manager) : IO Unit

Stop the manager's background sweep. The background task will exit after the current sleep interval completes.

Equations

• mgr.stop = liftM mgr.token.cancel

def System.TimeManager.Handle.tickle (h : Handle) (mgr : Manager) : IO Unit

Reset the timeout for this handle (called on activity). $$\text{tickle} : \text{Handle} \to \text{Manager} \to \text{IO}(\text{Unit})$$

Equations

• h.tickle mgr = do let now ← liftM IO.monoNanosNow have deadline : Nat := now + mgr.timeoutUs * 1000 ST.Ref.set h.state (System.TimeManager.HandleState.active deadline)

def System.TimeManager.Handle.cancel (h : Handle) : IO Unit

Cancel this handle's timeout. It will never fire. $$\text{cancel} : \text{Handle} \to \text{IO}(\text{Unit})$$

Equations

• h.cancel = ST.Ref.set h.state System.TimeManager.HandleState.canceled

def System.TimeManager.Handle.pause (h : Handle) : IO Unit

Pause the timeout. The handle won't expire until resumed. $$\text{pause} : \text{Handle} \to \text{IO}(\text{Unit})$$

Equations

• h.pause = ST.Ref.set h.state System.TimeManager.HandleState.paused

def System.TimeManager.Handle.resume (h : Handle) (mgr : Manager) : IO Unit

Resume a paused handle with a fresh deadline. $$\text{resume} : \text{Handle} \to \text{Manager} \to \text{IO}(\text{Unit})$$

Equations

• h.resume mgr = do let now ← liftM IO.monoNanosNow have deadline : Nat := now + mgr.timeoutUs * 1000 ST.Ref.set h.state (System.TimeManager.HandleState.active deadline)