OSTEP Chapter 8. Scheduling: The Multi-Level Feedback Queue

Multi-Level Feedback Queue (MLFQ) is a CPU scheduling algorithm that balances turnaround time and response time without prior knowledge of job characteristics. It uses multiple priority queues where jobs start at the highest priority and move down based on CPU usage, with periodic priority boosts to prevent starvation. The algorithm cleverly approximates Shortest Job First while remaining fair to long-running tasks. Originally invented by Corbato in 1962, MLFQ became the foundation for schedulers in BSD UNIX, Solaris, and Windows NT. The post includes a TLA+ formal model for visualizing the algorithm's behavior.