Skip to content
Open
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
6 changes: 4 additions & 2 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -52,10 +52,12 @@ cross:
python3 tools/check-entry.py

# kore-host drives real image files under POSIX record locks, which Miri does
# not model; `make test` exercises its procedure.
# not model; `make test` exercises its procedure. kore-rt's `bridge` suite runs
# the worker/host state machine on real threads, so Miri checks every hand-over
# of the cell the Lua VM and a C program's host share with thread 0.
miri:
cargo miri test --locked --workspace --all-features --exclude kore-wasi --exclude kore-host
cargo miri test --locked --manifest-path native/Cargo.toml -p kore-rt erased_poll_and_drop
cargo miri test --locked --manifest-path native/Cargo.toml -p kore-rt -- erased_poll_and_drop bridge::

native-check:
python3 tools/check-native.py
Expand Down
546 changes: 218 additions & 328 deletions crates/c/src/program.rs

Large diffs are not rendered by default.

679 changes: 288 additions & 391 deletions crates/lua/src/bridge.rs

Large diffs are not rendered by default.

5 changes: 3 additions & 2 deletions crates/lua/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -280,8 +280,9 @@ impl Policy {
/// interfaces.
///
/// Selection is by type instantiation, not runtime dispatch: `Host::start`
/// is generic over `E`, so `LIBRARIES` reaches the worker thread as
/// monomorphized static data with no global to publish it.
/// is generic over `E`, so `LIBRARIES` and `POLICY` are monomorphized static
/// data the host hands the worker thread in its first work item, with no
/// global to publish them.
///
/// There is deliberately **no `'static` bound**. The worker thread reads
/// only [`Extension::LIBRARIES`], which is `&'static` in its own right;
Expand Down
26 changes: 16 additions & 10 deletions docs/languages.md
Original file line number Diff line number Diff line change
Expand Up @@ -91,11 +91,14 @@ that joins `libkore.so` to the program's own `libc.a` — and gets:
- `kore_fs_run(step, user, &error)` (`kore/program.h`), which runs a
`KoreFsStep` program as the program's filesystem session.

The host is the shape `kore-lua`'s VM bridge has. `main` runs on a main
thread, a `DoorbellWorker` with a 1 MiB guarded stack
(`KORE_MAIN_STACK_BYTES`). Thread 0 is the process owner, and keeps the
executor and the launch's service faces. The two share one request cell and
one word. Every park is a doorbell park; nothing spins.
The host is the shape `kore-lua`'s VM and Kore's `tcc` have, and speaks
the same seam, kore-rt's `bridge`. `main` runs on a main thread, the
bridge's worker, with a 1 MiB guarded stack (`KORE_MAIN_STACK_BYTES`).
Thread 0 is the process owner, and keeps the executor and the launch's
service faces. The two share one request cell and one word, whose states,
ordering and hand-over are the bridge's. Every park is a doorbell park;
nothing spins, and a main thread that panics or cannot park is reported to
the host rather than waited for.

- **Filesystem.** `kore_fs_run` from the main thread posts the session and
waits. The host attaches the launch's filesystem face on first use, rooted
Expand All @@ -120,10 +123,11 @@ one word. Every park is a doorbell park; nothing spins.
stream's capacity when it has none — a slow terminal holds the program
back rather than losing its output — and wakes the writers waiting for
space, a pass at a time, serving the program's end and its sessions
between passes. The host's own writes (a filesystem step's callbacks) are
kept in order beside the ring, before any call another thread has in
progress. A launch without the stream has no sink, and a
write to either stream returns `EOF`.
between passes and draining beside a session in flight: the ring is the
bridge's side source (`WorkerHost::serve_beside`). The host's own writes
(a filesystem step's callbacks) are kept in order beside the ring, before
any call another thread has in progress. A launch without the stream has
no sink, and a write to either stream returns `EOF`.
- **The end.** The C library's `exit` and `_Exit` call
`__kore_program_exit(status, finalize)` after their `atexit` handlers, on
whatever thread called them. The first request wins and reaches the host,
Expand Down Expand Up @@ -203,7 +207,9 @@ mapped there. The rules follow from that:
holder may revoke, so the caller posts its request to thread 0, which
holds the supply's root, and waits as a filesystem session does. A mapping
is therefore the process's: any thread may `munmap` it, whole, by its base
and its length.
and its length. Thread 0 answers a request between the main thread's
sessions and beside one in flight, as it drains the ring: both are the
bridge's side source.
- **`munmap` parks the region.** The supply's cursors and the window's only
advance, so carved bytes and placed addresses never return to them. The
mapping is removed and a stale access faults, but the program keeps the
Expand Down
54 changes: 54 additions & 0 deletions docs/provenance.md
Original file line number Diff line number Diff line change
Expand Up @@ -351,3 +351,57 @@ C program (`docs/languages.md`). It is the first libkore package a C program
on Kore links without a Rust host. Its shared object is a distribution's
one-line `cdylib` over it. `tools/check-program.py` links that object for the
three Kore ISAs and checks its shape and its exact exported ABI.

## One bridge for a synchronous engine on a worker thread

The export records Kore `6a8c754bc959e9489a6fb18be642fcc881a65c48`, a commit
on Kore's `ft/festive-euler-sghq2d`, which carries the bridge and merges
MicroPerceptron/kore#1494's branch at `f2644e5b` (`eca08c04`). Since the last
export recorded here (`0018956a`), that branch's exports moved through four
Kore commits, and this export carries all four:
- `2a0730dd`, where threads that found take a founder's arena;
- `6c57f344`, where a founding's staged space waits for the reap;
- `2d4998ba`, which brings Kore's C library, `kore-c-shim`;
- `10c7b400`, where `kore-rt` names a task's link window and its free span
once (`738c3591`), and `kore-c-shim` gains `ENXIO`, `EFAULT` and `ENOTSUP`.

Against the export at `10c7b400`, the closure keeps its 27 packages and gains
one file (402):

- `kore-rt`'s `bridge`: one request cell and one word between a synchronous
engine on a worker thread and its async host. The word's states, the
park-and-kick ordering, the cell's hand-over and the worker's end live in one
place (`Bridge`, `Engine`, `Work`, `WorkerHost`), with a host suite that
drives the state machine on real threads. The host can also serve a side
source beside the worker (`Side`, `serve_beside`): work other threads hand it
through the same wake channel, armed and re-read with the word.
- `ThreadBlock`'s `hosted_bridge` tail slot, which names the bridge a worker
serves. With it come a bridge-worker notice in `entry::panic_refuse` and
`crash::report`, once the panic record is published, and the worker's exit
hook: a worker that ends its thread through `thread::exit` without saying
its last word has it said for it.
- `futex`'s sweep test judges only the rows it claims (`6a8c754b`). The sweep
reads every row, and the suite's other tests hold rows of their own
meanwhile, so it failed whenever one overlapped it: 8 runs in 300 of
`futex::tests`.
- The services' `boot.toml` digests are the base's seal at `f2644e5b`. Kore's
half reseals over its pin of this branch, so that seal follows this export
and cannot be in it.

`kore-lua`'s VM bridge and `kore-c`'s program host now speak the seam, as Kore's
`tcc` and its Lua REPL do upstream. Each keeps only its payload and its
dispatch. `kore-c` founds its main thread through `WorkerHost::spawn`, holding
the channel-space grant `b9eb3c2` gave it. What the program's other threads
hand thread 0 is the bridge's side source: the output ring `0460f5c` brought,
and the `mmap` cell `c876e43` brought. No exported manifest changed, so
`native/Cargo.lock` did not. `make miri` also runs the `bridge` suite, so Miri
checks every hand-over of the cell.

Locally, with the pinned nightly, `make fmt test check docs owners cross miri
bindings-check` passed on this export. That covers:
- the native `kore-rt` suite (477, the `bridge` suite's 13 among them) and the
`kore-dagfs` and `kore-vol` suites;
- the three Kore user-target checks, which take in `kore-lua`'s bridge;
- `check-program`, which links `libkore.so` for all three ISAs with exactly its
declared 129 exports, the five `c876e43` brought among them;
- Miri over the `bridge` suite (14 tests with `erased_poll_and_drop`).
Loading
Loading