Justifying the strong memory semantics of concurrent high-level programming languages for system programming

Abstract

In this thesis we justify the strong memory semantics of high-level concurrent languages, such as C11 or Java, when compiled to x86-like machines. Languages such as C11 guarantee that programs that obey a specific software discipline behave as if they were executed on a simple coherent shared memory multi-processor. Real x86 machines, on the other hand, do not provide a coherent shared memory, and compilers add slow synchronizing instructions to provide the illusion of coherency. We show that one software discipline that closely matches software disciplines of languages such as C11 and Java — in a nutshell, that racing memory accesses are annotated as such by the programmer — and one particular way to add relatively few synchronization instructions — in a nutshell, between an annotated store and an annotated load in the same thread — suffice to create this illusion. The software discipline has to be obeyed by the program in the semantics of the high-level language, therefore allowing the verification effort to take place completely in the strong memory semantics of the high-level language. We treat a machine with operating system support, and accordingly our theorems can be used to verify interruptible multi-core operating systems, including those where users can run unverified programs that do not obey the software discipline.

In dieser Dissertation rechtfertigen wir die sequentiell konsistente Semantik von parallelen Hochebenensprachen wie C11 oder Java, wenn diese für x86-ähnliche Architekturen übersetzt werden. Sprachen wie C11 garantieren dass Programme, welche eine bestimmte Software-Disziplin befolgen, sich so verhalten als würden sie auf einer einfachen kohärenten Mehrkernprozessor mit gemeinsamem Speicher ausgeführt werden. In echten x86 Maschinen ist der gemeinsame Speicher hingegen nicht kohärent, und Übersetzer fügen langsame Synchronisationsinstruktionen ein, um Kohärenz vorzugaukeln.Wir zeigen dass eine Software-Disziplin die sich stark an Software-Disziplinen solcher Programmiersprachen wie C11 und Java anlehnt — im Grunde, dass Speicher-zugriffe in einer Wettlaufsituation vom Programmierer annotiert werden — und eine bestimmte Methode, relativ wenige Synchronisationsinstruktionen einzufügen — im Grunde zwischen einem annotierten Schreibzugriff und einem annotierten Lesezugriff des gleichen Fadens — ausreichen, um diese Illusion zu gewährleisten. Die Software-Disziplin müssen bei individuellen Programmen nur in der sequentiell konsistenten Semantik der Hochebenensprache geprüft werden, so dass die gesamte Verifikationsarbeit in der sequentiell konsistenten Semantik der Hochebenensprache stattfinden kann. Wir behandeln eine Maschine mit Betriebssystemunterstützung, und unsere Theoreme können entsprechend auch zur Verifikation unterbrechbarer Mehrkern-Betriebssysteme verwendet werden, einschliesslich solcher, bei denen Benutzer unverifizierte Programme laufen lassen können, die nicht die Software-Disziplin befolgen.