Skip to content

Latest commit

 

History

History
112 lines (93 loc) · 5.67 KB

README.md

File metadata and controls

112 lines (93 loc) · 5.67 KB

LinxCoreModel

LinxCoreModel is the Rust modeling workspace for LinxCore.

Project policy and verification entrypoints:

Current workspace contents:

  • isa: shared architectural types and trace contracts
  • elf: static ELF loading for LinxISA user-mode programs
  • runtime: guest runtime state and syscall shim scaffolding
  • funcmodel: first functional engine path
  • camodel: first stage-structured cycle engine path
  • trace: commit JSONL and linxtrace.v1 emission
  • cosim: M1 JSONL lockstep protocol helpers
  • dse: sweep and report generation
  • lx-tools: lx-run, lx-cosim, lx-trace, lx-sweep

Current crate layout:

  • camodel: core/, frontend/, issue/, backend/, control/, decode/, trace/
  • funcmodel: core/, exec/, memory/, syscalls/, trace/
  • trace: linxtrace/, commit/, schema/
  • cosim: protocol/, compare/, qemu/
  • lx-tools: shared helpers in cli/, thin binaries in bin/

The current implementation lands the full workspace shape, executable lx-* surface, static ELF loading, runtime bootstrap, syscall allowlist scaffolding, commit/pipeview emission, lockstep compare helpers, and a full table-driven LinxISA v0.4 decoder sourced from a vendored copy of the canonical ISA JSON.

Current functional-engine status:

  • decodes the full canonical v0.4 instruction corpus, including 16/32/48/64-bit forms
  • bootstraps a Linux-style user stack and places the initial stack pointer in sp
  • executes a substantial user-mode scalar subset in Rust: ALU/immediate ops, W variants, compares, shifts, loads/stores, SETC, SETRET, J/JR, SSRGET/SSRSET, compressed scalar forms, and basic block/macro control flow
  • forwards the current user-mode syscall subset through a host shim: read, write, eventfd2, epoll_create1, epoll_ctl, epoll_pwait, openat, close, lseek, fstat, futex, getcwd, dup3, fcntl, ioctl, pipe2, pselect6, ppoll, newfstatat, readlinkat, getrandom, prctl, madvise, membarrier, rseq, sigaltstack, set_tid_address, set_robust_list, setuid, setgid, setresuid, getresuid, setresgid, getresgid, uname, getppid, wait4, sysinfo, prlimit64, brk, mmap, munmap, mprotect, rt_sigaction, rt_sigprocmask, clock_gettime, getpid, getuid, geteuid, getgid, getegid, gettid, exit, exit_group
  • enforces guest page permissions for architectural loads/stores and syscall copy-in/copy-out, including mprotect-driven access changes
  • normalizes host errno values to Linux guest errno numbers before returning through the Linx Linux-user syscall ABI
  • emits commit JSONL and linxtrace.v1 traces from the executing functional path

Still incomplete in this phase:

  • many ISA classes remain unsupported in the functional executor, especially FP, atomics, wide HL forms, and full privileged behavior
  • syscall ABI coverage is pragmatic bring-up coverage, not a complete Linux user ABI
  • futex currently implements the single-process WAIT/WAKE subset only; there is no real waiter queue or multi-thread scheduler yet
  • sysinfo and prlimit64 currently expose deterministic single-process model values suitable for libc bring-up, not host-kernel passthrough
  • setxid coverage is currently single-process identity-state emulation for libc startup and credential probes, not full Linux credential or threading semantics
  • getrandom currently returns deterministic model-generated bytes so user-mode bring-up and regression traces stay reproducible across hosts
  • prctl, madvise, and membarrier currently implement the small single-process subset needed for libc/thread-runtime bring-up, not the full Linux kernel surface
  • rseq currently supports deterministic single-thread register/unregister bring-up semantics and initializes the guest ABI fields the runtime is expected to read
  • ioctl currently implements deterministic tty-style TIOCGWINSZ, TIOCGPGRP, and TIOCSPGRP behavior for guest stdio fds only
  • ppoll currently marshals guest pollfd arrays onto host poll(2) and ignores signal-mask effects beyond guest-memory validation
  • pselect6 currently marshals guest fd_set bitmaps onto host poll(2) and validates, but does not apply, guest signal masks
  • eventfd2 and epoll_* currently run through a deterministic user-mode shim: eventfd readiness is backed by internal counter state plus a pollable host pipe, and epoll wait reuses host poll(2) across registered guest fds
  • wait4 currently reports deterministic single-process -ECHILD semantics after validating guest status/rusage pointers; there is not yet a modeled child-task table
  • sigaltstack currently tracks deterministic single-thread alternate-stack state for libc/runtime queries; it does not imply modeled signal delivery yet
  • bootstrap auxv now includes deterministic AT_MINSIGSTKSZ, AT_PLATFORM, AT_HWCAP*, AT_CLKTCK, and AT_SYSINFO_EHDR entries for libc startup paths
  • cycle-accurate execution and QEMU lockstep remain separate follow-on work

Verification

Minimum structural check:

bash tools/ci/check_repo_layout.sh

Full repo-local gate pack:

bash tools/regression/run_crosschecks.sh

To require the local CLI smoke on a previously built bring-up ELF:

bash tools/regression/run_crosschecks.sh --require-smoke