Uniqueness Types for Efficient and Verifiable Aliasing-Free Embedded Systems Programming

An important consequence of only having value types in an aliasing-free programming language is the significant reduction in annotation burden to verify programs using semi-automatic proof systems. However, values in such language are often copied implicitly which is detrimental to the execution speed and memory usage of practical systems. Moreover, embedded systems programmers need fine-grained control over the circumstances at which data is copied to be able to predict memory use and execution times. This paper introduces a new approach to using uniqueness types to enable building efficient and verifiable embedded systems using an aliasing-free programming language. The idea is to use uniqueness types for enforcing at-most-once consumption of unique values. The proposed model of uniqueness of values enables compiler optimizations such as elimination of physical copies and in-place mutation. In addition, the proposed approach provides a lightweight notation for the programmer to control copying behavior. We have implemented our method in Sim, a new language for the development of safety-critical software. Our validation cases suggest that our aliasing-free language allows one to verify the functional correctness of realistic embedded programs with only a small annotation overhead while keeping the run-time performance of the program up to par with hand-optimized code.status: Published onlin