As multicore processors have become the standard architecture for general-purpose machines, programmers are required to write software optimized for parallelism. Verifying parallel code is very complex, and new practical methods for verification are therefore very important. Tools that provide verification for complex parallel code are still missing. This dissertation introduces a method for testing the execution of code and shows that this method already provides valuable results for the application programmer. The verification method is used to prove whether a program trace is linearizable. In addition, some useful properties of algorithms are highlighted by which a practical use of the method can be optimized. Furthermore, this work provides a case study on priority queues of how this method can be applied. Our case study shows that practicable results can be obtained with this method.     «

As multicore processors have become the standard architecture for general-purpose machines, programmers are required to write software optimized for parallelism. Verifying parallel code is very complex, and new practical methods for verification are therefore very important. Tools that provide verification for complex parallel code are still missing. This dissertation introduces a method for testing the execution of code and shows that this method already provides valuable results for the appli...     »

Multicore Prozessoren sind inzwischen zur Standardarchitektur für Prozessoren geworden. Folglich sind Programmierer immer mehr dazu angehalten, optimierte parallele Software zu entwickeln. Die Verifikation von parallelem Code ist sehr komplex, was neue praktikable Verifikationsmethoden notwendig macht. Es fehlt immer noch an Tools, welche komplexe parallele Programme verifizieren können. Diese Dissertation stellt eine Methode vor, welche Ausführungen von Programmen testet und zeigt, dass diese Methode bereits wertvolle Resultate für den Anwendungsprogrammierer liefert. Die Verifikationsmethode wird verwendet um zu beweisen, dass ein Programm-Trace linearisierbar ist. Ferner liefert diese Arbeit ein Fallbeispiel anhand von Priority Queues um zu zeigen, wie diese Methode angewendet werden kann und zeigt, dass praktikable Resultate mithilfe dieser Methode erzeugt werden können.     «

Multicore Prozessoren sind inzwischen zur Standardarchitektur für Prozessoren geworden. Folglich sind Programmierer immer mehr dazu angehalten, optimierte parallele Software zu entwickeln. Die Verifikation von parallelem Code ist sehr komplex, was neue praktikable Verifikationsmethoden notwendig macht. Es fehlt immer noch an Tools, welche komplexe parallele Programme verifizieren können. Diese Dissertation stellt eine Methode vor, welche Ausführungen von Programmen testet und zeigt, dass diese M...     »