tsa-typedef-capability linux

tsa-typedef-capability-linux.md

Testing type-carried thread-safety capability requirements against the Linux kernel

Test report for the jn/tsa-typedef-capability branch (32-commit TSA series) built against the Linux kernel's Clang capability analysis (CONFIG_WARN_CONTEXT_ANALYSIS).

What was compared

Kernel	torvalds/linux @ 62cc90241, v7.2.0-rc5
Branch clang	24.0.0git @ a8ce063f39b6 ([TSA][30/N])
Baseline clang	24.0.0git @ 6bb30c03650c — the parent of the entire series
Config	x86_64 defconfig, CONFIG_WERROR=n, CONTEXT_ANALYSIS_TEST=y
Kernel analysis flags	-fexperimental-late-parse-attributes -Wthread-safety -Wthread-safety-pointer -Wthread-safety-beta

Two analysis scopes were built with each compiler (four builds total):

• Realistic — the kernel's shipped scripts/context-analysis-suppression.txt, i.e. only the opted-in subsystems (block/ crypto/ drivers/ata/ kernel/futex/ kernel/kcsan/ mm/kfence/ security/tomoyo/) plus the opt-in headers.
• Tree-wide — CONFIG_WARN_CONTEXT_ANALYSIS_ALL=y, so all of include/linux/* is analyzed in every TU. The kernel documents this as "likely to produce a large number of false positives"; it is used here purely to drive maximum code through the new paths.

Compile-only (make <subdirs>, no vmlinux link), 2965–3000 objects, identical counts under both compilers.

Result summary

	baseline	branch
Realistic config	0 diagnostics	2
Tree-wide	126,703	126,726
Unique diagnostics (tree-wide)	2014	2039
Objects compiled	2965	2965
lib/test_context-analysis.c (kernel's own false-positive test)	0	0

• 24 added diagnostics, 0 lost. Nothing the baseline reported changed or disappeared.
• All 24 are -Wthread-safety-conversion-drop.
• No new -Wthread-safety-analysis, no new -Wthread-safety-attributes, no crashes.

The 24 new findings

Every one has the same root cause: a function carrying a lock-transition annotation is stored into (or passed as) a plain function pointer, which discards the requirement, so the indirect call that actually performs the unlock goes unchecked. All are true positives by construction — the destination type carries no requirement, so the annotation is provably lost.

struct seq_operations — 20 of 24

The canonical seq_file idiom: .start takes a lock and .stop drops it. But

struct seq_operations {
	void * (*start) (struct seq_file *m, loff_t *pos);
	void (*stop) (struct seq_file *m, void *v);
	void * (*next) (struct seq_file *m, void *v, loff_t *pos);
	int (*show) (struct seq_file *m, void *v);
};

has plain function pointers, so the annotations are lost at the initializer and seq_file's own calls from seq_read_iter() are entirely unverified. 15 of the 20 are RCU.

Site	Function	Requirement dropped
crypto/proc.c:90	c_next	requires_shared_capability(&crypto_alg_sem)
crypto/proc.c:91	c_stop	release_shared_capability(&crypto_alg_sem)
drivers/md/md.c:9113	md_seq_stop	release_capability(&all_mddevs_lock)
fs/locks.c:3127	locks_stop	release_capability(&blocked_lock_lock)
kernel/resource.c:156	r_stop	release_capability(resource_lock)
kernel/trace/trace_events.c:2628	p_stop	release_capability(RCU)
kernel/trace/trace_events.c:2635	p_stop	release_capability(RCU)
net/core/net-procfs.c:162	dev_seq_stop	release_capability(RCU)
net/core/net-procfs.c:321	ptype_seq_stop	release_capability(RCU)
net/core/net-procfs.c:389	dev_seq_stop	release_capability(RCU)
net/core/sock.c:4432	proto_seq_stop	release_capability(proto_list_mutex)
net/ipv4/fib_trie.c:2815	fib_trie_seq_stop	release_capability(RCU)
net/ipv4/fib_trie.c:3004	fib_route_seq_stop	release_capability(RCU)
net/ipv4/ipmr.c:3188	ipmr_vif_seq_stop	release_capability(RCU)
net/ipv6/anycast.c:618	ac6_seq_stop	release_capability(RCU)
net/ipv6/ip6_flowlabel.c:874	ip6fl_seq_stop	release_capability(RCU)
net/ipv6/mcast.c:3018	igmp6_mc_seq_stop	release_capability(RCU)
net/ipv6/mcast.c:3146	igmp6_mcf_seq_stop	release_capability(RCU)
net/packet/af_packet.c:4751	packet_seq_stop	release_capability(RCU)
net/sunrpc/cache.c:1447	cache_seq_stop_rcu	release_capability(RCU)

Sample diagnostic:

crypto/proc.c:90:11: warning: 'c_next' drops the
  'requires_shared_capability(&crypto_alg_sem)' requirement when converted to
  'void *(*)(struct seq_file *, void *, loff_t *)'; calls through the result are
  not checked [-Wthread-safety-conversion-drop]
   90 |         .next           = c_next,
      |                           ^
crypto/proc.c:29:2: note: 'requires_shared_capability(&crypto_alg_sem)' requirement declared here
   29 |         __must_hold_shared(&crypto_alg_sem)

Three outliers — distinct "helper invokes callback" shapes

net/sunrpc/svcauth.c:233 — auth_domain_release drops release_capability(&auth_domain_lock). The clearest case for the feature: include/linux/kref.h states the contract in prose but types the parameter bare.

/* ... held.  The @release function will release the lock. */
static inline int kref_put_lock(struct kref *kref,
				void (*release)(struct kref *kref),   /* <-- unannotated */
				spinlock_t *lock)
	__cond_acquires(true, lock)
{
	if (refcount_dec_and_lock(&kref->refcount, lock)) {
		release(kref);

Annotating that one parameter type would check every release callback in the tree.

ipc/msg.c:1332 — freeque drops release_capability(RCU) via free_ipcs(ns, &msg_ids(ns), freeque).

drivers/net/netconsole.c:2371 and :2380 — netconsole_device_unlock drops release_capability(&target_list_lock) into struct console ops.

The drop/add asymmetry is correct on real code

crypto/proc.c is a natural experiment. All three of c_start/c_next/c_stop are annotated and all three lose their annotation at the same initializer, but only two are reported:

• c_start — __acquires_shared(&crypto_alg_sem) — not reported ✓
• c_next — __must_hold_shared(...) — reported
• c_stop — __releases_shared(...) — reported

That matches the documented soundness rule exactly: losing acquire can only cost false positives, never miss a race, so it stays quiet; losing requires/release can make the analysis believe a lock is held when it may not be.

Existing kernel patterns that could have regressed, but didn't

Capability attributes on function-pointer parameters. Commit 35af7eb9002a silently changes what these mean. A tree-wide scan found the kernel uses this pattern nowhere, so the change does not affect it. (drivers/base/power/runtime.c:375 looks like a hit but the attributes there bind to the enclosing __rpm_callback, not to its cb parameter.)

Capability attributes on function-pointer fields. Six exist:

Location	Attribute	Kind
include/linux/blkdev.h:1752,1758,1764,1770	__releases(&bdev->bd_holder_lock)	object-relative
include/linux/libata.h:988	__must_hold(&ap->host->eh_mutex)	object-relative
include/kvm/arm_vgic.h:223	__releases(&irq->irq_lock)	parameter-relative
security/landlock/object.h:26	__releases(object->lock)	parameter-relative
include/linux/soc/mediatek/mtk_wed.h:196	__releases(RCU)	global — foldable

The object/parameter-relative ones cannot be part of a type, so they stay declaration-scoped and keep working, exactly as the release notes claim. Verified with a probe reproducing the libata and mtk_wed shapes: byte-identical diagnostics from both compilers. block/ and drivers/ata/ are opted-in subsystems, so these are actively analyzed in the realistic build too.

Targeted probes

Compiled against real kernel headers with real kernel flags, using tomoyo's global tomoyo_policy_lock. All ten behaved as designed:

Probe	Expected	Result
indirect call with lock held	silent	✓
indirect call without lock	calling function 'cb' requires holding mutex 'tomoyo_policy_lock' exclusively	✓
requirement survives copy into a local	warns at the copy's call	✓
implicit conversion to plain fn ptr	-Wthread-safety-conversion-drop	✓
explicit cast	silent (TSA)	✓
gaining a requirement (plain fn → annotated type)	silent	✓
typedef'd struct field	checked	✓
attribute written directly on a field	checked	✓
object-relative typedef requirement	cannot become part of the type it names because the capability is relative to an object or a parameter; attribute ignored	✓
typedef redefined with differing requirements	union taken; -Wthread-safety-typedef-merge when enabled	✓

-Wno-thread-safety-conversion-drop correctly suppresses only the drop subgroup.

Baseline contrast. On the same probe the baseline emits only 'requires_capability' attribute only applies to functions, variables, and non-static data members [-Wignored-attributes] — i.e. before this series a capability attribute on a typedef was simply discarded and provided no checking at all.

Real multi-TU annotation test

tomoyo_update_policy() takes the global tomoyo_policy_lock and then invokes its check_duplicate callback with it held. Annotating that callback via a typedef:

/* security/tomoyo/common.h */
typedef bool (*tomoyo_check_duplicate_t)(const struct tomoyo_acl_head *,
					 const struct tomoyo_acl_head *)
	__must_hold(&tomoyo_policy_lock);

int tomoyo_update_policy(struct tomoyo_acl_head *new_entry, const int size,
			 struct tomoyo_acl_param *param,
			 tomoyo_check_duplicate_t check_duplicate);

Result across 4 translation units: zero warnings. The guarded call inside tomoyo_update_policy is accepted, and all six real call sites (domain.c:277,420, group.c:91,100,112, common.c:877) that pass plain unannotated functions stay silent — gaining a precondition only over-constrains the caller.

Negative control. Hoisting the callback invocation above the lock acquisition produces, as it should:

security/tomoyo/domain.c:40:6: warning: calling function 'check_duplicate' requires
  holding mutex 'tomoyo_policy_lock' exclusively [-Wthread-safety-analysis]

confirming the check is live rather than vacuously satisfied.

Separately, enabling CONFIG_SECURITY_TOMOYO surfaced 10 more pre-existing conversion-drop findings in security/tomoyo/common.c (tomoyo_write_domain, tomoyo_read_exception, tomoyo_write_manager, … all dropping requires_shared_capability(&tomoyo_ss) into struct tomoyo_io_buffer's plain read/write members). These come from existing kernel annotations, not from the typedef above.

Attempting to fix the 24 findings

Each finding was triaged by asking whether the dropped capability can actually be named in the callback's type. The answer splits sharply:

Shape	Count	Fixable?
free_ipcs callback (ipc/)	1	Yes — capability is a global (RCU)
kref_put_lock release callback	1	No — capability is a parameter (lock), different per call site
struct console device_lock/device_unlock	2	No — capability is per-driver
struct seq_operations .stop/.next	20	No — capability differs per instance

1 of 24 is fixable. The other 23 name a lock that is chosen by the callback's implementation, not by its type, so no single annotation on the shared struct or helper can be correct.

The one that works: ipc/ — net −3 warnings

free_ipcs() does rcu_read_lock(); ipc_lock_object(perm); free(ns, perm);, so RCU is held at the indirect call and all three callbacks (freeque, freeary, do_shm_rmid) do release it. Stating that on the parameter type fixes the drop:

 void free_ipcs(struct ipc_namespace *ns, struct ipc_ids *ids,
-		void (*free)(struct ipc_namespace *, struct kern_ipc_perm *));
+		void (*free)(struct ipc_namespace *, struct kern_ipc_perm *)
+			__releases_shared(RCU));

plus __releases_shared(RCU) on freeary and do_shm_rmid, which release RCU but never said so. Result over ipc/: 36 → 33 unique diagnostics. The target conversion-drop is resolved, and annotating freeary gave the analysis information it previously lacked, clearing two further pre-existing warnings in ipc/sem.c. One new warning remains (do_shm_rmid "RCU is still held at the end of function") because it releases via shm_destroy(), which is unannotated. The full patch is in fix-ipc.patch.

Sharedness matters, and getting it wrong is expensive. The first attempt used __releases(RCU) — copying what freeque already said. That produced two new releasing ... using exclusive access, expected shared access warnings, because rcu_read_lock() is __acquires_shared(RCU). So freeque's existing __releases(RCU) is a pre-existing kernel bug — the same class as the mtk_wed.h one below. With __releases_shared(RCU) the fix is clean.

Over-annotating backfires. Also annotating shm_destroy() (which does release RCU) made things worse: 33 → 38, because it is called both with and without RCU held. That is a real structural inconsistency in ipc/shm.c that no single annotation can express.

kref_put_lock: parameter-relative capabilities cannot be matched

Annotating the callback parameter fails outright, since the attribute cannot name a later parameter:

error: use of undeclared identifier 'lock'

Reordering so lock precedes the callback makes it parse, but the drop warning still fires and the destination type prints with no requirement — a parameter-relative requirement can never be part of a type, so it cannot be compared against the caller's global &auth_domain_lock.

Isolating the mechanism confirms this is specifically about parameter-relative capabilities, not about parameters: when the capability is the same global, annotating the callback parameter works exactly as well as annotating a typedef — both silence the drop and both correctly begin checking the indirect call. So the release notes' claim that requirements on a parameter "take part in the comparison" holds; kref_put_lock is simply outside what any type can express. An explicit cast is the only escape.

struct seq_operations: forcing an annotation makes it strictly worse

There is no wildcard capability (__releases(*) is a parse error) and generic only means shared-or-exclusive, not "any lock". To quantify the cost of forcing one anyway, struct seq_operations was annotated with the RCU contract that 15 of the 20 sites use (.start __acquires_shared(RCU), .stop __releases_shared(RCU), .next __must_hold_shared(RCU)), then rebuilt tree-wide.

Unique diagnostics	2039 → 2172
Added	154 (134 conversion-add, 20 conversion-drop)
Resolved	20
Net	+133

And the 20 "resolved" are the same 20 sites as the 20 newly-added drops — merely re-labelled from "drops … when converted to void (*)(struct seq_file *, void *)" to "drops … when converted to … __attribute__((release_shared_capability(RCU)))". The non-RCU cases (crypto's &crypto_alg_sem, md's &all_mddevs_lock, sock.c's proto_list_mutex, …) are not fixed at all. So annotating a widely-shared callback struct fixes nothing and costs 134 extra warnings.

The 134 additions are one per seq_file implementation that does not use RCU — e.g. arch/x86/kernel/cpu/proc.c:178, arch/x86/kernel/cpu/mce/severity.c:449 — each reporting that a plain .start gains an acquire_shared_capability(RCU) requirement it does not state. This is the -Wthread-safety-conversion-add subgroup doing exactly its job, and it is the knob that governs tolerability here: with -Wno-thread-safety-conversion-add the result is 20 added against 20 resolved — a wash, on identical sites.

Recording the handoff when the lock is internal: token capabilities

Since the actual lock is chosen by each implementation, the follow-up question is whether the handoff itself can still be recorded — an ACQUIRE(&param->field) or a generic ACQUIRE(&state). Both mechanisms exist (the kernel's token_context_lock() is how RCU itself is declared), both are enforced, and they behave completely differently at scale.

Measured tree-wide, annotating struct seq_operations three ways:

Annotation on .start/.stop/.next	Unique diags	Added	Enforced?
none (unmodified)	2039	—	—
global token — __acquires(seq_ctx)	2172	+154 (134 add, 20 drop)	yes
object-relative — __acquires(&m->iter_ctx)	2038	0	yes

The object-relative form, against a dedicated token field added to struct seq_file:

context_lock_struct(seq_iter_ctx) {};

struct seq_file {
	struct seq_iter_ctx iter_ctx;
	...
};

struct seq_operations {
	void * (*start) (struct seq_file *m, loff_t *pos) __acquires(&m->iter_ctx);
	void (*stop) (struct seq_file *m, void *v)        __releases(&m->iter_ctx);
	void * (*next) (struct seq_file *m, void *v, loff_t *pos)
							  __must_hold(&m->iter_ctx);
	int (*show) (struct seq_file *m, void *v);
};

costs zero new diagnostics across 2965 objects and all 294 initializers, and is genuinely live rather than inert. Probes confirm it catches ->next without ->start (calling function 'next' requires holding mutex 'm->lock' exclusively) and a missing ->stop ('m->lock' is still held at the end of function). A negative control on real code — deleting one m->op->stop() from traverse() in fs/seq_file.c — produces:

fs/seq_file.c:141:1: warning: seq_iter_ctx 'm->iter_ctx' is not held on every path
  through here [-Wthread-safety-analysis]

So the kernel's own seq_file protocol is verifiably correct today, and the annotation would guard it going forward. This is protection the kernel already has for blk_holder_ops and ata_port_operations and lacks for its most common callback struct.

Why object-relative wins. The trade is inverted from what one might expect: the weaker, declaration-scoped annotation is the deployable one precisely because an object-relative requirement can never be part of a type, so it never enters the conversion comparison — unannotated handlers stay silent. A global token is folded into the type, so every one of the 294 unannotated .start handlers reports gaining a requirement it does not state, which is the 134 conversion-add warnings.

Neither silences the original 20. Two probes pin down why:

• A handler naming its own private global (&crypto_alg_sem, &all_mddevs_lock) still reports the drop, because the destination prints as plain void (*)(struct seq_file *, void *) — an object-relative requirement cannot absorb a global one.
• Declaring only the token while doing the real lock work moves the complaint inside the handler: rw_semaphore 'my_sem' is still held at the end of function in start, and releasing 'my_sem' that was not held in stop. Suppressing that needs context_unsafe()/__no_context_analysis, discarding the in-body checking.

To silence a drop, the handler's stated requirements must be a subset of what the type carries. The handlers name globals that differ per implementation and a type carries one fixed set, so it is impossible by construction whichever mechanism is chosen. The token is therefore additive — new protocol checking at near-zero churn — and sits alongside the 20 reports rather than resolving them. Probes: probe4.c, probe5.c.

Transitive / returned capabilities: what exists, and why they cannot close it

lock_returned is the only capability-naming mechanism in the attribute set (there is no "acquires my return value"). All three candidate shapes were probed in C (probe7.c):

1. lock_returned works in C. A getter can name a capability, and the requirement resolves through the call:

static spinlock_t *foo_lock(struct foo *f) __attribute__((lock_returned(f->lock)))
{ return &f->lock; }

static int read_via_getter(struct foo *f) __must_hold(foo_lock(f))
{ return f->data; }            /* silent */

static int read_unlocked(struct foo *f)
{ return f->data; }            /* warning: reading variable 'data' requires
                                  holding spinlock '&foo::lock' */

This solves "which lock is get_lock(x)" — a different problem from "which lock does this callback use".

2. A token threaded through the callbacks is enforced at the generic call site.

struct ops_tok {
	void *(*start)(struct seq_file *m, struct seq_tok *t) __acquires(t);
	void *(*next)(struct seq_file *m, struct seq_tok *t, void *v) __must_hold(t);
	void (*stop)(struct seq_file *m, struct seq_tok *t, void *v) __releases(t);
};

Correct use is silent; ->next without ->start gives calling function 'next' requires holding seq_tok 't' exclusively; a missing ->stop gives seq_tok 't' is still held at the end of function. This is the C-expressible transitive form, and it is exactly as powerful as the &m->iter_ctx version above — the token is simply passed explicitly instead of reached through m.

3. An implementation cannot bind the token to its real lock. A handler annotated __releases_shared(&my_sem) assigned into a __releases(t) field still reports 'impl_stop' drops the 'release_shared_capability(&my_sem)' requirement. No relation between t and &my_sem is inferred — there is no capability polymorphism.

Why no attribute can fix this in C. fs/seq_file.c is compiled once for all 294 implementations. At m->op->start(m, &m->index) there is no static knowledge of which ops table is in play, so the specific lock (&crypto_alg_sem vs RCU vs &all_mddevs_lock) cannot be checked there even in principle. This is not a missing attribute — it is the absence of monomorphization. In C++ the same machinery would work, because a seq_operations<Lock> template is checked per instantiation and the branch already propagates requirements through template instantiation. A RETURN_CAPABILITY-style "acquires my return value" would only let .start hand the token back instead of receiving it, saving a parameter; it would not make the concrete lock visible at the shared site.

So the token approach already extracts all the checking available in C: the protocol is verified in the shared code, and each implementation's real lock is verified inside its own handler bodies. The only thing missing is the link between the two.

The real blocker for a .capability member: no receiver

RETURN_CAPABILITY(c) is the modern spelling of lock_returned(c), and it is an aliasing/naming facility, not a transfer one — the docs themselves document (ab)using it to give a private mutex a public name, where "the analysis thinks that c.getMu() == c.mu". So the natural design is a .capability member on the ops struct that the callback fields name, with each instantiation binding it to its own lock. Probed in C (probe8.c, probe9.c, probeA.c):

struct ops_sib {
	const struct seq_cap *capability;
	void *(*start)(struct seq_file *m, loff_t *pos) __acquires(capability);
	void *(*next)(struct seq_file *m, void *v, loff_t *pos) __must_hold(capability);
	void (*stop)(struct seq_file *m, void *v) __releases(capability);
};

This is accepted and enforced — ->next without ->start and a missing ->stop are both caught. But it loses instance identity: the diagnostic names the capability 'capability', not 'o->capability'. Consequences, both pre-existing (byte-identical on the baseline compiler):

• Cross-instance calls are accepted: a->start(...) then b->next(...) is silent, because both name the same unqualified capability.
• The docs' own example is unsatisfiable. For struct Cache { Mutex mu; void (*read)(void) REQUIRES(mu); }, all three of holding c->mu, holding a different d->mu, and holding nothing warn identically with requires holding mutex 'mu'. Acquiring the real member can never satisfy the requirement.

The distinguishing factor is whether a receiver is available to resolve the member against:

Form	Resolves to	Instance-qualified?
C++ method void read() REQUIRES(mu)	c.mu	yes — receiver is this
C++ fn-ptr member void (*read)(void) REQUIRES(mu)	mu	no
C fn-ptr field, sibling member __must_hold(capability)	capability	no
C fn-ptr field, parameter-rooted __must_hold(&o->mu)	c->mu	yes

The last row is why &m->iter_ctx worked: m is a parameter of the pointee type, so it is visible at the call and the capability is properly per-instance (cross() correctly warns requires holding mutex 'c->mu').

Also confirmed: lock_returned cannot be attached to a function-pointer field in C — 'lock_returned' attribute only applies to functions. So a literal .capability() accessor is not expressible; in C++ it would be a method, and C has none.

So the .capability design needs one specific, bounded extension: resolve a function-pointer field's sibling-member requirement against the object expression used to reach the field at the call site, so o->start(...) yields o->capability. That is the exact analogue of receiver resolution for C++ methods, it needs no monomorphization because it stays symbolic, and it would make per-instance protocol checking sound for callback tables. It would not by itself link o->capability to &crypto_alg_sem; that still wants an initializer-time alias, which is where a RETURN_CAPABILITY-style binding would come in — except that the target has to vary per instantiation, which is the part no existing attribute expresses.

Discharging the alias: the kernel already has the pattern

Binding an abstract capability to a concrete lock is not trivially sound, so it needs a proof obligation attached. The kernel already ships exactly this pattern — assume statically, verify dynamically:

/* include/linux/lockdep.h */
#define lockdep_assert_held(l)		\
	do { lockdep_assert(lockdep_is_held(l) != LOCK_STATE_NOT_HELD); \
	     __assume_ctx_lock(l); } while (0)

__assume_ctx_lock is assert_capability, which (per the kernel's own comment) "does not generate a check. Instead, it tells the analysis to assume the capability is held ... used for augmenting runtime assertions." And with !CONFIG_LOCKDEP it degrades to a bare assumption with no check at all (lockdep.h:392), so a graded soundness story is already accepted practice here.

The bridge works on exactly the shape that matters. For a parameter-rooted token reached through a callback field, an assertion discharges the requirement (probeB.c):

void bridge(const struct ops *o, struct sf *m)
{
	__assume_ctx_lock(&m->ctx);	/* what lockdep_assert_held() expands to */
	o->next(m);			/* silent */
}
void no_bridge(const struct ops *o, struct sf *m)
{
	o->next(m);			/* warning: calling function 'next' requires
					   holding seq_cap 'm->ctx' exclusively */
}

So the obligation decomposes into three sites, and only one needs the runtime escape:

Site	What is known	Discharge
The initializer	both abstract capability and concrete lock	mechanically checkable — substitute and compare against each handler's declared requirements
Generic code (fs/seq_file.c)	abstract capability only	sound already — symbolic protocol check, claims nothing concrete (measured: 0 added warnings)
A bridge where the ops identity is not static	neither	runtime assertion (lockdep_assert_held)

And the kernel's shape is favourable for the checkable sites: all 294 seq_operations tables are static initializers, so the substitution would be statically available wherever locks are actually involved. The one widespread dynamic constructor, single_open() (155 callers), heap-allocates its ops and fills them at runtime — but its single_start / single_next / single_stop handlers take no locks at all, so its binding is empty and the dynamic case is benign.

The novel compiler work is therefore bounded: substitution of the bound capability at the initializer, plus receiver resolution for callback fields (above). Everything else already exists.

Still open. The hard residue is flow sensitivity: an ops table can be assigned to a const struct seq_operations * and travel arbitrarily far from its initializer, so the binding has to travel with the pointer or be re-established at each use. Whether that is expressible without either monomorphization or a per-callsite assertion is exactly the part this testing did not settle.

Conclusion

The 294 seq_operations initializers across 256 files are the core difficulty: the kernel's dominant callback idiom hands a lock chosen by the implementation across a shared struct. Type-carried requirements are a good fit for the ipc/ shape (one helper, one global capability, all callbacks agreeing) and cannot express the rest. For the kernel, the practical disposition of the other 23 is an explicit cast at the initializer, or -Wno-thread-safety-conversion-drop for the affected files — not annotation.

This does not argue against the diagnostic. All 24 reports are true: the requirement really is discarded and the indirect call really is unchecked. It does suggest the drop warning will need a suppression story for shared callback structs before a codebase like the kernel could enable it tree-wide.

Incidental pre-existing kernel bugs (not caused by this branch)

• include/linux/soc/mediatek/mtk_wed.h:196 annotates mtk_wed_ops::attach with __releases(RCU) while callers hold RCU read-side (shared). Both compilers report releasing __ctx_lock_RCU 'RCU' using exclusive access, expected shared access. It probably wants __releases_shared(RCU).
• ipc/msg.c:274 has the same bug: freeque says __releases(RCU) where RCU is acquired shared.
• ipc/msg.c:275 — freeque's __releases(&msq->q_perm) names msq, a function-local variable, so the TU fails with error: use of undeclared identifier 'msq' whenever it is analyzed. Present identically on both compilers; ipc/msg.o never builds in tree-wide mode.