Der traurige Zustand von Property-Based-Testing-Bibliotheken

 (stevana.github.io)
1 Punkte von GN⁺ 2024-07-06 | 1 Kommentare | Auf WhatsApp teilen
  • Property-based Testing hat sich seit QuickCheck auf viele Sprachen verbreitet, doch Stand Juli 2024 bieten viele Bibliotheken zustandsbasiertes Testen und paralleles Testen, die bereits 2009 ausgearbeitet wurden, noch immer nicht ausreichend an
  • Die zentrale Lücke liegt in der Fähigkeit, sequentielle Zustandsänderungen mit einem Zustandsmaschinenmodell zu prüfen und dasselbe Modell für Linearisierbarkeits-Checks (linearisability) wiederzuverwenden, um bei paralleler Ausführung Race Conditions zu finden
  • Bei vielen untersuchten Projekten fehlt zustandsbasiertes Testen ganz oder ist experimentell, und paralleles Testen ist noch seltener; bei FsCheck, Gopter, RapidCheck, SwiftCheck und jsverify bestehen entsprechende Issues seit Jahren
  • Eine Haskell-Implementierung mit etwa 400 Zeilen reproduziert zustandsbasiertes und paralleles Property-based Testing und verwendet statt einer traditionellen Zustandsmaschinen-Spezifikation eine fake-basierte Referenzimplementierung als Modell, die Programmierern vertraut ist
  • Vertragsgetestete Fakes lassen sich nicht nur zur Verifikation einzelner Komponenten nutzen, sondern auch für schnelle und deterministische Integrationstests, in die sie anstelle echter Abhängigkeiten injiziert werden können

Die nach QuickCheck entstandene Funktionslücke

  • Property-based Testing verbreitete sich in vielen Programmiersprachen-Communities unter dem Motto: „Schreibe keine Tests, sondern generiere sie“
  • Auf der Wikipedia-Seite der ursprünglichen Haskell-Bibliothek QuickCheck sind 57 Reimplementierungen in anderen Sprachen aufgeführt
  • Das erste QuickCheck-Paper, QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs, wurde auf der ICFP 2000 vorgestellt, und der vollständige Quelltext der ersten Implementierung bestand aus rund 300 Zeilen Code im Anhang des Papers
  • Frühes QuickCheck konnte nur reine Funktionen testen; 2002 legte Testing monadic code with QuickCheck die Grundlage für den Umgang mit effektivem Code wie mutablem State, Datei-I/O und Networking

Das Aufkommen von zustandsbasierten und parallelen Tests

  • Quviq AB wurde 2006 von John Hughes und Thomas Arts gegründet; ein frühes Einsatzszenario war das Testen des Erlang-Projekts von Ericsson
  • Da Erlang keine rein funktionale Sprache ist und Nebenläufigkeit dort häufig vorkommt, war das bestehende monadische QuickCheck allein nicht bequem genug einsetzbar
  • Das Closed-Source-Erlang-QuickCheck von Quviq enthielt zwei Funktionen, die in vielen späteren Open-Source-Implementierungen fehlen
    • Sequentielles zustandsbasiertes Property-based Testing mit Zustandsmaschinenmodell
    • Paralleles Testen zur Erkennung von Race Conditions durch Wiederverwendung desselben sequentiellen Zustandsmaschinenmodells
  • Zustandsbasiertes Testen erscheint in seiner heutigen Form in QuickCheck testing for fun and profit (2007)
  • Paralleles Testen wird in Finding Race Conditions in Erlang with QuickCheck and PULSE (ICFP 2009) ausführlich behandelt und nutzt als Kerntechnik Linearizability: a correctness condition for concurrent objects (1990) von Herlihy und Wing
  • Der Bibliothekscode von Quviq QuickCheck wurde in den Papers nicht geteilt; veröffentlicht wurden nur die API und Testbeispiele, die diese API verwenden

Ergebnisse der Bibliotheksuntersuchung 2024

  • Der aktuelle state of the art sind modellbasierte stateful tests mit Zustandsmaschinen sowie parallel tests, die dasselbe sequentielle Modell mit Linearisierbarkeit kombinieren
  • Die Untersuchung basiert auf dem Lesen von Dokumentation, Issue-Trackern und teilweise Quellcode mit Stand Juli 2024
  • Viele Bibliotheken bieten zustandsbasiertes Testen nicht oder nur eingeschränkt an
    • Bei QuickCheck (Haskell) ist seit 2016 ein Issue zur Ergänzung zustandsbasierter Tests offen
    • Auch bei SwiftCheck ist seit 2016 ein Issue zur Ergänzung zustandsbasierter Tests offen
    • Bei jsverify besteht seit 2015 ein offenes Issue zur Ergänzung zustandsbasierter Tests
    • Für proptest (Rust) muss auf das separate proptest-state-machine verwiesen werden
  • Unterstützung für paralleles Testen ist noch seltener
    • Bei Gopter steht im README „No parallel commands … yet?“, dazu gibt es ein Issue von 2017
    • Bei FsCheck ist seit 2016 ein Issue zur Ergänzung von Parallel-Support offen
    • Bei RapidCheck ist seit 2015 ein Issue zur Ergänzung von Parallel-Support offen
    • Bei propcheck gibt es seit 2020 ein Issue zur Ergänzung von parallelem Testen
  • Als Open-Source-Beispiele mit Unterstützung für beide Funktionen werden PropEr, Hedgehog, qcheck-stm, quickcheck-state-machine und stateful-check genannt
  • Auch dort, wo Parallelfunktionen vorhanden sind, gibt es Einschränkungen
    • Im Quellcode von QuickTheories steht in einem Kommentar, dass bei parallelen Tests die Zahl möglicher Endzustände mit der Anzahl der Kommandos schnell wächst, weshalb die command list meist auf höchstens 10 Einträge begrenzt werden sollte
    • Die LevelDB- und Redis-Beispiele von ScalaCheck werden als sequentielle Beispiele mit threadCount = 1 gezeigt
    • Die Race-Condition-Unterstützung von fast-check scheint sich im Unterschied zu den parallelen Tests von Quviq QuickCheck nicht auf die Wiederverwendung eines sequentiellen Zustandsmaschinenmodells oder auf Linearisierbarkeit zu stützen
  • Ein klarer Fall, in dem paralleles Testen später hinzugefügt wurde, ist nicht erkennbar; wenn es nicht von Anfang an im API-Design berücksichtigt wird, könnte eine erhebliche Neugestaltung nötig sein

Warum sich die Funktionen nur langsam verbreitet haben

  • John Hughes nennt dafür drei Gründe
    • Zustandsbasierte und parallele Tests seien nicht so nützlich wie Tests reiner Funktionen
    • Das Schreiben von Zustandsmaschinenmodellen erfordere eine andere Denkweise als gewöhnliches Testen und brauche Schulung
    • Allein mit Open Source sei industrielle Adoption schwer gelungen; Closed-Source-Produkte sowie Schulung und Beratung hätten die Einführung unterstützt
  • Auch wenn man bereits viel gewinnt, wenn man nur reine funktionale Teile mit Property-based Testing testet, sind in industriellen Systemen Datenbanken, zustandsbehaftete Protokolle und nebenläufige Datenstrukturen häufig, sodass zustandsbasierte und parallele Tests fast genauso wichtig sind
  • Zustandsbasierte Spezifikationen sind nicht immer schwieriger als Spezifikationen reiner Funktionen
    • Ein Modell für einen Key-Value-Store kommt mit einer Liste von Key-Value-Paaren bereits erstaunlich weit
    • Im LevelDB-Fall fand ein einfaches Modell in wenigen Minuten ein auf 17 Schritte reduziertes Counterexample, und nach Googles Korrektur in wenigen weiteren Minuten ein Counterexample mit 31 Schritten
    • Das zweite Problem war ein Bug im Background-Compaction-Process; Compaction ist wichtig für bessere Leseleistung und die Rückgewinnung von Speicherplatz, wurde im Modell aber nicht explizit erfasst
  • Closed Source mag die industrielle Einführung unterstützt haben, für die Open-Source-Adoption habe es jedoch nicht geholfen
  • Um die Ergebnisse der Papers ohne Quviq-QuickCheck-Lizenz nachzubauen, wäre viel Reverse Engineering nötig, was praktisch kaum möglich sei

Vorschlag: kleine offene Implementierung und einfache Spezifikationen

  • Es gibt zwei Richtungen zur Verbesserung
    • Wie bei der ursprünglichen QuickCheck-Implementierung mit rund 300 Zeilen sollte eine kurze Open-Source-Implementierung für zustandsbasiertes und paralleles Property-based Testing bereitgestellt werden
    • Statt Zustandsmaschinen sollen zur Verringerung des Aufwands für Spezifikationen Konzepte wie Mock und Test Double wiederverwendet werden, mit denen Programmierer bereits vertraut sind
  • Um diese Hypothese zu prüfen, werden zwei Dinge gezeigt
    • Zustandsbasiertes und paralleles Property-based Testing wird in etwa 400 Zeilen Code implementiert
    • Als Modell wird statt einer state machine eine In-Memory-Referenzimplementierung verwendet, also ein Fake

Zusammenfassung von reinem Property-Based Testing

  • Beim Testen reiner Funktionen werden Eingaben erzeugt und es wird geprüft, welche Beziehung die Funktionsausgabe zur Eingabe erfüllt.
  • Zum Beispiel kann reverse mit der Property reverse (reverse xs) == xs für eine beliebige Liste xs getestet werden.
  • QuickCheck erzeugt standardmäßig 100 Tests und shrinkt bei einem Fehlschlag die Eingabe, um ein minimales Gegenbeispiel zu präsentieren.
  • Eine falsche Property wie reverse xs == xs wird zu einem minimalen Gegenbeispiel wie [0,1] verkleinert.
  • Häufig vorkommende Property-Muster sind Inverse, Idempotenz, Assoziativität, Axiome abstrakter Datentypen, metamorphische Properties usw.
    • Inverse: deserialise (serialise i) == i
    • Idempotenz: sort (sort xs) == sort xs
    • Assoziativität: (i + j) + k == i + (j + k)

Zustandsbasiertes Property-Based Testing

  • Zustandsbehaftete Komponenten erzeugen bei gleicher Eingabe nicht immer dieselbe Ausgabe.
    • Das Ergebnis des ersten incr und des zweiten incr eines Counters hängt vom vorherigen Zustand ab.
    • Auch bei Datenbanken und Dateisystemen beeinflusst die Historie vorheriger Eingaben die nächste Ausgabe.
  • Wenn Tests reiner Funktionen eine einzelne Eingabe behandeln, erzeugen zustandsbasierte Tests Eingabesequenzen, um zu prüfen, wie sich das System im Zeitverlauf verändert.
  • Das Modell wird als Fake in der Form m -> i -> (m, o) dargestellt.
    • Aus dem vorherigen Modellzustand m und der Eingabe i werden das nächste Modell und die Ausgabe o berechnet.
    • Die Ausgabe des realen Systems wird in jedem Schritt mit der Ausgabe des Fake verglichen.
    • Bei einer Abweichung wird die Eingabesequenz geshrinkt, um ein kleines Gegenbeispiel zu finden.

  • Counter-Beispiel

    • Als Testobjekt dient ein Haskell-Counter mit globaler veränderlicher Variable.
    • incr erhöht den Counter, get liest den aktuellen Wert aus.
    • Das Modell kommt mit einem einzigen Counter Int aus, und die StateModel-Instanz definiert den Anfangszustand Counter 0, Incr, Get, Incr_ (), Get_ Int, runFake, runReal und den Command-Generator.
    • Fügt man einen Bug wie incr42Bug ein, bei dem der Counter beim Wert 42 nicht erhöht wird, findet QuickCheck nach 66 Tests einen Fehlschlag und präsentiert nach 29 Shrinks als minimales Gegenbeispiel ein Get nach 43 Increments.
    • Wenn der reale globale Counter zwischen den Tests nicht per reset zurückgesetzt wird, startet das Modell zwar immer bei 0, der reale Counter behält aber den Zustand des vorherigen Tests, was zu einem Mismatch führt.

  • Zustandsbasierte Bibliotheks-Schnittstelle

    • Die StateModel-Schnittstelle betrachtet das zu testende System als Black Box, bei der Commands als Eingabe und Responses als Ausgabe dienen.
    • Die zentralen Bestandteile sind Command state, Response state, initialState, runFake, runReal und generateCommand.
    • Optionale Bestandteile sind die folgenden:
      • Reference: wird verwendet, wenn ein späterer Command auf eine Ressource verweist, die durch eine frühere Response erzeugt wurde, etwa ein File Handle.
      • PreconditionFailure: drückt einen Fehlschlag einer Vorbedingung aus, etwa dass nicht von einem Handle gelesen werden darf, das keine offene Datei ist.
      • CommandMonad: standardmäßig IO, es kann aber auch eine andere Monad verwendet werden.
      • monitoring, commandName: werden für Coverage und Statistiken verwendet.
    • Bei der Command-Erzeugung können Werte wie echte File Handles nicht erzeugt werden, daher werden symbolische Referenzen in der Form Var Int erzeugt und während der Ausführung durch echte Referenzen ersetzt.
    • Nach dem Shrinking werden Commands entfernt, die Vorbedingungen verletzen oder symbolische Referenzen außerhalb ihres Gültigkeitsbereichs verwenden.

  • Circular-Buffer-Beispiel

    • Eine in C geschriebene Circular Queue wird per Haskell FFI getestet, das Modell ist eine einfache listenbasierte Queue.
    • Die C-Implementierung enthält keine Fehlerprüfungen, sodass get bei einer leeren Queue nicht initialisierten Speicher zurückgeben kann.
    • Die reale Implementierung ist durch den zirkulären Index effizient, aber nicht offensichtlich korrekt; der Fake ist weniger effizient, was für Tests jedoch kein Problem ist.
    • Da new eine Queue-Referenz zurückgibt, verwaltet das Modell mehrere Queues in Map (Var Queue) FQueue.
    • Zunächst fehlte die Vorbedingung für put bei voller Queue; wenn man in eine Queue der Größe 1 0 und 1 einfügt und dann get aufruft, erwartet das Modell wegen FIFO 0, der C-Code liefert aber 1 zurück.
    • Das ist kein Implementierungsfehler, sondern eine fehlende Vorbedingung im Modell, und wird durch Hinzufügen der Vorbedingung QueueIsFull korrigiert.
    • Dass der Command Size im Generator fehlte, zeigte die Coverage-Ausgabe; nach dem Hinzufügen wurde ein Bug in der Berechnung der Queue-Größe gefunden.
    • Wenn man in eine Queue der Größe 1 ein Element einfügt und dann Size aufruft, ist der erwartete Wert 1, der reale Wert aber 0; als Korrektur wird vorgeschlagen, in new die interne Buffer-Größe auf n + 1 zu setzen.
    • Danach besteht abs(q->inp - q->outp) % q->size den Test bei Größe 1, scheitert aber erneut bei Größe 2; die endgültige Korrektur lautet (q->inp - q->outp + q->size) % q->size.

  • Die-Hard-3-Wasserkrug-Rätsel

    • Das Rätsel, mit einem 3-Liter- und einem 5-Liter-Krug genau 4 Liter herzustellen, wird mit zustandsbasiertem Testing gelöst.
    • Auch ohne reale Implementierung kann man nur Modell und Fake ausführen, einen Test fehlschlagen lassen, sobald ein bestimmter Zustand erreicht ist, und so eine geshrinkte Aktionssequenz erhalten.
    • Nach 199 Tests und 11 Shrinks wird folgende Sequenz präsentiert:
      • 5-Liter-Krug füllen
      • vom 5-Liter- in den 3-Liter-Krug gießen
      • 3-Liter-Krug leeren
      • erneut vom 5-Liter- in den 3-Liter-Krug gießen
      • 5-Liter-Krug füllen
      • vom 5-Liter- in den 3-Liter-Krug gießen
    • Im Trace werden Zwischenzustände angezeigt, sodass nachvollziehbar ist, wie der große Krug 4 Liter erreicht.

Paralleles Property-Based Testing

  • Bugs in nebenläufigem Code sind schwer zu reproduzieren und zu verifizieren, weil sich das Thread-Interleaving bei jeder Ausführung unterscheidet
  • Ziel ist es, parallele Tests ähnlich wie sequenzielle zustandsbasierte Tests zu ermöglichen, ohne dass Nutzer viel zusätzlichen Testcode schreiben müssen
  • Im Counter-Beispiel entsteht eine Race Condition, wenn incr nach readIORef ein nicht atomares writeIORef ausführt und dadurch zwei Threads gegenseitig ihre Inkremente überschreiben
  • Parallele Tests sammeln die Zeitpunkte von Invocation und Response der Commands während der Ausführung und erstellen daraus eine concurrent history; anschließend wird geprüft, ob sich diese History durch ein sequenzielles Interleaving erklären lässt
  • Wenn auch nur ein Interleaving zum sequenziellen Modell passt, gilt die History als linearisierbar und wird als korrekt bewertet
  • Wenn kein sequenzielles Interleaving die tatsächlichen Responses erklären kann, wird das Ergebnis als nicht linearisierbar behandelt

  • Erzeugung und Shrinking paralleler Commands

    • Ein paralleles Programm wird durch ParallelCommands und mehrere Forks dargestellt; die Commands innerhalb eines Fork werden parallel ausgeführt
    • Die Beispielimplementierung behandelt single-, double- und triple-threaded execution
    • Bei paralleler Ausführung kann sich der mögliche Modellzustand je nach Interleaving unterscheiden, etwa bei Fork [Write "a" "foo", Write "a" "bar"]
    • Das parallele Modell verwendet für Erzeugung und Shrinking von Commands nicht einen einzelnen State, sondern eine Menge von States
    • parallelSafe prüft, ob die Precondition in allen Permutationen der Commands innerhalb eines Fork erhalten bleibt
    • Befinden sich zum Beispiel Write "a" und Delete "a" im selben Fork, kann ein Command die Precondition des anderen verletzen
    • Auch im Shrinking bleiben nur Commands erhalten, die Precondition und den Gültigkeitsbereich symbolischer Referenzen bewahren

  • Parallele Ausführung und Prüfung der Linearisierbarkeit

    • Die parallele Ausführung protokolliert die Invoke- und Ok-Events jedes Commands als History
    • Wenn eine Response eine neue Referenz enthält, wird die Umgebung mit einem atomaren Counter erweitert, um Kollisionen von Referenznummern zwischen Threads zu vermeiden
    • Alle möglichen Interleavings aus der History werden als Rose-Tree aufgelistet
    • linearisable prüft, ob irgendein Pfad in diesem Tree mit dem sequenziellen runFake-Modell und den Responses übereinstimmt
    • Da parallele Tests letztlich das sequenzielle Modell wiederverwenden, erhalten Nutzer nach dem Schreiben des sequenziellen Modells mit wenig zusätzlichem Code auch parallele Tests

  • Beispiel: paralleler Counter

    • Um parallele Tests für den Counter zu aktivieren, wurden nur eine ParallelModel Counter-Instanz und die Property ergänzt
    • Mit dem nicht atomaren incrRaceCondition wird die Race Condition gefunden
    • Selbst wenn kleinere Testfälle ebenfalls eine Race Condition enthalten, kann QuickCheck das Shrinking beenden und den kleineren Testfall als erfolgreich ansehen, wenn sich der Fehler wegen eines anderen Interleavings nicht reproduzieren lässt
    • Die richtige Lösung ist ein deterministischer Thread-Scheduler; das Paper zu parallelen Tests verwendet ihn
    • Die Beispielimplementierung nutzt stattdessen einen einfacheren Workaround und fügt rund um Shared-Memory-Lese- und Schreibzugriffe kurze Sleeps ein, um die Wahrscheinlichkeit desselben Interleavings zu erhöhen
    • Die Sleeps werden nicht benötigt, um die Race Condition zu finden, sondern um den gefundenen Counterexample zu verkleinern
    • Nach dem Hinzufügen der Sleeps schrumpft das minimale Gegenbeispiel auf ParallelCommands [Fork [Incr,Incr],Fork [Get]]

  • Beispiel: Process Registry

    • Als Beispiel dient ein System ähnlich einer Erlang-Process-Registry, das Threads spawnt und ThreadId per Name registriert, nachschlägt, deregistriert und beendet
    • Das sequenzielle Modell verfolgt erzeugte Thread-IDs, registrierte Name-Thread-Paare und beendete Thread-IDs
    • Register und Unregister können fehlschlagen, daher verwendet die Response Either ErrorCall ()
    • Die Fehlerinformationen zur Fehlerposition in der realen Implementierung werden mit abstractError entfernt, damit sie zum Fake passen
    • monitoring zeigt die Coverage für RegisterFailed, RegisterSucceeded, UnregisterFailed und UnregisterSucceeded
    • Baut man absichtlich einen Bug ein, bei dem register die bestehende Registry überschreibt, entsteht ein sequenzielles Gegenbeispiel, bei dem ein bereits registriertes "e" nicht deregistriert werden kann
    • In parallelen Tests entsteht ein längeres Gegenbeispiel; mit SleepyIORef schrumpft es auf die Form Fork [Register "b" (Var 0), Register "c" (Var 0)]
    • Das Problem ist eine Race Condition, bei der sich zwischen der Prüfung mit readRegistry und dem Aufruf von atomicModifyIORef ein anderer Thread dazwischenschieben kann
    • Nachdem auf register, unregister und kill ein globaler Lock angewendet wurde, bestehen die parallelen Tests

Fake-basierte Modelle und Integrationstests

  • Anstelle traditioneller State-Machine-Spezifikationen mit Post-Conditions wird ein In-Memory-Fake als Reference Implementation verwendet
  • Edsko de Vries’ Artikel von 2019 wird als der erste Artikel vorgestellt, der vorschlägt, ein Fake auf einer zustandsmaschinenbasierten Spezifikation mit Post-Conditions aufzubauen
  • Das Fake wird ähnlich wie ein Mock als leichter zugänglicher Ansatz für Programmierer präsentiert, die mit formalen Spezifikationen nicht vertraut sind
  • Ein weiterer Vorteil von Fakes ist, dass sie in Integrationstests anstelle abhängiger Komponenten verwendet werden können
    • Die echte Dependency muss nicht gestartet oder aktiviert werden
    • Schnellere und deterministische Integrationstests lassen sich aufbauen
  • Das Problem, dass ein Fake falsch sein kann, wird mit Contract Tests behandelt
  • Da zustandsbasierte und parallele Property-Based-Tests die Übereinstimmung von Fake und realer Implementierung validieren, fungiert das Fake als vertragsgetestete Dependency

  • Tests und Deployment mit einem Queue-Fake entkoppeln

    • Das Queue-Interface IQueue besitzt iNew, iPut, iGet, iSize
    • Die reale Implementierung bindet den C-Queue-Wrapper unverändert an
    • Die Fake-Implementierung speichert den Modellzustand in IORef und aktualisiert ihn über fNew, fPut, fGet, fSize
    • Komponenten werden gegen das Interface IQueue q geschrieben
    • In Tests wird die fake-Instanz verwendet, im Deployment die real-Instanz
    • Zustandsbasierte Property-Based-Tests setzen die Annahme, dass das Fake der realen Implementierung faithful ist

  • File-System-Fake

    • Das File-System-Interface IFileSystem h besitzt iMkDir, iOpen, iWrite, iClose, iRead
    • Die reale Implementierung verwendet das tatsächliche File-System unter /tmp/qc-test
    • Das Fake wird als In-Memory-FakeFS mit Directory-Set, File-Content-Map, Open-Handle-Map und nächstem Handle implementiert
    • fOpen, fWrite, fClose, fRead modellieren Precondition-Fehler wie belegte Dateien, nicht vorhandene Verzeichnisse oder geschlossene Handles
    • Wenn getestet wurde, dass das Fake-File-System dem realen File-System faithful entspricht, können vom File-System abhängige Komponenten mit dem Fake integriert getestet und beim Deployment durch das reale File-System ersetzt werden
    • Wenn beim Austausch gegen das reale System Bugs auftreten, muss untersucht werden, wie ein Mismatch zwischen Fake und realer Implementierung die zustandsbasierten Property-Based-Tests passieren konnte

  • Größere Komponentensysteme

    • Auch ein System, in dem A von B abhängt und B von C, lässt sich auf dieselbe Weise erweitern
    • Für jede Komponente wird ein Interface definiert
      • iC :: IO IC
      • iB :: IC -> IO IB
      • iA :: IB -> IO IA
    • Die Teststrategie ist wie folgt
      • C wird mit zustandsbasierten und parallelen Property-Based-Tests validiert, um ein contract-getestetes Fake C zu erhalten
      • In den Integrationstests von B wird Fake C verwendet
      • Für Tests von A wird ein Fake B verwendet, das Fake C nutzt
    • Dieser Ansatz lässt sich mit demselben Muster auch auf mehr Komponenten oder Services ausweiten

Fazit

  • Zustandsbasierte und parallele Property-Based-Tests lassen sich in etwa 400 Zeilen Code implementieren; das ist eine Größenordnung, die mit der ersten QuickCheck-Implementierung ohne Shrinking von rund 300 Zeilen vergleichbar ist
  • Wenn ein Fake als Modell verwendet wird, wird die Spezifikation für zustandsbasierte und parallele Tests vertrauter in der Form und kann wiederverwendet werden, um größere Systeme kompositionell zu testen
  • Wenn die einzelnen Sprach-Communitys weiter experimentieren, besteht Spielraum, den Zustand von Property-Based-Testing-Bibliotheken zu verbessern

Verwandte Beiträge

1 Kommentare

 
GN⁺ 2024-07-06
Hacker-News-Kommentare

  • Coverage-basiertes Fuzzing ist aufgekommen und wird in Go auch gut unterstützt; ich frage mich, was einem entgeht, wenn man keine Property-Based-Testing-Bibliothek verwendet
    https://www.tedinski.com/2018/12/11/fuzzing-and-property-tes...
    Wenn man sich den folgenden Fuzz-Test und die dazugehörige Prüfung der Invarianten ansieht, wirkt das im Grunde fast wie ein Property Test
    https://github.com/ncruces/aa/blob/505cbbf94973042cc7af4d6be...
    https://github.com/ncruces/aa/blob/505cbbf94973042cc7af4d6be...

    • Die Unterscheidung zwischen Property-Based Testing und Fuzzing ist größtenteils eher eine grobe Einordnung nach Gefühl
      Es gibt zwar echte Unterschiede, aber die Grenzen sind ziemlich unscharf, und es ist nicht besonders wichtig, exakt festzulegen, was Fuzzing ist und was Property-Based Testing
      Schnell laufende Tests mit detaillierten Assertions sind Property-Based Testing; lange laufende Tests, die nur Crashes finden, sind Fuzzing; alles dazwischen ist uneindeutig
      https://hypothesis.works/articles/what-is-property-based-tes...
    • Coverage-basiertes Fuzzing und Property-Based Testing lassen sich durchaus kombinieren
      Als ich bei Google war, gab es ein internes Tool, das beides kombiniert hat, und das war wirklich gut. Man schrieb wie gewohnt Property-Based Tests; zur Laufzeit kompilierte das Test-Framework den Code speziell, um Coverage zu erfassen, und passte zufällige Eingaben an, um die Coverage zu erhöhen. Natürlich lief das vollautomatisch auf einem Cluster aus mehreren Maschinen
      Klassisches Property-Based Testing wird normalerweise nur als Bibliothek implementiert, daher stehen nicht unbedingt Coverage-Informationen zur Verfügung, um die Erzeugung zufälliger Eingaben zu steuern
    • Da hier Eigenschaften asserted werden, würde ich sagen, dass es per Definition zu Property-Based Testing zählt, etwa „alle Knoten mit Level größer als 1 haben zwei Kinder“
      Je nach Bibliothek bekommt man allerdings einiges an Komfortfunktionen. Eine der nützlichen Funktionen ist Shrinking; dazu kann man den Abschnitt „Shrinking“ hier lesen: https://tech.fpcomplete.com/blog/quickcheck-hedgehog-validit...
      Auch Kombinatoren zum Zusammensetzen von Generatoren sind großartig, und manche Bibliotheken enthalten bekannte Mengen „schlechter“ Werte, die außergewöhnliches Verhalten auslösen
    • Ich bin mir nicht sicher, wie sich Go-Fuzz-Tests von dem unterscheiden, was im verlinkten Artikel beschrieben wird, aber dort hieß es, dass ein richtiger Fuzzer Tage oder Wochen laufen müsse und dass man Property-Based Testing fast immer Fuzzing vorziehen sollte
      Ich möchte einen Schritt zurücktreten und eine eher metabezogene Frage zum Testen stellen: Bedeutet Testerfolg auch Code-Erfolg, und gilt das umgekehrt ebenfalls? Gibt es in Go einen Teil der Spezifikation, der festlegt, dass dieselbe Eingabe für denselben Code dieselbe Ausgabe liefert?
    • Aus API-Sicht bekommt man vor allem eine Kombinator-Bibliothek, um die gewünschten zufälligen Datenstrukturen zu erzeugen
      Wenn man mit einem Arbitrary-Typ arbeitet, der eine Menge zufälliger Objekte repräsentiert, kann man leicht wiederverwendbare Funktionen zum Erzeugen von Testeingaben schreiben. Solche Bibliotheken ließen sich wohl auch recht einfach zusammen mit Gos Fuzzing-Framework verwenden
      Trotzdem denke ich, dass gängige Kombinatoren wie map, filter, chain und oneOf etwas umständlich sein können; deshalb schreibe ich gerade eine neue Property-Testing-Bibliothek für JavaScript. Ziel ist, sie angenehmer benutzbar zu machen, aber sie ist noch experimentell und noch nicht veröffentlicht

  • clojure.spec.alpha war eine hervorragende Erfahrung, egal ob zusammen mit test.check oder nicht; als ich dann Pythons hypothesis ausprobierte, war es wirklich miserabel.
    Hypothesis schien einfache, aber „große“ Datenmengen vom Design her nicht verarbeiten zu können, wobei „groß“ hier in Wirklichkeit gar nicht besonders groß ist. [0] Es war so schmerzhaft, dass wir Hypothesis und generative Tests aus der Python-Testsuite bei der Arbeit komplett entfernt haben.
    [0] https://github.com/HypothesisWorks/hypothesis/issues/3493

    • In diesem Fall klingt es weniger so, als könne Hypothesis keine großen Datenmengen handhaben, sondern eher so, als würden viele der verkleinerten Fälle verworfen.
      Hypothesis versuchte, die erzeugte Ganzzahl auf 0 zu reduzieren, um zu prüfen, ob der Bug auch bei 0 existiert, und der Test behandelte 0 nicht als Fehlschlag, sondern verwarf den Fall, weil 0 enthalten war. Bei kleinen Fällen war das nur ineffizient, bei großen Fällen aber genug, dass Hypothesis aufgab.
      In dem Thread schlug jemand vor, eine andere Strategie zur Instanzerzeugung zu verwenden, die keine 0 erzeugen kann. Also nicht erst den Lieblingswert des Shrinkers von Hypothesis erzeugen und dann verwerfen, sondern ihn von Anfang an gar nicht erzeugen. Ich frage mich, ob das ausprobiert wurde.
      Außerdem frage ich mich, wie clojure.spec.alpha das anders behandelt.
      Der Kommentar von mjaniczek unter https://news.ycombinator.com/item?id=40876437 nennt diesen Fall als Nachteil des Hypothesis-Ansatzes.
      Sinngemäß: „Der Generator wird nun zu einem Byte-Listen-Parser, der fehlschlagen kann, was etwas Ineffizienz erzeugt, und Nutzer können seltsame Generatoren bauen, die der interne Shrinker nicht perfekt verkleinern kann. Trotzdem ist die Developer Experience unter den drei Ansätzen die beste …“
      Natürlich würde die Person vermutlich nicht zustimmen, dass der eigene Test auf „seltsame“ Weise geschrieben wurde.
    • An Clojures spec mochte ich, dass es wirklich einfach war, drumherum Dinge aufzubauen; nach dem Wechsel zu Elixir musste ich für solche Tests bis zur alten Erlang-Bibliothek propEr hinuntergehen. Ziemlich enttäuschend.
    • Das Beispiel im GitHub-Issue verwendet filter auf eine Weise, die das eigene Problem verursacht.
      Wenn man zufällig erzeugt und dann herausfiltert, was zu einer bestimmten Eigenschaft passt, kratzt man im Erzeugungsprozess faktisch Lose auf.

  • Die einfache Antwort auf die im Artikel gestellte Frage „Warum gibt es keine Anforderung, dass veröffentlichte Forschung mit Open-Source-Tools reproduzierbar sein muss, oder zumindest mit Tools, die der Öffentlichkeit und anderen Forschern kostenlos zur Verfügung stehen?“ lautet: Die unmittelbare Folge einer solchen Anforderung wäre, dass Arbeiten, die diese Bedingung nicht erfüllen, nicht veröffentlicht werden.
    Zum Beispiel wäre dann wohl auch das Quviq-QuickCheck-Paper, das für die Autoren und andere offenbar nützlich war, nicht veröffentlicht worden, und die Community hätte dieses Geschenk an Information verloren.

    • Es wäre gut, wenn einige Verlage Reproduzierbarkeit verlangen und andere nicht.
      Jede Anforderung hat eine ausschließende Wirkung, und es gibt immer Grenzfälle von Arbeiten, die nützlich sein können, auch wenn sie die Anforderungen nicht erfüllen.
    • Das ist keine eindeutig schwarz-weiße Frage und man könnte sie sogar eine politische Frage nennen, aber diese Verteidigungslinie ist trotzdem nicht besonders überzeugend.
      Wenn man diese Argumentation gelten lässt, kann man sie als Schutzschild für beliebig vieles verwenden. Wenn man Reproduzierbarkeit als Anforderung streicht, muss man nichts erklären, was man nicht erklären möchte. Man muss keine Daten zu Stichproben bereitstellen, keine Tests auf statistische Signifikanz. Ein vages Abstract, das behauptet, irgendein Ergebnis erreicht zu haben, reicht dann aus.
      Sogar Fermats berühmte Notiz am Rand seines privaten Exemplars der Arithmetica wäre dann ein vollkommen gültiger Forschungsartikel. Schließlich möchte man die wertvolle Information nicht verlieren, dass ein berühmter Mathematiker glaubte, einen knappen und eleganten Beweis für einen Satz zu haben. Auch wenn er ihn in Wirklichkeit natürlich höchstwahrscheinlich nicht hatte.
      Meine Meinung zu dieser politischen Frage ist, dass die aktuellen Standards zu lax sind. Niemand wird gezwungen, etwas zu veröffentlichen. Es gibt auf der Welt viel Forschung, die aus Gründen wie proprietärem Wert nirgends veröffentlicht wird, und diese Forschung wird nicht verschwinden.
      Aber wenn man in der Wissenschaft arbeitet, erst recht wenn man Forschungsgelder erhält, und sagt, das Ziel sei, das wissenschaftliche Wissen der Welt voranzubringen, dann ist es fair zu verlangen, dass man dieses Ziel tatsächlich verfolgt. Man sollte nicht nur so tun, als verfolge man es, um die akademische Karriereleiter hinaufzuklettern.
    • Es wäre doch vielleicht möglich, den Quellcode nur den Gutachtern offenzulegen.
      Dann müsste man auch alles mitliefern, was zum Ausführen des Codes nötig ist. Vielleicht wird das bereits so gemacht.
    • Weil Reproduzierbarkeit ein Grundpfeiler der wissenschaftlichen Methode ist.
    • Paper werden veröffentlicht, weil die Autoren ihren „Wichtigkeitsindex“ erhöhen möchten, und das hängt sehr direkt mit Bezahlung und akademischen Karrierechancen zusammen.
      Dass es für diesen Zweck zusätzliche Anforderungen gibt, wird die Zahl der veröffentlichten Arbeiten vermutlich kaum senken.
      Das schwerwiegendere Problem veröffentlichter Arbeiten ist, dass Fehler häufig absichtlich übergangen werden, um möglichst viel und möglichst schnell zu veröffentlichen. Wenn die Überprüfung von Papers einfacher wird, könnte sich diese Situation verbessern, aber ich würde nicht allzu viel erwarten. Menschen sind sehr gut darin, Abkürzungen zu finden.

  • Ich schreibe ziemlich häufig zustandsbehaftete Property-Tests mit Rusts proptest, meist direkt von Hand, und das ist ziemlich einfach
    Ein nicht triviales Beispiel, das sechs Bugs gefunden hat, findet sich unter https://github.com/sunshowers-code/buf-list/blob/main/src/cu...
    Parallele Tests können manchmal nützlich sein, aber oft ist es einfacher, einfach viele Tests parallel laufen zu lassen

    • Ich schreibe in Rust viele manuelle Property-Tests, und sie sehen im Großen und Ganzen so aus:
      Auf oberster Ebene verwende ich echte Zufälligkeit und darunter mehrere verschachtelte Schleifen, die von Fällen mit niedriger Komplexität zu Fällen mit hoher Komplexität hochgehen. Dann erzeuge ich einen Seed für einen deterministischen Pseudozufallszahlengenerator und gebe ihn aus. Wenn der Test fehlschlägt, kann man den Fehler-Seed kopieren und einfügen, um den Fehlerfall zu reproduzieren
      Solche manuellen Property-Tests empfand ich als schneller, flexibler und insgesamt weniger umständlich als jedes Framework oder jede Bibliothek
      Für wirklich robuste Concurrency-Tests empfehle ich allerdings nachdrücklich die AWS-Shuttle-Bibliothek (https://github.com/awslabs/shuttle). Sie kann unglaublich komplexe Race Conditions aufspüren. Ich habe dazu auch ein kleines Tutorial geschrieben: https://grantslatton.com/shuttle
      Bei AWS wurde diese Bibliothek verwendet, um ein eigenes Dateisystem zu verifizieren, das zum Betrieb von AWS S3 geschrieben wurde

  • Ich habe das verlinkte Paper „Testing Telecoms Software with Quviq QuickCheck“ kurz überflogen, aber keine unmittelbare Antwort auf die Frage gesehen: „Warum ist es nicht besser, diese zustandsbehaftete Arbeit einfach selbst zu machen?“
    Der Originaltext verweist hier auf ein Modell der Schlüssel-Wert-Paare eines Key-Value-Stores, aber ich sehe nicht, warum man nicht einfach eine Zustandsmaschine schreiben sollte oder warum dafür ein Framework nötig ist. Letzte Woche habe ich bei der Arbeit für Tests von Dateisystem-Interaktionen buchstäblich genau das gemacht, und am Ende lief es ungefähr auf type Instruction = | Read of stuff | Write of stuff | Seek of stuff | … hinaus
    Dann wird die Property zu „gegeben diese Liste von Befehlen, …“. Der Typ StateModel verlangt im Grunde dasselbe. Es ist schwer zu erkennen, dass StateModel viel beiträgt; es scheint nur eine sehr kleine Menge Testcode einzusparen, statt dafür viel mehr Framework-Code einzuführen, den man verstehen muss

    • Es gibt Tests, bei denen diese Einschätzung stimmt, aber das Shrinking von Fehlerfällen ist oft knifflig
      Wenn man nur „gültige“ Sequenzen von Zustandsübergängen erzeugen möchte, braucht man normalerweise einen Modellzustand, der festlegt, welche Testschritte in einem bestimmten Zustand gültig sind. Außerdem muss verhindert werden, dass beim Shrinking Testschritte entfernt werden und dadurch Vorbedingungen verletzt werden, die bei der ursprünglichen Erzeugung der einzelnen Schritte galten, was zu falschen Fehlschlägen führen würde
      Wenn in jedem Zustand jede Operation gültig ist und man nur eine völlig zufällige Sequenz beliebiger Operationen möchte, kann ein zustandsbehaftetes proptest-Framework überdimensioniert sein. Wenn man aber Modellzustand halten und Vorbedingungen für mehrere Operationen angeben muss, nimmt einem ein dediziertes Framework viel Arbeit ab
      Ich habe letztes Jahr einen Blogbeitrag zu diesem Thema geschrieben; wer ein ausführlicheres Beispiel sucht, kann dort nachsehen: https://readyset.io/blog/stateful-property-testing-in-rust
      Wie andere schon gesagt haben, sind parallele Zustandsmaschinen-Tests ebenfalls ein schöner Vorteil, den man von einem dedizierten Framework bekommen kann, aber sie sind nicht der einzige
    • Den zustandsbehafteten Teil deckt meiner Meinung nach modellbasiertes Testen besser ab
      Teststile kann man auch mischen. Es ist ja der eigene Code
    • Soweit ich paralleles QuickCheck verstehe, prüft es, ob alle möglichen Interleavings in einem Multithread-Programm letztlich einen Zustand erzeugen, der auch erreichbar wäre, wenn man die Befehle sequenziell aufgerufen hätte
      Das ist der Vorteil

  • Der Autor konzentriert sich auf Zustandsmaschinen und Parallelitätsaspekte von Property-Based Testing, aber es gibt auch andere Aspekte, die größere Wirkung haben könnten
    Einer davon ist Coverage-gesteuertes Property-Based Testing; dazu siehe den Beitrag von Dan Luu: https://danluu.com/testing/
    Ein weiterer, bei dem ich voreingenommen bin, ist die Automatisierung des Shrinkings, während alle Invarianten erhalten bleiben, die bei der Erzeugung der Werte aufgebaut wurden
    Kurz gesagt: Von QuickCheck abgeleitete Shrink-Funktionen, die auf Werten arbeiten (shrink : a -> [a]), haben Einschränkungen und Probleme, sodass Leute das Shrinking eher abschalten, statt sich mit dem Problem zu befassen
    Rose-Tree-„integriertes Shrinking“ (z. B. Hedgehog) hält sich an die Einschränkungen des Generators, hat aber Probleme mit Monad Bind, also wenn man das Ergebnis eines Generators nutzt, um zu einem anderen Generator zu verzweigen
    Der einzige Ansatz, der magisch „einfach funktioniert“, scheint das interne Shrinking von Hypothesis zu sein. Dabei wird eine Indirektionsschicht verwendet, die nicht den Wert selbst verkleinert, sondern die Liste zufälliger Entscheidungen. Der Nachteil ist, dass Generatoren nun zu Parsern für Byte-Listen werden, die fehlschlagen können, was etwas Ineffizienz erzeugt, und dass Nutzer seltsame Generatoren bauen können, die der interne Shrinker nicht perfekt verkleinern kann. Trotzdem bietet dieser Ansatz von den drei Varianten die beste Developer Experience, und wenn man bedenkt, dass es schon ein kleines Wunder ist, dass Leute überhaupt Tests schreiben, fühlt er sich als Autor einer Testbibliothek am ehesten lohnenswert an

    • Dass Rose-Tree-„integriertes Shrinking“ (z. B. Hedgehog) zwar den Einschränkungen des Generators folgt, aber Probleme mit Monad Bind hat, halte ich im Rahmen meines Amateurwissens für eine grundlegende Grenze von Monad Bind/Generatoren
      Stattdessen sollte man für optimales Shrinking applicative Generatoren bevorzugen: https://github.com/hedgehogqa/haskell-hedgehog/issues/473#is...
      Anders gesagt: Applicative Generatoren „verwenden das Generatorergebnis nicht, um zu einem anderen Generator zu verzweigen“, und wegen der „parallelen“ Natur von Applicative wird das Shrinking optimiert. Parallel ist hier nicht im Threading-Sinn des Artikels gemeint, sondern im monadischen Sinn. Applicatives sind „parallel“, daher können Generatoren unabhängig voneinander verkleinert werden. Monadische Generatoren sind dagegen „seriell“, sodass das Verkleinern eines Generators zwangsläufig das Verhalten der nachfolgenden Generatoren verändert
      Falls es einen öffentlichen Vortrag dazu gibt, würde ich gern einen Link sehen
    • Persönlich war Hypothesis für mich weit davon entfernt, „einfach zu funktionieren“
      Ich halte es nicht wirklich für production-ready, und das wirkt auch so, als sei es beabsichtigt.[0]
      Ich habe clojure.spec.alpha mit und ohne test.check recht ausführlich genutzt, war also trotz möglicher Unterschiede mit der allgemeinen Idee nicht völlig unvertraut
      [0] https://github.com/HypothesisWorks/hypothesis/issues/3493
    • Mein bevorzugtes Framework ist falsify, und es bietet „internes integriertes Shrinking“
      Ähnlich wie Hypothesis, verwendet aber statt linearer Sequenzen Generatorbäume. Es basiert auf selective functors, was auch für Dinge wie Validatoren ein gutes, nützliches Interface ist
      Laut https://hackage.haskell.org/package/falsify bietet diese Bibliothek Property-Based Testing mit Unterstützung für internes integriertes Shrinking. Integriert im Sinne von Hedgehog, also dass man keinen separaten Shrinker und Generator schreiben muss, und intern im Sinne von Hypothesis, also dass es auch über Monad Bind hinweg gut funktioniert

  • Ich habe versucht, Property-Based Testing einzusetzen, hatte aber immer das Gefühl, zwischen zwei Stühlen zu sitzen
    Wenn ich eine Eigenschaft gut genug verstehe, um sie streng zu testen, kann ich sie meist ins Typsystem schieben und per Konstruktion wahr machen. Wenn ich nur einen einfachen Smoke-Test will, ist eine einzelne beliebige Eingabe einfacher

    • Ich frage mich, welche Art von Eigenschaften du im Sinn hast
      Zum Beispiel hat man oft zwei Implementierungen, eine langsame, aber einfache naive und eine optimierte, und kann ihre Ausgaben für beliebige Eingaben vergleichen. Das ist eine einfache, leicht verständliche Eigenschaft, lässt sich aber normalerweise schwer ins Typsystem übertragen
      Ebenso könnte es egal sein müssen, in welcher Reihenfolge Eingaben präsentiert werden, oder es gibt eine Art, Daten aufzuteilen, sodass eine Eigenschaft wie max(Maximum von A, Maximum von B) = maximum(A union B) gilt. Wie könnte man so etwas im Typsystem kodieren?
      Oder Dinge wie „Für beliebige A und B ist irgendeine in A gefundene optimale Lösung nicht schlechter als irgendeine in A union B gefundene optimale Lösung“, oder Idempotenz wie f(f(A)) = f(A)
      All das sind leicht verständliche Eigenschaften, aber in den meisten Typsystemen nicht leicht auszudrücken
    • Wenn möglich, ist es eindeutig besser, Einschränkungen zur Compile-Zeit zu erzwingen
      Aber es gibt viele Einschränkungen, die gängige Type-Checker nicht abdecken können. Dependent Types würden viel helfen, scheinen aber noch auf Nischen wie Theorem Prover beschränkt zu sein

  • Ich frage mich, ob in der Liste nicht das ursprüngliche QuviQ Erlang QuickCheck fehlt
    Das vollständige Produkt ist proprietär, aber es gibt auch die kostenlose Version QuickCheck Mini: http://www.quviq.com/downloads/

  • Auch für Clojure gibt es inzwischen eine zustandsbehaftete quickcheck-Bibliothek: https://github.com/griffinbank/test.contract
    Paralleles Testen ist interessant, war für mich aber bisher noch keine große Schmerzquelle

  • Für C#/.NET-Tests habe ich CsCheck[0] verwendet und war ziemlich zufrieden damit
    Es war deutlich zugänglicher als Hedgehog oder FsCheck und auch recht schnell
    [0] https://github.com/AnthonyLloyd/CsCheck