In this paper we introduce High Assurance SPIRAL to solve the last mile problem for the synthesis of high assurance implementations of controllers for vehicular systems that are executed in today’s and future embedded and high performance embedded system processors. High Assurance SPIRAL is a scalable methodology to translate a high level specification of a high assurance controller into a highly resource-efficient, platform-adapted, verified control software implementation for a given platform in a language like C or C++. High Assurance SPIRAL proves that the implementation is equivalent to the specification written in the control engineer’s domain language. Our approach scales to problems involving floating-point calculations and provides highly optimized synthesized code. It is possible to estimate the available headroom to enable assurance/performance trade-offs under real-time constraints, and enables the synthesis of multiple implementation variants to make attacks harder. At the core of High Assurance SPIRAL is the Hybrid Control Operator Language (HCOL) that leverages advanced mathematical constructs expressing the controller specification to provide high quality translation capabilities. Combined with a verified/certified compiler, High Assurance SPIRAL provides a comprehensive complete solution to the efficient synthesis of verifiable high assurance controllers. We demonstrate High Assurance SPIRALs capability by co-synthesizing proofs and implementations for attack detection and sensor spoofing algorithms and deploy the code as ROS nodes on the Landshark unmanned ground vehicle and on a Synthetic Car in a real-time simulator.
Synthetic Aperture Radar (SAR) image processing platforms have to process increasingly large datasets under and hard
real-time deadlines. Upgrading these platforms is expensive. An attractive solution to this problem is to couple high
performance, general-purpose Commercial-Off-The-Shelf (COTS) architectures such as IBM's Cell BE and Intel's Core
with software implementations of SAR algorithms. While this approach provides great flexibility, achieving the requisite
performance is difficult and time-consuming. The reason is the highly parallel nature and general complexity of modern
COTS microarchitectures. To achieve the best performance, developers have to interweave of various complex optimizations
including multithreading, the use of SIMD vector extensions, and careful tuning to the memory hierarchy. In this
paper, we demonstrate the computer generation of high performance code for SAR implementations on Intel's multicore
platforms based on the Spiral framework and system. The key is to express SAR and its building blocks in Spiral's formal
domain-specific language to enable automatic vectorization, parallelization, and memory hierarchy tuning through rewriting
at a high abstraction level and automatic exploration of choices. We show that Spiral produces code for the latest Intel
quadcore platforms that surpasses competing hand-tuned implementations on the Cell Blade, an architecture with twice as
many cores and three times the memory bandwidth. Specifically, we show an average performance of 39 Gigaflops/sec for
16-Megapixel and 100-Megapixel SAR images with runtimes of 0.56 and 3.76 seconds respectively.