This document illustrates Mathematica as an executable design language for embedded, real-time software. It solves a difficult case of parsing noisy input from an inexpensive peripheral device that does not support error detection and correction. Rather than simply writing a regular expression that accepts only valid packets, the scanner must correct as many errors as it can. It so happens that most of the errors occur when the device is starting up. A string of any number of garbage bytes is emitted before the device settles down. The scanner must look for a packet-start signal, literal ue, in that stream. It also happens that ue might be part of garbage, so the scanner must report faults if the bytes following a ue don’t make sense. The caller of the scanner is responsible for correcting bad input, which the scanner will report to the caller. The scanner’s job is simply to detect errors, with the exception that it can correct stuttering of the initial u. That stuttering is a common error condition for the device.
The scanner must also be restartable and reentrant. It must also run in constant memory and constant time, being on the critical path of the real-time part of an integrated system.
The techniques are applicable to any similar situation, and the scanner accepts a finite state machine (FSM) as a parameter. Mathematica affords an extremely readable form for the FSMs, plus, they can be executed in the notebook as a final step of high assurance that we’ve done the best job possible with this situation.
Her is the original abstract written in 2016.
This document describes stateful, restartable scanners and parsers. The design in this document separates buffer management from recognition. Buffer management includes the saving of validated characters, rewinding over invalidated characters, keeping the values of matched forms, resynchronizing the scanner when some data have been missed, stuttered, or garbled, and transferring characters from input buffers to scanner and parser state variables.
This is an executable design or reference implementation for C code, but it’s written in Mathematica for convenience of visualization and proofs. The reference implementation is intended to be easy to transcribe into C with high assurance, taking no special advantage of Mathematica functionality. High assurance means that the transcription is:
◼
testable, exhaustively and / or statistically
◼
either automated or so straightforward that the chances for manual error are few and easily correctable by a POSITA (Person of Ordinary Skill In The Art)
Acknowledgment
Uri Ran (https://www.linkedin.com/in/uriran/) helped me develop some ideas in this document when he was an embedded systems engineer at Amazon. We implemented FSMs as described here in C++, in Common Lisp, and in Mathematica.
Motivating Example
We need a scanner (i.e., lexical analyzer or recognizer) that can be entered and exited repeatedly in the midst of recognizing a correct sequence of bytes and can restart in the midst of certain kinds of noise. Such a scanner is an alternative to more general error detection and correction (EDAC) for, say, inexpensive systems that furnish a checksum at most.
Syntax may be defined by regular expressions, or, more generally, by a formal grammar that corresponds to a deterministic finite automaton (DFA) and a finite state machine (FSM). Generally, we use the term scanning for matching regular expressions and the term parsing for matching more general formal grammars. For convenience and brevity in this document, we use the terms scanner and scanning.
The reason that a scanner must be restartable is that portions of syntactically correct sequences arrive at multiple times. Each time corresponds to a single root activation of a scanner routine.
A candidate syntactic unit may contain arbitrary noise. The example scanners and parsers in this document can handle noisy prefixes and can rewind when a checksum fails. Prefix noise may resemble a correct syntactic unit all the way down to the very last byte. The scanner must ultimately reject such noise and restart at its FSM’s mandatory Entry vertex. When a checksum fails, the scanner assumes a corrupted header leading to misinterpreted payload bytes. In this case, the scanner pushes back all the misinterpreted characters, discard the deceptive header bytes, and restart.
For instance, suppose we want to recognize the sequence ueTL, where u and e are literal characters, is an arbitrary byte denoting the type of the payload data, and is another byte whose value is the length of a following payload section, in bytes.
T
L
An FSM that can recognize such a sequence amidst arbitrary prefix bytes (special case of noise) appears below. The usual regular-expression notation obtains for negated character classes. That notation is a character sequence enclosed in square brackets with a leading caret. and are meta-variables that name the arbitrary characters denoted by the usual regex ‘dot,’ meaning “any character.”
T
L
In[]:=
Manipulate[Module[{init,a,b,c,d,exit,fault,vertices,vertexLabel,edgeLabel,placed,label,labeled},vertexLabel=vPlaced[v,Center];edgeLabel={e,bg}Framed[e,Backgroundbg];vertices={init,a,b,c,d,exit}={"Entry","A","B","C","D","Exit"};Row[{Graph[Property[Style[#,LightOrange],VertexLabelsvertexLabel[#]]&/@vertices,{Style[inita,Dotted],Property[Style[aa,Dashed],EdgeLabelsedgeLabel["[^u]",LightYellow]],Property[ab,EdgeLabelsedgeLabel["u",LightGreen]],Property[Style[ba,Thick],EdgeLabelsedgeLabel["[^ue]",LightRed]],Property[Style[bb,Dashed],EdgeLabelsedgeLabel["u",LightYellow]],Property[bc,EdgeLabelsedgeLabel["e",LightGreen]],Property[cd,EdgeLabelsedgeLabel["T:.",LightGreen]],Property[dexit,EdgeLabelsedgeLabel["L:.",LightGreen]]},VertexSizevs,ImageSizeis,GraphLayoutgl],Grid[{{Style["Legend","Text"],SpanFromLeft},{Style["Regular","Text"],Style["Save input","Text"]},{Style["Dashed","Text"],Style["Discard input","Text"]},{Style["Thick","Text"],Style["Clear all saved","Text"]},{Style["Dotted","Text"],Style["No changes","Text"]}},FrameAll,Alignment{Left,Left,{1,1}Center},Background{None,{White,LightGreen,LightYellow,LightRed,White}}]}]],{{gl,"TutteEmbedding","Graph Layout :"},Sort@{Automatic,"RadialEmbedding","SpectralEmbedding","PlanarEmbedding","GridEmbedding","LinearEmbedding","BalloonEmbedding","TutteEmbedding","StarEmbedding","CircularEmbedding","DiscreteSpiralEmbedding","SpiralEmbedding","SpringEmbedding","SpringElectricalEmbedding","HighDimensionalEmbedding"}},{{is,Medium,"Image Size :"},{Automatic,Tiny,Medium,Large,Full}},{{vs,Large,"Vertex Size :"},{Automatic,Tiny,Medium,Large}}]
Out[]=
Definitions
◼
buffer: a sequential container for data, of a fixed capacity and size. In C, an array. In Mathematica, a List.
◼
backwash: a bogus type byte, length byte, payload bytes, and checksum bytes. They are discovered to be bogus when the checksum fails. The backwash is pushed back into the input and the scanner restarts.
◼
length: (Abbreviation: len) the number of validated items in a buffer. The meaning of validated depends on context. In a scanner, it means characters that have been recognized. In an input buffer, it means characters that have been transferred from an input stream into application memory.
◼
capacity: (Abbreviation: cap) the maximum number of items, valid or not, that a buffer may hold.
◼
size: the number of bytes or 8-bit characters in a capacity. This term is equivalent to capacity in this document because we only consider character data. This definition is useful for generalizations to other kinds of data to be scanned or parsed.
◼
token: in this work, we think of something like a “game token” that moves amongst states in an FSM. In the usual language of scanners, token means an indivisible item of input. We use the word “item” in this work to distinguish our tokens—like game tokens—from input items.
◼
system: the undefined context of hardware and software that uses the code explained in this document
◼
interrupt service routine (ISR): an isolated block of code that runs from start to finish in response to hardware events, without interruption itself. An ISR has free access to system and application resources, including the data structures defined in this document, without concurrent contention from other code.
◼
application: whatever code is running, excluding ISRs, when an interruption occurs.
◼
state: Unfortunately, this word has multiple meanings in our context:
◼
In general, a state is an association of values to all the variables in some universe of discourse. Here, this means the current association, i.e., assignment, of values to variables in the various data structures controlling the restartable i/o, scanners, and parsers.
◼
the current vertex inhabited by the FSM representing the data to be recognized. Think of a game token that sits on one, and only one, vertex of the FSM graph at a time. The vertex on which the token sits is the state of the FSM. We write vertex to distinguish this meaning from the other meaning of state.
Stateful I/O
We achieve restartability with stateful I/O and with scanner routines that read from a scanner-state buffer and write back to scanner-state buffers from an input buffer. Instances of the Circular Buffer abstract data type described below control the scanner and input states and bound the memory used by the code.
INVARIANT: In our applications, the scanner-state circular buffer may contain only valid prefixes. In controlling the example FSM, for instance, the scanner state may contain nothing (written ε), ‘u’, ‘ue’, ‘ueL’, or ‘ueLT’. The last possibility is a full syntactic unit, without its checksum, but is also considered a valid prefix. Scanners must discard invalid characters.
◼
Circular Buffer
The following design could trivially be made generic in the type of its contents. However, it is expressed non-generically on unsigned 8-bit characters (uint8_t in the C language) because that’s the only type needed in the current application of parsing ASCII character data.
Though circular buffers seem like a trivial data type, we have found many bugs in practice, so we engineer a meticulous solution for the sake of high-assurance. A high-quality queue data type like Python’s bounded deque might be employed instead of this solution. In all cases, an implementation must be certified by testing or proofs to meet real-time deadline guarantees.
Design
Design
Attributes
Attributes
A circular buffer (CB) has
◼
a pointer to storage, origin
◼
a constant capacity cap, which is the maximum number of characters in origin (not necessarily the size in bytes, if this design were generalized to multibyte types of content)
◼
two indices into origin: head and tail
◼
a current length len, which is the number of valid characters stored in the CB and can be calculated on-the-fly
Semantics, Rules, and Restrictions
Semantics, Rules, and Restrictions
Characters are pushed to the tail and popped from the head. Pushed characters overwrite previous contents. Contents are not erased except by clearing the entire buffer or by pushing distinguished, invalid fill characters.
Tail indexes the next cell available for pushing and not valid data. Head indexes the first valid data item when the CB is not empty. Pushing a character increments tail, modulo cap. The CB is empty when .
tail===head
Notice that can never be exactly cap. When , the next push will fill the CB, but the CB will report that it's empty, i.e, that its length is zero. Thus, this overall design cannot distinguish a full CB from an empty CB. Distinguishing full from empty is the caller’s responsibility.
len
len=cap-1
To protect against improperly reading or testing invalid data, callers are advised to explicitly test for the empty condition of the CB and to initialize or clear the CB with a distinguished, invalid fill character that does not appear in normal use. The default distinguished, invalid fill character is zero.
This design is more efficient and less bug-prone than the alternatives, say of maintaining a separate length variable or of testing and setting a sentinel index for head. It is a well known solution. See http://embedjournal.com/implementing-circular-buffer-embedded-c/ for example.
We assume efficient implementations of mod operations with respect to the capacity. Examples of efficient implementations are presented below.
This design silently overwrites old data on overflow. Alternative designs, not considered here, might discard new data or signal on overflow. These alternatives are rejected on grounds of complexity (more computer work) and complication (more programmer work).
Operations
Operations
Summary
Summary
◼
reset [ CB, head:Index, tail:Index ] ~~> CB
◼
clear [ CB ] ~~> CB
◼
clear [ CB, fillCharacter ] ~~> CB
◼
push [ CB, Character ] ~~> CB
◼
pushIfDistinct [ CB, Character ] ~~> CB
◼
pushBack [ CB, Character ] ~~> CB
◼
pop [ CB ] ~~> Character
◼
backspace [ CB ] ~~> Character
◼
peek [ CB ] ~~> Character
◼
peek [ CB, Index ] ~~> Character
◼
peekLast [ CB ] ~~> Character
◼
peekLast [ CB, Index ] ~~> Character
◼
emptyQ [ CB ] ~~> Boolean
◼
fullQ [ CB ] ~~> Boolean
◼
almostFullQ [ CB ] ~~> Boolean
◼
len [ CB ] ~~> Index
Details
Details
The type Index is a non-negative integer. The type Character is an unsigned 8-bit integer, as noted above.
◼
reset [ CB, head:Index, tail:Index ] ~~> CB
Sets the head and tail of the CB to the given values. Used when the state of the CB is externally known.
Returns the modified CB for convenience in chained expressions.
◼
clear [ cb:CB ] ~~> CB
Fills cb.origin with zero, the default, invalid fill character, and resets cb.head and cb.tail to zero. The CB will report itself empty after a clear operation.
Doubles as initialization.
Returns the modified CB for convenience in chained expressions.
◼
clear [ cb:CB, fillCharacter:Character ] ~~> CB
Fills cb.origin with fillCharacter and resets cb.head and cb.tail to zero. The CB will report itself empty after a clear operation.
Doubles as initialization.
Returns the modified CB for convenience in chained expressions.
◼
push [ cb:CB, c:Character ] ~~> CB
Pushes character c (of type Character) onto the tail of cb (of type CB) incrementing cb.tail modulo cb.cap, even if the CB is full. This design silently overwrites the oldest bytes in the CB and may result in a newly empty CB containing arbitrary data.
Returns the modified CB for convenience in chained expressions.
◼
pushIfDistinct [ cb:CB, c:Character ] ~~> CB
The empty condition is significant because pushIfDistinct can test any character, not necessarily the one intended by the programmer. This operation may test the invalid fill character of cb or, in fact, any character left over in the CB from prior operations.
Callers are advised to explicitly test for an empty CB and to initialize or clear the CB with a distinguished, invalid fill character. The default distinguished, invalid fill character is zero.
Returns the modified CB for convenience in chained expressions.
◼
pushBack [ cb:CB, c:Character ] ~~> CB
Pushes character c (of type Character) onto the head of cb (of type CB) decrementing cb.head modulo cb.cap, even if the CB is full. This design silently overwrites prior bytes in the CB.
Returns the modified CB for convenience in chained expressions.
◼
pop [ cb:CB ] ~~> Character
Returns the character at the head of cb and advances cb.head modulo cb.cap, even if the CB is empty.
This overall design does not distinguish an empty CB from a full CB, so pop on an empty CB may return any character: the fill character or any character that may be left over from prior operations.
Callers are advised to explicitly test for an empty CB and to initialize or clear the CB with a distinguished, invalid fill character. The default distinguished, invalid fill character is zero.
◼
backspace [ cb:CB ] ~~> Character
This overall design does not distinguish an empty CB from a full CB, so backspace on an empty CB may return any character: the fill character or any character that may be left over from prior operations.
Callers are advised to explicitly test for an empty CB and to initialize or clear the CB with a distinguished, invalid fill character. The default distinguished, invalid fill character is zero.
◼
peek [ cb:CB ] ~~> Character
Returns the character at the head of cb without advancing cb.head, even if the CB is empty.
This overall design does not distinguish an empty CB from a full CB, so peek on an empty CB may return any character: the fill character or any character that may be left over from prior operations.
Callers are advised to explicitly test for an empty CB and to initialize or clear the CB with a distinguished, invalid fill character. The default distinguished, invalid fill character is zero.
◼
peek [ cb:CB, i:Index ] ~~> c
This overall design does not distinguish an empty CB from a full CB, so peek on an empty CB may return any character: the fill character or any character that may be left over from prior operations.
Callers are advised to explicitly test for an empty CB and to initialize or clear the CB with a distinguished, invalid fill character. The default distinguished, invalid fill character is zero.
◼
peekLast [ cb:CB ] ~~> Character
This overall design does not distinguish an empty CB from a full CB, so peekLast on an empty CB may return any character: the fill character or any character that may be left over from prior operations.
Callers are advised to explicitly test for an empty CB and to initialize or clear the CB with a distinguished, invalid fill character. The default distinguished, invalid fill character is zero.
◼
peekLast [ cb:CB, i:Index ] ~~> Character
This overall design does not distinguish an empty CB from a full CB, so peekLast on an empty CB may return any character: the fill character or any character that may be left over from prior operations.
Callers are advised to explicitly test for an empty CB and to initialize or clear the CB with a distinguished, invalid fill character. The default distinguished, invalid fill character is zero.
◼
emptyQ [ cb:CB ] ~~> Boolean
◼
fullQ [ cb:CB ] ~~> Boolean
◼
almostFullQ [ cb:CB ] ~~> Boolean
◼
len [ cb:CB ] ~~> non-negative integer
Reference Implementation
Reference Implementation
The following code is as close to C code as Mathematica allows us to write. Its purpose is to serve as an executable design for C code. The writing of high-assurance C code should be straightforward from this design.
Mathematica is semi-functional: values are immutable, but variables can be assigned. This has four ramifications for our reference implementation:
1
.We cannot modify values by side-effect. We can make modified copies, then assign the modified copies to variables.
2
.Function parameters are not variables. Inside functions, we must explicitly make temporary variables in Module forms and copy the values of parameters.
3
.In the pop and backspace operations, we return pairs of the modified (copies of) the CB and the character popped or backspaced over.
4
.In scanners and parsers, we make frequent use of multiple-return values in an obvious pattern similar to that for item 3, above.
Interactive Testing
Interactive Testing
Restartable Scanners
The system repeatedly interrupts the application with one or more new input bytes from an input stream, say a peripheral device. More concretely, the interrupt service routine, ISR, receives (a pointer to) the caller-maintained input buffer and a length, the number of characters transferred to the system from the peripheral. The ISR does not know the capacity of the caller-supplied input buffer: it’s the responsibility of the application to manage communication with the peripheral, to ensure there is enough enough room so that input buffers are never overflowed. In practice, static bounds may be available from the peripheral’s manufacturer, or a tuning phase before deployment may be necessary to establish practical or heuristic bounds.
Algorithm
Algorithm
A scanner and two FSMs are detailed below. The scanner models its current state with a circular buffer (CB) called scannerState, models partially validated results with another buffer called provisionalPayload, and wraps the input with another circular buffer called inputState. The scanner calls its FSM one character at a time. The FSM returns action specifications and a “next vertex” indicator to the scanner. The scanner performs the action to modify the buffers, fetches a new character, and calls the FSM at the “next vertex” if there is a new character.
The first FSM just processes headers and can correct certain kinds of errors. The second FSM processes payload bytes and can wash partially validated results back to the input to handle a broader class of errors. Both FSMs can be interrupted at any time and restarted later. The scanner will replay validated characters from scannerState to bring the FSM to its prior vertex, then continue with new input. When the input is exhausted, the scanner stops in its last-visited vertex after performing the specified action.
INVARIANT: scannerState only ever contains valid characters, either newly validated or already validated in a prior pass.
On a call or reentry, the scanner restarts its FSM at its unique Entry vertex and saves the current head index of scannerState. The reason is that the scanner may pop valid characters from scannerState for replay. Those characters are still valid and must be retained when the scanner resumes processing input at the prior last-visited vertex.
The scanner maintains two metrics: discarded and saved. The discarded metric counts the number of characters discarded while taking transitions along dashed edges in the diagram, edges with the “Discard input” label. The saved metric counts characters saved from the input to the scanner state while taking regular edges with the “Save input” label. While taking thick edges with the “Clear all saved” label, the discarded metric is incremented by the length of the scanner state, which is then cleared, and the saved metric is set to zero. “Washback” edges are described later. They do not appear in the FSM above, which only recognizes headers.
As usual when designing C code with Mathematica, we make temporary variables in a Module for mutable data, and initialize those temporaries from parameters. The reason is that parameters are not variables in Mathematica, thus parameters cannot be updated. The corresponding routines in C will simply modify variables and structs in-place.
FsmStep is a foldable function, meaning that the return value has the same type as the first input. This is important for high-assurance software: foldables can be tested independently of their callers (see A Tutorial on the Universality and Expressiveness of Fold by Paul Graham and this author’s Kalman Folding).
The return type of fsmStep is the same as the type of its first parameter. Both are Mathematica Lists in curly braces: prior vertex, action command, a parameter for the action, and the current matches dictionary. The FSMs ignore the input action and action parameter and pass back new actions and parameters to the scanner, which performs them. The returned actions are "save," "discard," "clear," "washback," or "no action."
NOTE: this executable design (or reference implementation) contains exception-throwing to assert invariants. Such constructs must not appear in embedded builds. Other exception-handling mechanisms must be devised for embedded builds.
A Stepping FSM for the Header
A Stepping FSM for the Header
A Restartable Scanner
A Restartable Scanner
Let’s write and test the scanner. It’s important to read some of the tests because they illustrate the metric difference between saving characters from input versus replaying them from scannerState.
Support Routines
Support Routines
The FSM gives the scanner action commands. Some action commands move characters from one buffer to another. The routines washback and transferAll support these commands.
Unit Test washback
Unit Test washback
Put the numbers 1 trough 7 into src. Wash back 4 of those characters to the buffer dest.
Washing back too many characters is not an error.
Unit test transferAll
Unit test transferAll
Scanner [ scannerStateCB, provisionalPayloadCB, inputStateCB, fsmStepper ] ⟶ scannerStateCB, provisionalPayloadCB, inputStateCB, metrics, matches
Scanner [ scannerStateCB, provisionalPayloadCB, inputStateCB, fsmStepper ] ⟶ scannerStateCB, provisionalPayloadCB, inputStateCB, metrics, matches
The caller, Scanner, furnishes three CBs that are modified by side effect. The three CBs are scannerState, provisionalPayload, and inputState.
Scanner is foldable in that its output type is the same as the type of its first input, but can’t be called from Fold because characters may wash back from provisional payload to the input. We have not experimented with a Fold that modifies the stream being folded over.
Action save
Action save
The action save with argument validated increments the metric for validated characters and pushes the character to scannerState. Save with argument provisional a character into provisionalPayload whence it can be washed back when a fault is detected.
Action clear
Action clear
The action clear ignores its argument, increments the metric for discarded characters by the number of characters in scannerState, sets the metric for saved characters to zero, and empties out scannerState. This action does not modify provisionalPayload or inputState.
Action discard
Action discard
The action discard ignores its argument, increments the metric for discarded characters by one, and does not modify buffers.
Action washback
Action washback
The action washback transfers a number of characters from provisionalPayload back to inputState. The number of characters is specified by the argument passed to washback. It does not modify metrics because it does not manipulate saved or discarded characters; it just puts them back into the input. The FSM above does not call washback, but the new one, below, does.
Scanner itself
Scanner itself
This scanner first replays all validated characters in scannerState to handle restart or re-entry. Any action but save during replay is a catastrophic error (Throw, useful only in simulation; some other method of handling catastrophic errors must be implemented in a real, embedded application).
Scanner performs actions before optimistically reading characters from inputState and transitioning to the next vertex. When inputState is empty, the scanner stops.
Scanning More
From study of the first FSM, we take it as understood that the scanner stops when input is exhausted, taking the action but not the transition of the final vertex. We also take the restart and replay semantics of the scanner as they affect the metrics as understood. These understandings help to shorten the prose below.
The Full FSM
The Full FSM
TODO: save payload fields in matches to aid correction logic.
The following is a manual “desk check” of the logic to test against various faults in the field portion, consider the only possible cases:
Not Enough Field Data
Not Enough Field Data
Just Enough Field Data
Just Enough Field Data
Too Much Field Data
Too Much Field Data
Without Checking ΣF
Without Checking ΣF
This shows the necessity of tracking the sum of the field-length bytes and of checking the invariant
With Checking ΣF
With Checking ΣF
Fletcher Checksum
Fletcher Checksum
newFsmStep
newFsmStep
Here the new FSM stepper described in prose above. Careful examination of the states will reveal how easily the logic in Mathematica matches the prose.
Inverting the Control
In this design, FSMs are responsible for recognizing characters one at a time and for requesting actions from the calling scanner. The scanner doesn’t know much about the FSM: only the list of commands that the FSM may request. The FSM knows nothing about its caller. Thus, the scanner can be tested independently of the FSM.
This could be further generalized by having the FSM return closures to the scanner, rather than strings commands. Such is overkill for the example.
Most parsers work by calling I/O routines such as getchar and pushback. They take actions directly inline, but are unprepared for i/o faults like exhaustion and overflow. This parser separates those concerns completely.
Sandbox
Stuff I am not ready yet to throw away.
Parser
Parser
A failing case without ΣF handling:
CITE THIS NOTEBOOK
CITE THIS NOTEBOOK
Wolfram Language as a design language for embedded, real-time software
by Brian Beckman
Wolfram Community, STAFF PICKS, March 6, 2024
https://community.wolfram.com/groups/-/m/t/3135874
by Brian Beckman
Wolfram Community, STAFF PICKS, March 6, 2024
https://community.wolfram.com/groups/-/m/t/3135874