| c53c6fe9 | 11-Aug-2025 |
Andrew Jeffery <andrew@codeconstruct.com.au> |
dsp: firmware_update: Run-time state machine for package parsing
Encoding the necessary sequence of calls with an approximation of linear
types is hampered by DSP0267's introduction of entirely new
dsp: firmware_update: Run-time state machine for package parsing
Encoding the necessary sequence of calls with an approximation of linear
types is hampered by DSP0267's introduction of entirely new sections
into the package format across revisions. The existing design enforced a
sequence that precluded _not_ calling the decoder for downstream device
records in the case of pinning to format revision 1. The choice had the
further effect of stunting the API to future expansion of the spec.
Switch from linear types to tracking parse state at runtime based on the
provided pin and the extracted package header.
The state machine implementation is modeled on the TLA+ specification
below, with NR_FORMATS set to 4 in the model:
```tla
---- MODULE pldm_package_parser ----
EXTENDS Integers, Sequences
\* pin and format have non-deterministic init, but are then constant
VARIABLE state, pin, format
vars == << state, pin, format >>
States == {
"Init",
"Header",
"FirmwareDevices",
"DownstreamDevices",
"ComponentImageInfos",
"Complete",
"Unsupported",
"Error"
}
Formats == 1..4
DecodeHeader ==
/\ state = "Init"
/\ state' = IF format <= pin THEN "Header" ELSE "Unsupported"
/\ UNCHANGED << pin, format >>
DecodeFirmwareDevices ==
/\ state = "Header"
/\ state' = "FirmwareDevices"
/\ UNCHANGED << pin, format >>
DecodeDownstreamDevices ==
/\ state = "FirmwareDevices"
/\ state' = IF pin = 1 THEN "Error" ELSE "DownstreamDevices"
/\ UNCHANGED << pin, format >>
DecodeComponentImageInfos ==
/\ \/ /\ state = "FirmwareDevices"
/\ pin = 1
\/ /\ state = "DownstreamDevices"
/\ pin \in ( Formats \ { 1 } )
/\ state' = "Complete"
/\ UNCHANGED << pin, format >>
Done == state \in { "Complete", "Unsupported", "Error" } /\ UNCHANGED vars
Init ==
/\ state = "Init"
/\ pin \in Formats
/\ format \in Formats
Next ==
\/ DecodeHeader
\/ DecodeFirmwareDevices
\/ DecodeDownstreamDevices
\/ DecodeComponentImageInfos
\/ Done
Spec == Init /\ [][Next]_vars /\ WF_state(Next)
TypeInvariant ==
/\ state \in States
/\ pin \in Formats
/\ format \in Formats
Safety ==
/\ TypeInvariant
/\ state \in States \ { "Init", "Unsupported" } => format <= pin
Liveness ==
/\ [][(state \in { "Complete", "Unsupported", "Error" } => UNCHANGED state)]_vars
/\ [][UNCHANGED <<pin, format>>]_vars
====
```
For an introduction to TLA+ see https://www.learntla.com/
Note that the implemented state machine does not exactly replicate that
specified in the model. Specifically:
- No "Unsupported" state is defined. Instead, the APIs return -ENOTSUP
- No "Error" state is defined. Instead, the APIs return -EPROTO
It is expected that callers perform appropriate error handling.
Change-Id: Id8780c1f5f130b77e6eea2519b5d5734aa79040e
Signed-off-by: Andrew Jeffery <andrew@codeconstruct.com.au>
show more ...
|