Compositional noninterference on hardware weak memory models

Weak memory models are employed by all modern multicore processors to improve their performance. For most code, the effects of such memory models can be largely ignored by the programmer. However, for low-level operating system or library code which can include data races for efficiency, these effects may lead to information leaks which cannot be detected without taking the specific memory model into account. While there have been some efforts to develop information flow logics which can detect such leaks, the existing approaches are either not compositional, hindering scalability, or support only a limited form of compositionality, reducing applicability to programs with only simple interactions between threads.