Skip to content
Draft
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
53 changes: 53 additions & 0 deletions AGENTS.md
Original file line number Diff line number Diff line change
Expand Up @@ -308,3 +308,56 @@ Project decision: commits in this tree use kernel style.

If agents keep making the same mistake, or a decision changes, propose an edit
here. Do not add workarounds in code.

### Printk LKMM access validation

The user approved using this scoped amendment while implementing printk
in PR #24. This authorizes investigation and implementation with the
validation below; it does not certify the C/Rust boundary or the port.

The printk ringbuffer reads ordinary payload memory speculatively and
validates the descriptor afterward. A direct Rust translation fails Loom's data-race
checks, including when descriptor operations are sequentially consistent.
The in-tree `rust/kernel/sync/atomic.rs` already distinguishes LKMM from
the userspace Rust memory model, but does not supply a contract for these
bulk copies.

Evidence: commit `818c24e` in `misttech/linux-rust`, on
`codex/gpt-6/feature/printk-port`, contains the reproducer at
`harness/printk_ringbuffer/loom/` and the record at
`units/printk_ringbuffer.md`. The speculative-copy test fails; the atomic
payload control passes. This is a minimal feasibility model, not a model
of the complete ringbuffer. The diagnostic and subsequent validation
commit `3edea95` are published on that branch.

For this port, investigate a split validation approach:

- Keep all ringbuffer decisions, reservation, recycling and descriptor
validation in Rust. Keep headers and C callers unchanged.
- Access intentionally racing C-owned memory only through a minimal C
boundary. Each helper must preserve an existing C access operation and
its barrier placement, with a documented U1 contract. This is not
permission to retain the C algorithm behind a wrapper.
The existing FFI rule remains binding: each helper is a single forwarding
call to an existing C function, inline or macro, with its prototype above
the definition. No helper loops, branches or new access algorithms are
authorized. If this boundary requires more, stop and propose a separate
amendment to the FFI rule.
- Never form Rust references to concurrently recycled payloads. Copies
returned to Rust remain untrusted until descriptor validation succeeds;
lengths, offsets and bit validity must be checked before use.
- Use Loom for protocols it can faithfully model. Preserve the failing
direct-translation diagnostic. An atomic payload model is a control,
not evidence that C's ordinary payload accesses are race-free.
- Use LKMM/herd7 litmus tests for the C boundary's publication and reuse
ordering. Derive them from the source's named LMM barrier pairs and
document which properties and accesses the model does not cover.
- Require a compiler/FFI argument for the boundary as well as layout,
differential, existing KUnit and C/Rust build validation. Passing herd7
alone does not establish Rust soundness or compiler correctness.

For the authorized printk work, criterion 2 allows this explicit
combination of Loom and LKMM evidence for printk only. All other ports
remain subject to the original criterion. Failure to establish the C/Rust
boundary contract still stops the port; acceptance is permission to investigate,
not certification of the implementation.
2 changes: 1 addition & 1 deletion Kbuild
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ $(port-layout-header): kernel/port-layout.s FORCE
define filechk_port_layout_rs
echo "// SPDX-License-Identifier: GPL-2.0"; \
echo "// Generated from the active C kernel configuration."; \
awk '/^#define PORT_LOCKREF_/ { \
awk '/^#define PORT_/ { \
type = ($$2 == "PORT_LOCKREF_DEAD_VAL" ? "i32" : "usize"); \
print "pub(crate) const " $$2 ": " type " = " $$3 ";"; \
if ($$2 == "PORT_LOCKREF_ALIGN") align = $$3; \
Expand Down
60 changes: 60 additions & 0 deletions kernel/port-layout.c
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@
#define COMPILE_OFFSETS
#include <linux/kbuild.h>
#include <linux/lockref.h>
#include "printk/printk_ringbuffer.h"

int main(void)
{
Expand All @@ -19,6 +20,65 @@ int main(void)
OFFSET(PORT_LOCKREF_LOCK_COUNT, lockref, lock_count);
#else
DEFINE(PORT_LOCKREF_LOCK_COUNT, 0);
#endif
#ifdef CONFIG_PRINTK
DEFINE(PORT_PRB_DATA_BLK_LPOS_SIZE, sizeof(struct prb_data_blk_lpos));
DEFINE(PORT_PRB_DATA_BLK_LPOS_ALIGN, __alignof__(struct prb_data_blk_lpos));
OFFSET(PORT_PRB_DATA_BLK_LPOS_BEGIN, prb_data_blk_lpos, begin);
OFFSET(PORT_PRB_DATA_BLK_LPOS_NEXT, prb_data_blk_lpos, next);
DEFINE(PORT_PRB_DESC_SIZE, sizeof(struct prb_desc));
DEFINE(PORT_PRB_DESC_ALIGN, __alignof__(struct prb_desc));
OFFSET(PORT_PRB_DESC_STATE_VAR, prb_desc, state_var);
OFFSET(PORT_PRB_DESC_TEXT_BLK_LPOS, prb_desc, text_blk_lpos);
DEFINE(PORT_PRB_DATA_RING_SIZE, sizeof(struct prb_data_ring));
DEFINE(PORT_PRB_DATA_RING_ALIGN, __alignof__(struct prb_data_ring));
OFFSET(PORT_PRB_DATA_RING_SIZE_BITS, prb_data_ring, size_bits);
OFFSET(PORT_PRB_DATA_RING_DATA, prb_data_ring, data);
OFFSET(PORT_PRB_DATA_RING_HEAD_LPOS, prb_data_ring, head_lpos);
OFFSET(PORT_PRB_DATA_RING_TAIL_LPOS, prb_data_ring, tail_lpos);
DEFINE(PORT_PRB_DESC_RING_SIZE, sizeof(struct prb_desc_ring));
DEFINE(PORT_PRB_DESC_RING_ALIGN, __alignof__(struct prb_desc_ring));
OFFSET(PORT_PRB_DESC_RING_COUNT_BITS, prb_desc_ring, count_bits);
OFFSET(PORT_PRB_DESC_RING_DESCS, prb_desc_ring, descs);
OFFSET(PORT_PRB_DESC_RING_INFOS, prb_desc_ring, infos);
OFFSET(PORT_PRB_DESC_RING_HEAD_ID, prb_desc_ring, head_id);
OFFSET(PORT_PRB_DESC_RING_TAIL_ID, prb_desc_ring, tail_id);
OFFSET(PORT_PRB_DESC_RING_LAST_FINALIZED_SEQ, prb_desc_ring, last_finalized_seq);
DEFINE(PORT_PRINTK_RINGBUFFER_SIZE, sizeof(struct printk_ringbuffer));
DEFINE(PORT_PRINTK_RINGBUFFER_ALIGN, __alignof__(struct printk_ringbuffer));
OFFSET(PORT_PRINTK_RINGBUFFER_DESC_RING, printk_ringbuffer, desc_ring);
OFFSET(PORT_PRINTK_RINGBUFFER_TEXT_DATA_RING, printk_ringbuffer, text_data_ring);
OFFSET(PORT_PRINTK_RINGBUFFER_FAIL, printk_ringbuffer, fail);
DEFINE(PORT_PRB_RESERVED_ENTRY_SIZE, sizeof(struct prb_reserved_entry));
DEFINE(PORT_PRB_RESERVED_ENTRY_ALIGN, __alignof__(struct prb_reserved_entry));
OFFSET(PORT_PRB_RESERVED_ENTRY_RB, prb_reserved_entry, rb);
OFFSET(PORT_PRB_RESERVED_ENTRY_IRQFLAGS, prb_reserved_entry, irqflags);
OFFSET(PORT_PRB_RESERVED_ENTRY_ID, prb_reserved_entry, id);
OFFSET(PORT_PRB_RESERVED_ENTRY_TEXT_SPACE, prb_reserved_entry, text_space);
DEFINE(PORT_PRINTK_RECORD_SIZE, sizeof(struct printk_record));
DEFINE(PORT_PRINTK_RECORD_ALIGN, __alignof__(struct printk_record));
OFFSET(PORT_PRINTK_RECORD_INFO, printk_record, info);
OFFSET(PORT_PRINTK_RECORD_TEXT_BUF, printk_record, text_buf);
OFFSET(PORT_PRINTK_RECORD_TEXT_BUF_SIZE, printk_record, text_buf_size);
DEFINE(PORT_PRINTK_INFO_SIZE, sizeof(struct printk_info));
DEFINE(PORT_PRINTK_INFO_ALIGN, __alignof__(struct printk_info));
OFFSET(PORT_PRINTK_INFO_SEQ, printk_info, seq);
OFFSET(PORT_PRINTK_INFO_TS_NSEC, printk_info, ts_nsec);
OFFSET(PORT_PRINTK_INFO_TEXT_LEN, printk_info, text_len);
OFFSET(PORT_PRINTK_INFO_FACILITY, printk_info, facility);
DEFINE(PORT_PRINTK_INFO_FLAGS_LEVEL, offsetof(struct printk_info, facility) + 1);
OFFSET(PORT_PRINTK_INFO_CALLER_ID, printk_info, caller_id);
#ifdef CONFIG_PRINTK_EXECUTION_CTX
OFFSET(PORT_PRINTK_INFO_CALLER_ID2, printk_info, caller_id2);
OFFSET(PORT_PRINTK_INFO_COMM, printk_info, comm);
DEFINE(PORT_PRINTK_INFO_COMM_SIZE, sizeof(((struct printk_info *)0)->comm));
#else
DEFINE(PORT_PRINTK_INFO_CALLER_ID2, 0);
DEFINE(PORT_PRINTK_INFO_COMM, 0);
DEFINE(PORT_PRINTK_INFO_COMM_SIZE, 0);
#endif
OFFSET(PORT_PRINTK_INFO_DEV_INFO, printk_info, dev_info);
DEFINE(PORT_PRINTK_INFO_DEV_INFO_SIZE, sizeof(struct dev_printk_info));
#endif
return 0;
}
2 changes: 1 addition & 1 deletion kernel/printk/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ obj-$(CONFIG_A11Y_BRAILLE_CONSOLE) += braille.o
obj-$(CONFIG_PRINTK_INDEX) += index.o

obj-$(CONFIG_PRINTK) += printk_support.o
printk_support-y := printk_ringbuffer.o
printk_support-y := $(if $(CONFIG_RUST_KERNEL),printk_ringbuffer_ffi.o,printk_ringbuffer.o)
printk_support-$(CONFIG_SYSCTL) += sysctl.o

obj-$(CONFIG_PRINTK_RINGBUFFER_KUNIT_TEST) += printk_ringbuffer_kunit_test.o
Loading