Well synchronized programs should not have data races, and programs whose sequentially consistent executions have no data races should run on weakly consistent multiprocessors as if they were sequentially consistent. The former claim comes from Dijkstra and Hoare through formalizations by O’Hearn and Brookes; the latter was stated by Saraswat et al. as a desideratum for compilers and multiprocessors.
We prove these claims for Concurrent Separation Logic, the CompCert C compiler, and the Intel x86 computer architecture. C programs proved in CSL, compiled with this optimizing C compiler and run on that machine, have the (sequentially consistent) behavior proved at the source level. Our proof is modular: a theorem about the soundness of CSL with respect to the operational semantics of C (and our 5 synchronization functions); a correctness theorem for the C compiler; a theorem about the Intel x86-TSO architecture.
This paper introduces a strengthening of the release-acquire fragment of the C11 memory model that
forbids dubious behaviors of programs such as 2+2W that are not observed in any implementation;
supports fence instructions that restore sequential consistency; and
admits an equivalent intuitive operational semantics based on point-to-point communication.
This strengthening has no additional implementation cost: it allows the same local optimizations as C11 release and acquire accesses, and has exactly the same compilation schemes to the x86-TSO and Power architectures. In fact, the compilation to Power is complete with respect to a recent axiomatic model of Power; that is, the compiled program exhibits exactly the same behaviors as the source one. Moreover, we provide criteria for placing enough fence instructions to ensure sequential consistency, and apply them to an efficient RCU implementation.
Recent advances in hardware design have demonstrated mechanisms allowing a wide range of low-level security policies micro-policies to be expressed using rules on metadata tags. We propose a methodology for defining and reasoning about such tag-based reference monitors in terms of a high-level "symbolic machine," and we use this methodology to define and formally verify micro-policies for dynamic sealing, compartmentalization, control-flow integrity, and memory safety; in addition, we show how to use the tagging mechanism to protect its own integrity. For each micro-policy, we prove by refinement that the symbolic machine instantiated with the policy's rules embodies a high-level specification characterizing a useful security property. Last, we show how the symbolic machine itself can be implemented in terms of a hardware rule cache and a software controller.