The structure corresponds to that proposed for the main AdaPilot repository.
Of particular interest is how "near the metal" we can get code that can be processed by SPARK GPL (2016).
The code here provides minimal layers between applications and hardware.
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 :-).
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):
- component_build.gpr calls component.gpr to build this component for the selected RTS (and MCU),
- component.gpr builds the component, calling in the GPRs of other components as required,
- component_gnatprove.gpr is for use with gnatprove.
The RTS/MCU selection supports building either
- for the AdaRacer platform (with the scenario variable
RTSset to, or left at, its default (
adaracer)), using the
- for the STM32F4Discovery kit (with the scenario variable
stm32f4), using the
The reason for a separate component_gnatprove.gpr 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.
AdaRacer uses two of the six SPI peripherals on STM32F42 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 gnatprep.
Preprocessing is triggered by
make sources, and the results have been checked into the repository; see
GNAT has a facility to integrate preprocessing, but it seems unlikely that this will work well with gnatprove.