40 - Separation algebra for CompCert

Summary

In building a Hoare logic over a language specified by an operational semantics, we can view the assertions of the Hoare logic as predicates on the states of the operational semantics. But we do this in two layers: first, relate the operational states into semantic worlds; then, apply the Hoare assertions to the worlds. We do this for several reasons: The operational states may contain information that we want to hide from the Hoare assertions, particularly control information (program counter, control stack) that is not supposed to be visible to a Hoare-logic assertion. The semantic worlds may contain information that we want to hide from the operational semantics, such as step-indexes, ghost variables, predicates in the heap (for modeling first-class functions or mutex locks), and permission-shares. For convenience in reasoning, we require Liebniz equality on worlds—equivalent worlds should be equal—but operational states do not generally satisfy Liebniz equality. In our two different toy examples (Chapter 9 and Chapter 39) we have separated operational states from semantic worlds, and we do so for the VST Separation Logic for CompCert C light.

Some components of the world are subject to separating conjunction (*), and others are not. Generally, to “heap” or “memory” or any other addressable component of the world, we apply separation in order to reason about antialiasing. Nonaddressable local variables (and the addresses of addressable local variables) do not require separation, because there is no aliasing to worry about.