On the membership and correctness problem for state serializability and value opacity
Creators: name: König, Jürgen
Publisher: name: Universität Paderborn
Year: 2023

description: Transaktionaler Speicher (TS) ist ein Konzept zur Kontrolle von Nebenläufigkeit, das die Zugriffe von mehreren Threads auf geteilten Speicher verwaltet. Threads können Transaktionen ausführen, die vom Speicher lesen und auf ihn schreiben können. Jede Transaktion soll nach außen so aussehen, als ob sie in einem atomaren Block ausgeführt wurde. Trotzdem kann eine TS Implementation mehrere Transaktionen nebenläufig ausführen solange nach außen hin die Ausführung korrekt erscheint. Es gibt mehrere Korrektheitsbedingungen, die formalisieren was "nach außen hin korrekt erscheinen" bedeutet. Obwohl schon viele Ansätze für das Überprüfen, ob einzelne Ausführungen oder ganze Implementationen von TSs diesen Bedinungen genügen, vorgestellt wurden, ist den zugrundeliegenden theoretischen Problemen weniger Aufmerksamkeit zuteilgeworden. Diese sind das Membershipproblem (überprüfen, ob eine einzelne Ausführung korrekt ist) und das Correctnessproblem (überprüfen, ob alle Ausführungen einer Implementation korrekt sind). In dieser Arbeit geben wir einen detaillierten Überblick über die existierenden Ergebnisse zur Komplexität dieser Probleme und präsentieren zwei eigene Ergebnisse für jedes dieser Probleme. Die Korrektheitsbedingungen, auf die wir uns hier konzentriert haben, sind Strict State Serializability (SSR) und Value Opacity (VO). Wir zeigen durch eine Reduktion von State Serializability, eine weniger strenge Version von SSR, dass das Membershipproblem für VO NP-vollständig ist. Außerdem präsentieren wir Annahmen, unter denen das Membershipproblem für VO äquivalent zu dem für Conflict Opacity, eine simplere Variante von VO, ist. In Bezug auf das Correctnessproblem zeigen wir seine Entscheidbarkeit für SSR und VO unter einschränkenden Annahmen.
description: Transactional memory is a concept of concurrency control managing the accesses of multiple threads to shared memory. Similar to databases, threads issue transactions that can read from and write to the shared memory. Each transaction is supposed to look to the outside as being executed as an atomic block. However, a transactional memory implementation may execute transactions concurrently to optimize runtime as long as to the outside the execution appears to be correct. There are multiple correctness conditions formalizing what exactly "appears to be correct" means. While numerous approaches for checking if single executions or complete implementations fulfil these conditions have been proposed, the underlying theoretical problems have received less attention. These are the membership problem (checking whether a single execution is correct) and the correctness problem (checking whether all possible executions of an implementation are correct). In this thesis we give a detailed overview over the complexity results for each of these problems and present two results of our own for each of them. The correctness conditions we focussed on were strict state serializability - a version of serializability - and value opacity, which is a correctness condition similar to serializability but specifically designed for transactional memory. We show that the membership problem for value opacity is NP-complete by reduction from state serializability, a less strict version of strict state serializability.Additionally, we give assumptions under which the membership problem for value opacity is equivalent to the membership problem for a variant of opacity called conflict opacity that is easier to solve. For the correctness problem we investigate its decidability for strict state serializability and value opacity under assumptions. We show that the correctness problems for both ...