pgo
1.0.0
PGO est un compilateur source de source qui traduit des spécifications modulaires Pluscal (qui utilisent un superset de Pluscal) en programmes GO.
En plus du compilateur PGO, cet arbre source comprend:
distsys , utilisée par le code GO généré par PGO, disponible dans le dossier distsys/ .systems/ dossiers, y compris un magasin de valeurs clés basé sur des radeaux.syntax/ Folder.Vous pouvez en savoir plus sur les aspects de recherche de notre travail dans notre article ASPLOS'23, dont une copie est incluse dans ce référentiel. Notre évaluation du prix Artefact Distinguished Artefact lors de cette conférence ?.
Nous avons également quelques vidéos que vous pouvez regarder:
Pluscal est un langage pour spécifier / modéliser des systèmes simultanés. Il a été conçu pour faciliter l'écriture de TLA +. En particulier, pluscal peut être compilé dans TLA +, qui peut être vérifié par rapport aux propriétés du système utiles (en utilisant le vérificateur du modèle TLC). Par exemple, voici un référentiel de formulations de plus de solutions au problème d'exclusion mutuelle.
GO est un langage basé sur C développé par Google pour la construction de systèmes distribués. Il a pris en charge la concurrence avec les canaux et les Goroutines, ce qui le rend idéal pour développer des systèmes distribués.
Actuellement, il n'y a pas d'outils qui correspondent à une spécification Pluscal / TLA + avec une implémentation de la spécification. PGO est un outil qui vise à connecter la spécification avec l'implémentation en générant du code GO basé sur une spécification écrite dans modular Pluscal. Le préfixe "modulaire" vient de la nécessité de distinguer la description d'un système du modèle de son environnement, qui est nécessaire pour la vérification du modèle. PGO permet à la traduction d'une description modulaire de plus d'un système distribué à vérifiable pluscal, ainsi qu'à un programme GO sémantiquement équivalent.
Activement en cours de développement. PGO prend en charge la compilation de toutes les constructions d'écoulement de contrôle pluscal. PGO prend également en charge une grande majorité du niveau de valeur TLA + pris en charge par TLC. Voir les demandes de traction et les problèmes de documentation des travaux en cours.
Dans son état de développement actif, nous ne fournissons pas de versions stables. Pour exécuter PGO, la meilleure façon est de cloner le référentiel et, sur la branche maître, l'exécutez via l'outil de construction SBT:
$ sbt
> run [command-line arguments]
Voir les notes d'utilisation ci-dessous pour les arguments que le programme accepte. Remarque: Si vous l'exécutez sur une seule ligne, vous devez citer les arguments, comme dans sbt run "[command-line arguments]" .
Pour apprendre à utiliser PGO pendant la vérification, consultez la page d'utilisation de PGO (avertissement: mise à jour en cours).
Pour les modes de compilation et les drapeaux de l'outil à un niveau élevé, voir ci-dessous.
Le texte d'aide de l'outil PGO se lit comme suit:
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
La sous-commande gogen demande que PGO génère un fichier GO à partir d'un module TLA + contenant MPcal. La majeure partie de la personnalisation de cette étape doit être effectuée en choisissant des paramètres spécifiques lors de l'appel du code GO généré, il n'y a donc que quelques options à considérer.
--out-file Spécifie le chemin d'accès au fichier de sortie GO, comme -o dans GCC.--spec-file Spécifie le chemin d'accès au fichier d'entrée TLA +--package-name permet la personnalisation du nom du package du fichier de sortie GO. Cela par défaut est une version désinfectée du nom de l'algorithme MPcal. La sous-commande pcalgen demande que PGO réécrit son fichier d'entrée TLA + contenant MPcal, de sorte qu'il contient une traduction pluscal de l'algorithme MPcal. La seule option, --spec-file , est le chemin d'accès au fichier de spécification, qui sera réécrit.
Pour insérer la traduction de Pluscal, PGO recherchera des commentaires comme, donner ou prendre un espace blanc:
* BEGIN PLUSCAL TRANSLATION
... any number of lines may go here
* END PLUSCAL TRANSLATION
S'il ne peut pas trouver l'un de ces deux commentaires dans cet ordre, il abandonnera un message d'erreur décrivant le problème et n'écrira aucune sortie.
PGO est un compilateur source de source écrit dans Scala. Il compile des spécifications écrites dans une extension de Pluscal, appelé modular Pluscal (voir la page modular Pluscal pour plus de détails), pour aller des programmes.
Le code Scala de PGO se construit via un projet SBT, avec ses dépendances gérées par Maven. PGO fournit en outre une bibliothèque de support d'exécution pour son code GO généré, qui vit dans le distsys/ sous-dossier. Ce code GO est un module GO standard, qui peut être importé via l'URL https://github.com/distcompiler/pgo/distys.
Le script de construction principal est la version de niveau supérieur.sbt. Pour construire à partir du terminal, exécutez sbt dans le répertoire racine et utilisez les commandes standard fournies par la console SBT. Ceux-ci incluent run <command-line args> pour (re) compiler et exécuter PGO, et test pour exécuter tous les tests, y compris les tests GO (TODO: Ajouter Runner pour les tests GO autoportants; celui-là, en particulier, il manque).
La version SBT peut également être importée automatiquement par le plugin Intellij Scala, ainsi que probablement tout autre IDE avec le support Scala.
Le code Scala de PGO a géré les dépendances sur un petit ensemble de bibliothèques de services publics:
Les suites de test de PGO dépendent en outre:
go . Les tests tenteront de trouver cela, probablement sur le $PATH ou l'équivalent, via le processus de recherche par défaut de JVM.La bibliothèque d'exécution GO de PGO dépend de:
Le PGO est testé à l'aide d'OpenJDK 1.11 à 1.16 et GO 1.18. OpenJDK 1.11+ est nécessaire en raison de l'utilisation standard de l'API. GO> = 1.18 est nécessaire à cause des génériques.
