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 called entries. The bufcache has a lock, lock_. Each entry has type bcentry, and contains a state estate_, a lock lock_, a disk block number bn_, a reference count ref_, 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.