Serve the non-blocking futex shapes from EL1

Merged
JS
2mo ago
+5811-1144

Serves the two futex shapes that cannot block from the EL1 shim and separates an unrelated vCPU watchdog rewrite that
had been sitting in the same change.

Commits

  1. Arm one repeating vCPU watchdog, not two a call. The run loop armed
    and disarmed alarm() around every hv_vcpu_run, and on macOS that is
    setitimer(ITIMER_REAL), so it cost two real syscalls per guest syscall:
    693 ns against a 1226 ns bare HVF round trip. One repeating timer plus a
    seqlock progress word replaces it. Unrelated to futex, hence its own
    commit.
  2. Serve the non-blocking futex shapes from EL1. A FUTEX_WAIT whose
    word already moved answers EAGAIN at EL1 (51 ns against a 2000 ns HVC
    round trip), and a FUTEX_WAKE with nobody parked answers 0 from a
    per-bucket census the wait paths publish into shim_data (1927 ns to
    77 ns). Also widens the bucket table to 1024 with a new hash, and fixes
    undefined behavior in the FUTEX_WAKE_OP operand decode, which was
    undefined for half its input range and included the shift operand that
    was CVE-2018-6927.
  3. Refuse to requeue a PI waiter, as Linux does.
  4. Give the analyzer Darwin's shapes, not Linux's. Five declarations
    where Frama-C's modeled libc uses the Linux layout and macOS does not,
    which is what kept the socket and abstract-socket paths outside the
    analyzer.
  5. Stop rebuilding guest state at EL1.
  6. Spin at EL1, and serve a timed futex wait too. Measured against the
    branch point: wake-wait-handoff 1104 ns to 103, wait-timed 1503 ns to 52.
  7. Prove the futex deadline arithmetic. verify-futexdeadline discharges
    128 of 128 obligations with -wp-rte.

Close #315

Summary by cubic

Serves non-blocking, timed, and wake futex shapes from the EL1 shim instead of round-tripping to the host, replaces the per-call alarm() watchdog with a repeating timer, fixes signal and ptrace handling inside the shim, and lets the Frama-C analyzer parse 5 more sources.

Futex

  • A FUTEX_WAIT with a moved word answers EAGAIN at EL1 (51 ns vs 2000 ns); the shim also spins on a matching word and serves timed waits, cutting a contended wake-wait-handoff from 1104 ns to 103 ns.
  • The EL1 wake path (77 ns vs 1927 ns for a wake with nobody parked) serves both wake shapes; it was briefly routed to the host when a contract assert flagged the bucket census, but the assert read a transient population and never survived a re-read, so the census holds and test-shim-futex-stats asserts the counters move.
  • Fixes undefined behavior in the FUTEX_WAKE_OP operand decode and masks an out-of-range shift operand to its low five bits, matching Linux; the shift fix is Linux commit 30d6e0a4190d, not CVE-2018-6927, which names a negative-count futex_requeue overflow still unmeasured in TODO.md.
  • Refuses to requeue a PI waiter, matching Linux.
  • Open defect: a signal during SVC return can re-execute the SVC as ENOSYS under load.

Watchdog, signals, and tooling

  • The run loop arms one repeating watchdog and publishes progress via a seqlock; this removes the two real syscalls per guest syscall that alarm() cost.
  • Signal delivery and ptrace stops taken inside the shim now establish EL0 before building a frame; PTRACE_INTERRUPT uses a new attention bit.
  • Adds Darwin-shaped stubs for sockaddr_un (one-byte family), sockaddr_storage, ipc_perm, msqid_ds, stat, and pthread_setname_np, plus check-stub-shadow to keep the rename trick sound; the gate honors the FRAMAC override, including an empty FRAMAC= as a clean skip.
  • Proves the futex deadline arithmetic (verify-futexdeadline discharges 128 of 128 obligations); futex_make_deadline stays unproved since the analyzer has no body for guest_read_small.
  • Five checks could not report what they guard: test-ptrace-interrupt's stop-PC ceiling never separated guest from shim PCs (now 16 GiB), test-matrix.sh counted that test without running it, bench-futex-contend ignored spawn results, two tests read errno after pthread_create, which never sets it, test-sleep-long accepted an unparsable argument, and test-shim-futex-stats aborted before its counter checks.