Module degradation 

Degrade truthfully: which resource is the bottleneck, the readings that show it, and what the person can do about it. Readings are sampled by the caller; this module only decides. The one state that stops the city taking on new work is a disk close to full, and the refusal carries that Degradation::DiskLow so the door can say how much to free. The part crates/kernel/spec/Degradation.lean specifies this module.

Structs

ResourceReadings

One sample of the resources the harness depends on.

VolumeSpace

The city’s volume: free space and capacity, read together.

Enums

Degradation

A resource that is the bottleneck, carrying the readings that decided it.

Recovery

What the person can do to end a degradation.

Constants

CPU_SATURATED_DELAY

One 60 Hz frame: the scheduling delay a person starts to see.

DISK_SLOW_FACTOR

How many commit floors the durable watermark may lag before the disk counts as slow. Relative, so a spinning disk whose fsync is simply slow is not reported as degraded.

DISK_SLOW_MIN

The lag below which the disk never counts as slow, so a fast device’s jitter of a few commit floors does not flap the state.

FREE_SPACE_FLOOR_DIVISOR

The free-space floor is this fraction of the volume, before clamping.

FREE_SPACE_FLOOR_MAX

A large volume does not hold back tens of gigabytes as its floor.

FREE_SPACE_FLOOR_MIN

Room for the next snapshot and git’s objects even on a small volume.

Functions

admit_work

Whether the city takes on new work. A volume below its free-space floor refuses with the Degradation::DiskLow it shows; every other degradation admits, because it only slows work down.

assess

Every degradation the readings show, in declaration order, without allocating.

free_space_floor

The free-space floor a volume of volume_bytes derives.