The header scan (Captain Bob, 2026-11-10): 788 source files -- 351 with the
SL-1.0 header, 12 with the old name (docs/working/experiments, kept by
ruling), 31 under someone else's licence (tools/kconfig, Linux's, GPL-2.0:
kept), and 394 with none. Ruled: the SPDX form; capsules (.4th, .f18) and
proofs (.thy) left for a ruling of their own (mkcapsule's 64x16 block format,
content-addressed capsules).
253 files now begin
SPDX-License-Identifier: LicenseRef-Starship-1.0
Copyright (c) 2023-2026 Robert A. James
as a /* */ block (C, headers, assembly, linker scripts) or # lines (scripts,
Makefiles, Kconfig; below a shebang or a coding line); tools/mkcapsule.c,
which had the copyright line, gets the SPDX line only.
Not touched: docs/working/ (archive and old campaign material, as the
ruling kept the experiments); v4/system/post_cases.c (generated by
v4/tools/mkpost.py, "do not edit" -- the generator has the header).
Comments only: the kernel builds on amd64, aarch64, riscv64; make -C v4
test-32: 39 programs, 0 failures; every changed script parses.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
76 lines
3.4 KiB
C
76 lines
3.4 KiB
C
/* SPDX-License-Identifier: LicenseRef-Starship-1.0
|
|
* Copyright (c) 2023-2026 Robert A. James
|
|
*/
|
|
/* exec.h -- instruction execution for v4.
|
|
*
|
|
* DECOMPOSITION.md section 1.2: "Slots execute left to right." A branch
|
|
* (jump, call, next, if, -if) takes its target from all bits to the right of
|
|
* its slot and replaces the same low bits of P (page-relative). Branches are
|
|
* legal in slots 0-3 only. Nothing to the right of a branch executes, taken
|
|
* or not, because those bits are its address.
|
|
*
|
|
* Section 1.4: "Every retired instruction increments that opcode's heat counter
|
|
* and advances the anti-clock; every `call` increments the heat counter of its
|
|
* target. None of this costs an instruction."
|
|
*
|
|
* The node owns P, A, B, the stacks and memory; heat and the anti-clock are
|
|
* separate physics state (section 7 names them as registers).
|
|
*
|
|
* THREE POINTS THE SPEC LEAVES TO THE F18, and which this model takes from it:
|
|
*
|
|
* - `ex` ends the word, like `;`. P has been replaced, so the remaining
|
|
* slots belong to a word that is no longer the current one.
|
|
* - `unext` restarts the *already fetched* word at slot 0. It does not
|
|
* refetch and does not move P, so `@p` and `!p` inside a unext loop step
|
|
* through the words that follow the loop word. When R reaches 0 the loop
|
|
* ends and execution continues with the slot after `unext`.
|
|
* - `+*` shifts T arithmetically (sign bit kept). Section 1.3 says only
|
|
* "shift T:A right one bit"; D-3 says plain F18 semantics.
|
|
*
|
|
* A branch opcode in slot 4 or 5 is outside the spec. The model does not trap
|
|
* it: it applies the 7- or 2-bit target the layout formula gives.
|
|
*/
|
|
#ifndef V4_EXEC_H
|
|
#define V4_EXEC_H
|
|
|
|
#include "v4/heat.h"
|
|
#include "v4/iword.h"
|
|
#include "v4/node.h"
|
|
|
|
typedef struct {
|
|
v4_uheat_t anticlock;
|
|
|
|
/* A node blocked at its port in the middle of an instruction word
|
|
* (node.h) goes on, when it has been served, from the slot after the
|
|
* store: the word and the slot are kept here meanwhile. */
|
|
int resume;
|
|
v4_iword resume_iw;
|
|
unsigned resume_slot;
|
|
unsigned resume_faults; /* n->faults when it blocked: a fault since then means P is a handler and the rest of the word is abandoned */
|
|
} v4_exec_state;
|
|
|
|
void v4_exec_reset(v4_exec_state *es);
|
|
|
|
/* Execute one instruction word: fetch at P, advance P, run the slots left to
|
|
* right until the word ends. A unext loop runs to completion inside one call,
|
|
* so the call does not return while R is nonzero at a `unext`. Returns the
|
|
* number of instructions retired.
|
|
*
|
|
* FAULTS (node.h; D-14 and D-16). Before an opcode runs, the stacks must
|
|
* hold what it takes -- a T or S it only reads counts -- and have room for
|
|
* what it leaves; and an address it uses, or P at the fetch, must be inside
|
|
* node memory. If not, that opcode and the rest of the word do not execute,
|
|
* both stacks are emptied, and P is that kind's word of the node's fault
|
|
* table on return. With no table the node stops, and this does nothing and
|
|
* returns 0 from then on. */
|
|
unsigned v4_exec_step_word(v4_node *n, v4_exec_state *es, v4_heat *h);
|
|
|
|
/* Execute a single opcode. The branch opcodes read their target from `w` and
|
|
* `slot`; every other opcode ignores both. `unext` here only updates R; the
|
|
* restart is v4_exec_step_word's. A value above 31 does nothing and retires
|
|
* nothing. */
|
|
void v4_exec_op(v4_node *n, v4_exec_state *es, v4_heat *h,
|
|
unsigned op, v4_iword w, unsigned slot);
|
|
|
|
#endif /* V4_EXEC_H */
|