An actor constraint prototype : verifying event order

Abstract

Diese Diplomarbeit beschreibt Design, Umsetzung und Analyse eines Prototyps, welcher die Definition eines Synchronisations-Protokolls zur Verifizierung der Reihenfolge von Nachrichten zwischen Aktoren erlaubt. Der Prototyp erweitert AKKA, ein etabliertes Aktoren-System und erlaubt es, mittels einer Domain-Specific-Language Regeln zu definieren. Der Prototyp stellt sicher, dass das das Aktoren-System diese Regeln einhält, indem er alle Nachrichten findet, die eine Regel verletzen. Zwei Versionen der Verifikation wurden implementiert. Beide verwenden dieselbe Verifikationslogik, unterscheiden sich aber in der Art und Weise, in der sie Interaktionen loggen und überprüfen, ob eine Regel feuert. History Logging Verification hält ein Log aller bisherigen Interaktionen mit einem Aktor, Automaton Verification erzeugt für jede Regel einen Automaten. Zur Evaluation des Prototyps wurde die Worst-Case Laufzeit der Verifikations-Algorithmen bestimmt, es wurden Tests mit Real-World Applikationen durchgeführt und ein Benchmark wurde durchgeführt. Für beide Verifikations-Algorithmen wurde die Worst-Case Laufzeit der Verifikation bestimmt. Für die Automaton Verification wurden zusätzlich die Worst-Case Laufzeiten für das Erzeugen sowie das Optimieren eines Automaten für eine Regel bestimmt. Um den Prototyp unter realen Bedingungen zu testen wurden zwei Applikationen implementiert: Die Erste realisiert das Chameneos Concurrency Game, die Zweite simuliert einen Token-Ring. Diese zweite Applikation wurde auch verwendet, um Benchmark-Tests mit dem Prototyp durchzuführen. Dazu wurde die Token-Ring-Applikation in verschiedenen Konfigurationen ohne Prototyp, mit der History Logging Verification und mit der Automaton Verification ausgeführt und die ermittelten Laufzeiten zusammengefasst sowie grafisch aufbereitet.

This thesis describes design, implementation and evaluation of a prototype that allows us to define synchronisation protocols for the verification of message orders between actors. The prototype extends AKKA, an existing actor concurrency implementation, provides a verification layer on top of it and a domain-specific language to write synchronization rules. Rules can be defined on a per-actor basis. The prototype makes sure the actor system complies with them and detects unwanted message orders. Two verification algorithms were implemented for the prototype. Both use the same basic verification logic, but differ in how they log interactions between actors and how they check firing of rules. History logging verification keeps a log of interactions for each actor and uses it to check if a rule fires. Because this approach proved to be memory intensive and not performant enough, a second algorithm was implemented which circumvents these issues. Automaton verification creates an automaton for each rule. Interactions with the actor are logged by changing the automaton-s active state and the active state of an automaton is used to determine if a rule fires. Evaluation of the prototype consisted of worst-case runtime determination, tests with real world applications and benchmarking. For both implemented verifiction algorithms the worst-case runtime of the verification itself was determined. For the automaton verification also the worst-case runtime of automaton creation and -optimization was determined. To test the prototype under real world conditions, two sample applications were written: One which implements the Chameneos Concurrency Game and another one which implements a token ring. The latter also was used to perform benchmark tests, by running the application in different configurations without the prototype, with the history logging verification and with the automaton verification and the resulting overall runtimes were measured and graphically evaluated.