In funktionalen datenparallelen Programmen werden Index-Array-Berechnungen in Sequenzen von Bulk-Parallelen Operatoren – map, Präfixsumme, scatter – getrennt und verwendet, um Elemente von Datenarrays zu sammeln oder zu streuen, wodurch die Eigenschaften des Datenarrays bestimmt werden. Dieser Programmierstil ist problematisch für allgemeine Verifizierungsrahmenwerke (z. B. Dafny, F*, Liquid Haskell), die flexibel und leistungsfähig sind, jedoch ausführliche Annotationen und nicht triviale Benutzerbeweise erfordern, was sie für Nicht-Experten unzugänglich macht. Wir präsentieren einen Compileransatz zur Überprüfung der Array-Eigenschaften mit hoher Automatisierung, der darauf abzielt, die Verifizierung von datenparallelen Programmen für Benutzer ohne Verifizierungsexpertise zugänglicher zu machen. Wir unterstützen eine kleine, aber leistungsstarke vordefinierte Menge von Eigenschaften – Äquivalenz, Bereich, Injektivität, Bijektivität, Monotonie, Filterung, Partitionierung –, die dem Compiler ermöglichen, auf einer höheren Abstraktionsebene (automatisch) zu argumentieren. Wir bewerten unseren Ansatz an herausfordernden Anwendungen mit nicht-linearer Indizierung, einschließlich Graphalgorithmen, Cooley-Tukey FFT, Filterung, mehrdimensionaler Partitionierung und flachen, unregelmäßigen, geschachtelten parallelen Programmen, die schwer zu verifizieren sind, wie Batch-Operationen an Arrays unterschiedlicher Größen.
Hinnerskov et al. (Mon,) untersuchten diese Frage.