The formalism underlying EASYMAP: A precompiler for refinement-based exploration of hierarchical data organizations

In the computer science community, data structure design is mainly conducted at a high level of abstraction under the implicit assumption that the platform contains a monolithic memory. Exploiting platform-related knowledge such as available on-chip and off-chip memory sizes, the cache size, and the number of banks is mainly conducted in the system engineering community when the refined data structure has already been chosen. A convergence of both communities is desirable since this can lead to powerful optimizations.To achieve the convergence mentioned above, data-related transformations have been researched extensively in the recent past. Many of these transformations have a direct and large impact on memory footprint, execution time and energy consumption. Unfortunately, however, the most effective transformations are applied manually (e.g. in C code) and these result in a very time-consuming and error-prone design process. To overcome this burden, our general research goal is to develop a computer-aided design tool, called , that helps the designer to correctly construct the C code of an efficient but difficult-to-understand data structure. The formal design of is the topic of this article with the emphasis on , the internal language of . is based on a novel extension of Separation Logic’s spatial conjunction operator (∗), allowing it to concisely describe access operations of an irregularly accessed complex data organization. is the basic building block of ; it serves the purpose of automating ’s refinement process and proving that it is correct by construction.