{'fraction_non_alphanumeric': 0.019243530192435302, 'fraction_numerical': 0.0, 'mean_word_length': 5.205761316872428, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Modular Metatheory for Memory Consistency Models

We present a framework based on operational semantics for formalizing shared-memory multithreaded programming languages with relaxed memory consistency models. The key feature of our framework is a division of each system’s semantics into two modules, the program semantics and the heap semantics. This modularization allows elegant, concise, and reusable components. It is trivial to use the same memory model with multiple languages and the same language with multiple memory models. We demonstrate the effectiveness of our framework by proving several results. First, we give a semantics for the Partial Store Order memory model, and prove that data-race-free programs exhibit sequentially-consistent semantics using this model. Critically, we did not need to define a specific language semantics to prove this result. We assumed only that the language satisfies certain sanity checks easily met by realistic languages. Second, we generalize the notion of type safety to arbitrary memory models, and prove type safety for a multithreaded simply-typed lambda calculus for any type-preserving memory model. Finally, we present a model of the MSI cache coherence protocol, and prove that it is semantically equivalent to sequential consistency for any language. We used the Coq proof assistant to carry out and mechanically verify all our work. Our Coq code is freely available and was modularly designed to support reuse for future extensions and projects.