Process Interruption and Idle Sleep
Lean 4 provides several mechanisms to manage concurrent tasks and handle interruptions. This section explores how to implement interruptible sleeps and "idle" states that wait for external signals. Check out how to put a Process to sleep at Putting a Process to Sleep.
Interruptible Sleep (The "Shift" Pattern)
A common requirement is to put a thread to sleep for a duration, but allow it to be "woken up" or interrupted before the time expires. In Lean, this can be achieved using IO.Promise, see reference. IO.Promise acts as a synchronization primitive that allows one thread to wait for a value that is provided by another thread at a later time. In this context, it serves as a "signal" or a "mailbox" where the sleeping thread waits for the promise to be fulfilled, effectively allowing an external trigger to interrupt the wait.
Using an Extra Task (Timeout Task)
This method involves spawning a separate task that resolves a promise after a delay. The main worker waits on that same promise.
def interruptibleWorker (p : IO.Promise Bool)
: IO Unit := do
IO.println "Worker: starting sleep (10s timeout)..."
let timeoutTask ← IO.asTask do
IO.sleep 10000
-- Resolve with 'false' to indicate timeout
p.resolve false
-- Wait for the promise to be resolved
-- (either by timeout or interrupt)
let interrupted ← IO.wait p.result!
-- CRITICAL: Cancel the timeout task
-- so the process can exit immediately
IO.cancel timeoutTask
if interrupted then
IO.println "Worker: interrupted early!"
else
IO.println "Worker: finished naturally (timeout)."
Using IO.waitAny (Without an Extra Task for Logic)
If you already have multiple tasks running and you want to wait for the first one to complete (or a specific "interrupt" task), you can use IO.waitAny.
def waitFirst (t1 t2 : Task α) : IO α := do
IO.waitAny [t1, t2]
You can also use IO.waitAny to implement a timeout mechanism by racing a computation task against a timer task.
/-- Waits for a task to complete or
returns a default value after a delay. -/
def waitWithTimeout {α : Type} (action : Task α)
(timeoutMs : UInt32) (default : α) : IO α := do
let timer ← BaseIO.asTask (do
IO.sleep timeoutMs
pure default
)
let finished ← IO.waitAny [action, timer]
return finished
Application: Interrupting Idle Sleep (OS-like Sleep)
An "idle sleep" is a state where a process does nothing and consumes minimal resources until it is explicitly woken up by an external event (like a signal or a message).
In Lean, you can implement this by waiting on a promise that has no timeout task associated with it.
def idleProcess (wakeUpSignal : IO.Promise Unit)
: IO Unit := do
IO.println "Process entering idle state..."
-- This will block indefinitely until
-- wakeUpSignal.resolve () is called
let _ ← IO.wait wakeUpSignal.result!
IO.println "Process woken up! Resuming execution..."
def runSystem : IO Unit := do
let signal ← IO.Promise.new
let procTask ← IO.asTask (idleProcess signal)
IO.println "System running... doing other work."
IO.sleep 3000
IO.println "Main: Triggering wake-up signal."
signal.resolve ()
let _ ← IO.wait procTask
IO.println "System shutdown."
In this pattern, the "sleep" is truly idle; there is no timer running. The process simply yields until the promise is resolved by another part of the system.