Synchronization invariants

This page lists synchronization invariants that hold in Chickadee. See also spinlocks.

Run queue invariants

Suspension invariants

Scheduling invariants

Process state invariants

Process table invariants

Page table invariants

Buffer cache invariants (Pset 4)

The buffer cache, bufcache, comprises a set of slots. The bufcache has a lock, lock_. Each slot has type bcslot, and contains a state state_, a lock lock_, a disk block number bn_, a reference count ref_, a write owner write_owner_ (initially nullptr), and a pointer to the cached data buf_. These data structures have nontrivial synchronization invariants because disks are slow, making fine-grained synchronization important for performance. As always, you can change these invariants, but understand the current invariants first.