pgo
1.0.0
PGO ist eine Quelle für den Quell -Compiler, der modulare Pluscal -Spezifikationen (die eine Superset von Pluscal verwenden) in GO -Programme übersetzt.
Zusätzlich zum PGO -Compiler enthält dieser Quellbaum:
distsys Support Library, die im generierten GO -Code von PGO verwendet wird, der im distsys/ Ordner erhältlich ist.systems/ Ordner gebaut wurden, einschließlich eines Raft-basierten Schlüsselwerts.syntax/ Ordner verfügbar sind.Sie können mehr über die Forschungsaspekte unserer Arbeit in unserem ASPLOS'23 -Papier erfahren, von denen eine Kopie in diesem Repository enthalten ist. Unsere Bewertung des PGO Distinguished Artefact Award auf dieser Konferenz?
Wir haben auch ein paar Videos, die Sie sich ansehen können:
Pluscal ist eine Sprache zur Spezifikation/Modellierung gleichzeitiger Systeme. Es wurde so konzipiert, dass es einfacher wird, TLA+zu schreiben. Insbesondere kann Pluscal in TLA+kompiliert werden, was mit nützlichen Systemeigenschaften (unter Verwendung des TLC -Modellprüfers) überprüft werden kann. Beispielsweise finden Sie hier ein Repository von Pluscal -Formulierungen von Lösungen zum gegenseitigen Ausschlussproblem.
GO ist eine von Google basierende Sprache, die von Google entwickelt wurde, um verteilte Systeme zu erstellen. Es hat die Unterstützung für Parallelität mit Kanälen und Goroutinen aufgebaut, was es für die Entwicklung verteilter Systeme hervorragend macht.
Derzeit gibt es keine Tools, die einer Pluscal/TLA+ -Pez mit einer Implementierung der Spezifikation entsprechen. PGO ist ein Tool, das darauf abzielt, die Spezifikation mit der Implementierung zu verbinden, indem GO -Code basierend auf einer in modularen Pluscal geschriebenen Spezifikation erstellt wird. Das "modulare" Präfix ergibt sich aus der Notwendigkeit, die Beschreibung eines Systems vom Modell seiner Umgebung zu unterscheiden, das für die Modellprüfung benötigt wird. PGO ermöglicht die Übersetzung einer modularen Pluskalbeschreibung eines verteilten Systems in überprüfbare Pluscal sowie in ein semantisch äquivalentes GO -Programm.
Aktiv in der Entwicklung. PGO unterstützt die Kompilierung aller Pluscal -Kontrollflusskonstrukte. PGO unterstützt auch eine überwiegende Mehrheit der von TLC unterstützten TLA+. Die Dokumentation der laufenden Arbeiten finden Sie in den Pull -Anfragen und Problemen.
In seinem Zustand der aktiven Entwicklung bieten wir keine stabilen Veröffentlichungen an. Um PGO auszuführen, besteht der beste Weg, das Repository zu klonen und auf dem Master -Zweig über das SBT -Build -Tool auszuführen:
$ sbt
> run [command-line arguments]
Die folgenden Nutzungsnotizen finden Sie in den Argumenten, die das Programm akzeptiert. Hinweis: Wenn Sie es in einer Zeile ausführen, müssen Sie die Argumente zitieren, wie in sbt run "[command-line arguments]" .
Um zu erfahren, wie Sie PGO während der Überprüfung verwenden, finden Sie auf der PGO -Nutzungsseite (Warnung: Update in Arbeit).
Die Kompilierungsmodi und -flaggen des Werkzeugs auf hohem Niveau finden Sie unten.
Der Hilfegtext des PGO Tools liest:
PGo compiler
-h, --help Show help message
Subcommand: gogen
-o, --out-file <arg>
-p, --package-name <arg>
-s, --spec-file <arg>
-h, --help Show help message
Subcommand: pcalgen
-s, --spec-file <arg>
-h, --help Show help message
Der gogen Unterbefehl fordert, dass PGO eine Go-Datei von einem mpcal-entsprechenden TLA+ -Modul generiert. Die meiste Anpassung dieser Phase sollte durch die Auswahl bestimmter Parameter beim Aufrufen des generierten GO -Codes durchgeführt werden. Daher müssen nur wenige Optionen berücksichtigt werden.
--out-file gibt den Pfad zur GO-Ausgabedatei wie -o in GCC an.--spec-file gibt den Pfad zur TLA+ -Negeldatei an--package-name ermöglicht die Anpassung des Paketnamens der GO-Ausgabedatei. Dies ist standardmäßig eine sanitäre Version des Namens von MPCal -Algorithmus. Der pcalgen Unterbefehl fordert, dass PGO seine mpcal-entsprechende TLA+ -Premserdatei umschreibt, sodass sie eine Pluscal-Übersetzung des MPCal-Algorithmus enthält. Die einzige Option, --spec-file , ist der Pfad zur Spezifikationsdatei, die umgeschrieben wird.
Um die Pluscal -Übersetzung einzufügen, sucht PGO nach Kommentaren wie Whitespace: Geben oder Nehmen Sie nach:
* BEGIN PLUSCAL TRANSLATION
... any number of lines may go here
* END PLUSCAL TRANSLATION
Wenn es keinen beiden Kommentaren in dieser Reihenfolge finden kann, wird eine Fehlermeldung aufgeben, die das Problem beschreibt und keine Ausgabe schreibt.
PGO ist eine in Scala geschriebene Quelle für die Quelle Compiler. Es kompiliert Spezifikationen, die in einer Erweiterung von Pluscal mit dem Namen Modular Pluscal (siehe modulare Pluscal -Seite für weitere Details) geschrieben wurden.
Der Scala -Code von PGO erstellt über ein SBT -Projekt, wobei die Abhängigkeiten von Maven verwaltet werden. PGO bietet zusätzlich eine Laufzeit -Support -Bibliothek für den generierten GO -Code an, der in distsys/ Subdolker lebt. Dieser GO -Code ist ein Standard -GO -Modul, das über die URL https://github.com/distcompiler/pgo/distys importiert werden kann.
Das Hauptaufbauskript ist das oberste Gebäude. Um aus dem Terminal zu erstellen, führen Sie sbt im Stammverzeichnis aus und verwenden Sie die von der SBT -Konsole bereitgestellten Standardbefehle. Dazu gehören run <command-line args> um PGO (neu) zu kompilieren und auszuführen, sowie test , um alle Tests auszuführen, einschließlich GO-Tests (Todo: Läufer für freistehende GO-Tests hinzufügen; diese fehlen insbesondere).
Der SBT-Build kann auch vom Intellij Scala-Plugin sowie wahrscheinlich jede andere IDE mit Scala-Unterstützung automatisch importiert werden.
Der Scala -Code von PGO hat Abhängigkeiten von einer kleinen Reihe von Versorgungsbibliotheken verwaltet:
Die Testsuiten von PGO hängen zusätzlich von:
go Executable. Die Tests werden versuchen, dies, wahrscheinlich auf dem $PATH oder gleichwertigen, über den Standard -Suchprozess des JVM zu finden.Die PGO's Go -Laufzeitbibliothek hängt davon ab:
PGO wird mit OpenJDK 1.11 bis 1.16 getestet und 1.18. OpenJDK 1.11+ wird aufgrund der Standard -API -Verwendung benötigt. Go> = 1.18 ist wegen Generika erforderlich.
