This is not the current version of the class.

# Synchronization invariants

### Run queue invariants

• A CPU’s run queue, which is implemented by members in cpustate and proc (cpustate::current_, cpustate::runq_, and proc::runq_links_), is protected by cpustate::runq_lock_. Reading or writing a CPU’s run queue requires that lock.

• cpustate::current_ is read-only, except that cpustate::schedule() can modify it.

• It is OK for a proc to simultaneously be current_ for some CPU, and on the run queue for that same CPU.

### Suspension invariants

• The proc::regs_ and proc::yields_ members are used to store resumption state. At most one of these members can be nonnull at a time.

• If nonnull, then proc::regs_ and proc::yields_ must point into the kernel task stack containing the proc.

• The proc::regs_ member can’t be accessed by kernel code, except:

• A running kernel task may set and modify its own proc::regs_ if interrupts are disabled and remain disabled until the next call to proc::yield_noreturn().

• After proc::init_user() is called, the new proc has a nonnull proc::regs_ pointer. It is safe to access that member and modify its contents, but only up to the point that the new proc is scheduled.

• The proc::resume() function may access and clear proc::regs_.

• The proc::yields_ member can’t be accessed by kernel code, except:

• A running kernel task may set and modify its own proc::yields_ if interrupts are disabled and remain disabled until the next call to proc::yield_noreturn(). (The proc::yield() function does this.)

• The proc::resume() function may access and clear proc::yields_.

• The proc::resume() function can only be called by cpustate::schedule().

• The proc::yield() function must be called with no spinlocks held.

• The proc::yield_noreturn() function must be called with no spinlocks held and with interrupts disabled.

### Scheduling invariants

• The cpustate::schedule() function must be called with no spinlocks held and with interrupts disabled.

• The cpustate::schedule() function must be called from the current CPU’s CPU stack. (The proc::yield_noreturn() function switches to that stack.)

• A task (that is, a proc) can run on at most one CPU at a time.

Note that for user threads, the “task” encompasses both privileged and unprivileged modes of execution: it is illegal for CPU 0 to execute a particular thread in unprivileged mode while CPU 1 executes on the corresponding kernel task stack in privileged mode. This is because the unprivileged code could trap at any time, which would cause two CPUs to simultaneously execute the same kernel task.

### Process state invariants

• The proc::state_ member may be read without locking.

• Modifications to proc::state_ may require synchronization. You must design a synchronization plan.

• Example plan 1: “proc::state_ may be modified only by the corresponding kernel task, except that blocked processes may be set to runnable by a wait queue wakeup operation.” (Our solutions use this plan.)

• Example plan 2: “proc::state_ may be modified only by atomic compare-and-swap operations.”

• Example plan 3: “proc::state_ may be modified only when proc::state_lock_ is held.”

• Most wait queue implementations transition proc::state_ between blocked and runnable. If you introduce new states, you will need to reason about interactions between those states and wait queue transitions: you don’t want a state to get lost because of a concurrent wakeup.

### Process table invariants

• Read or write access to the process table ptable requires the ptable_lock spinlock.

### Page table invariants

• You may free a process’s page table pages only if (1) the process is not present in ptable, or (2) the process’s page table lock is locked for writing (forcing proc::lock_pagetable_read() to block).

Note that in our handout code, proc::lock_pagetable_read() does nothing. We provide it as a hook for you to complete, in case you want to implement finer-grained page table management.

### 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 state_, 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.

• The bcentry::state_ and bcentry::ref_ members are protected by the entry’s bcentry::lock_.

• Exception: The bcentry::empty() function, which tests whether state_ == state_empty, may be called without locking the bcentry.
• Allocating an entry requires locking the global buffer cache lock, bufcache::lock_, as well as locking the entry’s own lock_. Specifically, changing an empty entry’s state_ to state_allocated and updating its bn_ requires both bufcache::lock_ and the entry’s bcentry::lock_.

• Loaded entries have read-only bcentry::bn_ and bcentry::buf_ members. If an entry is referenced, its bn_ and buf_ can be read without locking.

• Once an entry has been allocated, its bn_ does not change.

• Once an entry is loaded, its buf_ does not change.

• All nonempty entries have distinct bn_s.

• All loaded entries have distinct, nonnull buf_s, because each block is cached in different memory.

• Allocating or freeing an entry may change its bn_ and buf_. These operations require the entry’s lock_, and require that ref_ == 0.

• bufcache::lock_ precedes all entries’ bcentry::lock_s in the lock ordering. For example, the bufcache::get_disk_entry function initially acquires the bufcache::lock_, then acquires an entry’s bcentry::lock_ and releases the global bufcache::lock_.

• The bufcache::get_disk_entry function, which is the only way to obtain a new entry reference, yields until the relevant entry is fully loaded. Thus, if a kernel task holds a reference, that entry has buf_ != nullptr and state_ == state_clean. (When you add write support, you’ll most likely change this invariant.)