Concolic testing of concurrent software in the context of weak memory models

Abstract

Mit zunehmend komplexerer und gleichzeitig allgegenwärtig werdender Software wird die Verlässlichkeit von Software immer wichtiger. Forschung zu Testen und Verifikation von Software versucht automatisierte Lösungen zu finden, welche Software gründlich nach Fehlern durchsuchen. Ein Beispiel für Forschungserfolge ist Concolic Testing, eine Kombination aus konkretem und symbolischem Testen, welches in vielen aktuellen Test-Werkzeugen verwendet wird. Allerdings ist das Testen von nebenläufiger Software nach wie vor ein offenes Problem. Eine der Hauptschwierigkeiten beim Testen solcher Software ist das Bestimmen der Reihenfolge in welcher die Befehle der verschiedenen Programmstränge ausgeführt werden sollen. Der Grund für die Schwierigkeit dahinter liegt in der Zahl der Reihenfolgen der verschiedenen Reihenfolgen welche unlösbar groß sein kann. Hinzukommen sogenannte Weak Memory Models (WMMs), welche Speicherarchitekturen beschreiben und die Zahl der Reihenfolgen weiter erhöhen können. Weak Memory Models erlauben Abweichungen von dem erwarteten Prozesslokalem Programmablauf. Zum Beispiel kann es passieren, dass der Effekt eines Schreibzugriffs von einem Programmstrang auf eine Speicheradresse in einem anderen Programmstrang, welcher von dieser Adresse liest, nicht sofort für alle andere Threads sichtbar wird. Der Grund für diese Abweichungen liegt in modernen Speicherhierarchien welche es erlauben, dass Berechnungen über mehrere Prozessor-Kerne aufgeteilt werden. Aus diesem abweichenden Verhalten können Fehler resultieren, welche mit konventionellen Testtechniken nur schwer wenn nicht sogar unmöglich zu finden sind. Die meisten Test-Werkzeuge basieren auf der Annahme, dass diese Effekte nicht auftreten können. Dieses Annahme wird auch als sequentielle Konsistenz bezeichnet Diese Arbeit präsentiert C ON C REST WMM, ein Programm welches Concolic Testen verwendet um nebenläufige Software zu testen und welches in der Lage ist die Effekte von Weak Memory Models während der Ausführung von Tests zu simulieren. C ON C REST WMM wurde als eine Erweiterung von C ON C REST , ein Test-Werkzeug für nebenläufige Software, implementiert. Der WMM-Scheduler bildet eine zentrale Komponente von C ON C REST WMM. Durch die Verwendung von WMM-Schedules ist es möglich die Effekte eines WMMs auszuwählen und an einem bestimmten Punkt während der Ausführung eines Testfalls auszuführen. Als Konsequenz daraus ist es möglich mit C ON C REST WMM Fehler, welche auf modernen sequentiell inkonsistenten Prozessoren auftreten können, zu entdecken. Zwei Weak Memory Models werden als Teil dieser Arbeit präsentiert. Als erstes das WMM Sequential Consistency, welches verwendet werden kann um das Verhalten von C ON C REST zu simulieren und als zweites das Partial Store Order (PSO) WMM, ein Model, welches es ermöglicht die Effekte eines Schreib-Events zu verzögern. Speicher-Barrieren sind ein gebräuchliches Mittel um Abweichungen von sequentieller Konsistenz zu vermeiden. Durch die Verwendung von Speicher-Barrieren ist es möglich die Sichtbarkeit der Effekte von Schreib-Events sichtbar zu machen. Deshalb sind Speicher-Barrieren in C ON C REST WMM unterstützt. Da viele nebenläufige Programme und Datenstrukturen Compare and Swap (CAS) Operationen verwenden, ist sie auch in C ON C REST WMM realisiert. Die CAS Operation aktualisiert eine Speicheradresse mit einem neuen Wert sollte der Wert an der Adresse mit einem erwarteten Wert übereinstimmen. Die eingebaute Operation bietet die gleiche Semantik wie die vom GCC Compiler angebotene Boolsche CAS Operation und ist atomar. Zusätzlich ist die eingebaute CAS Operation mit symbolischer Information ausgestattet. Das ermöglicht es C ON C REST WMM nach Testfällen zu suchen welche beide Stränge der CAS Operation verwenden, d.h., dass Testfälle gesucht werden, welche den Wert an der Speicheradresse verändern und Testfälle welche dies nicht tun. Um die Implementierung von C ON C REST WMM zu Testen und ihre Fähigkeiten zu demonstrieren werden mehrere Beispiele durchgeführt. Diese Beispiele stammen aus der Literatur. Die Experimente zeigen, dass im Durchschnitt C ON C REST WMM nur einen konstanten Faktor von ~ 1.15 langsamer ist als C ON C REST wenn die Werkzeuge verglichen werden.

With software becoming ubiquitous and increasingly complex, software reliability also becomes more important. Research on software testing and verification tries to create automated solutions which exhaustively search for software bugs. One promising example for these research efforts is concolic testing, a testing technique that combines concrete with symbolic execution and which is implemented in various recent testing tools. However, testing of concurrent software still remains a challenge. One of the main difficulties for testing concurrent software is determining the order in which the statements from different threads have to be executed. The reason for this being a challenge is that the number of possible executions can be intractably big. Furthermore, weak memory models, which describe the memory architectures of modern processors, can further increase the number of possible executions. Weak memory models allow certain deviations from the expected thread-local program order. For example, the effects of a write from one thread to a memory location might not become immediately visible in another thread which reads from this particular memory address. This results from modern memory hierarchies when computations are distributed over several computing cores. The consequence of such behaviours can be software bugs that are hard or even impossible to detect with conventional testing techniques. Most testing tools are based on the assumption of the Sequential Consistency model, i.e., that these effects cannot occur. This thesis presents C ON C REST WMM, a concolic testing tool for concurrent software that is able to simulate the effects of weak memory models during an execution of a program under test. C ON C REST WMM is implemented as an extension of the tool C ON C REST , a testing tool for concurrent software. As a central component, C ON C REST WMM adds a WMM-Scheduler. By using WMM-schedules it is possible to select a WMM and to trigger effects of this model at specific points during the execution of a test case. Thus, the tool C ON C REST WMM offers the possibility to discover bugs that can occur on real-world processor architectures that do not adhere to Sequential Consistency but to another WMM. Two WMMs are implemented as part of this thesis. First, the WMM Sequential Consistency which can be used to simulate the behaviour of C ON C REST and second, the Partial Store Order (PSO) WMM, a model which allows to delay the effect of a write event. Memory barriers are a common means to limit the deviation of executions from Sequential Consistency. By using memory barriers it is possible to force the effect of writes to become visible. Support for memory barriers is also implemented in C ON C REST WMM. Since many concurrent applications and data structures make use of a Compare and Swap (CAS) operation, a CAS operation is also implemented as part of C ON C REST WMM. The CAS operation updates a memory cell with a new value if the cell contains an expected old value. The built-in operation offers the same semantics as the Boolean CAS operation offered by the compiler GCC and is atomic. Moreover, the built-in CAS operation is equipped with symbolic information. This enables C ON C REST WMM to search for test cases covering both branches of the CAS-operation, i.e., finding test cases where the value at the memory location is changed and test cases where the value is not changed. To test the implementation of C ON C REST WMM and to show its capabilities, several experiments were performed. These examples are taken from the literature. The experiments show that on average C ON C REST WMM is only a constant factor of ~ 1.15 slower than C ON C REST when comparing both tools.