Home

Awesome

multiplexed-io

This contains explorations, for AdaPilot, of implementing drivers for the AdaRacer MCU, using the Ravenscar profile of Ada 2012 from AdaCore and device bindings generated using SVD2Ada.

The structure corresponds to that proposed for the main AdaPilot repository.

Proof

Of particular interest is how "near the metal" we can get code that can be processed by SPARK GPL (2016).

The Ada Drivers Library imposes quite a lot of code between applications and the hardware, and that code is not in SPARK (nor is a move in this direction planned).

The code here provides minimal layers between applications and hardware.

Volatility

A major problem is dealing with volatile objects.

The device bindings declare registers as Volatile_Full_Access, which allows you to write code like

   bitfield_of_component := value;

which looks great, but under the hood GNAT implements this as

   local_variable := register;
   bitfield_of_local_variable := value;
   register := local_variable;

and suffers the usual concurrency-related problems. The only apparent solution to the gnatprove issue (not, of course, to the underlying concurrency vulnerability) is to mark the subprograms that have to modify device registers as being out of SPARK (pragma SPARK_Mode (Off);), and supply alternative reasoning to justify the code (I haven't done this :-).

Concurrent access

We have two devices using SPI2, the BARO (MS5611) and the FRAM (FM25V02). It is absolutely vital that they don't interfere with each other.

One approach would be to arrange a schedule so that each device is given its own time slot(s). That would be fine for the MS5611 on its own - bearing in mind that it requires two accesses to perform a measurement, the first to start the process and the second to fetch the result, which must occur after an interval depending on the measurement precision (9 ms for the highest precision). However the purpose of the FRAM is to store application parameters and checkpoint data, which might be quite hard to schedule with the MS5611.

Here, I've used an Ada protected object. Writing a command and its parameter, and retrieving the associated data, is performed within one protected action, so that other Ada tasks that try to access the same SPI will be blocked. One might want to arrange that these activities take place at a lower priority than others (RMA scheduling, perhaps), and there's the protected object's ceiling priority to organise also (the default is System.Priority'Last, i.e. the highest priority).

Timing remains to be done.

GNAT Project Files

Each component directory has three GNAT Project (.gpr) files (actually, the test directory breaks this to some extent):

The RTS/MCU selection supports building either

The reason for a separate <tt><i>component</i>_gnatprove.gpr</tt> is that gnatprove doesn't understand runtime or target settings within a GPR; proof is essentially platform-independent, so it's OK to use the host runtime.

Device variants

AdaRacer uses two of the six SPI peripherals on STM32F42[79] MCUs, which means that there is considerable commonality between the code for SPI1 and SPI2. Trying to address this using a generic resulted in a lot of problems at the proof stage, so instead this work uses template processing with <i>gnatprep</i>.

Preprocessing is triggered by make sources, and the results have been checked into the repository; see drivers/spi/, drivers/spi1, and drivers/spi2.

GNAT has a facility to integrate preprocessing, but it seems unlikely that this will work well with gnatprove.