V4.1 capacity measurement: startup receipt, Engram residency, probe, staircase, production gate

dag/extdeps/linux/cgroup_v2_memory.dag

@@ -1,12 +1,15 @@
 module extdeps.linux.cgroup_v2_memory
 
+import v2.std.algebra { filter }
+import v2.std.collection { list_at_optional }
 import std.algebra { trim }
 import std.checked_arithmetic { nat_magnitude }
 import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef }
 import std.decl_ref { DeclarationRef, WholeDeclaration }
 import extdeps.uri { Https, Uri }
 import std.measure { ByteSize, byte_size, byte_size_count }
 import std.types { Int, NonEmptyStr, String, List }
+import std.nat { Nat }
 import v2.std.optional { Present, Absent }
 
 data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
@@ -192,3 +195,68 @@ fn cgroup_v2_bounding_dirs(mount_point: NonEmptyStr, relative_path: NonEmptyStr)
       CgroupBoundingDirsFold { prefix: next, dirs: acc.dirs |> list_push(next as NonEmptyStr) }
     }).dirs
 }
+
+// ── memory.stat: THE FIVE KEYS A RESIDENCY READING NEEDS ───────────────────────────────────────
+//
+// cgroup-v2 ("memory.stat") documents the file as flat "key value" lines. Its keys have two
+// different kinds. anon, file and file_mapped are Instantaneous byte counts. workingset_refault_file
+// and pgmajfault are CumulativeCounter event counts, so only a before/after pair of them measures an
+// interval. The kinds are named per field here because this one file mixes them; that is also why
+// memory.stat is not a CgroupMemoryInterfaceFile variant with a single kind.
+type CgroupMemoryStat {
+  anon: ByteSize
+  file: ByteSize
+  file_mapped: ByteSize
+  workingset_refault_file: Nat
+  pgmajfault: Nat
+}
+
+type CgroupMemoryStatReading
+  = CgroupMemoryStatRead { stat: CgroupMemoryStat }
+  | CgroupMemoryStatIncomplete { missing: List<String> }
+
+fn cgroup_memory_stat_value(body: String, key: String) -> Nat? {
+  list_at_optional(xs: flat_map(split(s: body, delimiter: "\n"), line => {
+    let words = filter(split(s: trim(s: line), delimiter: " "), w => w != "")
+    match list_at_optional(xs: words, index: 0) {
+      Absent => [] as List<Nat>
+      Present { value: k } =>
+        if k != key { [] as List<Nat> } else {
+          match list_at_optional(xs: words, index: 1) {
+            Absent => [] as List<Nat>
+            Present { value: v } => match parse_int(s: v) {
+              Absent => [] as List<Nat>
+              Present { value: n } => if n < 0 { [] as List<Nat> } else { [nat_magnitude(a: n)] }
+            }
+          }
+        }
+    }
+  }), index: 0)
+}
+
+fn parse_cgroup_memory_stat(body: String) -> CgroupMemoryStatReading {
+  let keys = ["anon", "file", "file_mapped", "workingset_refault_file", "pgmajfault"]
+  let missing = filter(keys, k => match cgroup_memory_stat_value(body: body, key: k) { Present { value: _ } => false  Absent => true })
+  match cgroup_memory_stat_value(body: body, key: "anon") {
+    Absent => CgroupMemoryStatIncomplete { missing: missing }
+    Present { value: anon } => match cgroup_memory_stat_value(body: body, key: "file") {
+      Absent => CgroupMemoryStatIncomplete { missing: missing }
+      Present { value: file } => match cgroup_memory_stat_value(body: body, key: "file_mapped") {
+        Absent => CgroupMemoryStatIncomplete { missing: missing }
+        Present { value: mapped } => match cgroup_memory_stat_value(body: body, key: "workingset_refault_file") {
+          Absent => CgroupMemoryStatIncomplete { missing: missing }
+          Present { value: refault } => match cgroup_memory_stat_value(body: body, key: "pgmajfault") {
+            Absent => CgroupMemoryStatIncomplete { missing: missing }
+            Present { value: majfault } => CgroupMemoryStatRead { stat: CgroupMemoryStat {
+              anon: byte_size(count: anon),
+              file: byte_size(count: file),
+              file_mapped: byte_size(count: mapped),
+              workingset_refault_file: refault,
+              pgmajfault: majfault,
+            } }
+          }
+        }
+      }
+    }
+  }
+}

dag/extdeps/linux/diskstats.dag

@@ -0,0 +1,144 @@
+module extdeps.linux.diskstats
+
+import v2.std.algebra { filter }
+import v2.std.collection { list_at_optional }
+import std.types { Bool, List, NonEmptyStr, String }
+import std.algebra { trim }
+import std.nat { Nat }
+import std.checked_arithmetic { nat_magnitude }
+import std.measure { ByteSize, byte_size, byte_size_count, Microsecond, microsecond, Millisecond, millisecond, millisecond_count }
+import std.decl_ref { DeclarationRef, WholeDeclaration }
+import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef }
+import extdeps.uri { Https, Uri }
+import extdeps.linux.kernel { LinuxKernelRelease }
+import v2.std.optional { Present, Absent }
+
+// /proc/diskstats, Documentation/admin-guide/iostats.rst. The 14-field-after-name layout this
+// module reads has been stable since 2.6; later kernels APPEND discard (4.18) and flush (5.5)
+// fields, which is why fields are read by position from the front and never by line length.
+data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
+  uri: Uri {
+    scheme: Https
+    locator: "docs.kernel.org/admin-guide/iostats.html"
+  }
+}
+
+data extdeps_model_scope: ExternalModelScope = ExternalModelScope {
+  subject: ExternalSubjectRef {
+    declaration: DeclarationRef {
+      module_path: "extdeps.linux.diskstats",
+      decl_name: "DiskstatsRow",
+      field: WholeDeclaration
+    }
+  },
+  first_citation: extdeps_external_authority_anchor,
+  further_citations: []
+}
+
+data diskstats_positional_layout_since_release: LinuxKernelRelease = "2.6" as LinuxKernelRelease
+
+// iostats.rst: "sectors" in this file are ALWAYS 512 bytes, whatever the device's logical block
+// size is. Multiplying by the device's own sector size would be a wrong reading on 4Kn drives.
+data diskstats_sector_bytes: ByteSize = byte_size(count: 512)
+
+// The read-side fields, by their iostats.rst numbers (field 1 = first after the device name).
+// Write-side fields are not read here because the measurement that consumes this is read-only
+// against the Engram files; a later consumer adds them as fields, not as a second row type.
+type DiskstatsRow {
+  device: NonEmptyStr
+  reads_completed: Nat
+  sectors_read: Nat
+  read_ticks: Millisecond
+  in_flight: Nat
+}
+
+type DiskstatsReading
+  = DiskstatsDeviceRead { row: DiskstatsRow }
+  | DiskstatsDeviceAbsent { device: NonEmptyStr }
+  | DiskstatsUnparseable { device: NonEmptyStr, line: String }
+
+fn diskstats_nat_at(words: List<String>, index: Nat) -> Nat? {
+  match list_at_optional(xs: words, index: index) {
+    Absent => none
+    Present { value: w } => match parse_int(s: w) {
+      Absent => none
+      Present { value: n } => if n < 0 { none } else { Present { value: nat_magnitude(a: n) } }
+    }
+  }
+}
+
+// Word 2 is the device name; words 3, 5, 6 and 11 are iostats fields 1, 3, 4 and 9.
+fn diskstats_row_of_line(device: NonEmptyStr, line: String) -> DiskstatsReading? {
+  let words = filter(split(s: trim(s: line), delimiter: " "), w => w != "")
+  match list_at_optional(xs: words, index: 2) {
+    Absent => none
+    Present { value: name } =>
+      if name != (device as String) {
+        none
+      } else {
+        match diskstats_nat_at(words: words, index: 3) {
+          Absent => Present { value: DiskstatsUnparseable { device: device, line: line } }
+          Present { value: reads } => match diskstats_nat_at(words: words, index: 5) {
+            Absent => Present { value: DiskstatsUnparseable { device: device, line: line } }
+            Present { value: sectors } => match diskstats_nat_at(words: words, index: 6) {
+              Absent => Present { value: DiskstatsUnparseable { device: device, line: line } }
+              Present { value: ticks } => match diskstats_nat_at(words: words, index: 11) {
+                Absent => Present { value: DiskstatsUnparseable { device: device, line: line } }
+                Present { value: inflight } => Present { value: DiskstatsDeviceRead { row: DiskstatsRow {
+                  device: device,
+                  reads_completed: reads,
+                  sectors_read: sectors,
+                  read_ticks: millisecond(count: ticks),
+                  in_flight: inflight,
+                } } }
+              }
+            }
+          }
+        }
+      }
+  }
+}
+
+fn parse_diskstats(body: String, device: NonEmptyStr) -> DiskstatsReading {
+  match list_at_optional(xs: flat_map(split(s: body, delimiter: "\n"), l => match diskstats_row_of_line(device: device, line: l) {
+    Present { value: r } => [r]
+    Absent => [] as List<DiskstatsReading>
+  }), index: 0) {
+    Present { value: r } => r
+    Absent => DiskstatsDeviceAbsent { device: device }
+  }
+}
+
+// A READ INTERVAL IS A DELTA OF TWO CUMULATIVE ROWS. iostats.rst warns the counters may wrap; a
+// field that went backwards is a wrap or a device re-registration, and the pair measures nothing.
+// The mean await is the kernel's own definition (read ticks spent per completed read), floored to
+// whole microseconds; with no completed reads there is no await, which is a distinct arm from zero.
+type DiskReadInterval
+  = DiskReadMeasured { read_bytes: ByteSize, reads: Nat, mean_read_await: Microsecond? }
+  | DiskReadUnmeasurable { cause: NonEmptyStr }
+
+fn disk_read_interval(before: DiskstatsReading, after: DiskstatsReading) -> DiskReadInterval {
+  match before {
+    DiskstatsDeviceAbsent { device: d } => DiskReadUnmeasurable { cause: "the device is absent from the before reading" as NonEmptyStr }
+    DiskstatsUnparseable { device: _, line: _ } => DiskReadUnmeasurable { cause: "the before line is unparseable" as NonEmptyStr }
+    DiskstatsDeviceRead { row: b } => match after {
+      DiskstatsDeviceAbsent { device: d } => DiskReadUnmeasurable { cause: "the device is absent from the after reading" as NonEmptyStr }
+      DiskstatsUnparseable { device: _, line: _ } => DiskReadUnmeasurable { cause: "the after line is unparseable" as NonEmptyStr }
+      DiskstatsDeviceRead { row: a } =>
+        if b.device != a.device {
+          DiskReadUnmeasurable { cause: "the two readings name different devices" as NonEmptyStr }
+        } else if a.reads_completed < b.reads_completed || a.sectors_read < b.sectors_read
+          || millisecond_count(m: a.read_ticks) < millisecond_count(m: b.read_ticks) {
+          DiskReadUnmeasurable { cause: "a cumulative field went backwards (wrap or re-registration)" as NonEmptyStr }
+        } else {
+          let reads = a.reads_completed - b.reads_completed
+          let ticks = millisecond_count(m: a.read_ticks) - millisecond_count(m: b.read_ticks)
+          DiskReadMeasured {
+            read_bytes: byte_size(count: (a.sectors_read - b.sectors_read) * byte_size_count(b: diskstats_sector_bytes)),
+            reads: reads,
+            mean_read_await: if reads == 0 { none } else { Present { value: microsecond(count: (ticks * 1000) / reads) } },
+          }
+        }
+    }
+  }
+}

dag/extdeps/linux/mincore.dag

@@ -0,0 +1,66 @@
+module extdeps.linux.mincore
+
+import std.types { Bool, NonEmptyStr, String }
+import std.nat { Nat }
+import std.measure { ByteSize, byte_size, byte_size_count }
+import std.decl_ref { DeclarationRef, WholeDeclaration }
+import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef }
+import extdeps.uri { Https, Uri }
+
+// mincore(2): "determine whether pages are resident in memory". For a mapping of a file it returns
+// one byte per page of the range, whose least significant bit is set when the page is resident in
+// the page cache. It answers RESIDENCY at the instant of the call, and nothing about which pages any
+// process touched: a page read by readahead, by a checksum pass, or by another process is resident
+// exactly like a page a lookup fetched. That is the whole reason this reading is never a touch count.
+data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
+  uri: Uri {
+    scheme: Https
+    locator: "man7.org/linux/man-pages/man2/mincore.2.html"
+  }
+}
+
+data extdeps_model_scope: ExternalModelScope = ExternalModelScope {
+  subject: ExternalSubjectRef {
+    declaration: DeclarationRef {
+      module_path: "extdeps.linux.mincore",
+      decl_name: "MincoreFileResidency",
+      field: WholeDeclaration
+    }
+  },
+  first_citation: extdeps_external_authority_anchor,
+  further_citations: []
+}
+
+// The vector covers ceil(length / page_size) pages; the resident count is the number of bytes in it
+// with bit 0 set. Resident BYTES are pages times page size, so the file's partial last page counts
+// whole -- that is what the page cache holds, and it can exceed the file length by less than a page.
+type MincoreFileResidency sole_constructor {
+  file: NonEmptyStr
+  file_bytes: ByteSize
+  page_bytes: ByteSize
+  resident_pages: Nat
+}
+
+type MincoreResidencyAdmission
+  = MincoreResidencyAdmitted { residency: MincoreFileResidency }
+  | MincoreResidencyRefused { file: NonEmptyStr, cause: NonEmptyStr }
+
+fn mincore_page_count(file_bytes: ByteSize, page_bytes: ByteSize) -> Nat {
+  (byte_size_count(b: file_bytes) + byte_size_count(b: page_bytes) - 1) / byte_size_count(b: page_bytes)
+}
+
+fn mincore_file_residency(file: NonEmptyStr, file_bytes: ByteSize, page_bytes: ByteSize, resident_pages: Nat) -> MincoreResidencyAdmission {
+  if byte_size_count(b: page_bytes) == 0 {
+    MincoreResidencyRefused { file: file, cause: "a zero page size is not a page size" as NonEmptyStr }
+  } else if resident_pages > mincore_page_count(file_bytes: file_bytes, page_bytes: page_bytes) {
+    MincoreResidencyRefused { file: file, cause: "more resident pages than the file has pages; the vector covered a different range" as NonEmptyStr }
+  } else {
+    MincoreResidencyAdmitted { residency: MincoreFileResidency {
+      file: file, file_bytes: file_bytes, page_bytes: page_bytes, resident_pages: resident_pages,
+    } }
+  }
+}
+
+fn mincore_resident_bytes(r: MincoreFileResidency) -> ByteSize {
+  byte_size(count: r.resident_pages * byte_size_count(b: r.page_bytes))
+}