The interpreter shall be resumable
Operation with fuel or other implementations of bounded run-time requires that the interpreter can be halted. Conversely, later on the interpreter may be resumed, as if it was not halted in the first place.
-
1.6.1. Stackless UID: REQ-2 parent relations: STATEMENT: The interpreter shall be stackless
RATIONALE: A stackless interpreter is one that does not use function calls in the host environment to implement function calls inside the interpreter. Instead, the stack of the interpreted bytecode is stored in a traditional data structure (such as a Vec<u8>). Interpretation can be interrupted between any two virtual instructions of the bytecode, and crucially so resumed from there.
Further information: https://kyju.org/blog/piccolo-a-stackless-lua-interpreter/#a-stackless-interpreter-design
The interpreter shall be executable on bare-metal environments
No reliance on any specific functionality from the provided execution environment is acceptable, as the interpreter shall be ready for embedding to any environment that Rust can compile for.
-
1.6.2. no_std UID: REQ-4 parent relations: STATEMENT: The interpreter shall be implemented in no_std Rust
RATIONALE: Only relying on the functionality that is provided by no_std enables execution on bare environments where operating system is available.
COMMENT: Reliance on alloc is allowable, as an allocator can be implemented without further reliance on the execution environment.
The interpreter shall yield back control flow eventually
A user shall be able to call the interpreter with a bound, expecting a result in a finite amount of time or bytecode operations. Even if the bytecode itself does never finish execution (i.e. due to a infinite loop), the interpreter shall yield eventually, by pausing the bytecode execution.
It is not acceptable to constraint the interpreter to only those bytecode instances for which the halting-problem is solvable.
-
1.6.3. Fuel UID: REQ-6 parent relations: STATEMENT: The interpreter shall support fuel bounded execution
RATIONALE: Fuel is a mechanism to limit the amount of bytecode operations conducted when calling the interpreter. Each bytecode instruction is associated with a specific amount of fuel consumed when executing it. The interpreter is provided a finite amount of fuel, that is deplete during execution, until the amount of fuel is insufficient to conduct further bytecode operations. At this point, the interpreter yields back the control flow. Later on, the execution may be resumed.
Further information: https://docs.rs/wasmtime/latest/wasmtime/struct.Config.html#method.consume_fuel
The interpreter state shall be able to halt on one computer and continue execution on another
This enables various workflows in deployments of multiple computers. For load-balancing or redundancy purposes, running applications can be migrated to other computers without disruption.
-
1.6.4. De-/Serializable UID: REQ-13 parent relations: STATEMENT: The interpreter state shall be de-/serializable
RATIONALE: If the interpreter state can be serialized to and deserialized from a canonical representation, migration to other computers as well as check-point/lock-step like execution become simple to implement.
No dependencies but those explicitly allowed by a requirement shall be used
Dependencies have to forego the full V&V process as well, which quickly adds enormous work.
This requirement constraints the usage and introduction of normal dependencies, but not Dev Dependencies [1] and not Build Dependencies [2] .
[1] | https://doc.rust-lang.org/cargo/reference/specifying-dependencies.html#development-dependencies |
[2] | https://doc.rust-lang.org/cargo/reference/specifying-dependencies.html#build-dependencies |
Exceptions to this, i.e. allowed dependencies, must refer to this requirement as their parent.
All requirements that allow a dependency must specify the exact version of the dependency (at least major, minor and patch release)
-
1.6.5. Allow log dependency UID: REQ-15 parent relations: STATEMENT: The interpreter shall have an optional dependency on the log crate version 0.4.22
RATIONALE: Logging is an essential tool to make a system observable, and aid in debugging. Bespoke crate is widely used in the Rust ecosystem and can be attached to any (or no) logging backend. Using conditional compilation, all of the log crate's footprint in the WASM interpreter (foremost the debug, error, info, trace and warn macro) can be expanded to empty statements to avoid any run-time impact when opting out of the dependency on log.
-
1.6.6. Allow libm dependency UID: REQ-16 parent relations: STATEMENT: The interpreter may depend on the libm crate version 0.2.8
RATIONALE: Rust does not expose all floating point operations in a bare-metal (as in no_std) target, as to not introduce any dependency on the C standard library's libm (respective PR: https://github.com/rust-lang/rust/pull/27823). However, we identified at least the following operations to be required for WASM interpretation while unavailable in no_std:
- abs
- ceil
- floor
- trunc
- round
- sqrt
- copysign
In order use these operations, having the libm crate as dependencies of the WASM interpreter is an acceptable trade-off.
-
1.1. Resumable UID: REQ-1 child relations: STATEMENT: The interpreter shall be resumable
RATIONALE: Operation with fuel or other implementations of bounded run-time requires that the interpreter can be halted. Conversely, later on the interpreter may be resumed, as if it was not halted in the first place.
The interpreter shall be stackless
A stackless interpreter is one that does not use function calls in the host environment to implement function calls inside the interpreter. Instead, the stack of the interpreted bytecode is stored in a traditional data structure (such as a Vec<u8>). Interpretation can be interrupted between any two virtual instructions of the bytecode, and crucially so resumed from there.
Further information: https://kyju.org/blog/piccolo-a-stackless-lua-interpreter/#a-stackless-interpreter-design
-
1.2. Baremetal UID: REQ-3 child relations: STATEMENT: The interpreter shall be executable on bare-metal environments
RATIONALE: No reliance on any specific functionality from the provided execution environment is acceptable, as the interpreter shall be ready for embedding to any environment that Rust can compile for.
The interpreter shall be implemented in no_std Rust
Only relying on the functionality that is provided by no_std enables execution on bare environments where operating system is available.
Reliance on alloc is allowable, as an allocator can be implemented without further reliance on the execution environment.
-
1.3. Bounded execution UID: REQ-5 child relations: STATEMENT: The interpreter shall yield back control flow eventually
RATIONALE: A user shall be able to call the interpreter with a bound, expecting a result in a finite amount of time or bytecode operations. Even if the bytecode itself does never finish execution (i.e. due to a infinite loop), the interpreter shall yield eventually, by pausing the bytecode execution.
COMMENT: It is not acceptable to constraint the interpreter to only those bytecode instances for which the halting-problem is solvable.
The interpreter shall support fuel bounded execution
Fuel is a mechanism to limit the amount of bytecode operations conducted when calling the interpreter. Each bytecode instruction is associated with a specific amount of fuel consumed when executing it. The interpreter is provided a finite amount of fuel, that is deplete during execution, until the amount of fuel is insufficient to conduct further bytecode operations. At this point, the interpreter yields back the control flow. Later on, the execution may be resumed.
Further information: https://docs.rs/wasmtime/latest/wasmtime/struct.Config.html#method.consume_fuel
-
1.4. Migrateable UID: REQ-12 child relations: STATEMENT: The interpreter state shall be able to halt on one computer and continue execution on another
RATIONALE: This enables various workflows in deployments of multiple computers. For load-balancing or redundancy purposes, running applications can be migrated to other computers without disruption.
The interpreter state shall be de-/serializable
If the interpreter state can be serialized to and deserialized from a canonical representation, migration to other computers as well as check-point/lock-step like execution become simple to implement.
-
1.5. No Dependencies UID: REQ-14 child relations: STATEMENT: No dependencies but those explicitly allowed by a requirement shall be used
RATIONALE: Dependencies have to forego the full V&V process as well, which quickly adds enormous work.
COMMENT: This requirement constraints the usage and introduction of normal dependencies, but not Dev Dependencies [1] and not Build Dependencies [2] .
[1] https://doc.rust-lang.org/cargo/reference/specifying-dependencies.html#development-dependencies [2] https://doc.rust-lang.org/cargo/reference/specifying-dependencies.html#build-dependencies COMMENT: Exceptions to this, i.e. allowed dependencies, must refer to this requirement as their parent.
COMMENT: All requirements that allow a dependency must specify the exact version of the dependency (at least major, minor and patch release)
The interpreter shall have an optional dependency on the log crate version 0.4.22
Logging is an essential tool to make a system observable, and aid in debugging. Bespoke crate is widely used in the Rust ecosystem and can be attached to any (or no) logging backend. Using conditional compilation, all of the log crate's footprint in the WASM interpreter (foremost the debug, error, info, trace and warn macro) can be expanded to empty statements to avoid any run-time impact when opting out of the dependency on log.
-
1.5. No Dependencies UID: REQ-14 child relations: STATEMENT: No dependencies but those explicitly allowed by a requirement shall be used
RATIONALE: Dependencies have to forego the full V&V process as well, which quickly adds enormous work.
COMMENT: This requirement constraints the usage and introduction of normal dependencies, but not Dev Dependencies [1] and not Build Dependencies [2] .
[1] https://doc.rust-lang.org/cargo/reference/specifying-dependencies.html#development-dependencies [2] https://doc.rust-lang.org/cargo/reference/specifying-dependencies.html#build-dependencies COMMENT: Exceptions to this, i.e. allowed dependencies, must refer to this requirement as their parent.
COMMENT: All requirements that allow a dependency must specify the exact version of the dependency (at least major, minor and patch release)
The interpreter may depend on the libm crate version 0.2.8
Rust does not expose all floating point operations in a bare-metal (as in no_std) target, as to not introduce any dependency on the C standard library's libm (respective PR: https://github.com/rust-lang/rust/pull/27823). However, we identified at least the following operations to be required for WASM interpretation while unavailable in no_std:
- abs
- ceil
- floor
- trunc
- round
- sqrt
- copysign
In order use these operations, having the libm crate as dependencies of the WASM interpreter is an acceptable trade-off.
The interpreter shall compile on Rust 1.76.0 and later versions
An MSRV should be clearly stated to specify which toolchain is acceptable.
The interpreter shall implement means for instrumentation
Instrumentation is needed to generate evidence for certification. Instrumentation eases debugging. Instrumentation enables elaborate run-time monitoring.
-
2.2.1. Statement Coverage UID: REQ-8 parent relations: STATEMENT: The instrumentation shall enable the measurement of statement coverage
RATIONALE: Statement coverage is required by DO-178C starting at DAL-C (6.4.4.c)
-
2.2.2. Decision Coverage UID: REQ-9 parent relations: STATEMENT: The instrumentation shall enable the measurement of decision coverage
RATIONALE: Decision coverage is required by DO-178C starting at DAL-B (6.4.4.c)
-
2.2.3. Modified Condition/Decision Coverage UID: REQ-10 parent relations: STATEMENT: The instrumentation shall enable the measurement of modified condition/decision coverage
RATIONALE: Modified condition/decision coverage is required by DO-178C starting at DAL-A (6.4.4.c)
-
2.1. Instrumentation UID: REQ-7 child relations: STATEMENT: The interpreter shall implement means for instrumentation
RATIONALE: Instrumentation is needed to generate evidence for certification. Instrumentation eases debugging. Instrumentation enables elaborate run-time monitoring.
-
2.2.4. Certification Evidence UID: REQ-11 child relations: STATEMENT: The interpreter shall support the generation of certification evidence
The instrumentation shall enable the measurement of statement coverage
Statement coverage is required by DO-178C starting at DAL-C (6.4.4.c)
-
2.1. Instrumentation UID: REQ-7 child relations: STATEMENT: The interpreter shall implement means for instrumentation
RATIONALE: Instrumentation is needed to generate evidence for certification. Instrumentation eases debugging. Instrumentation enables elaborate run-time monitoring.
-
2.2.4. Certification Evidence UID: REQ-11 child relations: STATEMENT: The interpreter shall support the generation of certification evidence
The instrumentation shall enable the measurement of decision coverage
Decision coverage is required by DO-178C starting at DAL-B (6.4.4.c)
-
2.1. Instrumentation UID: REQ-7 child relations: STATEMENT: The interpreter shall implement means for instrumentation
RATIONALE: Instrumentation is needed to generate evidence for certification. Instrumentation eases debugging. Instrumentation enables elaborate run-time monitoring.
-
2.2.4. Certification Evidence UID: REQ-11 child relations: STATEMENT: The interpreter shall support the generation of certification evidence
The instrumentation shall enable the measurement of modified condition/decision coverage
Modified condition/decision coverage is required by DO-178C starting at DAL-A (6.4.4.c)
The interpreter shall support the generation of certification evidence
-
2.2.1. Statement Coverage UID: REQ-8 parent relations: STATEMENT: The instrumentation shall enable the measurement of statement coverage
RATIONALE: Statement coverage is required by DO-178C starting at DAL-C (6.4.4.c)
-
2.2.2. Decision Coverage UID: REQ-9 parent relations: STATEMENT: The instrumentation shall enable the measurement of decision coverage
RATIONALE: Decision coverage is required by DO-178C starting at DAL-B (6.4.4.c)
-
2.2.3. Modified Condition/Decision Coverage UID: REQ-10 parent relations: STATEMENT: The instrumentation shall enable the measurement of modified condition/decision coverage
RATIONALE: Modified condition/decision coverage is required by DO-178C starting at DAL-A (6.4.4.c)