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 sdrah 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 easymap, that helps the designer to correctly construct the C code of an efficient but difficult-to-understand data structure. The formal design of easymap is the topic of this article with the emphasis on cha, the internal language of easymap. Cha 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. Cha is the basic building block of easymap; it serves the purpose of automating easymap's refinement process and proving that it is correct by construction.