132 lines
5.8 KiB
Markdown
132 lines
5.8 KiB
Markdown
# Dynamic Semantics - Execution Model Decision
|
|
|
|
Status: Accepted (Implemented)
|
|
Cycle: Initial execution-model closure pass
|
|
|
|
## 1. Context
|
|
|
|
PBS needs a closed execution-model baseline before effect surfaces and memory/lifetime semantics can be specified normatively.
|
|
|
|
The key open questions were:
|
|
|
|
- whether execution is single-threaded per program instance,
|
|
- which runtime effects are observable to user code,
|
|
- what the default evaluation order is,
|
|
- which constructs guarantee single evaluation,
|
|
- how abrupt completion behaves,
|
|
- how `result<Error>` differs from `trap`,
|
|
- and how host calls interact with `FRAME_SYNC` without perturbing user-visible sequencing.
|
|
|
|
## 2. Decision
|
|
|
|
PBS v1 adopts the following execution-model baseline:
|
|
|
|
1. Execution is single-threaded per program instance.
|
|
2. User-visible execution is deterministic and does not expose concurrent interleaving.
|
|
3. The default evaluation rule is strict left-to-right unless a construct explicitly states otherwise.
|
|
4. Call evaluation proceeds by forming the call target first, then evaluating arguments left-to-right, then invoking the target.
|
|
5. Abrupt completion terminates the current construct immediately and prevents later sibling evaluation.
|
|
6. Recoverable, expected failures belong to `result<Error>`, not to `trap`.
|
|
7. `trap` is reserved for non-recoverable runtime failures outside ordinary userland error flow.
|
|
8. Any trap aborts the current PBS program execution rather than returning control to ordinary userland flow.
|
|
9. `FRAME_SYNC` is the only normative safepoint in PBS v1.
|
|
10. `FRAME_SYNC` remains the execution boundary for userland progress; host-side work during that boundary must not reorder PBS-observable semantics.
|
|
|
|
## 3. Invariants
|
|
|
|
- PBS v1 does not expose a user-visible concurrent execution model.
|
|
- User-visible sequencing is defined by evaluation order, branch selection, abrupt completion, result propagation, trap propagation, and host-call boundaries.
|
|
- Traps are not recoverable in userland and do not resume PBS execution.
|
|
- VM-internal frame layout, temporary storage, and lowering steps are not observable unless they change the semantic effects above.
|
|
- Unless a construct states otherwise, subexpressions are evaluated once and in left-to-right order.
|
|
- `return`, `break`, `continue`, result propagation via `!`, and `trap` abort further evaluation in the current construct.
|
|
- Host calls must not introduce user-visible reordering of already-defined PBS evaluation order.
|
|
- No normative safepoint exists in v1 other than `FRAME_SYNC`.
|
|
|
|
## 4. Call Evaluation Rule
|
|
|
|
The runtime call rule for v1 is:
|
|
|
|
1. Form the call target.
|
|
2. Evaluate any receiver that participates in target formation.
|
|
3. Evaluate arguments in source order from left to right.
|
|
4. Invoke the resolved target.
|
|
5. Produce one of:
|
|
- normal return,
|
|
- explicit `result<Error>` propagation,
|
|
- or `trap`.
|
|
|
|
This rule applies to canonical `apply` and to ordinary call sugar that desugars to `apply`.
|
|
|
|
## 5. Error Boundary
|
|
|
|
`result<Error>` and `trap` are distinct runtime categories.
|
|
|
|
### 5.1 `result<Error>`
|
|
|
|
`result<Error>` is the required mechanism for failures that are:
|
|
|
|
- expected by the API contract,
|
|
- recoverable in ordinary userland control flow,
|
|
- modelable through an explicit PBS error type.
|
|
|
|
Such failures may be:
|
|
|
|
- processed with `handle`,
|
|
- propagated with `!`,
|
|
- and discussed as part of ordinary function contract design.
|
|
|
|
### 5.2 `trap`
|
|
|
|
`trap` is reserved for failures that are:
|
|
|
|
- outside the ordinary userland contract,
|
|
- not suitably representable as the declared `result<Error>` surface,
|
|
- caused by runtime or host invariant failure,
|
|
- or severe enough that ordinary userland recovery is not part of the v1 language model.
|
|
|
|
PBS v1 does not define `try/catch` for traps.
|
|
Traps are not part of ordinary recoverable control flow.
|
|
Once a trap is raised, PBS userland execution aborts and control transfers to runtime or firmware crash handling outside the ordinary language model.
|
|
|
|
## 6. Consequences
|
|
|
|
- User-authored code does not explicitly throw traps as part of ordinary PBS semantics.
|
|
- API surfaces must not use trap as a substitute for a modelable `result<Error>` failure.
|
|
- Host-backed operations must expose predictable operational failures through `result<Error>` when those failures are part of the callable contract.
|
|
- Residual host or runtime failures that cannot be represented by the declared PBS contract may still trap.
|
|
- The language-level consequence of trap is program abort rather than catchable failure handling.
|
|
- In v1, no safepoint inventory is normative beyond `FRAME_SYNC`.
|
|
|
|
## 7. Explicit Non-Decisions
|
|
|
|
This decision does not yet close:
|
|
|
|
- the exact list of constructs with explicit single-evaluation wording as finally integrated into the dynamic-semantics spec,
|
|
- the final wording split between dynamic semantics and runtime-initialization for trap/crash handoff.
|
|
|
|
Those points must be integrated by the remaining dynamic-semantics and memory/lifetime decisions.
|
|
|
|
## 8. Spec Impact
|
|
|
|
This decision should feed at least:
|
|
|
|
- `docs/pbs/specs/9. Dynamic Semantics Specification.md`
|
|
- `docs/pbs/specs/10. Memory and Lifetime Specification.md`
|
|
- `docs/general/specs/16. Runtime Execution and Initialization Specification.md`
|
|
|
|
It should also constrain future work in:
|
|
|
|
- `docs/pbs/specs/12. Diagnostics Specification.md`
|
|
- `docs/general/specs/13. Conformance Test Specification.md`
|
|
|
|
## 9. Validation Notes
|
|
|
|
The intended rule is:
|
|
|
|
- expected domain failure: `result<Error>`
|
|
- remappable, processable, or propagatable failure: `result<Error>`
|
|
- runtime invariant breakage or non-contract catastrophic failure: `trap`
|
|
|
|
In practical terms, a host-backed API must not rely on trap for ordinary operational failures if those failures can be declared and modeled explicitly in PBS. The only normative safepoint in v1 is `FRAME_SYNC`, and any trap aborts PBS userland execution rather than returning through an in-language recovery path.
|