Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
34 changes: 34 additions & 0 deletions dag/extdeps/systemd/systemctl.dag
Original file line number Diff line number Diff line change
Expand Up @@ -53,6 +53,15 @@ fn systemctl_enable_argv(unit: NonEmptyStr) -> List<String> {
["systemctl", "enable", unit as String]
}

// START IS NOT RESTART, AND FOR A SLICE THE DIFFERENCE IS DESTRUCTIVE RATHER THAN STYLISTIC. Stopping a
// slice kills every process in it (systemd.slice(5)), so `restart` applied to a compile pool would terminate
// the compilers the pool exists to hold. `start` on an already-active slice is a no-op that re-applies the
// unit's resource directives, which is what a converger wants. The modeled `Start` operation already exists
// on the service surface; this is its argv authority for the shell-body realization edge.
fn systemctl_start_argv(unit: NonEmptyStr) -> List<String> {
["systemctl", "start", unit as String]
}

fn systemctl_restart_argv(unit: NonEmptyStr) -> List<String> {
["systemctl", "restart", unit as String]
}
Expand Down Expand Up @@ -128,6 +137,14 @@ fn systemctl_user_start_argv(unit: NonEmptyStr) -> List<String> {
["systemctl", "--user", "start", unit as String]
}

// LoadState is the only observation that distinguishes an ABSENT unit from a present one, which is why the
// `ShowLoadState` operation on the service surface above is its own operation rather than a
// SystemdUnitProperty arm: that coproduct is numeric cgroup evidence sharing one numeric mock, and a wire
// value of `not-found` is not a magnitude. Cited to systemd.unit(5) LoadState -- `loaded`, `not-found`,
// `bad-setting`, `error`, `masked` -- of which `not-found` is the one this corpus reads positively.
// `systemctl show` exits 0 for a unit the manager has never heard of and prints not-found, so a nonzero exit
// means the MANAGER was unreadable, which is a different refusal from an absent unit and must not be folded
// into it.
fn systemctl_show_load_state_argv(unit: NonEmptyStr) -> List<String> {
["systemctl", "show", unit as String, "--property=LoadState", "--value"]
}
Expand Down Expand Up @@ -302,6 +319,23 @@ service systemd.Systemctl {
}
}

operation ShowLoadState {
input { unit: NonEmptyStr }
output {
value: String from "stdout"
success: Bool from "exit_success"
}
readonly
transport shell { argv: ["systemctl", "show", "{unit}", "--property=LoadState", "--value"] }
exit {
0 => Unit
nonzero => String "systemctl show LoadState failed"
}
mock_response {
0 => { value: "not-found", success: true } "hermetic systemd.Systemctl.ShowLoadState"
}
}

operation ListUnits {
input {
pattern: NonEmptyStr,
Expand Down
179 changes: 179 additions & 0 deletions dag/gunbc/compile_pool_observe.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,179 @@
module gunbc.compile_pool_observe

import std.types { String, NonEmptyStr, Bool }
import std.measure { ByteSize }
import std.disposition { Disposition, SingleAuthority }
import std.algebra { trim }
import extdeps.systemd {
SystemdUnitProperty,
MemoryMax,
MemoryHigh,
MemoryCurrent,
SystemdCgroupMemoryLimit,
MemoryLimitBytes,
MemoryLimitUnbounded,
MemoryLimitAbsent,
parse_systemd_memory_limit_show,
systemd_unit_load_state_not_found_wire,
}
import gunbc.host_effect { HostEffectTransport }
import gunbc.systemctl_show_read {
SystemdPropertyCapture,
SystemdPropertyCaptured,
SystemdPropertyCaptureRefused,
systemctl_show_property_read,
systemctl_show_load_state_read,
}
import gunbc.build_cache_instance {
CgroupMemoryLimits,
EndpointObservationUnavailableReason,
ReachRefused,
}
import gunbc.host_compile_pool {
CompilePoolObservation,
CompilePoolSliceObserved,
CompilePoolSliceAbsent,
CompilePoolObservationUnavailable,
}

data compile_pool_observe_scope_disposition: Disposition = SingleAuthority

// THE MISSING PRODUCER. gunbc.host_compile_pool declares CompilePoolObservation and gunbc.compile_pool_ensure
// consumes it, and until this module existed every value of that type in the tree was hand-authored inside a
// test -- so the admission that decides whether a host may have its compile-pool slice written was proven over
// fixtures and computed over nothing. That is the same shape gunbc.build_cache_endpoint_observe closed for the
// endpoint observation, and this is the slice half of it.
//
// WHAT IT READS AND IN WHICH ORDER. LoadState first, because it is the only reading that separates an absent
// slice from a present one (extdeps.systemd.systemctl ShowLoadState carries the citation: `systemctl show`
// answers `infinity` for MemoryMax on a unit the manager never heard of, identically to a loaded unit with no
// ceiling). Only under a loaded unit are the three cgroup magnitudes read. A slice that is loaded but reports
// no numeric ceiling is NOT folded into absent and NOT folded into a zero: `infinity` and an unparseable value
// are both refusals carrying what was read, because a pool with no ceiling is precisely the unbounded charge
// the managed slice exists to replace and reporting it as a size would fabricate the thing being checked.
//
// WHAT IT DOES NOT DO: it decides nothing. Whether the observed slice is large enough, correctly named, or
// permitted to be written is gunbc.compile_pool_ensure's and gunbc.host_compile_pool's judgement over this
// value; this module only reports what the host said.

fn compile_pool_reach_refusal(slice_unit: NonEmptyStr, what: String, why: String) -> CompilePoolObservation {
CompilePoolObservationUnavailable {
reason: ReachRefused {
detail: join(
["compile-pool slice ", slice_unit as String, ": ", what, " -- ", why],
"",
) as NonEmptyStr,
},
}
}

fn compile_pool_limit_bytes(lim: SystemdCgroupMemoryLimit) -> ByteSize? {
match lim {
MemoryLimitBytes { bytes: b } => Present { value: b }
MemoryLimitUnbounded => none
MemoryLimitAbsent => none
}
}

fn compile_pool_limit_label(lim: SystemdCgroupMemoryLimit) -> String {
match lim {
MemoryLimitBytes { bytes: _ } => "a byte count"
MemoryLimitUnbounded => "infinity (no ceiling -- an unbounded slice is the charge the managed pool replaces, not a size)"
MemoryLimitAbsent => "empty or unparseable"
}
}

// MemoryCurrent IS READ EVEN THOUGH NO JUDGEMENT USES IT, AND AN UNREADABLE ONE REFUSES. CgroupMemoryLimits
// carries three magnitudes and the two judgements over this observation read only two -- the ensure admission
// compares memory.max and memory.high against the derived size, the readiness check compares memory.max. The
// third is required to CONSTRUCT the record, so this module cannot report an observation without it, and it
// does not invent one: a zero would be a fabricated live charge that reads as an idle pool, which is exactly
// the state an operator would act on. So a slice that is loaded but never started -- systemd answers
// `[not set]` for MemoryCurrent until the cgroup exists -- is reported unavailable with that reading quoted,
// and the next pass observes it after the start. RUNG: mitigatable, and the deficit is a carrier shape rather
// than a read -- a limit PAIR and a live magnitude fused into one record. NEXT-RUNG TRIGGER: CgroupMemoryLimits
// split so observed ceilings can be reported without a current charge, at which point this arm is
// unrepresentable rather than refused.
type CompilePoolLimitRead
= CompilePoolLimitBytes { bytes: ByteSize }
| CompilePoolLimitRefused { observation: CompilePoolObservation }

fn compile_pool_limit_of_capture(
slice_unit: NonEmptyStr,
property_name: String,
capture: SystemdPropertyCapture,
) -> CompilePoolLimitRead {
match capture {
SystemdPropertyCaptureRefused { reason: why } =>
CompilePoolLimitRefused {
observation: compile_pool_reach_refusal(
slice_unit: slice_unit,
what: join(["could not read ", property_name], ""),
why: why,
),
}
SystemdPropertyCaptured { value: raw } => {
let lim = parse_systemd_memory_limit_show(raw: trim(raw))
match compile_pool_limit_bytes(lim: lim) {
Present { value: b } => CompilePoolLimitBytes { bytes: b }
Absent =>
CompilePoolLimitRefused {
observation: compile_pool_reach_refusal(
slice_unit: slice_unit,
what: join([property_name, " is not a ceiling"], ""),
why: compile_pool_limit_label(lim: lim),
),
}
}
}
}
}

fn compile_pool_slice_limits_from_reads(
slice_unit: NonEmptyStr,
max_read: SystemdPropertyCapture,
high_read: SystemdPropertyCapture,
current_read: SystemdPropertyCapture,
) -> CompilePoolObservation {
match compile_pool_limit_of_capture(slice_unit: slice_unit, property_name: "MemoryMax", capture: max_read) {
CompilePoolLimitRefused { observation: o } => o
CompilePoolLimitBytes { bytes: max } =>
match compile_pool_limit_of_capture(slice_unit: slice_unit, property_name: "MemoryHigh", capture: high_read) {
CompilePoolLimitRefused { observation: o } => o
CompilePoolLimitBytes { bytes: high } =>
match compile_pool_limit_of_capture(slice_unit: slice_unit, property_name: "MemoryCurrent", capture: current_read) {
CompilePoolLimitRefused { observation: o } => o
CompilePoolLimitBytes { bytes: current } =>
CompilePoolSliceObserved {
slice_unit: slice_unit,
limits: CgroupMemoryLimits {
memory_max: max,
memory_high: high,
memory_current: current,
},
}
}
}
}
}

fn observe_compile_pool_slice(
transport: HostEffectTransport,
slice_unit: NonEmptyStr,
) -> CompilePoolObservation {
match systemctl_show_load_state_read(transport: transport, unit: slice_unit) {
SystemdPropertyCaptureRefused { reason: why } =>
compile_pool_reach_refusal(slice_unit: slice_unit, what: "could not read LoadState", why: why)
SystemdPropertyCaptured { value: raw } =>
if trim(raw) == (systemd_unit_load_state_not_found_wire as String) {
CompilePoolSliceAbsent { slice_unit: slice_unit }
} else {
compile_pool_slice_limits_from_reads(
slice_unit: slice_unit,
max_read: systemctl_show_property_read(transport: transport, unit: slice_unit, property: MemoryMax),
high_read: systemctl_show_property_read(transport: transport, unit: slice_unit, property: MemoryHigh),
current_read: systemctl_show_property_read(transport: transport, unit: slice_unit, property: MemoryCurrent),
)
}
}
}
1 change: 1 addition & 0 deletions dag/gunbc/host_effect.dag
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,7 @@ type HostEffect =
| OsInstallActuatorToolchainEnsure {}
| EnsureBuildCacheInstance { desired: BuildCacheInstance }
| ProvisionCodexRuntime {}
| EnsureCompilePoolSlice {}
| SetHostnameCas { hostnamectl_path: NonEmptyStr, base: DnsLabel, desired: DnsLabel }
| ReadEffectivePosixPrincipal { read: EffectivePosixPrincipalRead }
| SudoNopasswdExecuteProbe { probe: SudoNopasswdExecuteProbeShape }
Expand Down
Loading
Loading