Application: Scheduling Processes with RBMap
In CFS (Completely Fair Scheduler), Linux uses a red-black tree to manage processes based on their virtual runtime. Each process is represented as a node in the tree, and the scheduler can efficiently find the process with the smallest virtual runtime.
structure Proc where
pid : Nat
vruntime : Nat := 0
workLeft : Nat
weight : Nat := 1 -- priority weight
deriving Repr, Inhabited
/--
Order processes primarily by virtual runtime.
Use PID as a tie-breaker.
-/
instance : Ord Proc where
compare p1 p2 :=
match compare p1.vruntime p2.vruntime with
| .eq => compare p1.pid p2.pid
| ord => ord
/- A scheduler state: a set of processes
ordered by vruntime -/
abbrev Scheduler := RBMap Proc Unit compare
namespace Scheduler
def empty : Scheduler := RBMap.empty
/-- Create a new process with a unique PID based
on current scheduler state -/
def createProc (s : Scheduler) (workLeft : Nat)
(weight : Nat := 1) : Proc :=
if s.isEmpty then
{ pid := 1, vruntime := 0, workLeft, weight }
else
let maxPid := (s.toList.map (λ (p, _) =>
p.pid)).foldl max 0
{ pid := maxPid + 1, vruntime := 0, workLeft, weight }
/-- Add a process to the scheduler -/
def add (s : Scheduler) (p : Proc) : Scheduler :=
s.insert p ()
/-- Measure for termination: total remaining
work across all processes -/
def totalWork (s : Scheduler) : Nat :=
s.toList.foldl (init := 0)
(fun acc (p, _) => acc + p.workLeft)
/-- Simulate the actual work of a process -/
def doWork (pid : Nat) : IO Unit := do
IO.println s!" [executing PID {pid} ...]"
IO.sleep 10 -- Simulate a brief period of execution
/-- Run the next process for a time quantum (pure logic) -/
def step (s : Scheduler) (quantum : Nat := 10)
: Option (Proc × Scheduler) := do
-- Pick the process with the smallest vruntime
let (p, _) ← s.min
let s' : Scheduler := s.erase p
let runTime := min p.workLeft quantum
let vruntimeDelta := (runTime * 10) / p.weight
let newProc := { p with
workLeft := p.workLeft - runTime,
vruntime := p.vruntime + vruntimeDelta
}
-- If it still has work, put it back in the tree
if newProc.workLeft > 0 then
some (p, Scheduler.add s' newProc)
else
some (p, s')
-- Dynamic simulation loop
partial def simulate (s : Scheduler) : IO Unit := do
if s.isEmpty then
IO.println "\nAll processes finished."
else
match _h_step : s.step 10 with
| some (p, s') =>
doWork p.pid
let log := s!"Finished quantum for PID {p.pid} " ++
s!"(vruntime: {p.vruntime}, " ++
s!"remaining: {p.workLeft})"
IO.println log
s'.simulate
| none => return ()
-- termination_by s.totalWork
-- decreasing_by sorry
end Scheduler
def egRunSchedule : IO Unit := do
let mut s := Scheduler.empty
s := s.add (s.createProc 30 1)
s := s.add (s.createProc 40 2)
s := s.add (s.createProc 20 1)
IO.println "Starting CFS Simulation..."
s.simulate
#eval! egRunSchedule