Achieving real-time performance improvements within the SPARK framework

RapiTime is the only commercial tool on the market suitable for optimising reactive, real-time software, where average case performance is irrelevant and the worst-case performance must be studied.

Working on SPARK projects has highlighted an issue which we decided to bring to your attention. When RapiTime highlights potential optimisation candidates, we are informed that the code may be inefficient but it conforms to SPARK guidelines.

Any changes that require a deviation from the SPARK subset of Ada lead to additional validation and maintenance costs. These costs may well be justified using the evidence from RapiTime so this is not an insurmountable obstacle.

However, you may be surprised how often it is possible to retain SPARK conformance whilst still meeting challenging real-time requirements. In AdaCore's Ada Gem #80, Rod Chapman writes specifically about shift and rotate operations but the technique described is more generic and can be used to preserve SPARK conformance when performing a number of potent optimisations.