"""libos port receive-path model (the B5 message-loop blocker, first half). Status: **offline development tool (new, additive)**. This module models the part of the GSP firmware's libos *port receive* machinery that the B3 message-loop task needs before it can make progress: the argument contract of ``TASK_PORT_SEND_RECV_WAIT`` (syscall 1), the asynchronous receive post, the synchronous send/reply, the cross-payload handoff performed when a receive completes, and the external-interrupt port retirement that a host doorbell wake performs. Evidence kind: **firmware use + RTOS port implementation** (the same evidence class as :mod:`sim.libos`). Every structure below was observed on the real 570.144 image, not inferred from a stub: * the message-loop task posts four asynchronous receives through a wrapper at firmware vaddr ``0x4018000`` that moves its arguments ``a0-a3`` into ``a4-a7``, zeroes ``a0-a3`` and ``t1``/``t2``, and executes ``ecall`` with ``t0 = 1`` (an async receive post): ``(shuttle 10, port 6, payload 0, size 0)`` immediately followed by ``INTERRUPT_ARM_EXTERNAL(0xFF)`` -- the external-interrupt receive; ``(shuttle 11, port 7, payload 0x5ba8e10, size 4)``; ``(shuttle 9, port 8, payload 0x4015070, size 0x808)``; ``(shuttle 14, port 13, payload 0x5ba8e20, size 0x24)``; * it then performs one synchronous send on the default shuttle id (1) to port 12 with a zero-length payload, ``waitId = 1``, ``timeout = -1`` (infinite); * it blocks in ``PortWait(LIBOS_SHUTTLE_ANY, timeout = -1)`` (ecall at ``0x4019df4``); * on an external interrupt the port that was armed retires with ``error_code = LIBOS_OK`` and ``payload_size = 0`` (the report path), and the wait returns with ``a0 = status``, ``a4 = completedSize``, ``a5 = completedRemoteTaskId``, ``a6 = completedShuttle``. The argument contract modelled (mirrors the RTOS ``libosPortSendRecvAndWait``): =============== ========================================================= register meaning at ``ecall`` =============== ========================================================= ``t0`` syscall number (1) ``a0`` send shuttle id (0 = none) ``a1`` send port id ``a2``/``a3`` send payload address / size ``a4`` receive shuttle id (0 = none) ``a5`` receive port id ``a6``/``a7`` receive payload address / capacity ``t1`` wait id (0 = do not block, ``0xFFFF`` = any) ``t2`` timeout in ns (``0xFFFFFFFFFFFFFFFF`` = infinite) =============== ========================================================= On return: ``a0`` = status, ``a4`` = completed size, ``a5`` = originating task id, ``a6`` = completed shuttle (local handle). Honesty rules (mandatory; docs/51 section 6, docs/06-ACCURACY.md): * the model is **data-driven by observation**: port roles come from the posted receive sequence of the real image; nothing infers a port number that was not observed; * every modelled event carries ``"modelled": true`` and a label -- the host doorbell wake is ``shim:host-doorbell-wake``, the boot handshake send is ``modelled:peer-consumes-on-send``. These are not firmware behaviour; * **receives are never completed with invented payloads**: a wake only retires the external-interrupt receive with the RTOS report contract (rare, zero length). No command, status or event payload is fabricated; * wait semantics are strictly "return the first completed shuttle or stop"; the model never returns from a blocking wait that nothing completed; * L0/L1 only: no timing (L2) and no device-environment (L3) claim; with a single modelled task there is no scheduler and no other task is run. Development-only, offline: no GPU, kernel module, mdev, guest, network, QEMU, ``/dev`` access or reboot. Nothing here is a product dependency and nothing is injected into a guest. """ from __future__ import annotations from sim.libos import ( INTERRUPT_ARM_EXTERNAL, NAMES, TASK_PORT_SEND_RECV_WAIT, ) #: Report schema tag for :meth:`LibosPortModel.state`. REPORT_FORMAT = "greeneye-msgq-port/1" #: ``LIBOS_SHUTTLE_ANY`` (RTOS port API). SHUTTLE_ANY = 0xFFFF #: The task's default shuttle id (RTOS port API). SHUTTLE_DEFAULT = 1 #: ``LIBOS_TIMEOUT_INFINITE``. TIMEOUT_INFINITE = 0xFFFFFFFFFFFFFFFF #: LIBOS_OK. LIBOS_OK = 0 #: Observed port roles for the real 570.144 message-loop task. The values are #: the port ids carried by the task's posted receives (resource handles); the #: labels describe behaviour only. PORT_ROLES = { 6: "extintr", # external-interrupt receive (armed with 0xFF) 7: "notification", # 4-byte notification buffer 8: "request", # 0x808-byte request/reply buffer 12: "handshake", # zero-length boot handshake send target 13: "event", # 36-byte event buffer } #: Port label used when a port was not part of the observed post sequence. ROLE_DATA = "data" #: The wake contract observed for the external-interrupt receive: the RTOS #: report retires the waiting shuttle with error LIBOS_OK and a zero payload. EXTINTR_WAKE_CONTRACT = "shim:host-doorbell-wake" HANDSHAKE_CONTRACT = "modelled:peer-consumes-on-send" def role_for(port: int) -> str: """Role label for a port id (observed table; ``"data"`` otherwise).""" return PORT_ROLES.get(int(port), ROLE_DATA) class LibosPortModel: """Deterministic model of the libos receive path for one GSP task. The model is a ``Machine.syscall_handler``: it owns syscall 1 (``TASK_PORT_SEND_RECV_WAIT``) and the interrupt-arm call, and delegates every other syscall to ``base`` (:class:`sim.libos.LibosSyscalls`, which keeps recording). ``machine.x`` is the only machine state touched. """ name = "libos-port-model" def __init__(self, base=None, *, task: str = "gsp-rm-task"): self.base = base self.task = task #: Async receive posts in observation order. self.posts: list[dict] = [] #: Pending receives by shuttle id. self.pending: dict[int, dict] = {} #: Completed handoffs awaiting a wait (FIFO). self.completed: list[dict] = [] #: Synchronous sends observed (send payloads are not copied; the peer #: side is not modelled). self.sends: list[dict] = [] #: Blocking waits observed. self.waits: list[dict] = [] #: Labelled model events (every one is explicitly ``modelled``). self.events: list[dict] = [] #: External interrupt mask last armed (RTOS ``IRQMSET`` semantics). #: An installed base model may already have observed an arm before this #: model was attached (the recorded boot arm), so seed from it. self.armed_mask = int(getattr(base, "armed_mask", 0)) #: Recorded host doorbell wakes. self.host_kicks = 0 #: Host wakes not yet handed to a receive (the firmware may post and #: arm after the host has rung the doorbell; the pending interrupt is #: delivered at the first armed receive). self.kicks_pending = 0 #: The request that stopped the run (unmodelled or blocking), if any. self.stopped: dict | None = None # -- observation ------------------------------------------------------- def _event(self, name: str, **fields) -> dict: event = {"event": name, "modelled": True, "task": self.task} event.update(fields) self.events.append(event) return event def host_kick(self, *, label=EXTINTR_WAKE_CONTRACT, queue=None, value=None, bit=None) -> dict: """Record the host doorbell write; deliver it when a receive is armed. The host submit path writes ``NV_PGSP_QUEUE_HEAD(0)``; the mapping from that write to a falcon interrupt bit is **not modelled** (unobserved). The wake is delivered to the external-interrupt receive once it has been posted and interrupts are armed (the firmware may do both after the host has already rung). Returns the event; ``"delivered"`` is the retired shuttle id, or ``None`` when the wake remains pending. """ self.host_kicks += 1 self.kicks_pending += 1 delivered = self._try_kick() return self._event( "host_kick", contract=label, queue=queue, value=value, falcon_irq_bit=bit, delivered=delivered, pending=bool(self.kicks_pending), note=("queue-head write -> falcon interrupt bit is unobserved; " "the wake is the documented shim"), ) def _try_kick(self): """Deliver one pending host wake to an armed extintr receive, if any.""" if not self.kicks_pending or not self.armed_mask: return None for shuttle in sorted(self.pending): post = self.pending[shuttle] if post["role"] != "extintr": continue self.kicks_pending -= 1 self._complete( shuttle, payload_size=0, origin_task=0, contract=EXTINTR_WAKE_CONTRACT, reason="external-interrupt report (armed mask " f"{self.armed_mask:#x}, pending host doorbell wake)", ) return shuttle return None def _complete(self, shuttle: int, *, payload_size: int, origin_task: int, contract: str, reason: str) -> dict: post = self.pending.pop(int(shuttle)) entry = { "shuttle": int(shuttle), "port": int(post["port"]), "role": post["role"], "payload": int(post["payload"]), "capacity": int(post["capacity"]), "payload_size": int(payload_size), "origin_task": int(origin_task), "contract": contract, "reason": reason, "post_pc": int(post["pc"]), } self.completed.append(entry) self._event("receive_complete", **entry) return entry # -- syscall surface --------------------------------------------------- def handle(self, machine, pc: int = 0): """``Machine`` syscall hook: ``(handled, result)``.""" num = int(machine.x[5]) if num == TASK_PORT_SEND_RECV_WAIT: return self._handle_port(machine, pc) if num == INTERRUPT_ARM_EXTERNAL: self.armed_mask |= int(machine.x[10]) self._event("interrupt_arm_external", mask=int(machine.x[10]), pc=pc) self._try_kick() if self.base is not None: handled, result = self.base.handle(machine, pc) else: handled, result = (True, LIBOS_OK) if num == INTERRUPT_ARM_EXTERNAL \ else (False, None) if not handled and self.stopped is None: entry = getattr(self.base, "stopped", None) number = int(entry["num"]) if entry else num self.stopped = { "num": number, "name": (entry or {}).get("name", NAMES.get(number, f"unknown_{number}")), "pc": int(pc), "reason": "unmodelled-syscall", } return handled, result def _handle_port(self, machine, pc: int): a0, a1, a2, a3 = (int(machine.x[10]), int(machine.x[11]), int(machine.x[12]), int(machine.x[13])) a4, a5, a6, a7 = (int(machine.x[14]), int(machine.x[15]), int(machine.x[16]), int(machine.x[17])) t1, t2 = int(machine.x[6]), int(machine.x[7]) send = a0 != 0 or a1 != 0 recv = a4 != 0 or a5 != 0 if recv: self._post(shuttle=a4, port=a5, payload=a6, capacity=a7, pc=pc, wait_id=t1, timeout=t2) if send: self._send(shuttle=a0, port=a1, payload=a2, size=a3, wait_id=t1, timeout=t2, pc=pc, machine=machine) return True, LIBOS_OK if recv: # Async receive post: the kernel returns LIBOS_OK without touching # the wait outputs (a4-a6 still hold the receive arguments). return True, LIBOS_OK # Pure blocking wait: return the first completed shuttle, or stop. if not self.completed: self._try_kick() if self.completed: entry = self.completed.pop(0) machine.x[14] = entry["payload_size"] & 0xFFFFFFFFFFFFFFFF machine.x[15] = entry["origin_task"] & 0xFFFFFFFFFFFFFFFF machine.x[16] = entry["shuttle"] & 0xFFFFFFFFFFFFFFFF machine.x[17] = 0 record = { "pc": int(pc), "wait_id": t1, "timeout": t2, "completed": entry["shuttle"], "payload_size": entry["payload_size"], "origin_task": entry["origin_task"], "role": entry["role"], "contract": entry["contract"], } self.waits.append(record) self._event("wait_complete", **record) return True, LIBOS_OK record = { "pc": int(pc), "wait_id": t1, "timeout": t2, "reason": "port-wait-blocks", "pending": sorted(self.pending), } self.waits.append(record) self._event("wait_block", **record) if self.stopped is None: self.stopped = { "num": TASK_PORT_SEND_RECV_WAIT, "name": "task_port_send_recv_wait", "pc": int(pc), "reason": "port-wait-blocks", "pending": sorted(self.pending), } return False, None def _post(self, *, shuttle: int, port: int, payload: int, capacity: int, pc: int, wait_id: int, timeout: int) -> dict: post = { "shuttle": int(shuttle), "port": int(port), "role": role_for(port), "payload": int(payload), "capacity": int(capacity), "pc": int(pc), "wait_id": int(wait_id), "timeout": int(timeout), } self.posts.append(post) self.pending[int(shuttle)] = post self._event("receive_post", **post) self._try_kick() return post def _send(self, *, shuttle: int, port: int, payload: int, size: int, wait_id: int, timeout: int, pc: int, machine) -> dict: """Model a synchronous send/reply as completed by its peer. Only the boot handshake shape was observed (zero-length payload to port 12 on the default shuttle). The peer is not modelled: consumption is an explicit, labelled assumption. The wait outputs receive the RTOS transcribe contract for a completed send (``a4`` = copied size, ``a5`` = 0, ``a6`` = send shuttle). """ record = { "shuttle": int(shuttle), "port": int(port), "role": role_for(port) if port else "reply", "payload": int(payload), "size": int(size), "pc": int(pc), "wait_id": int(wait_id), "timeout": int(timeout), "contract": HANDSHAKE_CONTRACT, } self.sends.append(record) machine.x[14] = int(size) & 0xFFFFFFFFFFFFFFFF machine.x[15] = 0 machine.x[16] = int(shuttle) & 0xFFFFFFFFFFFFFFFF machine.x[17] = 0 self._event("send_complete", **record) return record # -- report surface ---------------------------------------------------- def state(self) -> dict: """Deterministic serialisable state for the ``greeneye-msgq-attach/1`` report (no host timestamps).""" return { "format": REPORT_FORMAT, "task": self.task, "armed_mask": int(self.armed_mask), "host_kicks": int(self.host_kicks), "kicks_pending": int(self.kicks_pending), "posts": [dict(post) for post in self.posts], "pending": sorted(self.pending), "completed": [dict(entry) for entry in self.completed], "sends": [dict(record) for record in self.sends], "waits": [dict(record) for record in self.waits], "events": [dict(event) for event in self.events], "stopped": dict(self.stopped) if self.stopped else None, }