219 lines
8.5 KiB
Python
219 lines
8.5 KiB
Python
#!/usr/bin/env python3
|
|
# SPDX-License-Identifier: GPL-3.0-or-later
|
|
"""Pure offline trace model for a future nonblocking host adapter.
|
|
|
|
No socket, selector, address, DNS, OS call, real clock, CLI or file output is
|
|
present. The model only validates caller-supplied synthetic operation traces.
|
|
"""
|
|
|
|
from __future__ import annotations
|
|
|
|
from dataclasses import dataclass
|
|
import math
|
|
|
|
|
|
MAX_TRACE_EVENTS = 512
|
|
MAX_BATCH_BYTES = 1035
|
|
MAX_RECEIVE_BYTES = 65_536
|
|
MAX_DEADLINE_SECONDS = 10.0
|
|
|
|
RECEIPT_CREATED = "RECEIPT_CREATED"
|
|
SOCKET_CREATED = "SOCKET_CREATED"
|
|
SET_NONBLOCKING = "SET_NONBLOCKING"
|
|
CONNECT_IMMEDIATE = "CONNECT_IMMEDIATE"
|
|
CONNECT_PENDING = "CONNECT_PENDING"
|
|
READY_WRITE = "READY_WRITE"
|
|
SO_ERROR_ZERO = "SO_ERROR_ZERO"
|
|
SEND_BYTES = "SEND_BYTES"
|
|
READY_READ = "READY_READ"
|
|
RECV_BYTES = "RECV_BYTES"
|
|
RECV_EOF = "RECV_EOF"
|
|
WAIT_INTERRUPTED = "WAIT_INTERRUPTED"
|
|
WAIT_TIMEOUT = "WAIT_TIMEOUT"
|
|
DEADLINE_REACHED = "DEADLINE_REACHED"
|
|
SANITIZER_ACCEPTED = "SANITIZER_ACCEPTED"
|
|
LOCAL_CLOSE = "LOCAL_CLOSE"
|
|
OUTPUT_CREATED = "OUTPUT_CREATED"
|
|
|
|
OPERATIONS = {
|
|
RECEIPT_CREATED, SOCKET_CREATED, SET_NONBLOCKING, CONNECT_IMMEDIATE,
|
|
CONNECT_PENDING, READY_WRITE, SO_ERROR_ZERO, SEND_BYTES, READY_READ,
|
|
RECV_BYTES, RECV_EOF, WAIT_INTERRUPTED, WAIT_TIMEOUT, DEADLINE_REACHED,
|
|
SANITIZER_ACCEPTED, LOCAL_CLOSE, OUTPUT_CREATED,
|
|
}
|
|
|
|
|
|
class TraceModelError(RuntimeError):
|
|
"""Fail-closed synthetic trace error."""
|
|
|
|
|
|
@dataclass(frozen=True)
|
|
class TraceEvent:
|
|
operation: str
|
|
at_seconds: float
|
|
value: int = 0
|
|
|
|
def __post_init__(self) -> None:
|
|
if self.operation not in OPERATIONS:
|
|
raise TraceModelError("trace operation is invalid")
|
|
if not isinstance(self.at_seconds, (int, float)) or isinstance(
|
|
self.at_seconds, bool) or not math.isfinite(self.at_seconds) or \
|
|
self.at_seconds < 0:
|
|
raise TraceModelError("trace time is invalid")
|
|
if not isinstance(self.value, int) or isinstance(self.value, bool) or \
|
|
self.value < 0:
|
|
raise TraceModelError("trace value is invalid")
|
|
if self.operation not in {SEND_BYTES, RECV_BYTES} and self.value != 0:
|
|
raise TraceModelError("valueless trace operation has a value")
|
|
if self.operation in {SEND_BYTES, RECV_BYTES} and self.value == 0:
|
|
raise TraceModelError("byte operation has no progress")
|
|
|
|
|
|
@dataclass(frozen=True)
|
|
class TraceAssessment:
|
|
classification: str
|
|
batch_bytes_sent: int
|
|
receive_bytes: int
|
|
receipt_before_create: bool
|
|
nonblocking_before_connect: bool
|
|
complete_send_loop: bool
|
|
deadline_only_completion: bool
|
|
local_close_observed: bool
|
|
exact_identity_proven: bool = False
|
|
device_behavior_proven: bool = False
|
|
live_transport_present: bool = False
|
|
|
|
|
|
def assess_nonblocking_trace(
|
|
batch_size: int, deadline_seconds: float, events: tuple[TraceEvent, ...],
|
|
) -> TraceAssessment:
|
|
"""Validate one exact synthetic lifecycle; raise on every ambiguity."""
|
|
if not isinstance(batch_size, int) or isinstance(batch_size, bool) or \
|
|
not 1 <= batch_size <= MAX_BATCH_BYTES:
|
|
raise TraceModelError("batch size is invalid")
|
|
if not isinstance(deadline_seconds, (int, float)) or isinstance(
|
|
deadline_seconds, bool) or not math.isfinite(deadline_seconds) or \
|
|
not 0 < deadline_seconds <= MAX_DEADLINE_SECONDS:
|
|
raise TraceModelError("deadline is invalid")
|
|
if not isinstance(events, tuple) or not 1 <= len(events) <= MAX_TRACE_EVENTS or \
|
|
any(type(event) is not TraceEvent for event in events):
|
|
raise TraceModelError("trace shape is invalid")
|
|
|
|
state = "START"
|
|
last_time = -1.0
|
|
sent = 0
|
|
received = 0
|
|
write_ready = False
|
|
read_ready = False
|
|
connected = False
|
|
deadline_seen = False
|
|
sanitizer_seen = False
|
|
close_seen = False
|
|
|
|
for event in events:
|
|
if event.at_seconds < last_time:
|
|
raise TraceModelError("trace time moved backward")
|
|
last_time = float(event.at_seconds)
|
|
operation = event.operation
|
|
|
|
if deadline_seen and operation not in {
|
|
SANITIZER_ACCEPTED, LOCAL_CLOSE, OUTPUT_CREATED}:
|
|
raise TraceModelError("I/O occurred after deadline")
|
|
if not deadline_seen and event.at_seconds >= deadline_seconds and \
|
|
operation != DEADLINE_REACHED:
|
|
raise TraceModelError("nondeadline operation reached deadline")
|
|
|
|
if operation == RECEIPT_CREATED:
|
|
if state != "START":
|
|
raise TraceModelError("receipt ordering is invalid")
|
|
state = "RECEIPT"
|
|
elif operation == SOCKET_CREATED:
|
|
if state != "RECEIPT":
|
|
raise TraceModelError("socket creation precedes receipt")
|
|
state = "CREATED"
|
|
elif operation == SET_NONBLOCKING:
|
|
if state != "CREATED":
|
|
raise TraceModelError("nonblocking setup ordering is invalid")
|
|
state = "NONBLOCKING"
|
|
elif operation == CONNECT_IMMEDIATE:
|
|
if state != "NONBLOCKING":
|
|
raise TraceModelError("immediate connect ordering is invalid")
|
|
connected = True
|
|
state = "CONNECTED"
|
|
elif operation == CONNECT_PENDING:
|
|
if state != "NONBLOCKING":
|
|
raise TraceModelError("pending connect ordering is invalid")
|
|
state = "CONNECT_PENDING"
|
|
elif operation == READY_WRITE:
|
|
if state == "CONNECT_PENDING":
|
|
state = "CONNECT_READY"
|
|
elif connected and not deadline_seen:
|
|
write_ready = True
|
|
else:
|
|
raise TraceModelError("write readiness is unexpected")
|
|
elif operation == SO_ERROR_ZERO:
|
|
if state != "CONNECT_READY":
|
|
raise TraceModelError("SO_ERROR ordering is invalid")
|
|
connected = True
|
|
state = "CONNECTED"
|
|
elif operation == SEND_BYTES:
|
|
if not connected or not write_ready or sent >= batch_size:
|
|
raise TraceModelError("send ordering is invalid")
|
|
if event.value > batch_size - sent:
|
|
raise TraceModelError("send exceeded exact batch")
|
|
sent += event.value
|
|
write_ready = False
|
|
elif operation == READY_READ:
|
|
if not connected or sent != batch_size or deadline_seen:
|
|
raise TraceModelError("read readiness is unexpected")
|
|
read_ready = True
|
|
elif operation == RECV_BYTES:
|
|
if not read_ready:
|
|
raise TraceModelError("receive occurred without readiness")
|
|
if received + event.value > MAX_RECEIVE_BYTES:
|
|
raise TraceModelError("receive bound exceeded")
|
|
received += event.value
|
|
read_ready = False
|
|
elif operation == RECV_EOF:
|
|
raise TraceModelError("EOF is not a completion event")
|
|
elif operation in {WAIT_INTERRUPTED, WAIT_TIMEOUT}:
|
|
if not connected or deadline_seen:
|
|
raise TraceModelError("wait event ordering is invalid")
|
|
write_ready = False
|
|
read_ready = False
|
|
elif operation == DEADLINE_REACHED:
|
|
if event.at_seconds < deadline_seconds or not connected or \
|
|
sent != batch_size or received == 0:
|
|
raise TraceModelError("deadline preconditions are incomplete")
|
|
deadline_seen = True
|
|
write_ready = False
|
|
read_ready = False
|
|
elif operation == SANITIZER_ACCEPTED:
|
|
if not deadline_seen or sanitizer_seen:
|
|
raise TraceModelError("sanitizer ordering is invalid")
|
|
sanitizer_seen = True
|
|
elif operation == LOCAL_CLOSE:
|
|
if not deadline_seen or not sanitizer_seen or close_seen:
|
|
raise TraceModelError("local close ordering is invalid")
|
|
close_seen = True
|
|
elif operation == OUTPUT_CREATED:
|
|
if not close_seen or state == "COMPLETE":
|
|
raise TraceModelError("output ordering is invalid")
|
|
state = "COMPLETE"
|
|
else:
|
|
raise TraceModelError("unhandled trace operation")
|
|
|
|
if state != "COMPLETE" or not deadline_seen or not sanitizer_seen or \
|
|
not close_seen or sent != batch_size:
|
|
raise TraceModelError("trace is incomplete")
|
|
return TraceAssessment(
|
|
classification="OFFLINE_NONBLOCKING_SEQUENCE_FEASIBLE",
|
|
batch_bytes_sent=sent,
|
|
receive_bytes=received,
|
|
receipt_before_create=True,
|
|
nonblocking_before_connect=True,
|
|
complete_send_loop=True,
|
|
deadline_only_completion=True,
|
|
local_close_observed=True,
|
|
)
|