English | 中文

NEU Operating Systems Lab

Three OS experiments from Northeastern University (NEU) Software College, 2025–2026. Each lab goes beyond the required specification: Lab 1 adds a TLA+ model-checked formalization and a Go implementation; Lab 2 adds CFS and MLFQ schedulers with a quantitative comparison; Lab 3 adds an OPT simulator, a Belady anomaly probability heatmap, and a journaling file system.

Contents

• Lab 1 — Process Synchronization
• Lab 2 — CPU Scheduling
• Lab 3 — Memory Management
• Build
• Dependencies
• Visualization
• Formal Verification

---

Lab 1 — Process Synchronization

Required

Program	Algorithm	Lang
c/pc.c	Producer–Consumer with bounded buffer (3 semaphores)	C11 + pthreads
c/rw.c	Readers–Writers (reader-preference, counting semaphore)	C11 + pthreads
c/dining.c	Dining Philosophers (resource hierarchy solution)	C11 + pthreads

c/ring.h implements the shared circular buffer used by pc.c. The three-semaphore design (mutex, empty, full) enforces the invariant that mutex is acquired only after empty/full; reversing the order produces deadlock, which pc.c demonstrates through an optional --no-mutex flag.

Extended

go/pc.go reimplements the producer–consumer using Go channels and sync.WaitGroup. The channel is unbuffered by default; buffer size is a command-line flag. Requires Go >= 1.22 (math/rand/v2).

The tla/ directory contains a TLA+ specification of the blocking queue and its model-checked verification — see Formal Verification.

cd lab1 && make        # builds dining, pc, rw
cd lab1 && make run    # runs all three sequentially

---

Lab 2 — CPU Scheduling

Required

Program	Algorithm	Lang
c/priority.c	Priority scheduling with aging (priority decrements each time slice)	C11
c/rr.c	Round-Robin with configurable time quantum	C11

Both programs take process parameters from stdin and print per-time-slice PCB state tables to stdout. Output format matches the textbook examples exactly.

Extended

cpp/mlfq.cpp implements a 3-level Multi-Level Feedback Queue: processes demote on time-slice exhaustion and promote after a configurable starvation threshold. cpp/cfs.cpp models Linux CFS using a red-black tree ordered by virtual runtime (vruntime); weight is derived from niceness following the Linux scheduler table. cpp/compare.cpp runs all four schedulers on the same process set and emits JSON for viz/gantt.py to render.

cd lab2 && make           # builds priority, rr, cfs, mlfq, compare
cd lab2 && make run       # runs priority and rr with sample input

---

Lab 3 — Memory Management

Required

Program	Algorithm	Lang
c/addr.c	Logical-to-physical address translation (segmented paging)	C11
c/fifo.c	FIFO page replacement (step-by-step with dirty-bit tracking)	C11
c/lru.c	LRU page replacement (doubly linked list, O(1) hit)	C11

c/vmm.c runs FIFO, LRU, and OPT on the 12-instruction reference string from the textbook (0 1 2 3 0 6 4 5 1 2 4 6), reports fault counts for each algorithm, and sweeps frame counts from 1 to 7 to detect Belady anomalies in FIFO. On the standard string: FIFO=7 faults, LRU=6, OPT=6.

c/fs.c simulates a FAT-style flat file system in a 512-byte in-memory image with 16-byte blocks. Supported operations: create, write, read, delete, ls, stat.

Extended

c/fs_ext.c extends the flat file system with tree-structured directories (inode-based, unlimited depth) and write-ahead journaling. A crash between journal_write and journal_commit leaves the journal intact; the next mount replays it. The persistent image is written to fs.img; the journal lives in fs.journal.

go/fs.go reimplements the file system as a Go package with an HTTP-style command interface. It adds a cp command and persists state to fs_go.bin.

cd lab3 && make           # builds addr, fifo, lru, vmm, fs, fs_ext
cd lab3 && make run       # runs the textbook examples
cd lab3/go && go run fs.go

fs.img, fs.journal, and fs_go.bin are runtime-generated and excluded from the repository. Do not create them manually.

---

Build

Each lab has a standalone Makefile.

cd lab1 && make      # CC=gcc, CFLAGS=-std=c11 -Wall -Wextra -pthread
cd lab2 && make      # CC=gcc (C), CXX=g++ -std=c++17 (C++)
cd lab3 && make      # CC=gcc, CFLAGS=-std=c11 -Wall -Wextra

make clean removes compiled binaries and runtime-generated files (fs.img, fs.journal, go/fs_go.bin). It does not touch source files or visualization output.

---

Dependencies

Tool	Version	Used by
GCC	>= 9 (C11)	lab1, lab3 C programs
G++	>= 9 (C++17)	lab2 C++ programs
Go	>= 1.22	lab1/go, lab3/go
Python 3	>= 3.9	all viz/ scripts
matplotlib, numpy	latest	viz/gantt.py, viz/belady_heatmap.py, viz/memviz.py
Java	>= 11	TLA+ model checking
Graphviz (fdp)	any	lab1/tla/render_dot.py
PlantUML	any	.puml flowchart sources

Linux (including WSL2) is the only tested environment. pthread_create behavior on macOS differs in stack size defaults.

---

Visualization

All visualization scripts live in labN/viz/. They require compiled binaries in the same lab directory.

Lab 1 — viz/plot_pc.py forks ./c/pc, captures line-by-line output, and renders a buffer-state heatmap plus a producer/consumer count bar chart.

Lab 2 — viz/gantt.py calls ./cpp/compare (JSON output), then renders two Gantt charts: one comparing priority/RR/MLFQ/CFS side by side, one dedicated to MLFQ queue-level breakdown.

Lab 3 — viz/memviz.py contains a self-contained Python simulation of FIFO, LRU, OPT, and Clock, producing a per-reference-string frame snapshot animation (mem_replace.gif). viz/belady_heatmap.py reads belady.csv (generated by vmm) and plots the Belady anomaly probability matrix across frame counts and sequence perturbation levels.

cd lab2 && python3 viz/gantt.py
cd lab3 && python3 viz/memviz.py
cd lab3 && python3 viz/belady_heatmap.py   # requires belady.csv from vmm

Visualization outputs are not tracked in this repository. Re-generate them by running the scripts after building.

---

Formal Verification

lab1/tla/ contains a TLA+ specification of the blocking queue and its model-checked proofs.

File	Role
BlockingQueue.tla	Core spec: Put/Get actions, FairSpec (WF on Put, SF on Get)
BlockingQueueMC.tla	MC configuration: 3 producers, 4 consumers, 8-slot buffer
BlockingQueueSmall.tla	Reduced configuration: 2 producers, 2 consumers, 2-slot buffer

The spec verifies two invariants: TypeInv (type safety of all variables) and Invariant (no complete deadlock — at least one thread always makes progress). The liveness property FairSpec verifies that under weak fairness on producers and strong fairness on consumers, every Put eventually completes.

states.dot is the raw state graph emitted by TLC. render_dot.py compresses node labels and runs fdp to produce states_clean.dot and states.png. tla2tools.jar is not tracked; obtain it from the TLA+ GitHub releases.

cd lab1/tla
java -cp tla2tools.jar tlc2.TLC BlockingQueueMC

---

License

MIT