A framework for embedded software portability and verification: from formal models to low-level code

Event-B is a formal method for system-level modeling and analysis [2, 21] derived from the B formalism [1]. Based on set theory and state transitions, Event-B supports refinements to model different abstraction levels, while mathematical proofs verify correctness and consistency between refinements. The Rodin Platform [37], an Event-B IDE based on Eclipse, supports the development and refinement of models with automatic generation and partial discharging of mathematical Proof Obligations (POs). POs are mathematical formulas that must be proved (discharged) to ensure correctness of the model. Several plugins are available to Rodin that aid in, e.g., automatic PO discharging and model checking.

In order to ease the understanding of readers unfamiliar with Event-B, we introduce the components of Event-B models and then present a model with most of these components to show how they can model a sequential program. Listing 1 and Listing 2 present the model explained later, and can also be used as reference to the keywords and components explained next. We assume the reader is familiar with basic set theory notation.

The two top elements of a model in Event-B are contexts and machines. The term context is overloaded in the domains of OSs and formal methods. Hence, we will always refer to a context in Event-B as Event-B context. In contrast, just context refers to task context in operating systems. Event-B contexts describe all static information about the system and can have carrier sets and constants. Axioms are the predicates that the constants obey and will be available as hypotheses in the POs. It is also possible to add theorems which must be proved. If an Event-B context extends others, it can reference sets and constants of the extended Event-B contexts and any they also extend. Dynamic information about the system is described in the machines. A machine can see Event-B contexts, such that it can use their sets and constants to relate static and dynamic information, as well as axioms and theorems to discharge POs. Machines can have variables that obey predicates given by their invariants, and theorems can be added and proved. Considering machine states as sets of the variables’ values, each event represents a state transition. An event is said to be enabled if the state satisfies its guard condition. The mandatory event initialisation serves as a starting point, has no guards, and only runs once to initialize all variables. Event-B does not define which event will be executed in case more than one is enabled simultaneously. The execution of an event modifies the current state according to its actions, which are executed simultaneously. It is possible to limit how often an event may be enabled using a variant, which is either a numeric expression or a finite set whose free identifiers are constants or concrete variables. Events always have a status, which can be either ordinary (default status, the event may occur arbitrarily often), convergent (the event must decrease the variant), or anticipated (the event must not increase the variant). When a machine refines another one, it may introduce details or more variables. The machine events must be refined or kept as they were. In special cases, when the event can never be enabled, it may be deleted from the refined machine. POs define what is to be proved for a model and are automatically generated by Rodin. For example, the POs guarantee that invariants always hold and that refined events do not contradict abstract ones.

Listing 1 and Listing 2 reproduce an example from Abrial’s book: the binary search in a sorted array (Section 15.4 of [2]). We have only created a Rodin project and copied the Event-B model from the book into it, correcting some typos present in the original and discharging the POs Rodin generated. To complete our example here, we also added the Event-B context c1 (Listing 1b), which is not present in the original model. With this example, we can show Event-B ’s notation and model components, as well as some concepts for modeling sequential programs introduced by Abrial and used in our models. In this model, we only have four events and the state is composed of a few variables. Still, it can be challenging to understand how state transitions occur and which effect events may have on each other. Therefore, it is helpful to visualize the model graphically. Many tools can create visualizations from Event-B models, producing intricate and detailed graphs. For the sake of simplicity, however, we present simple state-machine-like graphs representing our models. As an example, Fig. 1 presents a visualization of the concrete Event-B model of the binary search. The nodes represent the events’ guards, and edges represent the possible state transitions caused by their actions when they execute. The dashed boxes are the guard expressions defining the state that enables the respective event.

Listing 1a shows the Event-B context with the binary search pre-conditions: f is an array of natural numbers with size n, and v is a value in the range of f (i.e., an element of the array). The program (modeled in the machine, explained later) will search for the index r in the array, such that f(r) \(=\) v. The axiom axm0_4 tells us that the array f is sorted in a non-decreasing way, and the theorem thm0_1 states that there is at least one element in the array. Listing 1b is not part of the model. However, it shows how an Event-B context can extend another to use (and further detail) elements of the extended context, for example, defining the size n of the array f. It also defines a carrier set S and new constants. The axiom setDef defines S as a partition of three subsets with one element each, effectively creating an enumerated set of three elements. The machine of the initial model (Listing 1c) sees the Event-B context c0 and declares the variable r, which represents the index that the program must find. Besides the mandatory initialisation event, we add two others. Event final represents the specification of the program, i.e., its post-condition. It has no actions (skip), and its guards represent the state where the program has found r. Note that axm0_3 states that v is in the range of f, guaranteeing the program will find r. The other event we add is the anticipated event progress, which modifies r in a non-deterministic way. Its refinements will detail how r is to be found and will eventually be made convergent on a variant, such that the loop it creates is guaranteed to terminate eventually. In the first refinement m1 (Listing 2a), two new variables, p and q, are introduced, representing search indexes of the array f. The abstract event progress is split into events inc and dec, which are made convergent on the variant q −p. Since inv1_3 has been introduced, the guard grd0_fin_1 in final of Listing 1c always holds and can therefore be removed from the refined machine m1. The second refinement m2 (Listing 2b) defines how r is to be found within inc and dec, defining the increment and decrement intervals that were non-deterministic in m1. Note that, since event final remains exactly the same as its abstraction, its guard is omitted and the word refines is replaced by extends. The goal state is still f(r) \(=\) v.

While we assume the reader is familiar with basic set theory, our models use some set and relation operators that are less generally known. To ensure understanding of the models, we explain the meaning of these operators with an example. Listing 3 defines two sets, s1 and s2, where s2 is a subset of s1. The set s1 is a partition of constants a to e (definition omitted for simplicity). A relation r is a set of pairs where its domain dom(r) is the set of all elements occurring on the left side of the pairs and its range ran(r) is the set of elements on the right side. A function is a special case of relation, where each element of the domain is uniquely related to one element of the range. The two relations defined in Listing 3, r1 and r2, are partial functions from, respectively, s1 and s2 to . Table 1 shows the values in each relation range. Columns r1 and r2 show the range values defined for these relations, each cell representing the value mapped to the corresponding set element. If an element is not in the relation’s domain, the cell is marked with “-”. If it is, but there is no mapping for it in the relation the cell is left blank. The other columns represent the result of some operations with r1: The domain subtraction s2 r1 removes all s2 from r1 ’s domain, leaving only two mapped values. Domain restriction s2 r1 is the inverse, only leaving values mapped to elements present in s2. The overwrite operation r1 r2 overwrites the r1 relation with values from r2. Finally, Listing 3 also shows the results of two other operations as theorems: s1 minus s2 results in a set with all elements from s1 that are not in s2 (thm1). Brackets are used to access a relation element, as exemplified by thm2.

Temporal logic [52, 59] is a logic system that formally describes properties of time. Linear Temporal Logic (LTL) is the most popular and widely used temporal logic in computer science to specify and verify the correct behavior of reactive and concurrent programs [30]. It is particularly useful for expressing properties such as safety (given a precondition, then undesirable states that violate the safety condition will never occur), liveness (given a precondition, then a desirable state will eventually be reached), and fairness (involves combinations of temporal patterns of the form a predicate holds “infinitely often” or “eventually always”). ProB is an animator, constraint solver, and model checker for the B-Method [47] that integrates as a plugin-in Rodin and can be easily used for LTL model checking of our RTOS models.

Next, we present the main characteristics of the two HW architectures we use as examples for the architecture-specific instantiations of our model in Sect. 5.3.

MSP430 The TI MSP430 [36] family of MCUs comprises a range of ultra-low power devices featuring 16 and 20-bit RISC architectures with a large variation of on-chip peripherals, depending on the variant. Among its 16 registers are general purpose registers, the program counter PC, the stack pointer SP, and the status register SR, which stores status flags, such as interrupt enabled, overflow, etc. The MSP430 offers a very simple architecture with only one execution mode and a fully orthogonal instruction set. There is no privileged mode, nor any memory protection or memory management unit. Once an interrupt occurs, the PC and SR registers are pushed onto the stack. Then, further interrupt requests (IRQs) are disabled and the PC is overwritten with the address of the first instruction of the corresponding interrupt handler. The return from interrupt instruction, i.e., RETI, restores SR and PC from the stack and finally continues where the handler has interrupted the regular execution flow.

RISC-V The open RISC-V instruction set architecture [63] was originally developed by UC Berkeley and is meanwhile supported by a highly active community of software and hardware innovators with more than 100 members from industry and academia. The RISC-V is a load-store architecture, and its specification [78] defines privilege levels used to provide protection between different components of the software stack. We refer to an implementation that supports user and machine modes, with 32-bit integer and multiplication/division instructions (RV32IM) [77]. There are 32 registers available in all modes, including a zero register and the program counter pc. The calling convention specification assigns meanings to the other registers, such as a stack pointer sp, function arguments and return values. Additionally, Control and Status Registers (CSRs) with special access instructions are available for, e.g., managing the CPU or accessing on-chip peripherals in defined privilege levels. An IRQ switches the CPU into a higher privilege level, while software can issue an ECALL instruction for that. In both cases, returning to user level is done by the instruction URET.

The LLVM Compiler Infrastructure is a collection of compiler and toolchain components designed as a set of reusable libraries [50]. All components have well-defined interfaces, and one of the most important aspects of LLVM for this paper is the LLVM Intermediate Representation (LLVM IR). The LLVM IR is a language with well-defined semantics and a RISC-like virtual instruction set that supports simple instructions like add, subtract, compare, and branch. It is strongly typed and uses an infinite set of temporary registers prefixed with a % character. LLVM IR is defined in three forms: a textual format of the language in .ll files, an in-memory data structure used by optimizers, and an on-disk binary “bitcode” [45], with tools provided to transform one form into another.

We modeled SmartOS [66], an embedded RTOS we have developed and used for many years. This section summarizes its architecture and requirements. An important concept to understand is the context (not in the sense of Event-B, but in the sense of operating systems): A context is a set of information and configuration of a CPU or a CPU core that is required to control the execution flow of software, i.e., code sequences. Depending on the CPU state and external events, cores can usually switch between different code sequences by loading their respective context. To be able to continue an earlier code sequence from the interrupted instruction, its context is saved before the switch. The actual switching process as well as the composition of the contexts is defined by the interrupt concept of the CPU; in any case, the hardware automatically saves and loads the contexts. If, in addition to interrupts of the hardware, an OS supports preemptive, i.e., interleaved executable tasks (or threads or processes), the context is extended. In order to switch between tasks, this extended information is saved (previous task) and loaded (next task) by the kernel. Next, we describe our general assumptions about the computing platform and present SmartOS’s requirements.

The model has several refinements and showing all would be too cumbersome. So, we divide it into six levels of abstraction (referred to as Level). Each Level is composed of several refinements and addresses a new set of requirements (Table 2).¹ Up to and including Level 4, the model remains generic, only requiring the generic hardware features described in Sect. 5.1.1. We only introduce further hardware details in Level 5, where we instantiate the model for specific target architectures. This section introduces the general idea of each Level, while Sect. 5.3 details how each level was modeled. This model focuses on the interface between hardware and software in order to model the kernel’s interleaved execution of concurrently running tasks. The goal is to prove that the kernel does not corrupt any task’s context by properly saving and loading them, as well as to guarantee that tasks and kernel body run in the appropriate conditions described by the requirements from Sect. 5.1.

The state of an Event-B machine is the set of its variables’ values, and state transitions are represented by the machine’s events. In our model, these events represent the different parts of the kernel, building a state machine that starts with the switch into the kernel and finishes with the switch back to a task. The events, therefore, are modeled such that their order is well-defined, in the order the kernel parts must run: kernel entry executes first, then body, and finally exit; and the automatic part of entry executes before the manual part that must be executed in software (OS7), and in exit manual executes before automatic (OS9).

This section details the generic part of the context switch model, i.e., Levels 0 to 4 from Sect. 5.2. Please, refer to Sect. 3.1 for the Event-B notation used in the following listings.

This section shows the properties we verified via theorem proving in Rodin and LTL model checking.

From the requirements in Sect. 5.1.2, we elaborate some safety properties to be proved: (S1) Contexts are never corrupted by the kernel (OS2), (S2) osBody always runs in the specified conditions for its execution, and osFinal is reached with the specified conditions for task execution (OS5, OS6). Details for verifying the other OS requirements are omitted in this paper since the concept is the same. Instead, we also show how to verify some liveness properties: To guarantee that the model reaches the intended states, we verify that the steps resulting from the OS requirements are executed in the appropriate orders. (L1) The kernel executes in the correct order, and (L2) always finishes execution by always reaching osFinal.

The factorial of a natural number n, denoted n!, is the product of all natural numbers from 1 to n. The factorial of 0 is, by definition, \(0! = 1\). Factorial is often implemented recursively, where f(n) = n * f(n-1). Our Event-B model will use recursion for the model checking. However, the intended implementation is an iterative one, as Listing 17 shows. This C code is not relevant for code generation, but just to (1) present the algorithm in comparison to the model and (2) to compare the final binaries compiled from the C code and our generated LLVM IR.

Following our modeling strategy described in Sect. 5, the model’s machine is shown in Listing 18. It contains the fFinal event that models the goal of the factorial function in its guards, and has no actions (skip). The guard assures the correctness of the calculated result. Since some parts of the model are not intended for code generation, such as this guard, any statement with the label starting with “model” will be ignored by EB2LLVM. The event where the factorial of input is calculated is calc (Listing 18, Line 16). This event is equivalent to the while block in Listing 17.

The model sets the function’s pre-conditions in the axioms of Listing 19. Therefore, the generated function factorial will assume that these pre-conditions hold, and will not, e.g., check if \(\texttt {input} \in 0..\texttt {maxInput} \).

Since the factorial model does not make any use of, e.g., registers or interrupts, its instantiation consists of only defining the data type as a function of the target’s bit-width. It is important to notice that, currently, EB2LLVM only supports signed integers with the architecture’s bit-width. Therefore, even though the model’s variables could potentially be represented, e.g., by unsigned long integers, the instantiation must consider them signed integers. It follows that , where b is the bit-width of the target. For the 16-bit MSP430, this means \(\texttt {maxInt} = (2^{15}-1)\), while for the 32-bit RISC-V, \(\texttt {maxInt} = (2^{31}-1)\).

We will now explain the LLVM IR generated from our models and shown in Listing 20 for the MSP430³: In the enabling analysis generated by ProB (Table 4) the connection between fFinal with itself is syntactic_independent, since once the event executes, the state does not change anymore. EB2LLVM interprets this as a return instruction. The possible connections in the enabling analysis will all generate conditional branches at the end of the origin block. The condition is generated from the guards of the destination. All possible destinations will be considered: having INITIALIZATION as origin, both calc and fFinal are possible. Therefore, two conditional branches will be generated. The first, in Listing 20 (Lines 7–10) branches to calc if \(cnt < input\), as required by the guard . Otherwise, it jumps to a newly created block INITIALIZATION_fFinal (Lines 32–36) that then jumps to fFinal if \(cnt = input\) (Line 26). Otherwise, it jumps to the default error block (Line 29). Similarly, calc may either jump back to itself (Lines 21–24) or to calc_fFinal (Lines 38–42).

In this example, one can also notice several load and store instructions generated from Event-B variable reads and assignments. Basic arithmetics are also translated to their LLVM equivalents. In the factorial example, we have addition and multiplication being converted to, respectively, the instructions add and mul.

The last step in the code generation is to compile the LLVM IR into assembly with llc, LLVM’s static compiler. For the factorial example, we use the default optimization -O2 to generate assembly code for the targets MSP430 and RISC-V. The generated code is shown in Listing 21a and Listing 22a respectively. The code generated from the Event-B model, can be compared to the code compiled from the C factorial function in Listing 17. For the MSP430, we used the MSPgcc 6.2.1 compiler, and the resulting assembly is shown in Listing 21b. A clang compiler was available for RISC-V, and we used version RISC-V rv32gc clang 9.0.0 (with the -march=rv32i option), the same LLVM version we use in our code generation. The compiled code is shown in Listing 22b. Both used the same level of optimization -O2.

The code compiled from C for the MSP430 (Listing 21b) is a few instructions longer than the one we generated from the Event-B model (Listing 21a). One of the reasons is that the gcc compiler inserted prologue and epilogue to save and restore registers used within the function. Since our code generator aims at generating exactly what is modeled, these registers are silently overwritten.⁴ Further, the gcc version has more instructions to prepare for the while loop, however the instructions sequence inside the loop is more optimized.

A note about the compare instruction in Listing 21a, Line 19: our code generator correctly generated it from Listing 20, Lines 39 to 41, however the corresponding branch in Line 42 was omitted. This is functionally correct, since both destinations of this branch (fFinal and error) would result in the execution of a return instruction, which follows the compare in the generated assembly code. However, this renders the compare instruction useless. A similar situation happens in the code generated for RISC-V: all the load instructions between Lines 24 and 31 in Listing 22a are generated from Listing 20, Lines 39 to 41, but never used in the compare/branch for which they were intended.

Also similarly to the MSP430, the assembly code generated by clang for the RISC-V (Listing 22b) has prologue and epilogue, while the code generated from Event-B (Listing 22a) does not. The while loop is also more optimized, and instead of storing partial results in each iteration, clang only stores the end values before return. Though slightly less efficient, the code generated from Event-B for both MSP430 and RISC-V can be compiled into binaries that execute as intended.

Generating code for our context switch model requires more complex features from EB2LLVM. Since the context switch must communicate with the hardware directly, the code generator must know how to, e.g., translate and interpret register accesses, interrupts, and specific instructions. The model also uses array accesses, sets and relations, and equations that need to be used in the code generation, as opposed to the factorial model, where these were only used for the model verification.

For the two architectures shown in Fig. 7, each inner-most box (representing the concrete events) results in one block of code. They are executed sequentially, and the enabling analysis from ProB reflects that dubbing each connection guaranteed, while other possible connections are impossible. The guaranteed connections generate unconditional branches from the origin block to the destination.

In our models, events model what the hardware does when an interrupt occurs and when a return from interrupt instruction is issued. The actions within these events should, therefore, not produce any code. Furthermore, an event modeling a specific instruction, such as the return from interrupt, should be translated to the equivalent instruction. This is achieved by using pre-defined names for these events to indicate to the code generator which instruction to use. For example, the code generator will ignore events called interrupt, and automatically generate a return from interrupt instruction when it finds an event named reti.

The context switch model is much larger than the factorial, and, to demonstrate its code generation, we selected one crucial snippet of it: the save action from Listing 15a. Besides showing the remaining features of EB2LLVM, this is also the action that allows the model to remain mostly generic up to refinement Level 4 and yet detailed enough to generate architecture-specific code from refinement Level 5. In the save action, the context is saved into t_saved. We know from the model that t_saved is a two-dimensional array, with one block of savedctx elements for each task in the system (see Fig. 3b). The running task rTask is our reference here, and each context element is to be stored in the array t_saved[rTask]. EB2LLVM will use the HW models (Listing 16) to unroll the action into several store instructions, according to the other elements of the expression. It applies transform to save each cpuCtx and temp value into their appropriate saved context index, filtering only manual* cpuCtx values due to the restriction operator ( ). The results of this process for both MSP430 and RISC-V are shown in Listing 15b and Listing 15c, respectively.

However, the definition of transform involves further axioms and its evaluation during code generation is rather complex. Listing 23 shows it step by step for saving one MSP430 register. First, the save action is unrolled, resulting in several expressions like ①. Then, the code generator matches the right-hand side (②) to axm7 from Listing 7, also using the hardware-specific definition of ctx2saved (axm22 in Listing 16a) to solve ③. Finally, ctxTransform (④) is evaluated in a similar way. In this particular case it does nothing (i.e., \(\texttt {ctxTransform} (\texttt {el})(\texttt {ctx} (\texttt {el}))=\texttt {ctx} (\texttt {el}))\), so the final expression that will be translated into LLVM IR shows in ⑤. If a modification was defined by ctxTransform in the model, it would be taken into account and the appropriate instruction would be generated.

The save operation can then be translated into LLVM IR⁵ as shown in Listing 24. The register access \(\texttt {cpuCtx} (\texttt {R8})\) (Listing 23, ⑤) is converted to a call to the intrinsic LLVM function read_register (\(\rightarrow \) Line 1). In Lines 4 and 6 we can see that the accesses to elements in a relation are converted to LLVM’s GEP instruction⁶, and the value from the register is finally stored in the appropriate array position mR8. Note that the save index mR8 is defined, in the model, as a constant value, and therefore expressed as the immediate value 5 in Line 6. This is repeated for each element that must be saved, according to the model. The LLVM IR code for RISC-V is similar to Listing 24: The register name and its index, as well as the data sizes are replaced according to the RISC-V model.

Finally, assembly code is generated from the automatically generated LLVM IRs by llc. This time, we turn off optimizations (-O0) to assure that unintended modifications to the model’s logic will not occur. For the MSP430, each block that saves one register (such as in Listing 24) is translated to assembly as shown in Listing 25a. The index for the array access in Line 3 is automatically calculated by llc as \(\texttt {mR8} * ByteWidth\), and since the MSP430 is a 16-bit (2 bytes) architecture: \(5 * 2 = 10\) (Line 3). Listing 25b shows the RISC-V generated code to save register x8 in the save index \(\texttt {mX8} = 7\). Our model only uses the architecture’s specified register names, but llc uses the Abstract Binary Interface (ABI) names (x8 = s0). The index calculated for RISC-V ’s 32-bit (4 bytes) architecture is \(7 * 4 = 28\) (Line 7).