Programming device drivers requires certain practices or operations. These include, for example, the multitude of volatile variables in the code. Volatiles are necessary to read from/to hardware registers for the device to function correctly and can be modified by the program's external environment.

On the other hand, SPARK imposes a number of restrictions on programs and also limits the use of certain practices permitted in Ada. The conventions imposed by SPARK are not all compatible with this type of code at first sight, so a “SPARKification” step is necessary in order to move on to SPARK-compatible code.

Here's a list of hurdles I encountered during my internship involving driver code and the rules authorized by SPARK. I also present ways of getting around these problems, as well as some best practices for having the most SPARK-compatible code in advance. This list is not exhaustive.

For your information, the examples given in this blog post are code snippets from the library I based my work on during my internship, made by Jeremy Grosser. For the sake of clarity, some parts of the code have been truncated to improve comprehension. You can find the same code after the modifications I've made here.

Volatile object

As mentioned in the introduction, volatile variables are very often present in drivers code, but SPARK imposes very restricted handling of them. Let's take a look at the code below as an example, where XOSC_Periph.CTRL.STABLE is a volatile variable.

This piece of code may seem correct, but it doesn't respect SPARK's rules. Indeed, if we look at SPARK reference manual, section 7.1.3 (10) tells us:

"Contrary to the general SPARK rule that expression evaluation cannot have side effects, a read of an effectively volatile object for reading is considered to have a side effect. To reconcile this discrepancy, a name denoting such an object shall only occur in a non-interfering context."

Even though the SPARK team is considering relaxing the restrictions to accept the original code as well, for the moment we have to deal with it.

We can see that this situation, in which the variable is volatile, does not correspond to a "non-interfering context". It is therefore necessary to transform the code so that it respects this rule. Let's consider this case authorized by the reference manual:

"A name occurs in a non-interfering context if it is: [...] the [right-hand side] expression of an assignment statement"

So, in order to bypass the restriction and allow this volatile variable to be used, we can assign its value to a temporary variable and reuse it later.

There is also a restriction on the declaration of volatiles, as shown in the following code.

We cannot declare the variable Flags like that because it must be declared at a library level. This is what the reference manual explains in section 7.1.3 (3):

"The declaration of an effectively volatile stand-alone object or type shall be a library-level declaration. [In particular, it shall not be declared within a subprogram.]"

So it is needed to declare the object in the library and not in a program. In our case, this is not possible because it depends on the function parameter. To avoid this problem, we need to assign every possible Flags value to a variable so that we can reuse it later.

The last point about volatile is that the function doesn't support volatiles but if the variable is just an input variable, the function can be annotated with "Volatile_Function". Like in this example where CLOCKS_Periph is a volatile record.

Use of global parameters

Another problem of becoming SPARK-compatible is the use of global parameters. As you may know (or not) functions and procedures are not the same, the distinction between the two is that a function returns a value, and a procedure does not. In SPARK, the difference is even stronger, as a function is not allowed to have side effects (no modification on the variables).

This is an example of a simple function. At first it seems compatible with SPARK restriction but as CLOCKS_Periph is a global parameter it is not permitted for this subprogram to be a function due to the side effect I mentioned before. So we have to transform it into a procedure. In some cases it can be easy or not very disturbing but sometimes you will need the result of the function in preconditions for example so the adaptation is then more complicated.

The following snippet has the same functionality as the above code but implements it as a procedure while the return value is an out parameter.

If you intend your code to be validated in SPARK, let's keep in mind that global variables can be problematic so try to limit the use of functions as much as possible.

Access to variables

Writing device drivers sometimes involves reading and having access to multiple instances of the same peripheral, in such cases it can be interesting to use pointers. Pointers are not a big problem because they are permitted in SPARK, but not when a variable is volatile and just like I said before volatiles are part and parcel of the device code.

We can take, for example, this function which calls PLL_SYS_Periph and PLL_USB_Periph instances of the PLL_Peripheral type by access.

An error is raised by SPARK as both variables are volatile. To avoid this problem, we introduce an auxiliary function into the main function, with the variable initially pointed to by access as an additional argument.

Thus, we can call the inner function with the right parameters depending on the value wanted.

Note that we used this trick for the SPI and UART ports to call the right peripherals. This was possible as there were only two ports for each protocol.

You can also see below how the port declarations were adapted to avoid using pointers. Instead of having the pointer, we give the correct variable depending on the port concerned.

This was possible as there were not a lot of ports, but we can see the limits here and how it can be difficult not to use access.

These restrictions also led us to modify a large part of the program by removing the HAL abstraction initially present. Indeed, interface accesses are not supported in SPARK at the moment. For the purposes of this internship, we have therefore chosen to remove this abstraction, which may be problematic in the context of a larger project where the code will be multiplied.

Address

The address clause is authorized under certain conditions but in the example below it is not permitted as the object is not fully initialized at declaration.

In this case to avoid having problems with SPARK, it is recommended to rename the variable as it corresponds to the same operation. The fewer clause addresses you use, the fewer problems you will encounter.

If renaming is not possible, it's best to avoid accessing the address of values when not required. If the address is mandatory, use SPARK_Mode => Off.

Numeric type and conversion

A basic recommendation is that the data type should be as precise as possible. Even if this has no direct impact, it greatly facilitates proof by SPARK. It's also easy to specify types in this kind of application, where data is often constrained by the environment or hardware.

It's also recommended to be careful with type conversions, as a wrong conversion can corrupt data integrity. For example, SPARK does not yet allow conversion between fixed-point and floating-point. The use of unchecked conversions must be limited, and the size of both types must be specified and equal.

Conclusion

So we've looked at a few tricks for adapting existing low-level code to SPARK and reconciling SPARK restrictions with the needs of driver code. While SPARK imposes certain restrictions on device driver programming, it presents an opportunity to create secure and reliable code. By embracing the challenges and following best practices, developers can achieve SPARK-compatible solutions that ensure robustness and improve the overall quality of their projects.