Skip to content

DEBT-3 census bound: two blocked-state publication shapes neither census sees (struct-literal construction, ThreadState import alias) #650

Description

@ryanbreen

Summary

The two blocked-state censuses added by PR #648 (tests/teardown_structure.rs) see the class of
publications through two complementary shapes. Two further shapes fall outside both. Neither
exists on the tree today, so this is a bound on the guarantee, not a live defect — filed so the
"the census sees the class" claim is written down with its edges, rather than being read as
unqualified by a later phase.

Raised as note F3 in the #580/DEBT-3 review of fix/580-blocking-inventory, and named as a
disclosed blind spot in the T3-G green-gate exit assessment (§3, item 5). E3 filed it rather than
fixing it because closing either shape changes what the anchor tables mean, and both are best done
with the P9 admission-interlock work that will touch these publications anyway.

Shape 1 — construction already blocked

Thread { state: ThreadState::Blocked, .. }

Census A (blocked_state_publication_offsets) requires an = immediately before the
ThreadState::Blocked path, which is what excludes comparisons and matches! arms by
construction. A struct-literal field is state: ThreadState::Blocked — a :, not an = — so the
publication is invisible to it. Census B (opaque_thread_state_store_offsets) requires a .state =
field store, so it does not see the literal either.

All eleven state: struct-literal fields on the tree today are Ready or Running
(kernel/src/task/thread.rs ×8, kernel/src/task/strand_oracle.rs ×1,
kernel/src/test_framework/registry.rs ×2). A thread constructed already-blocked would
be a new publication site that neither census reports.

Shape 2 — import alias

use crate::task::thread::ThreadState as TS;
// ...
thread.state = TS::Blocked;

Census A's needle is the literal ThreadState::Blocked, and path_expression_start walks back over
the qualifying segments of that spelling — an alias renames the type, so the needle never matches.
Census B excludes any right-hand side containing ::, which TS::Blocked does. No alias of
ThreadState exists in kernel/src today.

Already knowingly excluded (context, not part of this issue)

The censuses deliberately exclude call arguments, so
core::mem::replace(&mut thread.state, ThreadState::Blocked) also escapes. That exclusion is what
keeps comparisons and matches! arms out of the census; it was a stated design choice, whereas the
two shapes above were simply not considered.

What a fix would look like

Both are addressable as shapes, not name lists, in the same spirit as the existing censuses:

  1. A third census over struct-literal state: fields whose value is a ThreadState::Blocked* path,
    anchored the same way — today's rows are all Ready/Running, so it starts non-empty and a
    blocked construction arrives as a new row.
  2. Either resolve use ... as aliases of ThreadState in the source under census and add the alias
    spelling to the needle set, or census the aliases themselves and require the set to be empty
    (the tree has none, so an alias arriving is the deliberate re-anchor).

Both change what the anchor tables mean, so they want to land with a deliberate re-anchor rather
than being bolted onto a detector-repair PR.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions